Lemma 4.5: Order-Raising Operators Yield Order-Matchings (General Case)

Formalizes the general statement of Lemma 4.5 from Stanley's Algebraic Combinatorics. The existing OrderRaising.lean handles the Boolean algebra specialization; this file states the general result for arbitrary graded posets.

Main results

• order_matching_of_injective_order_raising — Lemma 4.5 (injective case). For any graded poset P with level sets P_i and P_{i+1}, if there exists an injective linear map U : ℝ^{P_i} → ℝ^{P_{i+1}} that is order-raising (meaning U(e_x)(y) ≠ 0 implies x < y), then there exists an injective function μ : P_i → P_{i+1} with x < μ(x) for all x in P_i.

• order_matching_of_surjective_order_raising — Lemma 4.5 (surjective case). Similarly, if U is surjective, then there exists an injective function μ : P_{i+1} → P_i with μ(y) < y for all y in P_{i+1}.

def SpernerProperty.IsOrderRaisingLinearMap {α : Type u_1} {β : Type u_2} [DecidableEq α] (U : (α → ℝ) →ₗ[ℝ] β → ℝ) (r : α → β → Prop) : Prop

A linear map U : (α → ℝ) →ₗ[ℝ] (β → ℝ) is order-raising with respect to a relation r : α → β → Prop if for every standard basis element eₓ and every y : β, U(eₓ)(y) ≠ 0 implies r x y.

This captures the key property from Lemma 4.5: for all x ∈ P_i, U(x) is a linear combination of elements y ∈ P_{i+1} satisfying x < y.

theorem SpernerProperty.order_matching_of_injective_order_raising {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] [Fintype β] (r : α → β → Prop) (U : (α → ℝ) →ₗ[ℝ] β → ℝ) (hU_inj : Function.Injective ⇑U) (hU_ord : IsOrderRaisingLinearMap U r) : ∃ (μ : α → β), Function.Injective μ ∧ ∀ (x : α), r x (μ x)

Lemma 4.5 (injective case). For any graded poset P, if there exists an injective order-raising linear map U : ℝ^{P_i} → ℝ^{P_{i+1}}, then there exists an order-matching μ : P_i → P_{i+1}.

The proof represents U as a matrix M (via LinearMap.toMatrix') whose columns are linearly independent (since U is injective). Hall's marriage theorem is then applied: for any subset S of columns, the support (set of rows with nonzero entries) has cardinality ≥ |S|, because the columns restricted to the support remain linearly independent in a space of dimension equal to the support size. Hall's theorem yields an injection f with M(f(x), x) ≠ 0 for all x, and the order-raising property gives r x (f x).

theorem SpernerProperty.order_matching_of_surjective_order_raising {α : Type u_1} {β : Type u_2} [DecidableEq α] [Fintype α] [Fintype β] (r : α → β → Prop) (U : (α → ℝ) →ₗ[ℝ] β → ℝ) (hU_surj : Function.Surjective ⇑U) (hU_ord : IsOrderRaisingLinearMap U r) : ∃ (μ : β → α), Function.Injective μ ∧ ∀ (y : β), r (μ y) y

Lemma 4.5 (surjective case). For any graded poset P, if there exists a surjective order-raising linear map U : ℝ^{P_i} → ℝ^{P_{i+1}}, then there exists an order-matching μ : P_{i+1} → P_i.

The proof reduces to the injective case by transposing the matrix representation. If M = toMatrix' U and U is surjective, then M has a right inverse B (M * B = 1), so Mᵀ has a left inverse Bᵀ (Bᵀ * Mᵀ = 1), making the transpose linear map V = toLin' Mᵀ injective. The order-raising property transfers to V with the flipped relation, and the injective case theorem yields the desired matching.