Schur's lemma for Lie modules to Weyl's theorem as a…

TheoremSchur's lemma for Lie modules#

Over an algebraically closed field, a morphism of a finite-dimensional irreducible L-module to itself is multiplication by a scalar: an eigenvalue exists, and the corresponding eigenspace is a nonzero Lie submodule, hence everything.

TauCeti.exists_forall_apply_eq_smul.{u, v, w} (K : Type u) [Field K] (L : Type v) [LieRing L]
  [LieAlgebra K L] (M : Type w) [AddCommGroup M] [_root_.Module K M] [LieRingModule L M]
  [LieModule K L M] [LieModule.IsIrreducible K L M] [IsAlgClosed K] [FiniteDimensional K M]
  (f : M →ₗ⁅K,L⁆ M) : ∃ c, ∀ (m : M), f m = c • m

Lean

Formalized in Tau Ceti as TauCeti.exists_forall_apply_eq_smul.

Other forms

Schur's lemma for finite-dimensional irreducible Lie modules over an algebraically closed field, in its dimension form. Formalized in Tau Ceti as TauCeti.LieModule.finrank_lieModuleHom.

TauCeti.LieModule.finrank_lieModuleHom.{u, v, w, w₁} (K : Type u) (L : Type v) {M : Type w}
  {N : Type w₁} [Field K] [IsAlgClosed K] [LieRing L] [LieAlgebra K L] [AddCommGroup M]
  [_root_.Module K M] [LieRingModule L M] [LieModule K L M] [AddCommGroup N] [_root_.Module K N]
  [LieRingModule L N] [LieModule K L N] [FiniteDimensional K M] [LieModule.IsIrreducible K L M]
  [LieModule.IsIrreducible K L N] :
  Module.finrank K (M →ₗ⁅K,L⁆ N) = if Nonempty (M ≃ₗ⁅K,L⁆ N) then 1 else 0

Schur's lemma for Lie modules, in its bijectivity form. Formalized in Tau Ceti as TauCeti.LieModule.bijective_of_ne_zero.

