Raising/Lowering Operators as LinearMaps

This file defines the raising operator U and lowering operator D on the free ℤ-module YoungDiagram →₀ ℤ as proper LinearMaps, along with iteration and walk-application infrastructure for Theorem 8.3.

Main definitions

• WalkCountFormula.liftU : (YoungDiagram →₀ ℤ) →ₗ[ℤ] (YoungDiagram →₀ ℤ) — the raising operator
• WalkCountFormula.liftD : (YoungDiagram →₀ ℤ) →ₗ[ℤ] (YoungDiagram →₀ ℤ) — the lowering operator
• WalkCountFormula.iterU : iterated raising operator U^n
• WalkCountFormula.iterD : iterated lowering operator D^n
• WalkCountFormula.emptyBasis : the basis element ⊥ (empty partition)
• WalkCountFormula.applyWord : application of a word w = (r₁,s₁)...(rₖ,sₖ) as U^{r₁}D^{s₁}...U^{rₖ}D^{sₖ}

Key properties

Being LinearMaps, liftU and liftD automatically satisfy map_add and map_smul, which eliminates the need to prove smul compatibility manually.

noncomputable def WalkCountFormula.liftU : (YoungDiagram →₀ ℤ) →ₗ[ℤ] YoungDiagram →₀ ℤ

The raising operator U as a ℤ-linear map on the free module YoungDiagram →₀ ℤ.

On a basis element λ, U(λ) = ∑_{σ ∈ coversUp(λ)} σ. This is the linear extension of YoungDiagram.raisingOp to formal ℤ-linear combinations.

noncomputable def WalkCountFormula.liftD : (YoungDiagram →₀ ℤ) →ₗ[ℤ] YoungDiagram →₀ ℤ

The lowering operator D as a ℤ-linear map on the free module YoungDiagram →₀ ℤ.

On a basis element λ, D(λ) = ∑_{ν ∈ coversDown(λ)} ν. This is the linear extension of YoungDiagram.loweringOp to formal ℤ-linear combinations.

noncomputable def WalkCountFormula.iterU (n : ℕ) : (YoungDiagram →₀ ℤ) →ₗ[ℤ] YoungDiagram →₀ ℤ

U^n — the raising operator iterated n times.

noncomputable def WalkCountFormula.iterD (n : ℕ) : (YoungDiagram →₀ ℤ) →ₗ[ℤ] YoungDiagram →₀ ℤ

D^n — the lowering operator iterated n times.

noncomputable def WalkCountFormula.emptyBasis : YoungDiagram →₀ ℤ

The empty partition as a basis element in YoungDiagram →₀ ℤ.

noncomputable def WalkCountFormula.applyWord (w : List (ℕ × ℕ)) : (YoungDiagram →₀ ℤ) →ₗ[ℤ] YoungDiagram →₀ ℤ

Apply a word w = [(r₁,s₁), ..., (rₖ,sₖ)] as the composition U^{rₖ} D^{sₖ} ∘ ⋯ ∘ U^{r₁} D^{s₁}.

Note: the list is applied left-to-right, so the first pair acts first.

Basic API lemmas

@[simp]

theorem WalkCountFormula.liftU_single (lam : YoungDiagram) (c : ℤ) : liftU (Finsupp.single lam c) = c • lam.raisingOp

@[simp]

theorem WalkCountFormula.liftD_single (lam : YoungDiagram) (c : ℤ) : liftD (Finsupp.single lam c) = c • lam.loweringOp

theorem WalkCountFormula.liftU_single_one (lam : YoungDiagram) : liftU (Finsupp.single lam 1) = lam.raisingOp

theorem WalkCountFormula.liftD_single_one (lam : YoungDiagram) : liftD (Finsupp.single lam 1) = lam.loweringOp

theorem WalkCountFormula.bot_colLen_zero : ⊥.colLen 0 = 0

theorem WalkCountFormula.removableRows_bot : ⊥.removableRows = ∅

theorem WalkCountFormula.coversDown_bot : ⊥.coversDown = ∅

The empty Young diagram has no removable rows.

