Sperner property of the weak order

DefinitionInversion set of a permutation#✓fully proved

For a permutation \(\sigma\) of \(\{0, \dots, n-1\}\), the inversion set of \(\sigma\) is the set of pairs of positions \((i, j)\) with \(i < j\) and \(\sigma(j) < \sigma(i)\).

def inversions {n : ℕ} (σ : Equiv.Perm (Fin n)) : Finset (Fin n × Fin n) :=
  Finset.univ.filter fun p => p.1 < p.2 ∧ σ p.2 < σ p.1

Used by 2

Used byWeak order on the symmetric group · Sperner property of the weak order

DefinitionWeak order on the symmetric group#✓fully proved

For permutations \(\sigma\) and \(\tau\) of \(\{0, \dots, n-1\}\), \(\sigma \le \tau\) in the weak order when the inversion set of \(\sigma\) (its pairs of positions \((i, j)\) with \(i < j\) and \(\sigma(j) < \sigma(i)\)) is contained in the inversion set of \(\tau\).

def weakLE {n : ℕ} (σ τ : Equiv.Perm (Fin n)) : Prop :=
  inversions σ ⊆ inversions τ

Uses 1 · Used by 1

Statement usesInversion set of a permutation

Used bySperner property of the weak order

DefinitionSperner property of the weak order#✓fully proved

This is the statement that for every \(n\) and every antichain \(A\) of the weak order on the permutations of \(\{0, \dots, n-1\}\) (where \(\sigma \le \tau\) when the inversion set of \(\sigma\) is contained in that of \(\tau\)), there is a \(k\) such that \(A\) has at most as many elements as there are permutations with exactly \(k\) inversions. Equivalently, no antichain is larger than the largest rank level, the rank of a permutation being its number of inversions.

def weakOrderSperner : Prop :=
  ∀ (n : ℕ) (A : Finset (Equiv.Perm (Fin n))), IsAntichain weakLE (A : Set (Equiv.Perm (Fin n))) →
    ∃ k : ℕ, A.card ≤
      (Finset.univ.filter fun σ : Equiv.Perm (Fin n) => (inversions σ).card = k).card

Uses 2 · Used by 1

Statement usesInversion set of a permutation · Weak order on the symmetric group

Used byThe weak order on the symmetric group is Sperner

TheoremThe weak order on the symmetric group is Sperner#●ready to prove

For every \(n\) and every antichain \(A\) of the weak order on the symmetric group \(S_n\) of permutations of \(\{0, \dots, n-1\}\) (where \(\sigma \le \tau\) when the inversion set of \(\sigma\) is contained in that of \(\tau\)), there is a \(k\) such that \(A\) has at most as many elements as there are permutations with exactly \(k\) inversions.

Resolved true: Gaetz and Gao prove Stanley's conjecture that the weak order on \(S_n\) is strongly Sperner (a Peck poset); in particular it is Sperner.

public theorem_wanted weakOrderSperner_holds : weakOrderSperner

Sources

• J. Cooper, Combinatorial Problems I Like (2020 snapshot), Matroids, Lattices, and Posets, item 39, https://people.math.sc.edu/cooper/combprob.html; resolution: C. Gaetz and Y. Gao, A combinatorial sl₂-action and the Sperner property for the weak order, Proc. Amer. Math. Soc. 148 (2020); arXiv:1811.05501, abstract: the sl₂-representation resolves Stanley's conjecture that the weak order has the strong Sperner property (and is a Peck poset); strongly Sperner implies Sperner, https://doi.org/10.1090/proc/14655.

Uses 1

Statement usesSperner property of the weak order

3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.