Order-Raising Operators and Matchings on the Boolean Algebra

This file formalizes the order-raising operator U_i on the Boolean algebra B_n and proves that it gives rise to order-raising matchings, as described in Lemma 4.5 of Stanley's Algebraic Combinatorics (Section 4).

Main results

• upward_local_LYM: The upward local LYM inequality — for a sized-i family 𝒜, |𝒜| * (card α - i) ≤ |∂⁺ 𝒜| * (i + 1).
• boolean_hall_condition: Hall's marriage condition for the Boolean lattice — for any sub-family of P_i in B_n with 2i + 1 ≤ n, the upper shadow is at least as large.
• booleanPoset_hasOrderRaisingMatching: The Boolean algebra B_n has order-raising matchings at every level i with 2 * i + 1 ≤ n.

Proof strategy

The proof uses Hall's marriage theorem via the upward local LYM inequality (double counting). For each element S ∈ P_i, the number of supersets of size i + 1 is n - i. Each element T ∈ P_{i+1} has at most i + 1 subsets of size i. When n - i ≥ i + 1 (equivalently 2i + 1 ≤ n), the double counting gives Hall's condition, and Hall's marriage theorem produces the injective matching.

theorem SpernerProperty.upward_local_LYM {α : Type u_1} [DecidableEq α] [Fintype α] {𝒜 : Finset (Finset α)} {i : ℕ} (h𝒜 : Set.Sized i ↑𝒜) : 𝒜.card * (Fintype.card α - i) ≤ 𝒜.upShadow.card * (i + 1)

Upward local LYM inequality. For a sized-i family 𝒜 of finsets over a fintype α, the upper shadow satisfies |𝒜| * (card α - i) ≤ |∂⁺ 𝒜| * (i + 1).

This is the upward analog of card_mul_le_card_shadow_mul. The proof uses double counting (card_mul_le_card_mul): each S ∈ 𝒜 has card α - i upper neighbors (via insertion of elements from Sᶜ), and each T ∈ ∂⁺ 𝒜 has at most i + 1 lower neighbors (subsets of size i are obtained by erasing one of T's i + 1 elements).

theorem SpernerProperty.boolean_hall_condition {n i : ℕ} (hn : 2 * i + 1 ≤ n) (𝒜 : Finset (Finset (Fin n))) (h𝒜 : Set.Sized i ↑𝒜) : 𝒜.card ≤ 𝒜.upShadow.card

Hall's marriage condition for the Boolean lattice: for any sub-family 𝒜 of i-element subsets of Fin n with 2i + 1 ≤ n, the upper shadow ∂⁺ 𝒜 is at least as large as 𝒜.

noncomputable def SpernerProperty.upNbhd (n i : ℕ) (s : { s : Finset (Fin n) // s.card = i }) : Finset { t : Finset (Fin n) // t.card = i + 1 }

Neighborhood function for Hall's theorem: for each i-element subset s of Fin n, the set of (i+1)-element supersets.

theorem SpernerProperty.biUnion_upNbhd_image_eq {n i : ℕ} (A : Finset { s : Finset (Fin n) // s.card = i }) : Finset.image Subtype.val (A.biUnion (upNbhd n i)) = (Finset.image Subtype.val A).upShadow

The image of the biUnion of neighborhoods under Subtype.val equals the upper shadow.

theorem SpernerProperty.hall_condition_subtypes {n i : ℕ} (hn : 2 * i + 1 ≤ n) (A : Finset { s : Finset (Fin n) // s.card = i }) : A.card ≤ (A.biUnion (upNbhd n i)).card

Hall's condition on the subtype level: for any family A of i-element subsets of Fin n with 2i + 1 ≤ n, the biUnion of upper neighborhoods is at least as large.

theorem SpernerProperty.boolean_order_raising_matching_exists {n i : ℕ} (hn : 2 * i + 1 ≤ n) : ∃ (f : { s : Finset (Fin n) // s.card = i } → { t : Finset (Fin n) // t.card = i + 1 }), Function.Injective f ∧ ∀ (s : { s : Finset (Fin n) // s.card = i }), ↑s ⊂ ↑(f s)

Existence of an order-raising matching on the Boolean lattice at level i, via Hall's marriage theorem. There exists an injective function from i-subsets to (i+1)-subsets with S ⊂ φ(S) for all S.

theorem SpernerProperty.booleanPoset_hasOrderRaisingMatching (n i : ℕ) (hn : 2 * i + 1 ≤ n) : HasOrderRaisingMatching i

Lemma 4.5 (Stanley). The boolean algebra B_n has order-raising matchings at every level i with 2 * i + 1 ≤ n: there exists an injection φ : P_i → P_{i+1} with S ⊂ φ(S) for all S ∈ P_i. (Lemma 4.5, Section 4)