DU - UD Commutation Relation for the Boolean Algebra

This file formalizes Lemma 4.6 from Stanley's Algebraic Combinatorics.

Main results

• boolean_DU_UD_commutator: Lemma 4.6 — For the boolean algebra B_n, D_{i+1}U_i − U_{i−1}D_i = (n−2i)·Id on the rank-i level.

Proof strategy

Diagonal: (n−i) − i = n − 2i. Off-diagonal: both counts agree.

def BooleanCommutator.DU_coeff {n : ℕ} (i : ℕ) (x z : Finset (Fin n)) : ℕ

The (x,z)-entry of [D_{i+1}][U_i]: #{y : |y|=i+1, x⊆y, z⊆y}.

def BooleanCommutator.UD_coeff {n : ℕ} (i : ℕ) (x z : Finset (Fin n)) : ℕ

The (x,z)-entry of [U_{i−1}][D_i]: #{w : |w|=i−1, w⊆x, w⊆z}. When i = 0, D_0 = 0 by convention, so this is 0.

theorem BooleanCommutator.card_supersets_insert {n : ℕ} (x : Finset (Fin n)) : {y : Finset (Fin n) | y.card = x.card + 1 ∧ x ⊆ y}.card = n - x.card

#{y : |y| = |x|+1, x ⊆ y} = n − |x|.

theorem BooleanCommutator.DU_coeff_diag {n : ℕ} (i : ℕ) (x : Finset (Fin n)) (hx : x.card = i) : DU_coeff i x x = n - i

Equation (22) diagonal. #{y : |y|=i+1, x ⊆ y} = n − i.

theorem BooleanCommutator.UD_coeff_diag {n : ℕ} (i : ℕ) (x : Finset (Fin n)) (hx : x.card = i) : UD_coeff i x x = i

Equation (23) diagonal. #{w : |w|=i−1, w ⊆ x} = i.

theorem BooleanCommutator.DU_UD_coeff_off_diag {n : ℕ} (i : ℕ) (x z : Finset (Fin n)) (hx : x.card = i) (hz : z.card = i) (hne : x ≠ z) : DU_coeff i x z = UD_coeff i x z

Off-diagonal equality. For x ≠ z with |x| = |z| = i, DU_coeff = UD_coeff.

theorem BooleanCommutator.boolean_DU_UD_commutator {n : ℕ} (i : ℕ) (x z : Finset (Fin n)) (hx : x.card = i) (hz : z.card = i) (hi : i ≤ n) : ↑(DU_coeff i x z) - ↑(UD_coeff i x z) = if z = x then ↑n - 2 * ↑i else 0

Lemma 4.6 (Stanley). D_{i+1}U_i − U_{i−1}D_i = (n−2i)·Id on level P_i of B_n.

For x, z ∈ (B_n)_i, the matrix entry DU_coeff − UD_coeff equals n−2i if z = x, else 0.