Bridge: Normal Ordering Applied to the Empty Partition

This file proves DplusU_pow_emptyBasis_eq_sum_bijCoeff_iterU: the normal ordering expansion applied to the empty partition ∅.

Transfer map from ℤ to ℚ

noncomputable def WalkCountBridge.toQ : (YoungDiagram →₀ ℤ) → YoungDiagram →₀ ℚ

@[simp]

theorem WalkCountBridge.toQ_apply (f : YoungDiagram →₀ ℤ) (a : YoungDiagram) : (toQ f) a = ↑(f a)

@[simp]

theorem WalkCountBridge.toQ_single (a : YoungDiagram) (c : ℤ) : toQ (Finsupp.single a c) = Finsupp.single a ↑c

theorem WalkCountBridge.toQ_zero : toQ 0 = 0

theorem WalkCountBridge.toQ_add (f g : YoungDiagram →₀ ℤ) : toQ (f + g) = toQ f + toQ g

theorem WalkCountBridge.toQ_sub (f g : YoungDiagram →₀ ℤ) : toQ (f - g) = toQ f - toQ g

theorem WalkCountBridge.toQ_smul (c : ℤ) (f : YoungDiagram →₀ ℤ) : toQ (c • f) = ↑c • toQ f

ℚ-linear operators

noncomputable def WalkCountBridge.liftU_Q : (YoungDiagram →₀ ℚ) →ₗ[ℚ] YoungDiagram →₀ ℚ

noncomputable def WalkCountBridge.liftD_Q : (YoungDiagram →₀ ℚ) →ₗ[ℚ] YoungDiagram →₀ ℚ

noncomputable def WalkCountBridge.emptyBasis_Q : YoungDiagram →₀ ℚ

@[simp]

theorem WalkCountBridge.liftU_Q_single (a : YoungDiagram) (c : ℚ) : liftU_Q (Finsupp.single a c) = c • toQ a.raisingOp

@[simp]

theorem WalkCountBridge.liftD_Q_single (a : YoungDiagram) (c : ℚ) : liftD_Q (Finsupp.single a c) = c • toQ a.loweringOp

Intertwining

theorem WalkCountBridge.toQ_liftU (f : YoungDiagram →₀ ℤ) : toQ (WalkCountFormula.liftU f) = liftU_Q (toQ f)

theorem WalkCountBridge.toQ_liftD (f : YoungDiagram →₀ ℤ) : toQ (WalkCountFormula.liftD f) = liftD_Q (toQ f)

theorem WalkCountBridge.toQ_emptyBasis : toQ WalkCountFormula.emptyBasis = emptyBasis_Q

theorem WalkCountBridge.toQ_DplusU_pow (n : ℕ) (f : YoungDiagram →₀ ℤ) : toQ (((WalkCountFormula.liftD + WalkCountFormula.liftU) ^ n) f) = ((liftD_Q + liftU_Q) ^ n) (toQ f)

theorem WalkCountBridge.toQ_liftU_pow (n : ℕ) (f : YoungDiagram →₀ ℤ) : toQ ((WalkCountFormula.liftU ^ n) f) = (liftU_Q ^ n) (toQ f)

Commutation for ℚ operators

theorem WalkCountBridge.liftD_Q_comp_liftU_Q_sub (f : YoungDiagram →₀ ℚ) : liftD_Q (liftU_Q f) - liftU_Q (liftD_Q f) = f

theorem WalkCountBridge.liftD_Q_mul_liftU_Q_sub : liftD_Q * liftU_Q - liftU_Q * liftD_Q = 1

D_Q kills empty basis

theorem WalkCountBridge.liftD_Q_emptyBasis_Q : liftD_Q emptyBasis_Q = 0

theorem WalkCountBridge.liftD_Q_pow_emptyBasis_Q {j : ℕ} (hj : 0 < j) : (liftD_Q ^ j) emptyBasis_Q = 0

pairsLE filter

theorem WalkCountBridge.pairsLE_filter_snd_zero (ℓ : ℕ) : {p ∈ NormalOrderCoeff.pairsLE ℓ | p.2 = 0} = Finset.map { toFun := fun (i : ℕ) => (i, 0), inj' := ⋯ } (Finset.range (ℓ + 1))

Helper: evaluate normal order sum at a point

theorem WalkCountBridge.normalOrder_term_apply (c : ℚ) (i j : ℕ) : ((algebraMap ℚ (Module.End ℚ (YoungDiagram →₀ ℚ))) c * (liftU_Q ^ i * liftD_Q ^ j)) emptyBasis_Q = c • (liftU_Q ^ i) ((liftD_Q ^ j) emptyBasis_Q)

Evaluate a normal-ordered operator term at emptyBasis_Q: algebraMap c * (U^i * D^j) applied to emptyBasis_Q equals c • (U^i (D^j emptyBasis_Q)).

Main theorem: normal order at ∅ in ℚ

theorem WalkCountBridge.normalOrder_emptyBasis_Q (ell : ℕ) : ((liftD_Q + liftU_Q) ^ ell) emptyBasis_Q = ∑ i ∈ Finset.range (ell + 1), NormalOrderCoeff.normalOrderCoeff i 0 ell • (liftU_Q ^ i) emptyBasis_Q

The main bridge theorem

theorem WalkCountBridge.DplusU_pow_emptyBasis_eq_sum_bijCoeff_iterU (ell : ℕ) (lam : YoungDiagram) : ↑((((WalkCountFormula.liftD + WalkCountFormula.liftU) ^ ell) WalkCountFormula.emptyBasis) lam) = ∑ i ∈ Finset.range (ell + 1), NormalOrderCoeff.bijCoeff i 0 ell * ↑(((WalkCountFormula.iterU i) WalkCountFormula.emptyBasis) lam)