Walk Operator Lemmas

This file proves the key operator identity D ∘ U^{i+1} = U^{i+1} ∘ D + (i+1) • U^i (Equation 43 from the textbook), which follows from the commutation relation DU - UD = I (Lemma 8.2) by induction. This identity is used to push D past blocks of U operators in the proof of Theorem 8.3.

Main results

• WalkCountFormula.liftD_comp_iterU_succ : The operator-level identity liftD ∘ₗ iterU (n + 1) = iterU (n + 1) ∘ₗ liftD + (n + 1) • iterU n
• WalkCountFormula.liftD_comp_iterU_succ_apply : The pointwise version applied to an element.

theorem WalkCountFormula.liftD_mul_liftU_sub : liftD * liftU - liftU * liftD = 1

The commutation relation DU - UD = 1 in the endomorphism ring Module.End ℤ (YoungDiagram →₀ ℤ). This recasts the operator identity liftD_liftU_sub_liftU_liftD as a ring equation.

theorem WalkCountFormula.liftD_comp_iterU_succ (n : ℕ) : liftD ∘ₗ iterU (n + 1) = iterU (n + 1) ∘ₗ liftD + (n + 1) • iterU n

Equation 43 (operator form). The key identity for pushing D past U-blocks: D ∘ U^{n+1} = U^{n+1} ∘ D + (n+1) • U^n.

This specializes the abstract ring identity comm_D_U_pow_succ to the concrete endomorphism ring of YoungDiagram →₀ ℤ, using the commutation DU - UD = I from Lemma 8.2 of the textbook.

theorem WalkCountFormula.liftD_comp_iterU_succ_apply (n : ℕ) (f : YoungDiagram →₀ ℤ) : liftD ((iterU (n + 1)) f) = (iterU (n + 1)) (liftD f) + (n + 1) • (iterU n) f

Equation 43 (pointwise form). For any f : YoungDiagram →₀ ℤ, D(U^{n+1}(f)) = U^{n+1}(D(f)) + (n+1) • U^n(f).

theorem WalkCountFormula.liftD_iterU_succ_emptyBasis (n : ℕ) : liftD ((iterU (n + 1)) emptyBasis) = (n + 1) • (iterU n) emptyBasis

Specialization of Equation 43 to the empty basis element. Since D(∅) = 0, we get D(U^{n+1}(∅)) = (n+1) • U^n(∅).

theorem WalkCountFormula.iterU_liftU_comm (n : ℕ) (f : YoungDiagram →₀ ℤ) : (iterU n) (liftU f) = liftU ((iterU n) f)

Commutativity of liftU with iterU n: U^n(U(f)) = U(U^n(f)). This follows from the fact that powers of U commute with U.