Assembly of the Schur package

The choice of a simple submodule realizing each Jacobi–Trudi character, and the construction of a SchurPackage from the theory. The branching field and the factorial bound enter as parameters, discharged in PairingPos.lean and Common/FactorialBound.lean.

noncomputable def RS.jtSimple (μ : YoungDiagram) : Submodule (MonoidAlgebra ℂ (Equiv.Perm (Fin μ.card))) (MonoidAlgebra ℂ (Equiv.Perm (Fin μ.card)))

The chosen simple submodule realizing jtChar μ.

Equations

• RS.jtSimple μ = Classical.choose ⋯

theorem RS.jtSimple_simple (μ : YoungDiagram) : IsSimpleModule (MonoidAlgebra ℂ (Equiv.Perm (Fin μ.card))) ↥(jtSimple μ)

The chosen submodule is simple.

theorem RS.jtSimple_char (μ : YoungDiagram) (π : Equiv.Perm (Fin μ.card)) : jtChar μ π = nChar (jtSimple μ) π

And its character is the Jacobi–Trudi one it was chosen for.

theorem RS.charIdempotent_jtSimple (μ : YoungDiagram) : charIdempotent (nDim (jtSimple μ)) (jtChar μ) = nProjector (jtSimple μ)

The chosen idempotent is the native projector.

noncomputable def RS.schurPackageOf (H3 : ∀ (n : ℕ), n ^ n ≤ 3 ^ n * n.factorial) (Hbranch : ∀ (lam mu : YoungDiagram), lam ≤ mu → ∀ (h : lam.card ≤ mu.card), charIdempotent (nDim (jtSimple mu)) (jtChar mu) * (symCast h) (charIdempotent (nDim (jtSimple lam)) (jtChar lam)) * charIdempotent (nDim (jtSimple mu)) (jtChar mu) ≠ 0) : SchurPackage

The Schur package, given the branching fact and the factorial bound.

Equations

• One or more equations did not get rendered due to their size.