Quotient Poset B_n / G

This file formalizes Definition 5.4 from Chapter 5 of Algebraic Combinatorics by Richard Stanley.

Definition

Let G be a subgroup of 𝔖_n (the symmetric group on n elements). The group G acts on B_n (the boolean lattice of subsets of {1,...,n}) by σ · S = {σ(i) : i ∈ S}. The quotient poset B_n / G has:

• Elements: the orbits of G acting on B_n
• Ordering: [S] ≤ [T] iff there exist S' ∈ [S], T' ∈ [T] with S' ⊆ T'
• Rank function: rank([S]) = |S| (well-defined since G preserves cardinality)

The quotient poset B_n / G is a graded poset of rank n and is rank-symmetric (Proposition 5.6, proof left as an exercise by the book).

Implementation notes

The action of Equiv.Perm (Fin n) on Finset (Fin n) is the pointwise action from Mathlib's Finset.mulActionFinset, available via open scoped Pointwise. This gives σ • S = S.image σ for σ : Equiv.Perm (Fin n) and S : Finset (Fin n).

The orbit relation uses MulAction.orbitRel, and the quotient type is MulAction.orbitRel.Quotient G (Finset (Fin n)).

The ordering [S] ≤ [T] is defined as: there exist representatives S' ∈ [S], T' ∈ [T] with S' ⊆ T'.

For antisymmetry: if S₁ ⊆ T₁ and S₂ ⊆ T₂ with S₁, T₂ in orbit a and T₁, S₂ in orbit b, then by cardinality preservation |S₁| ≤ |T₁| and |S₂| ≤ |T₂| with |S₁| = |T₂| and |T₁| = |S₂|, giving |S₁| = |T₁|, so S₁ = T₁ and the orbits coincide.

The quotient type

@[reducible, inline]

abbrev SpernerProperty.QuotientPoset (n : ℕ) (G : Subgroup (Equiv.Perm (Fin n))) : Type

