Concrete Young Lattice Family Instance #

This file constructs a concrete YoungLatticeFamily instance from the raising/lowering operators on Young's lattice, making young_lattice_eigenvalues_closed (Theorem 8.8) apply unconditionally.

Main results #

youngLatticeInstance : YoungEigenvalues.YoungLatticeFamily — The concrete instance.
young_lattice_eigenvalues_unconditional — Theorem 8.8 with no parameters.

Strategy #

The construction bridges:

PartitionSpace i = Nat.Partition i →₀ ℝ (the typed level spaces)
YoungDiagram.coversUp / coversDown (the covering relations)
partitionEquiv i : Nat.Partition i ≃ {μ : YoungDiagram // μ.card = i}
young_commutation_coeff (the coefficient-level DU - UD = δ identity)

Card lemmas for addCell and removeCell #

source

theorem YoungDiagram.addCell_card (μ : YoungDiagram) (i : ℕ) (hadd : i = 0 ∨ μ.rowLen (i - 1) > μ.rowLen i) :

(μ.addCell i hadd).card = μ.card + 1

Adding a cell increases the card by 1.

source

theorem YoungDiagram.removeCell_card (μ : YoungDiagram) (i : ℕ) (hrem : i + 1 = μ.colLen 0 ∨ μ.rowLen i > μ.rowLen (i + 1)) :

(μ.removeCell i hrem).card = μ.card - 1

Removing a cell decreases the card by 1.

source

theorem YoungDiagram.card_of_mem_coversUp {μ σ : YoungDiagram} (hσ : σ ∈ μ.coversUp) :

σ.card = μ.card + 1

If σ ∈ coversUp(μ), then σ.card = μ.card + 1.

source

theorem YoungDiagram.card_of_mem_coversDown {μ ν : YoungDiagram} (hν : ν ∈ μ.coversDown) :

ν.card = μ.card - 1

If ν ∈ coversDown(μ), then ν.card = μ.card - 1.

Bridge between Nat.Partition and YoungDiagram #

source

@[reducible, inline]

abbrev YoungLatticeFamilyInstance.toYD {i : ℕ} (μ : i.Partition) :

YoungDiagram

Convert Nat.Partition i to YoungDiagram.

Instances For

source

theorem YoungLatticeFamilyInstance.toYD_card {i : ℕ} (μ : i.Partition) :

(toYD μ).card = i

The card of the YoungDiagram for Nat.Partition i is i.

source

@[reducible, inline]

abbrev YoungLatticeFamilyInstance.fromYD {i : ℕ} (σ : YoungDiagram) (hσ : σ.card = i) :

i.Partition

Convert a YoungDiagram with card = i to Nat.Partition i.

Instances For

source

theorem YoungLatticeFamilyInstance.fromYD_toYD {i : ℕ} (μ : i.Partition) :

fromYD (toYD μ) ⋯ = μ

source

theorem YoungLatticeFamilyInstance.toYD_fromYD {i : ℕ} (σ : YoungDiagram) (hσ : σ.card = i) :

toYD (fromYD σ hσ) = σ

Image functions for U and D #

source

noncomputable def YoungLatticeFamilyInstance.raiseImage {i : ℕ} (μ : i.Partition) :

YoungEigenvalues.PartitionSpace (i + 1)

The image of a basis partition μ ⊢ i under the raising operator: ∑_{σ ∈ coversUp(toYD μ)} δ_{fromYD σ} in PartitionSpace (i+1).

Instances For

source

noncomputable def YoungLatticeFamilyInstance.lowerImage {i : ℕ} (ν : (i + 1).Partition) :

YoungEigenvalues.PartitionSpace i

The image of a basis partition ν ⊢ i+1 under the lowering operator: ∑_{ρ ∈ coversDown(toYD ν)} δ_{fromYD ρ} in PartitionSpace i.

Instances For

source

theorem YoungLatticeFamilyInstance.raiseImage_dite_pos {i : ℕ} (μ : i.Partition) {σ : YoungDiagram} (hσ : σ ∈ (toYD μ).coversUp) :

σ.card = i + 1

The dite in raiseImage is always the positive branch.

source

theorem YoungLatticeFamilyInstance.lowerImage_dite_pos {i : ℕ} (ν : (i + 1).Partition) {ρ : YoungDiagram} (hρ : ρ ∈ (toYD ν).coversDown) :

ρ.card = i

The dite in lowerImage is always the positive branch.

Concrete raising and lowering operators as linear maps #

source

noncomputable def YoungLatticeFamilyInstance.concreteU (i : ℕ) :

YoungEigenvalues.PartitionSpace i →ₗ[ℝ ] YoungEigenvalues.PartitionSpace (i + 1)

The concrete raising operator at level i.

Instances For

source

noncomputable def YoungLatticeFamilyInstance.concreteD (i : ℕ) :

YoungEigenvalues.PartitionSpace (i + 1) →ₗ[ℝ ] YoungEigenvalues.PartitionSpace i

The concrete lowering operator at level i.

Instances For

Properties of the concrete operators #

The following four properties are consequences of Lemma 8.2 in the book. Their proofs require lifting the coefficient-level commutation identity young_commutation_coeff through the partitionEquiv bridge and the Finsupp.linearCombination layer — a substantial Finsupp manipulation. The book proves these facts (Lemma 8.2) but the formalized coefficient-level result operates on YoungDiagram →₀ ℤ while the structure requires linear maps on Nat.Partition i →₀ ℝ. Bridging these requires extensive infrastructure not yet present.

source

theorem YoungLatticeFamilyInstance.toYD_injective {n : ℕ} :

Function.Injective toYD

toYD is injective.

source

theorem YoungLatticeFamilyInstance.fromYD_eq_iff {n : ℕ} (σ : YoungDiagram) (h : σ.card = n) (ν : n.Partition) :

fromYD σ h = ν ↔ σ = toYD ν

fromYD σ h = ν ↔ σ = toYD ν.

source

theorem YoungLatticeFamilyInstance.raiseImage_apply {i : ℕ} (μ : i.Partition) (ν : (i + 1).Partition) :

(raiseImage μ) ν = if toYD ν ∈ (toYD μ).coversUp then 1 else 0

raiseImage μ evaluated at ν is 1 if toYD ν ∈ coversUp(toYD μ), else 0.

source

theorem YoungLatticeFamilyInstance.lowerImage_apply {i : ℕ} (ν : (i + 1).Partition) (μ : i.Partition) :

(lowerImage ν) μ = if toYD μ ∈ (toYD ν).coversDown then 1 else 0

lowerImage ν evaluated at μ is 1 if toYD μ ∈ coversDown(toYD ν), else 0.

source

theorem DUCoeff_eq_UDCoeff_add_delta (lam mu : YoungDiagram) :

↑(lam.DUCoeff mu) = (if lam = mu then 1 else 0) + ↑(lam.UDCoeff mu)

source

theorem YoungLatticeFamilyInstance.DU_single_coeff {i : ℕ} (μ ν : (i + 1).Partition) :

((Finsupp.linearCombination ℝ lowerImage) (raiseImage μ)) ν = ↑((toYD μ).DUCoeff (toYD ν))

LHS of commutation on single μ, evaluated at ν, equals DUCoeff.

source

theorem YoungLatticeFamilyInstance.id_UD_single_coeff {i : ℕ} (μ ν : (i + 1).Partition) :

(Finsupp.single μ 1) ν + ((Finsupp.linearCombination ℝ raiseImage) (lowerImage μ)) ν = (if toYD μ = toYD ν then 1 else 0) + ↑((toYD μ).UDCoeff (toYD ν))

RHS of commutation on single μ, evaluated at ν, equals δ + UDCoeff.

source

theorem YoungLatticeFamilyInstance.concrete_commutation (i : ℕ) (w : YoungEigenvalues.PartitionSpace (i + 1)) :

(concreteD (i + 1)) ((concreteU (i + 1)) w) = w + (concreteU i) ((concreteD i) w)

The commutation relation at level i (Lemma 8.2, Finsupp-level).

source

theorem YoungLatticeFamilyInstance.raiseImage_eq_lowerImage_swap {i : ℕ} (μ : i.Partition) (ν : (i + 1).Partition) :

(raiseImage μ) ν = (lowerImage ν) μ

U and D are adjoint: raiseImage(μ)(ν) = lowerImage(ν)(μ).

source

theorem YoungLatticeFamilyInstance.exists_lowerImage_one {i : ℕ} (μ : i.Partition) :

∃ (ν : (i + 1).Partition), (lowerImage ν) μ = 1

Every partition of i appears in some lowerImage(ν).

source

theorem YoungLatticeFamilyInstance.concreteUD_kernel_trivial (j : ℕ) (d : YoungEigenvalues.PartitionSpace (j + 1)) (haz : d + (concreteU j) ((concreteD j) d) = 0) :

d = 0

If d + concreteU j (concreteD j d) = 0 then d = 0. This is the shared sum-of-squares / adjointness argument used by both concreteD_surjective and concreteU_injective.

source

theorem YoungLatticeFamilyInstance.concreteD_surjective (i : ℕ) :

Function.Surjective ⇑(concreteD i)

Surjectivity of concreteD i for all i.

source

theorem YoungLatticeFamilyInstance.concreteU_injective (i : ℕ) :

Function.Injective ⇑(concreteU i)

Injectivity of the concrete raising operator (Lemma 8.2 consequence). Proved using the norm-squared / adjointness argument: if U(w) = 0 then from DU = Id + UD we get w + U'D'w = 0, so ⟨w,w⟩ + ⟨D'w, D'w⟩ = 0, hence w = 0.

source

noncomputable def YoungLatticeFamilyInstance.concreteOps (i : ℕ) :

YoungEigenvalues.YoungLatticeOps i

The concrete Young lattice operators at level i.

Instances For

source

theorem YoungLatticeFamilyInstance.base_DU_eq_id :

(concreteOps 0).D ∘ₗ (concreteOps 0).U = LinearMap.id

Base case of Lemma 8.2: D₁ ∘ U₀ = Id on PartitionSpace 0.

source

noncomputable def YoungLatticeFamilyInstance.youngLatticeInstance :

YoungEigenvalues.YoungLatticeFamily