Graded Posets and the Sperner Property

This file formalizes Definition 4.1 and related notions from Chapter 4 of Algebraic Combinatorics by Richard Stanley.

Definitions

• Poset: A partially ordered set (Definition 4.1), defined as a finite set with a reflexive, antisymmetric, and transitive binary relation ≤. Formalized as a class bundling PartialOrder and Fintype.
• Boolean algebra B_n: The poset of all subsets of {1,...,n} ordered by inclusion, modeled as Finset (Fin n) with its natural partial order.
• Graded poset: A finite poset with a rank function ρ : P → ℕ such that minimal elements have rank 0 and if x ⋖ y (covers) then ρ(y) = ρ(x) + 1. Formalized using Mathlib's GradeMinOrder ℕ α.
• GradedPoset: A class that records the maximum rank n of a finite poset already equipped with a GradeMinOrder ℕ grading, capturing the book's notion of a graded poset of rank n.
• Rank-symmetric: |P_i| = |P_{n-i}| for all 0 ≤ i ≤ n.
• Rank-unimodal: The sequence |P_0|, ..., |P_n| is unimodal.
• Antichain: A subset where no two elements are comparable, using Mathlib's IsAntichain.
• Sperner property: A graded poset has the Sperner property if the maximum antichain size equals the maximum level size max{|P_i| : 0 ≤ i ≤ n}.

Implementation notes

The book's poset is finite by definition. We capture this with Fintype α. Mathlib's GradeMinOrder ℕ α provides a rank function where minimal elements have grade 0 and covers increase grade by 1. This matches the book's rank function ρ.

For B_n, we use Finset (Fin n) which already has instances for PartialOrder, BoundedOrder, Fintype, and GradeMinOrder ℕ.

Posets

class SpernerProperty.Poset (α : Type u_1) extends PartialOrder α, Fintype α : Type u_1

Definition 4.1 (Poset). A poset (partially ordered set) is a finite set together with a binary relation ≤ satisfying:

• (P1) Reflexivity: x ≤ x for all x ∈ P;
• (P2) Antisymmetry: if x ≤ y and y ≤ x then x = y;
• (P3) Transitivity: if x ≤ y and y ≤ z then x ≤ z.

In Lean/Mathlib, properties (P1)–(P3) are captured by the PartialOrder typeclass, and finiteness by Fintype.

• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• elems : Finset α
• complete (x : α) : x ∈ elems

@[implicit_reducible]

instance SpernerProperty.Poset.mk' (α : Type u_1) [PartialOrder α] [Fintype α] : Poset α

Any type with PartialOrder and Fintype instances is a Poset.

Graded Posets

class SpernerProperty.GradedPoset (α : Type u_1) [PartialOrder α] [Fintype α] [GradeMinOrder ℕ α] : Type

A graded poset of rank n is a finite partially ordered set equipped with an ℕ-grading (rank function) where minimal elements have grade 0 and the maximum grade attained is n. This formalizes Definition 4.1 from the book, specifically the notion of a poset that is "graded of rank n".

We assume GradeMinOrder ℕ α is already available (so the grading is provided externally, e.g., by Mathlib instances for Finset), and record only the maximum rank and the boundedness condition.

• rank : ℕ

  The rank of the graded poset (length of every maximal chain).

• grade_le_rank (a : α) : grade ℕ a ≤ rank α

  Every element has grade at most rank.

• grade_rank_exists : ∃ (a : α), grade ℕ a = rank α

  The maximum grade rank is attained by some element.

Rank counting

def SpernerProperty.rankCount {α : Type u_1} [PartialOrder α] [Fintype α] [GradeMinOrder ℕ α] (i : ℕ) : ℕ

The number of elements of rank i in a graded poset. This is p_i = |P_i| in the book's notation where P_i = ρ⁻¹(i).

Rank-symmetric

def SpernerProperty.IsRankSymmetric {α : Type u_1} [PartialOrder α] [Fintype α] [GradeMinOrder ℕ α] [GradedPoset α] : Prop