The quotient poset B_n / G is the set of orbits of G ≤ 𝔖_n acting on B_n = Finset (Fin n). (Definition 5.4, Stanley's Algebraic Combinatorics)

Cardinality is preserved by the group action

theorem SpernerProperty.card_eq_of_orbitRel {n : ℕ} {G : Subgroup (Equiv.Perm (Fin n))} {S T : Finset (Fin n)} (h : (MulAction.orbitRel (↥G) (Finset (Fin n))) S T) : S.card = T.card

Two elements in the same orbit have the same cardinality.

theorem SpernerProperty.card_eq_of_mk_eq {n : ℕ} {G : Subgroup (Equiv.Perm (Fin n))} {S T : Finset (Fin n)} (h : ⟦S⟧ = ⟦T⟧) : S.card = T.card

Elements whose orbit-quotient classes coincide have the same cardinality.

The rank of an orbit

noncomputable def SpernerProperty.quotientPosetRank (n : ℕ) (G : Subgroup (Equiv.Perm (Fin n))) : QuotientPoset n G → ℕ

The rank of an orbit [S] in the quotient poset is the cardinality |S| of any representative. This is well-defined because permutations preserve cardinality.

@[simp]

theorem SpernerProperty.quotientPosetRank_mk {n : ℕ} {G : Subgroup (Equiv.Perm (Fin n))} (S : Finset (Fin n)) : quotientPosetRank n G ⟦S⟧ = S.card

theorem SpernerProperty.quotientPosetRank_le {n : ℕ} {G : Subgroup (Equiv.Perm (Fin n))} (q : QuotientPoset n G) : quotientPosetRank n G q ≤ n

The rank is bounded by n.

theorem SpernerProperty.quotientPosetRank_univ {n : ℕ} {G : Subgroup (Equiv.Perm (Fin n))} : quotientPosetRank n G ⟦Finset.univ⟧ = n

There is an orbit of rank n (the orbit of Finset.univ).

Partial order on the quotient poset

theorem SpernerProperty.mk_smul_eq {n : ℕ} {G : Subgroup (Equiv.Perm (Fin n))} (g : ↥G) (S : Finset (Fin n)) : ⟦g • S⟧ = ⟦S⟧

Helper: g • S is in the same orbit as S, so their quotient classes agree.

@[implicit_reducible]

instance SpernerProperty.quotientPosetPartialOrder {n : ℕ} {G : Subgroup (Equiv.Perm (Fin n))} : PartialOrder (QuotientPoset n G)

The ordering on the quotient poset: [S] ≤ [T] iff there exist representatives S' ∈ [S], T' ∈ [T] with S' ⊆ T'. (Definition 5.4)

Fintype instance

@[implicit_reducible]

noncomputable instance SpernerProperty.quotientPosetFintype {n : ℕ} {G : Subgroup (Equiv.Perm (Fin n))} : Fintype (QuotientPoset n G)

The quotient poset B_n/G is finite (it is a quotient of a finite type).

Helper: constructing strict inequalities in the quotient poset

theorem SpernerProperty.quotientPoset_ne_of_card_ne {n : ℕ} {G : Subgroup (Equiv.Perm (Fin n))} {S T : Finset (Fin n)} (hcard : S.card ≠ T.card) : ⟦S⟧ ≠ ⟦T⟧

If [S] ≤ [T] and |S| ≠ |T| then [S] ≠ [T] in the quotient poset.

GradeMinOrder and GradedPoset

theorem SpernerProperty.quotientPosetRank_strictMono (n : ℕ) (G : Subgroup (Equiv.Perm (Fin n))) : StrictMono (quotientPosetRank n G)

The rank function on the quotient poset is strictly monotone: if [S] < [T] then |S| < |T|.

theorem SpernerProperty.quotientPosetRank_covBy (n : ℕ) (G : Subgroup (Equiv.Perm (Fin n))) {a b : QuotientPoset n G} (hcov : a ⋖ b) : quotientPosetRank n G a ⋖ quotientPosetRank n G b

If [S] ⋖ [T] in the quotient poset, then |S| ⋖ |T| (i.e., |T| = |S| + 1).

theorem SpernerProperty.quotientPosetRank_isMin (n : ℕ) (G : Subgroup (Equiv.Perm (Fin n))) {a : QuotientPoset n G} (hmin : IsMin a) : IsMin (quotientPosetRank n G a)

Minimal elements of the quotient poset have rank 0.

@[implicit_reducible]

noncomputable instance SpernerProperty.quotientPoset_gradeMinOrder (n : ℕ) (G : Subgroup (Equiv.Perm (Fin n))) : GradeMinOrder ℕ (QuotientPoset n G)

Proposition 5.6 (grading). The quotient poset B_n/G is ℕ-graded by the cardinality rank function: the grade of an orbit [S] is |S|.

@[implicit_reducible]

noncomputable instance SpernerProperty.quotientPoset_gradedPoset (n : ℕ) (G : Subgroup (Equiv.Perm (Fin n))) : GradedPoset (QuotientPoset n G)

Proposition 5.6 (rank n). The quotient poset B_n/G is a graded poset of rank n. The rank of every orbit [S] is at most n (since |S| ≤ n for S ⊆ Fin n), and the orbit of Finset.univ attains rank exactly n.

Rank-Symmetry

theorem SpernerProperty.smul_compl_eq {n : ℕ} {G : Subgroup (Equiv.Perm (Fin n))} (g : ↥G) (S : Finset (Fin n)) : g • (Finset.univ \ S) = Finset.univ \ g • S

The complement map S ↦ Finset.univ \ S commutes with the group action: g • (univ \ S) = univ \ (g • S).

noncomputable def SpernerProperty.quotientPosetCompl {n : ℕ} {G : Subgroup (Equiv.Perm (Fin n))} : QuotientPoset n G → QuotientPoset n G

The complement map descends to orbits: complementing commutes with the orbit quotient.

@[simp]

theorem SpernerProperty.quotientPosetCompl_mk {n : ℕ} {G : Subgroup (Equiv.Perm (Fin n))} (S : Finset (Fin n)) : quotientPosetCompl ⟦S⟧ = ⟦Finset.univ \ S⟧

theorem SpernerProperty.quotientPosetCompl_involutive {n : ℕ} {G : Subgroup (Equiv.Perm (Fin n))} : Function.Involutive quotientPosetCompl

The complement map is an involution on orbits.

theorem SpernerProperty.quotientPosetCompl_bijective {n : ℕ} {G : Subgroup (Equiv.Perm (Fin n))} : Function.Bijective quotientPosetCompl

The complement map is a bijection on orbits.

theorem SpernerProperty.quotientPosetRank_compl {n : ℕ} {G : Subgroup (Equiv.Perm (Fin n))} (q : QuotientPoset n G) : quotientPosetRank n G (quotientPosetCompl q) = n - quotientPosetRank n G q

The rank of the complement orbit is n - rank.

theorem SpernerProperty.quotientPoset_rankCount_eq {n : ℕ} {G : Subgroup (Equiv.Perm (Fin n))} (i : ℕ) (hi : i ≤ n) : {q : QuotientPoset n G | quotientPosetRank n G q = i}.card = {q : QuotientPoset n G | quotientPosetRank n G q = n - i}.card

Key lemma for rank-symmetry: the number of orbits of rank i equals the number of orbits of rank (n-i), proved via the complement bijection.

theorem SpernerProperty.quotientPoset_isRankSymmetric (n : ℕ) (G : Subgroup (Equiv.Perm (Fin n))) : IsRankSymmetric

Proposition 5.6 (rank-symmetry). B_n/G is rank-symmetric: the number of orbits of rank i equals the number of orbits of rank n - i.

The proof uses the complement map S ↦ Finset.univ \ S which induces a bijection between orbits of i-element subsets and orbits of (n-i)-element subsets, since |Finset.univ \ S| = n - |S| and the complement commutes with the group action.