Documentation

TauCeti.Algebra.Lie.HighestWeight.Tensor

Tensor multiplicities of irreducible modules #

Let L be a finite-dimensional Lie algebra with non-degenerate Killing form over an algebraically closed field of characteristic zero, H a Cartan subalgebra and b a base of its root system. The tensor multiplicity TauCeti.tensorMultiplicity b lam mu nu is the dimension of the space of morphisms L(nu) →ₗ⁅K,L⁆ L(lam) ⊗ L(mu). For dominant integral lam and mu the tensor product is a finite-dimensional L-module, so Weyl's theorem decomposes it into irreducibles, and at a nu with L(nu) nonzero, hence irreducible, that dimension is the number of copies of L(nu) in the decomposition, the structure constant c^nu_{lam mu}. The definition itself, and the lemmas reading irreducibility off a nonzero multiplicity, ask only for a triangularizable Cartan subalgebra; algebraic closure enters with the character identity, which calls on Weyl's complete reducibility theorem.

The theorem about it is the character identity

ch L(lam) · ch L(mu) = ∑_nu c^nu_{lam mu} · ch L(nu),

which combines two facts already in place: formal characters are multiplicative on tensor products (TauCeti.formalCharacter_tensor), and the character of a finite-dimensional module is the multiplicity-weighted sum of the irreducible characters (TauCeti.formalCharacter_eq_finsum_isotypicMultiplicity_smul). It is what makes the tensor multiplicities computable from characters, and the identity a Pieri or Littlewood-Richardson rule evaluates.

Every L(nu) is irreducible, the Verma module M(nu) being nonzero (TauCeti.vermaGenerator_ne_zero), so the identity is a statement about honest irreducibles, and it never degenerates to 0 = 0: some c^nu_{lam mu} is nonzero (TauCeti.exists_tensorMultiplicity_ne_zero), because L(lam) ⊗ L(mu) is a nonzero finite-dimensional module.

Main definitions #

Main results #

References #

This is the tensor-multiplicity item of the milestone "tensor multiplicities and the minuscule Pieri rule" in the Layer 6 decomposition toolkit of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md, which asks for c^ν_{λμ} "with the character identity ch L(λ) · ch L(μ) = Σ_ν c^ν_{λμ} ch L(ν) through formalCharacter_tensor". The minuscule Pieri rule itself, which evaluates these multiplicities, awaits the Weyl character formula.

source
noncomputable def TauCeti.tensorMultiplicity {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (b : (LieAlgebra.IsKilling.rootSystem H).Base) (lam mu nu : Module.Dual K ↥H) :
ℕ

The tensor multiplicity c^nu_{lam mu}: the multiplicity of L(nu) in L(lam) ⊗ L(mu) in the sense of LieModule.isotypicMultiplicity, that is the dimension of the space of morphisms L(nu) →ₗ⁅K,L⁆ L(lam) ⊗ L(mu).

It is the number of copies of L(nu) in a decomposition of the tensor product into irreducibles when that reading is available: lam and mu dominant integral, so that the tensor product is finite-dimensional and completely reducible, L(nu) being irreducible.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.tensorMultiplicity_def {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (b : (LieAlgebra.IsKilling.rootSystem H).Base) (lam mu nu : Module.Dual K ↥H) :
    tensorMultiplicity b lam mu nu = LieModule.isotypicMultiplicity K L (TensorProduct K (irreducibleQuotient b lam) (irreducibleQuotient b mu)) (irreducibleQuotient b nu)

    The tensor multiplicity is the multiplicity of L(nu) in the tensor product.

    The character identity #

    The character of L(lam) is the character of a decomposition into irreducibles, so from here on the field is algebraically closed: that is what Weyl's complete reducibility theorem is available over in TauCeti/Algebra/Lie/HighestWeight/Decomposition.lean.

    source
    theorem TauCeti.irreducibleFormalCharacter_mul_eq_finsum_tensorMultiplicity_smul {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (b : (LieAlgebra.IsKilling.rootSystem H).Base) [IsAlgClosed K] (lam mu : { l : Module.Dual K ↥H // IsDominantIntegral b l }) :
    irreducibleFormalCharacter b lam * irreducibleFormalCharacter b mu = ∑ᶠ (nu : { l : Module.Dual K ↥H // IsDominantIntegral b l }), ↑(tensorMultiplicity b ↑lam ↑mu ↑nu) • irreducibleFormalCharacter b nu

    The character identity for a tensor product of highest weight modules: the product of the characters of L(lam) and L(mu) is the sum of the characters of the L(nu), weighted by the tensor multiplicities.

    Formal characters are multiplicative on tensor products, so the left-hand side is the character of L(lam) ⊗ L(mu); that module is finite-dimensional, so its character is the multiplicity-weighted sum of the irreducible characters.

    source
    theorem TauCeti.exists_tensorMultiplicity_ne_zero {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] (b : (LieAlgebra.IsKilling.rootSystem H).Base) [IsAlgClosed K] (lam mu : { l : Module.Dual K ↥H // IsDominantIntegral b l }) :
    ∃ (nu : { l : Module.Dual K ↥H // IsDominantIntegral b l }), tensorMultiplicity b ↑lam ↑mu ↑nu ≠ 0

    The character identity is never a statement about zero modules. L(lam) ⊗ L(mu) is a nonzero finite-dimensional module, so at least one tensor multiplicity is nonzero, and the sum ch L(lam) · ch L(mu) = ∑_nu c^nu_{lam mu} · ch L(nu) has a term that survives.