A graded poset of rank n is rank-symmetric if |P_i| = |P_{n-i}| for all 0 ≤ i ≤ n. (Definition 4.1, Stanley's Algebraic Combinatorics)

Rank-unimodal

def SpernerProperty.IsRankUnimodal {α : Type u_1} [PartialOrder α] [Fintype α] [GradeMinOrder ℕ α] [GradedPoset α] : Prop

A graded poset of rank n is rank-unimodal if there exists j with 0 ≤ j ≤ n such that |P_0| ≤ |P_1| ≤ ... ≤ |P_j| ≥ |P_{j+1}| ≥ ... ≥ |P_n|. (Definition 4.1, Stanley's Algebraic Combinatorics)

Antichain

def SpernerProperty.IsAntichainSet {α : Type u_1} [PartialOrder α] (s : Set α) : Prop

An antichain in a poset P is a subset A of P such that no two distinct elements of A are comparable, i.e., we never have x, y ∈ A with x < y. This uses Mathlib's IsAntichain (· ≤ ·). (Definition 4.1, Stanley)

Sperner Property

def SpernerProperty.maxRankCount {α : Type u_1} [PartialOrder α] [Fintype α] [GradeMinOrder ℕ α] [GradedPoset α] : ℕ

The maximum rank count of a graded poset, i.e., max{|P_i| : 0 ≤ i ≤ n} where n is the rank. This uses Finset.sup over Finset.range (rank + 1), which for ℕ returns the maximum value (with ⊥ = 0 for the empty range, which cannot occur here since rank + 1 > 0).

def SpernerProperty.HasSpernerProperty {α : Type u_1} [PartialOrder α] [Fintype α] [GradeMinOrder ℕ α] [GradedPoset α] : Prop

A graded poset of rank n has the Sperner property if max{|A| : A is an antichain of P} = max{|P_i| : 0 ≤ i ≤ n}. Equivalently (as stated in the book, Definition 4.2), no antichain is larger than the largest level P_i. Since each level P_i is itself an antichain, the maximum antichain size is at least maxRankCount α; hence the Sperner property reduces to the upper bound. (Definition 4.2, Stanley's Algebraic Combinatorics)

Boolean Algebra B_n

@[reducible, inline]

abbrev SpernerProperty.BooleanPoset (n : ℕ) : Type

The Boolean algebra B_n is the poset of all subsets of [n] = {1,...,n} ordered by inclusion. We model this as Finset (Fin n) with its natural subset ordering. We use the name BooleanPoset to avoid conflict with Mathlib's BooleanAlgebra class. (Definition 4.1, Stanley's Algebraic Combinatorics)

theorem SpernerProperty.booleanPoset_grade (n : ℕ) (s : BooleanPoset n) : grade ℕ s = Finset.card s

The rank (grade) of a subset s in B_n is its cardinality.

@[implicit_reducible]

instance SpernerProperty.booleanPoset_gradedPoset (n : ℕ) : GradedPoset (BooleanPoset n)

B_n is a graded poset of rank n.

Order-Matchings

def SpernerProperty.HasOrderRaisingMatching {α : Type u_1} [PartialOrder α] [GradeMinOrder ℕ α] (i : ℕ) : Prop

An order-raising matching at rank i is a one-to-one function φ : P_i → P_{i+1} satisfying x < φ(x) for all x ∈ P_i. (Definition before Proposition 4.4, Stanley's Algebraic Combinatorics).

Formalized as the existence of a total function φ : α → α that is grade-raising, order-raising, and injective when restricted to grade-i elements.

def SpernerProperty.HasOrderLoweringMatching {α : Type u_1} [PartialOrder α] [GradeMinOrder ℕ α] (i : ℕ) : Prop

An order-lowering matching at rank i is a one-to-one function ψ : P_i → P_{i-1} satisfying ψ(x) < x for all x ∈ P_i. (Definition before Proposition 4.4, Stanley's Algebraic Combinatorics).

def SpernerProperty.HasOrderMatchings {α : Type u_1} [PartialOrder α] [Fintype α] [GradeMinOrder ℕ α] [GradedPoset α] (j : ℕ) : Prop

The hypothesis of Proposition 4.4: there exists a pivot j with 0 ≤ j ≤ n and order-matchings P_0 → P_1 → ⋯ → P_j ← P_{j+1} ← ⋯ ← P_n.

Iterated matching helpers

noncomputable def SpernerProperty.raise {α : Type u_1} (φ : ℕ → α → α) (start : ℕ) : ℕ → α → α

Iterate raising matchings k steps starting from rank start. raise φ start k x applies φ_start, φ_{start+1}, ..., φ_{start+k-1} to x.

noncomputable def SpernerProperty.lower {α : Type u_1} (ψ : ℕ → α → α) (start : ℕ) : ℕ → α → α

Iterate lowering matchings k steps starting from rank start. lower ψ start k x applies ψ_start, ψ_{start-1}, ..., ψ_{start-k+1} to x.

theorem SpernerProperty.raise_grade {α : Type u_1} [PartialOrder α] [GradeMinOrder ℕ α] (φ : ℕ → α → α) (start : ℕ) (hφ : ∀ (i : ℕ) (x : α), grade ℕ x = i → grade ℕ (φ i x) = i + 1) (x : α) (hx : grade ℕ x = start) (k : ℕ) : grade ℕ (raise φ start k x) = start + k

theorem SpernerProperty.raise_le {α : Type u_1} [PartialOrder α] [GradeMinOrder ℕ α] (φ : ℕ → α → α) (start : ℕ) (hφ_grade : ∀ (i : ℕ) (x : α), grade ℕ x = i → grade ℕ (φ i x) = i + 1) (hφ_lt : ∀ (i : ℕ) (x : α), grade ℕ x = i → x < φ i x) (x : α) (hx : grade ℕ x = start) (k : ℕ) : x ≤ raise φ start k x

theorem SpernerProperty.raise_injective {α : Type u_1} [PartialOrder α] [GradeMinOrder ℕ α] (φ : ℕ → α → α) (start : ℕ) (hφ_grade : ∀ (i : ℕ) (x : α), grade ℕ x = i → grade ℕ (φ i x) = i + 1) (hφ_inj : ∀ (i : ℕ) (x y : α), grade ℕ x = i → grade ℕ y = i → φ i x = φ i y → x = y) (x y : α) (hx : grade ℕ x = start) (hy : grade ℕ y = start) (k : ℕ) : raise φ start k x = raise φ start k y → x = y

theorem SpernerProperty.raise_split {α : Type u_1} (φ : ℕ → α → α) (start k m : ℕ) (x : α) : raise φ start (k + m) x = raise φ (start + k) m (raise φ start k x)

theorem SpernerProperty.lower_grade {α : Type u_1} [PartialOrder α] [GradeMinOrder ℕ α] (ψ : ℕ → α → α) (start : ℕ) (hψ : ∀ (i : ℕ) (x : α), grade ℕ x = i → grade ℕ (ψ i x) = i - 1) (x : α) (hx : grade ℕ x = start) (k : ℕ) (hk : k ≤ start) : grade ℕ (lower ψ start k x) = start - k

theorem SpernerProperty.lower_le {α : Type u_1} [PartialOrder α] [GradeMinOrder ℕ α] (ψ : ℕ → α → α) (start : ℕ) (hψ_grade : ∀ (i : ℕ) (x : α), grade ℕ x = i → grade ℕ (ψ i x) = i - 1) (hψ_lt : ∀ (i : ℕ) (x : α), grade ℕ x = i → ψ i x < x) (x : α) (hx : grade ℕ x = start) (k : ℕ) (hk : k ≤ start) : lower ψ start k x ≤ x

theorem SpernerProperty.lower_injective {α : Type u_1} [PartialOrder α] [GradeMinOrder ℕ α] (ψ : ℕ → α → α) (start : ℕ) (hψ_grade : ∀ (i : ℕ) (x : α), grade ℕ x = i → grade ℕ (ψ i x) = i - 1) (hψ_inj : ∀ (i : ℕ) (x y : α), grade ℕ x = i → grade ℕ y = i → ψ i x = ψ i y → x = y) (x y : α) (hx : grade ℕ x = start) (hy : grade ℕ y = start) (k : ℕ) (hk : k ≤ start) : lower ψ start k x = lower ψ start k y → x = y

theorem SpernerProperty.lower_split {α : Type u_1} (ψ : ℕ → α → α) (start k m : ℕ) (x : α) (hkm : k + m ≤ start) : lower ψ start (k + m) x = lower ψ (start - k) m (lower ψ start k x)

theorem SpernerProperty.raise_comparable {α : Type u_1} [PartialOrder α] [GradeMinOrder ℕ α] (φ : ℕ → α → α) (j : ℕ) (hφ_grade : ∀ i < j, ∀ (x : α), grade ℕ x = i → grade ℕ (φ i x) = i + 1) (hφ_lt : ∀ i < j, ∀ (x : α), grade ℕ x = i → x < φ i x) (hφ_inj : ∀ i < j, ∀ (x y : α), grade ℕ x = i → grade ℕ y = i → φ i x = φ i y → x = y) (x y : α) (hx : grade ℕ x ≤ j) (hy : grade ℕ y ≤ j) (hxy : grade ℕ x ≤ grade ℕ y) (heq : raise φ (grade ℕ x) (j - grade ℕ x) x = raise φ (grade ℕ y) (j - grade ℕ y) y) : x ≤ y

If two raising-side elements map to the same rank-j element, the one with smaller grade is ≤ the other. Key step for the antichain injectivity. Uses bounded hypotheses: φ properties only required for i < j.

theorem SpernerProperty.lower_comparable {α : Type u_1} [PartialOrder α] [GradeMinOrder ℕ α] (ψ : ℕ → α → α) (j n : ℕ) (hψ_grade : ∀ (i : ℕ), j < i → i ≤ n → ∀ (x : α), grade ℕ x = i → grade ℕ (ψ i x) = i - 1) (hψ_lt : ∀ (i : ℕ), j < i → i ≤ n → ∀ (x : α), grade ℕ x = i → ψ i x < x) (hψ_inj : ∀ (i : ℕ), j < i → i ≤ n → ∀ (x y : α), grade ℕ x = i → grade ℕ y = i → ψ i x = ψ i y → x = y) (x y : α) (hx : j ≤ grade ℕ x) (hy : j ≤ grade ℕ y) (hxn : grade ℕ x ≤ n) (hyn : grade ℕ y ≤ n) (hxy : grade ℕ y ≤ grade ℕ x) (heq : lower ψ (grade ℕ x) (grade ℕ x - j) x = lower ψ (grade ℕ y) (grade ℕ y - j) y) : y ≤ x

If two lowering-side elements map to the same rank-j element, the one with larger grade is ≥ the other. Key step for the antichain injectivity. Uses bounded hypotheses: ψ properties only required for j < i and i ≤ n.

theorem SpernerProperty.raise_le_bounded {α : Type u_1} [PartialOrder α] [GradeMinOrder ℕ α] (φ : ℕ → α → α) (start bound : ℕ) (hφ_grade : ∀ i < bound, ∀ (x : α), grade ℕ x = i → grade ℕ (φ i x) = i + 1) (hφ_lt : ∀ i < bound, ∀ (x : α), grade ℕ x = i → x < φ i x) (x : α) (hx : grade ℕ x = start) (k : ℕ) (hk : start + k ≤ bound) : x ≤ raise φ start k x

Bounded raise_le: x ≤ raise φ start k x when φ properties hold for i < bound.

theorem SpernerProperty.lower_le_bounded {α : Type u_1} [PartialOrder α] [GradeMinOrder ℕ α] (ψ : ℕ → α → α) (start j_bound n_bound : ℕ) (hψ_grade : ∀ (i : ℕ), j_bound < i → i ≤ n_bound → ∀ (x : α), grade ℕ x = i → grade ℕ (ψ i x) = i - 1) (hψ_lt : ∀ (i : ℕ), j_bound < i → i ≤ n_bound → ∀ (x : α), grade ℕ x = i → ψ i x < x) (x : α) (hx : grade ℕ x = start) (k : ℕ) (hk : k ≤ start - j_bound) (hn : start ≤ n_bound) : lower ψ start k x ≤ x

Bounded lower_le: lower ψ start k x ≤ x when ψ properties hold for j < i ≤ n.

Proposition 4.4

theorem SpernerProperty.rankCount_le_succ_of_raising {α : Type u_1} [PartialOrder α] [Fintype α] [GradeMinOrder ℕ α] (i : ℕ) (hmatch : HasOrderRaisingMatching i) : rankCount i ≤ rankCount (i + 1)

theorem SpernerProperty.rankCount_le_pred_of_lowering {α : Type u_1} [PartialOrder α] [Fintype α] [GradeMinOrder ℕ α] (i : ℕ) (hmatch : HasOrderLoweringMatching i) : rankCount i ≤ rankCount (i - 1)

theorem SpernerProperty.rankCount_le_maxRankCount {α : Type u_1} [PartialOrder α] [Fintype α] [GradeMinOrder ℕ α] [GradedPoset α] (j : ℕ) (hj : j ≤ GradedPoset.rank α) : rankCount j ≤ maxRankCount

theorem SpernerProperty.orderMatchings_imp_unimodal {α : Type u_1} [PartialOrder α] [Fintype α] [GradeMinOrder ℕ α] [GradedPoset α] (j : ℕ) (hmatch : HasOrderMatchings j) : IsRankUnimodal

Proposition 4.4 (Rank-unimodal part). If a graded poset P of rank n has order-matchings P_0 → P_1 → ⋯ → P_j ← P_{j+1} ← ⋯ ← P_n, then P is rank-unimodal.

theorem SpernerProperty.orderMatchings_imp_sperner {α : Type u_1} [PartialOrder α] [Fintype α] [DecidableEq α] [GradeMinOrder ℕ α] [GradedPoset α] (j : ℕ) (hmatch : HasOrderMatchings j) : HasSpernerProperty

Proposition 4.4 (Sperner property part). If a graded poset P of rank n has order-matchings P_0 → P_1 → ⋯ → P_j ← P_{j+1} ← ⋯ ← P_n, then P has the Sperner property.

Proof: Define a graph G whose edges come from the matchings. G decomposes into disjoint paths (chains in P), all passing through P_j. Any antichain meets each chain at most once, so |A| ≤ p_j ≤ maxRankCount.

Transfer of Sperner property via order isomorphism

theorem SpernerProperty.hasSpernerProperty_of_orderIso {P : Type u_2} {Q : Type u_3} [PartialOrder P] [Fintype P] [DecidableEq P] [GradeMinOrder ℕ P] [GradedPoset P] [PartialOrder Q] [Fintype Q] [DecidableEq Q] [GradeMinOrder ℕ Q] [GradedPoset Q] (e : P ≃o Q) (hgrade : ∀ (p : P), grade ℕ (e p) = grade ℕ p) (hP : HasSpernerProperty) : HasSpernerProperty

If P has the Sperner property and e : P ≃o Q is an order isomorphism that preserves grades, then Q also has the Sperner property.

The key idea: an order isomorphism maps antichains bijectively (preserving cardinality), and if it preserves grades then rankCount and maxRankCount are the same on both sides.

theorem SpernerProperty.isRankUnimodal_of_orderIso {P : Type u_2} {Q : Type u_3} [PartialOrder P] [Fintype P] [DecidableEq P] [GradeMinOrder ℕ P] [GradedPoset P] [PartialOrder Q] [Fintype Q] [DecidableEq Q] [GradeMinOrder ℕ Q] [GradedPoset Q] (e : P ≃o Q) (hgrade : ∀ (p : P), grade ℕ (e p) = grade ℕ p) (hP : IsRankUnimodal) : IsRankUnimodal

A grade-preserving order isomorphism transfers rank-unimodality. If e : P ≃o Q preserves grades and P is rank-unimodal, then so is Q.