TauCeti.LieModule.bijective_of_ne_zero.{u, v, w, w₁} {R : Type u} {L : Type v} {M : Type w}
  {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [_root_.Module R M] [LieRingModule L M]
  [AddCommGroup N] [_root_.Module R N] [LieRingModule L N] [LieModule.IsIrreducible R L M]
  [LieModule.IsIrreducible R L N] {f : M →ₗ⁅R,L⁆ N} (hf : f ≠ 0) : Function.Bijective ⇑f

Sources

• Tau Ceti documentation: TauCeti.exists_forall_apply_eq_smul
• Source of TauCeti.exists_forall_apply_eq_smul in TauCeti/Algebra/Lie/Weights/Central.lean

LeanTauCeti.exists_forall_apply_eq_smul · TauCeti.LieModule.finrank_lieModuleHom · TauCeti.LieModule.bijective_of_ne_zero

Used by 2

Used byTauCeti.LieAlgebra.exists_eq_smul_killingForm · The Brauer–Klimyk formula, in group-algebra form

TheoremThe structure theorem for reductive Lie algebras#

Over a field of characteristic zero, a finite-dimensional Lie algebra is reductive (its solvable radical is its centre) if and only if it is the direct sum of its centre and its derived ideal, with the derived ideal semisimple.

The reverse implication only uses the second conjunct: semisimplicity of the derived ideal alone implies reductivity, through TauCeti.hasCentralRadical_of_hasTrivialRadical_derivedSeries, and hence the first conjunct. The first conjunct alone is not enough: the semidirect product sl₂ ⋉ K² with the standard module has trivial centre and is its own derived ideal, so it satisfies the first conjunct without being reductive.

TauCeti.hasCentralRadical_iff_isCompl_center_derivedSeries.{u, v} (K : Type u) (L : Type v)
  [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] :
  LieAlgebra.HasCentralRadical K L ↔
    IsCompl (LieAlgebra.center K L) (LieAlgebra.derivedSeries K L 1) ∧
      LieAlgebra.IsSemisimple K ↥(LieAlgebra.derivedSeries K L 1)

Lean

Formalized in Tau Ceti as TauCeti.hasCentralRadical_iff_isCompl_center_derivedSeries.

Sources

• Tau Ceti documentation: TauCeti.hasCentralRadical_iff_isCompl_center_derivedSeries
• Source of TauCeti.hasCentralRadical_iff_isCompl_center_derivedSeries in TauCeti/Algebra/Lie/Reductive/Basic.lean

LeanTauCeti.hasCentralRadical_iff_isCompl_center_derivedSeries

Uses 1

Proof usesWeyl's theorem as a decomposition

TheoremThe Weyl character formula#

For a finite-dimensional module M generated by a highest weight vector of weight lam, the formal character of M times the Weyl denominator is the Weyl numerator of lam: ch M · ∏_{α>0} (1 - e^{-α}) = ∑_{w ∈ W} sgn(w) e^{w(lam + ρ) - ρ}.

Both sides are alternating for the dot action and supported in lam - Q⁺, so TauCeti.formalCharacter_mul_weylDenominator_eq_of_forall_coeff_isDominantIntegral_eq reduces the identity to the coefficients at the dominant integral weights. There both sides are 1 at lam and 0 elsewhere: on the left by the two coefficient computations above and coeff_formalCharacter_mul_weylDenominator_eq_one_of_isHighestWeightVector_of_lieSpan_eq_top, on the right because the dot orbit of a dominant integral weight is free and meets the dominant integral weights only at lam.

Such an M is irreducible, by TauCeti.isIrreducible_of_isHighestWeightVector_of_lieSpan_eq_top, so this is the character of L(lam); it is stated for M itself so that no identification with L(lam) is needed to use it.

TauCeti.formalCharacter_mul_weylDenominator_eq_weylNumerator.{u, v, w} {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] {M : Type w}
  [AddCommGroup M] [_root_.Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M]
  [IsAlgClosed K] {b : (LieAlgebra.IsKilling.rootSystem H).Base} {lam : Module.Dual K ↥H} {v : M}
  (hv : TauCeti.IsHighestWeightVector b lam v) (hgen : LieSubmodule.lieSpan K L {v} = ⊤)
  [Fintype ↥(LieAlgebra.IsKilling.rootSystem H).weylGroup] :
  TauCeti.formalCharacter K (↥H) M * TauCeti.weylDenominator (LieAlgebra.IsKilling.rootSystem H) b =
    TauCeti.weylNumerator (LieAlgebra.IsKilling.rootSystem H) b lam

Lean

Formalized in Tau Ceti as TauCeti.formalCharacter_mul_weylDenominator_eq_weylNumerator.

Sources

• Tau Ceti documentation: TauCeti.formalCharacter_mul_weylDenominator_eq_weylNumerator
• Source of TauCeti.formalCharacter_mul_weylDenominator_eq_weylNumerator in TauCeti/Algebra/Lie/HighestWeight/Weyl/Character.lean

LeanTauCeti.formalCharacter_mul_weylDenominator_eq_weylNumerator

Uses 1 · Used by 3

Proof usesFreudenthal's multiplicity formula

Used byKostant's multiplicity formula · The Brauer–Klimyk formula, in group-algebra form · The Weyl dimension formula (TauCeti.finrank_eq_prod_coweightPairing_div)

TheoremThe Weyl dimension formula (TauCeti.finrank_eq_prod_coweightPairing_div)#

For a finite-dimensional module M generated by a highest weight vector of weight lam,

dim M = ∏_{α>0} ⟨lam + ρ, α^∨⟩ / ⟨ρ, α^∨⟩,

the product running over the positive roots, with ρ the Weyl vector of the base and ⟨·, α^∨⟩ the integer coroot pairing TauCeti.coweightPairing. Such an M is irreducible, so this is the dimension of L(lam) for every dominant integral weight lam at which L(lam) is nonzero.

TauCeti.finrank_eq_prod_coweightPairing_div.{u, v, w} {K : Type u} {L : Type v} [Field K]
  [CharZero K] [IsAlgClosed K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L]
  [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] {M : Type w}
  [AddCommGroup M] [_root_.Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M]
  {b : (LieAlgebra.IsKilling.rootSystem H).Base} {lam : Module.Dual K ↥H} {v : M}
  (hv : TauCeti.IsHighestWeightVector b lam v) (hgen : LieSubmodule.lieSpan K L {v} = ⊤) :
  ↑(Module.finrank K M) =
    ∏ i ∈ TauCeti.posRootsFinset (LieAlgebra.IsKilling.rootSystem H) b,
      ↑(TauCeti.coweightPairing (lam + TauCeti.weylVector (LieAlgebra.IsKilling.rootSystem H) b)
            i) /
        ↑(TauCeti.coweightPairing (TauCeti.weylVector (LieAlgebra.IsKilling.rootSystem H) b) i)

Lean

Formalized in Tau Ceti as TauCeti.finrank_eq_prod_coweightPairing_div.

Other forms

The Weyl dimension formula, division-free. Formalized in Tau Ceti as TauCeti.finrank_mul_prod_coweightPairing_weylVector_eq.

TauCeti.finrank_mul_prod_coweightPairing_weylVector_eq.{u, v, w} {K : Type u} {L : Type v} [Field K]
  [CharZero K] [IsAlgClosed K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L]
  [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] {M : Type w}
  [AddCommGroup M] [_root_.Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M]
  {b : (LieAlgebra.IsKilling.rootSystem H).Base} {lam : Module.Dual K ↥H} {v : M}
  (hv : TauCeti.IsHighestWeightVector b lam v) (hgen : LieSubmodule.lieSpan K L {v} = ⊤) :
  ↑(Module.finrank K M) *
      ∏ i ∈ TauCeti.posRootsFinset (LieAlgebra.IsKilling.rootSystem H) b,
        TauCeti.coweightPairing (TauCeti.weylVector (LieAlgebra.IsKilling.rootSystem H) b) i =
    ∏ i ∈ TauCeti.posRootsFinset (LieAlgebra.IsKilling.rootSystem H) b,
      TauCeti.coweightPairing (lam + TauCeti.weylVector (LieAlgebra.IsKilling.rootSystem H) b) i

Sources

• Tau Ceti documentation: TauCeti.finrank_eq_prod_coweightPairing_div
• Source of TauCeti.finrank_eq_prod_coweightPairing_div in TauCeti/Algebra/Lie/HighestWeight/Weyl/Dimension.lean

LeanTauCeti.finrank_eq_prod_coweightPairing_div · TauCeti.finrank_mul_prod_coweightPairing_weylVector_eq

Uses 2

Proof usesThe Weyl character formula · The Weyl dimension formula (TauCeti.sum_coeff_mul_prod_coroot'_weylVector_eq)

TheoremWeyl's complete reducibility theorem#

Over a field of characteristic zero, every Lie submodule of a finite-dimensional module over a Lie algebra with nondegenerate Killing form has a complement, so the module is a direct sum of irreducibles.

The sl₂ case, TauCeti.exists_isCompl_of_toLieSubalgebra_eq_top, is the rank-one instance of the same argument, run with the concrete Casimir operator of an sl₂ triple.

TauCeti.exists_isCompl_of_isKilling.{u, v, w} {K : Type u} {L : Type v} [Field K] [CharZero K]
  [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {M : Type w}
  [AddCommGroup M] [_root_.Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M]
  (N : LieSubmodule K L M) : ∃ N', IsCompl N N'

Lean

Formalized in Tau Ceti as TauCeti.exists_isCompl_of_isKilling.

Sources

• Tau Ceti documentation: TauCeti.exists_isCompl_of_isKilling
• Source of TauCeti.exists_isCompl_of_isKilling in TauCeti/Algebra/Lie/HighestWeight/CompleteReducibility.lean

LeanTauCeti.exists_isCompl_of_isKilling

Used by 4

Used byMatsushima's criterion, affine direction, in characteristic zero · Weyl's theorem for algebraic groups · The lattice form of Weyl's theorem · Weyl's theorem as a decomposition

TheoremWeyl's theorem as a decomposition#

A finite-dimensional module over a Lie algebra with nondegenerate Killing form, over a field of characteristic zero, is the internal direct sum of a finite family of irreducible Lie submodules.

TauCeti.exists_isInternal_isIrreducible_of_isKilling.{u, v, w} (K : Type u) (L : Type v) [Field K]
  [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L]
  (M : Type w) [AddCommGroup M] [_root_.Module K M] [LieRingModule L M] [LieModule K L M]
  [FiniteDimensional K M] :
  ∃ k N, (DirectSum.IsInternal fun i => ↑(N i)) ∧ ∀ (i : Fin k), LieModule.IsIrreducible K L ↥(N i)

Lean

Formalized in Tau Ceti as TauCeti.exists_isInternal_isIrreducible_of_isKilling.

Other forms

Weyl's theorem for an action through a quotient. Formalized in Tau Ceti as LieSubmodule.exists_isCompl_of_le_ker.

LieSubmodule.exists_isCompl_of_le_ker.{u, v, w} {K : Type u} {L : Type v} [Field K] [CharZero K]
  [LieRing L] [LieAlgebra K L] {M : Type w} [AddCommGroup M] [_root_.Module K M] [LieRingModule L M]
  [LieModule K L M] [FiniteDimensional K M] (N : LieSubmodule K L M) {I : LieIdeal K L}
  [LieAlgebra.IsKilling K (L ⧸ I)] [FiniteDimensional K (L ⧸ I)] (hI : I ≤ LieModule.ker K L M) :
  ∃ N', IsCompl N N'

Sources

• Tau Ceti documentation: TauCeti.exists_isInternal_isIrreducible_of_isKilling
• Source of TauCeti.exists_isInternal_isIrreducible_of_isKilling in TauCeti/Algebra/Lie/HighestWeight/CompleteReducibility.lean

LeanTauCeti.exists_isInternal_isIrreducible_of_isKilling · LieSubmodule.exists_isCompl_of_le_ker

Uses 2 · Used by 4

Proof usesThe lattice form of Weyl's theorem · Weyl's complete reducibility theorem

Used byWhitehead's second lemma, as an equality of submodules · Matsushima's criterion, affine direction, in characteristic zero · Levi's theorem · The structure theorem for reductive Lie algebras

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.