theorem WalkCountFormula.loweringOp_bot : ⊥.loweringOp = 0

The lowering operator sends the empty partition to zero.

theorem WalkCountFormula.liftD_emptyBasis : liftD emptyBasis = 0

The lowering operator applied to the empty partition gives zero, since ⊥ has no diagrams below it.

@[simp]

theorem WalkCountFormula.iterU_zero : iterU 0 = LinearMap.id

iterU 0 = id.

@[simp]

theorem WalkCountFormula.iterD_zero : iterD 0 = LinearMap.id

iterD 0 = id.

theorem WalkCountFormula.iterU_succ (n : ℕ) : iterU (n + 1) = iterU n ∘ₗ liftU

iterU (n + 1) = iterU n ∘ liftU.

theorem WalkCountFormula.iterD_succ (n : ℕ) : iterD (n + 1) = iterD n ∘ₗ liftD

iterD (n + 1) = iterD n ∘ liftD.

@[simp]

theorem WalkCountFormula.applyWord_nil : applyWord [] = LinearMap.id

The empty word applies as the identity.

theorem WalkCountFormula.applyWord_singleton (r s : ℕ) : applyWord [(r, s)] = iterD s ∘ₗ iterU r

Applying a single block (r, s).

Helper lemmas for the commutation relation

theorem WalkCountFormula.raisingOp_apply (ν mu : YoungDiagram) : ν.raisingOp mu = if mu ∈ ν.coversUp then 1 else 0

Evaluation of the raising operator at a point.

theorem WalkCountFormula.loweringOp_apply (σ mu : YoungDiagram) : σ.loweringOp mu = if mu ∈ σ.coversDown then 1 else 0

Evaluation of the lowering operator at a point.

theorem WalkCountFormula.liftD_raisingOp_apply (lam mu : YoungDiagram) : (liftD lam.raisingOp) mu = lam.DU_apply mu

liftD (raisingOp lam) evaluated at mu equals DU_apply lam mu.

theorem WalkCountFormula.liftU_loweringOp_apply (lam mu : YoungDiagram) : (liftU lam.loweringOp) mu = lam.UD_apply mu

liftU (loweringOp lam) evaluated at mu equals UD_apply lam mu.

theorem WalkCountFormula.DU_apply_eq_DUCoeff (lam mu : YoungDiagram) : lam.DU_apply mu = ↑(lam.DUCoeff mu)

DU_apply lam mu equals ↑(DUCoeff lam mu).

theorem WalkCountFormula.UD_apply_eq_UDCoeff (lam mu : YoungDiagram) : lam.UD_apply mu = ↑(lam.UDCoeff mu)

UD_apply lam mu equals ↑(UDCoeff lam mu).

theorem WalkCountFormula.liftD_comp_liftU_sub (f : YoungDiagram →₀ ℤ) : liftD (liftU f) - liftU (liftD f) = f

The commutation relation DU - UD = I for all f : YoungDiagram →₀ ℤ. This is the operator-level version of Lemma 8.2.

theorem WalkCountFormula.liftD_liftU_sub_liftU_liftD : liftD ∘ₗ liftU - liftU ∘ₗ liftD = LinearMap.id

The commutation relation DU - UD = I as an identity of linear operators. This is Lemma 8.2 of the textbook, lifted to the operator level.

theorem WalkCountFormula.iterU_succ' (n : ℕ) : iterU (n + 1) = liftU ∘ₗ iterU n

iterU (n + 1) = liftU ∘ iterU n.

theorem WalkCountFormula.liftD_liftU_eq (f : YoungDiagram →₀ ℤ) : liftD (liftU f) = liftU (liftD f) + f

The commutation relation DU(f) = UD(f) + f.

theorem WalkCountFormula.liftD_iterU_emptyBasis (k : ℕ) : liftD ((iterU k) emptyBasis) = ↑k • (iterU (k - 1)) emptyBasis

Applying D to U^k(∅) gives k · U^{k-1}(∅). This follows from DU = UD + I and D(∅) = 0 by induction on k.