Abstract Jordan decomposition… to The Racah–Speiser formula, in…

TheoremAbstract Jordan decomposition, existence#

In a finite-dimensional Lie algebra with nondegenerate Killing form over an algebraically closed field, every element x is a sum n + s of commuting elements with ad n nilpotent and ad s semisimple. Both ad n and ad s are polynomials in ad x.

TauCeti.exists_isNilpotent_ad_isSemisimple_ad.{u_1, u_2} {K : Type u_1} {L : Type u_2} [Field K]
  [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsKilling K L] [IsAlgClosed K]
  (x : L) :
  ∃ n s,
    (LieAlgebra.ad K L) n ∈ K[(LieAlgebra.ad K L) x] ∧
      (LieAlgebra.ad K L) s ∈ K[(LieAlgebra.ad K L) x] ∧
        IsNilpotent ((LieAlgebra.ad K L) n) ∧
          ((LieAlgebra.ad K L) s).IsSemisimple ∧ ⁅n, s⁆ = 0 ∧ x = n + s
Lean

Formalized in Tau Ceti as TauCeti.exists_isNilpotent_ad_isSemisimple_ad.

Other forms

Abstract Jordan decomposition, existence for split elements. Formalized in Tau Ceti as TauCeti.exists_isNilpotent_ad_isSemisimple_ad_of_iSup_maxGenEigenspace_eq_top.

TauCeti.exists_isNilpotent_ad_isSemisimple_ad_of_iSup_maxGenEigenspace_eq_top.{u_1, u_2}
  {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L]
  [LieAlgebra.IsKilling K L] (x : L) (hx : ⨆ μ, ((LieAlgebra.ad K L) x).maxGenEigenspace μ = ⊤) :
  ∃ n s,
    (LieAlgebra.ad K L) n ∈ K[(LieAlgebra.ad K L) x] ∧
      (LieAlgebra.ad K L) s ∈ K[(LieAlgebra.ad K L) x] ∧
        IsNilpotent ((LieAlgebra.ad K L) n) ∧
          ((LieAlgebra.ad K L) s).IsSemisimple ∧ ⁅n, s⁆ = 0 ∧ x = n + s

Abstract Jordan decomposition, uniqueness. Formalized in Tau Ceti as TauCeti.isNilpotent_ad_isSemisimple_ad_unique.

TauCeti.isNilpotent_ad_isSemisimple_ad_unique.{u_1, u_2} {K : Type u_1} {L : Type u_2} [Field K]
  [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieModule.IsFaithful K L L] [PerfectField K]
  {n₁ s₁ n₂ s₂ : L} (hn₁ : IsNilpotent ((LieAlgebra.ad K L) n₁))
  (hs₁ : ((LieAlgebra.ad K L) s₁).IsSemisimple) (hn₂ : IsNilpotent ((LieAlgebra.ad K L) n₂))
  (hs₂ : ((LieAlgebra.ad K L) s₂).IsSemisimple) (hc₁ : ⁅n₁, s₁⁆ = 0) (hc₂ : ⁅n₂, s₂⁆ = 0)
  (h : n₁ + s₁ = n₂ + s₂) : n₁ = n₂ ∧ s₁ = s₂
Sources
LeanTauCeti.exists_isNilpotent_ad_isSemisimple_ad · TauCeti.exists_isNilpotent_ad_isSemisimple_ad_of_iSup_maxGenEigenspace_eq_top · TauCeti.isNilpotent_ad_isSemisimple_ad_unique
Uses 1
Proof usesJordan–Chevalley decomposition of a derivation

TheoremThe Brauer–Klimyk formula, in group-algebra form#

for dominant integral weights lam and nu and a finite-dimensional L-module M, the multiplicity of L(nu) in L(lam) ⊗ M is the coefficient at nu of ch M · N(lam).

This combines Weyl-alternating inversion (TauCeti.coeff_formalCharacter_mul_weylDenominator_eq_isotypicMultiplicity) on L(lam) ⊗ M, multiplicativity of formal characters (TauCeti.formalCharacter_tensor), and the Weyl character formula ch L(lam) · Δ = N(lam).

TauCeti.isotypicMultiplicity_tensor_eq_coeff_formalCharacter_mul_weylNumerator.{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]
  (b : (LieAlgebra.IsKilling.rootSystem H).Base) {M : Type w} [AddCommGroup M] [_root_.Module K M]
  [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M]
  [Fintype ↥(LieAlgebra.IsKilling.rootSystem H).weylGroup] {lam nu : Module.Dual K ↥H}
  (hlam : TauCeti.IsDominantIntegral b lam) (hnu : TauCeti.IsDominantIntegral b nu) :
  ↑(LieModule.isotypicMultiplicity K L (TensorProduct K (TauCeti.irreducibleQuotient b lam) M)
        (TauCeti.irreducibleQuotient b nu)) =
    (TauCeti.formalCharacter K (↥H) M *
          TauCeti.weylNumerator (LieAlgebra.IsKilling.rootSystem H) b lam).coeff
      nu
Lean

Formalized in Tau Ceti as TauCeti.isotypicMultiplicity_tensor_eq_coeff_formalCharacter_mul_weylNumerator.

Other forms

The Brauer–Klimyk formula, expanded over the Weyl group. Formalized in Tau Ceti as TauCeti.isotypicMultiplicity_tensor_eq_sum_weylSign_mul_formalCharacter_coeff.

TauCeti.isotypicMultiplicity_tensor_eq_sum_weylSign_mul_formalCharacter_coeff.{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]
  (b : (LieAlgebra.IsKilling.rootSystem H).Base) {M : Type w} [AddCommGroup M] [_root_.Module K M]
  [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M]
  [Fintype ↥(LieAlgebra.IsKilling.rootSystem H).weylGroup] {lam nu : Module.Dual K ↥H}
  (hlam : TauCeti.IsDominantIntegral b lam) (hnu : TauCeti.IsDominantIntegral b nu) :
  ↑(LieModule.isotypicMultiplicity K L (TensorProduct K (TauCeti.irreducibleQuotient b lam) M)
        (TauCeti.irreducibleQuotient b nu)) =
    ∑ w,
      ↑((TauCeti.weylSign (LieAlgebra.IsKilling.rootSystem H) b) w) *
        (TauCeti.formalCharacter K (↥H) M).coeff
          (nu - TauCeti.dotAction (LieAlgebra.IsKilling.rootSystem H) b w lam)
Sources
LeanTauCeti.isotypicMultiplicity_tensor_eq_coeff_formalCharacter_mul_weylNumerator · TauCeti.isotypicMultiplicity_tensor_eq_sum_weylSign_mul_formalCharacter_coeff
Uses 4 · Used by 1
Proof usesFreudenthal's multiplicity formula · The lattice form of Weyl's theorem · Schur's lemma for Lie modules · The Weyl character formula
Used byThe Racah–Speiser formula, in group-algebra form

TheoremCartan's formula ι_x d ω = L_x ω - d ι_x ω# 

TauCeti.LieModule.Cohomology.curryLeft_d_succ.{u_1, u_2, u_3} {R : Type u_1} [CommRing R]
  {L : Type u_2} [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [_root_.Module R M]
  [LieRingModule L M] [LieModule R L M] {n : ℕ} (ω : L [⋀^Fin (n + 1)]→ₗ[R] M) (x : L) :
  ((TauCeti.LieModule.Cohomology.d R L M (n + 1)) ω).curryLeft x =
    ⁅x, ω⁆ - (TauCeti.LieModule.Cohomology.d R L M n) (ω.curryLeft x)
Lean

Formalized in Tau Ceti as TauCeti.LieModule.Cohomology.curryLeft_d_succ.

Sources
LeanTauCeti.LieModule.Cohomology.curryLeft_d_succ
Used by 1
Used byThe Chevalley–Eilenberg formula for the differential of a cochain of positive degree

TheoremChevalley's rank-one identity#

Chevalley's rank-one identity xᵢ(u) xⱼ(-u⁻¹) xᵢ(u) = h_c(u) n, over every value ring and at every unit u. Here (eᵢ, eⱼ) is a root pair whose sl₂ triple has Cartan index c, h_c(u) is the coordinate cocharacter at c and n = xᵢ(1) xⱼ(-1) xᵢ(1) is the Weyl representative, and α is the weight of eᵢ, so that eⱼ has weight -α.

TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupParam_mul_mul_eq_kostantCoordinateCocharacter_mul_kostantWeylGL.{u,
    v, w, u_1, u_2, u_3}
  {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type u_1} {κ : Type u_2} {V : Type v}
  [AddCommGroup V] [_root_.Module ℚ V] (e : ι → L) (h : κ → L)
  (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V)
  (hM : ∀ u ∈ TauCeti.UniversalEnvelopingAlgebra.kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M)
  {η : Type u_3} (b : Module.Basis η ℤ ↥M) (wt : η → κ → ℤ) [Fintype κ] [DecidableEq κ]
  (hwt : ∀ (x : η), TauCeti.UniversalEnvelopingAlgebra.IsCartanWeightVector h ρ (wt x) ↑(b x))
  {i j : ι} {c : κ} {α : κ → ℤ}
  (hT :
    IsSl2Triple (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (h c)))
      (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j))))
  (hi : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))))
  (hj : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e j))))
  (hα : ∀ (j' : κ), ⁅h j', e i⁆ = ↑(α j') • e i)
  (hαneg : ∀ (j' : κ), ⁅h j', e j⁆ = -(↑(α j') • e j)) (A : CommAlgCat ℤ) (u : (↑A)ˣ) :
  (TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupParam e h ρ M hM i hi A)
          (Multiplicative.ofAdd ↑u) *
        (TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupParam e h ρ M hM j hj A)
          (Multiplicative.ofAdd (-↑u⁻¹)) *
      (TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupParam e h ρ M hM i hi A)
        (Multiplicative.ofAdd ↑u) =
    (TauCeti.UniversalEnvelopingAlgebra.kostantCoordinateCocharacter M b wt (↑A) c) u *
      TauCeti.UniversalEnvelopingAlgebra.kostantWeylGL e h ρ M hM hi hj ↑A
Lean

Formalized in Tau Ceti as TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupParam_mul_mul_eq_kostantCoordinateCocharacter_mul_kostantWeylGL.

Sources
LeanTauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupParam_mul_mul_eq_kostantCoordinateCocharacter_mul_kostantWeylGL
Used by 1
Used byTwo morphisms out of the short-root type-F₄ carrier agree as soon as they agree on its eight numbered root subgroups

TheoremThe Chevalley–Eilenberg formula for the differential of a cochain of positive degree#

(d ω)(x₀, …, xₙ₊₁) = ∑ i, (-1)^i ⁅xᵢ, ω(…, x̂ᵢ, …)⁆ + ∑_{i < j} (-1)^(i + j) ω(⁅xᵢ, xⱼ⁆, …), where the pairs i < j are written as (i.castSucc, j.succ) with i ≤ j.

TauCeti.LieModule.Cohomology.d_succ_apply.{u_1, u_2, u_3} {R : Type u_1} [CommRing R] {L : Type u_2}
  [LieRing L] [LieAlgebra R L] {M : Type u_3} [AddCommGroup M] [_root_.Module R M]
  [LieRingModule L M] [LieModule R L M] {n : ℕ} (ω : L [⋀^Fin (n + 1)]→ₗ[R] M)
  (v : Fin (n + 2) → L) :
  ((TauCeti.LieModule.Cohomology.d R L M (n + 1)) ω) v =
    ∑ i, (-1) ^ ↑i • ⁅v i, ω (i.removeNth v)⁆ +
      ∑ i,
        ∑ j ≥ i,
          (-1) ^ (↑i + ↑j + 1) •
            ω (Matrix.vecCons ⁅v i.castSucc, v j.succ⁆ (j.removeNth (i.castSucc.removeNth v)))
Lean

Formalized in Tau Ceti as TauCeti.LieModule.Cohomology.d_succ_apply.

Sources
LeanTauCeti.LieModule.Cohomology.d_succ_apply
Uses 1
Proof usesCartan's formula ι_x d ω = L_x ω - d ι_x ω

DefinitionThe first isomorphism theorem for a surjective homomorphism of Lie algebras#

the quotient by its kernel is isomorphic to the target.

LieHom.quotKerEquivOfSurjective.{u_1, u_2, u_3} {R : Type u_1} {L : Type u_2} {L' : Type u_3}
  [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R⁆ L')
  (hf : Function.Surjective ⇑f) : (L ⧸ f.ker) ≃ₗ⁅R⁆ L'
Lean

Formalized in Tau Ceti as LieHom.quotKerEquivOfSurjective.

Sources
LeanLieHom.quotKerEquivOfSurjective
Used by 2
Used byWhitehead's second lemma, as an equality of submodules · Levi's theorem

TheoremFreudenthal's multiplicity formula#

Let M be a finite-dimensional module generated by a highest weight vector of weight λ. Then for every linear form μ on the Cartan subalgebra,

(⟨λ + ρ, λ + ρ⟩ - ⟨μ + ρ, μ + ρ⟩) · dim Mμ = 2 ∑_{α > 0} ∑_{j ≥ 1} dim M_{μ + jα} · ⟨μ + jα, α⟩,

the inner sum running over the α-string above μ with the rung μ itself removed; the double sum is TauCeti.freudenthalRHS.

Together with dim Mλ = 1 at the top weight this is the recursion for the multiplicities below λ; solved for dim Mμ it is TauCeti.coeff_formalCharacter_eq_freudenthalRHS_div.

TauCeti.freudenthal_multiplicity_formula.{u, v, w} {K : Type u} {L : Type v} [Field K] [LieRing L]
  [LieAlgebra K L] {H : LieSubalgebra K L} {M : Type w} [AddCommGroup M] [_root_.Module K M]
  [LieRingModule L M] [LieModule K L M] [CharZero K] [LieAlgebra.IsKilling K L]
  [FiniteDimensional K L] [H.IsCartanSubalgebra] [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} = ⊤)
  (mu : Module.Dual K ↥H) :
  ((TauCeti.invForm (lam + TauCeti.weylVector (LieAlgebra.IsKilling.rootSystem H) b))
          (lam + TauCeti.weylVector (LieAlgebra.IsKilling.rootSystem H) b) -
        (TauCeti.invForm (mu + TauCeti.weylVector (LieAlgebra.IsKilling.rootSystem H) b))
          (mu + TauCeti.weylVector (LieAlgebra.IsKilling.rootSystem H) b)) *
      ↑(Module.finrank K ↥(LieModule.genWeightSpace M ⇑mu)) =
    2 * TauCeti.freudenthalRHS M b mu
Lean

Formalized in Tau Ceti as TauCeti.freudenthal_multiplicity_formula.

Sources
LeanTauCeti.freudenthal_multiplicity_formula
Used by 2
Used byThe Brauer–Klimyk formula, in group-algebra form · The Weyl character formula

TheoremThe Frobenius commutator identity#

In exponential characteristic p, taking the p ^ n-th power in the algebra A and iterating the commutator p ^ n times in Module.End R A give the same endomorphism.

TauCeti.LieAlgebra.ad_pow_expChar_pow.{u_1, u_2} {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A]
  [Algebra R A] (p : ℕ) [ExpChar A p] (a : A) (n : ℕ) :
  (LieAlgebra.ad R A) (a ^ p ^ n) = (LieAlgebra.ad R A) a ^ p ^ n
Lean

Formalized in Tau Ceti as TauCeti.LieAlgebra.ad_pow_expChar_pow.

Sources
LeanTauCeti.LieAlgebra.ad_pow_expChar_pow
Used by 2
Used byAdo's theorem in characteristic zero · Hochschild's strengthening of the Ado–Iwasawa theorem

TheoremThe Jacobi identity, for a positive definite B with even diagonal# 

Matrix.FullShellLieAlgebra.lie_jacobi.{u_1, u_2} {I : Type u_1} [Fintype I] {B : Matrix I I ℤ}
  {Y : Type u_2} [AddCommGroup Y] {D : B.ShellCartanDatum Y} [LinearOrder I] (hB : B.PosDef)
  (hdiag : ∀ (i : I), Even (B i i)) (x y z : Matrix.FullShellLieAlgebra D) :
  ⁅x, ⁅y, z⁆⁆ + ⁅y, ⁅z, x⁆⁆ + ⁅z, ⁅x, y⁆⁆ = 0
Lean

Formalized in Tau Ceti as Matrix.FullShellLieAlgebra.lie_jacobi.

Other forms

The Jacobi identity, for a positive definite B with even diagonal. Formalized in Tau Ceti as Matrix.ShellLieAlgebra.lie_jacobi.

Matrix.ShellLieAlgebra.lie_jacobi.{u_1} {I : Type u_1} [Fintype I] {B : Matrix I I ℤ}
  [LinearOrder I] (hB : B.PosDef) (hdiag : ∀ (i : I), Even (B i i)) (x y z : B.ShellLieAlgebra) :
  ⁅x, ⁅y, z⁆⁆ + ⁅y, ⁅z, x⁆⁆ + ⁅z, ⁅x, y⁆⁆ = 0
Sources
LeanMatrix.FullShellLieAlgebra.lie_jacobi · Matrix.ShellLieAlgebra.lie_jacobi
Used by 1
Used byThe Leibniz form of the Jacobi identity, for a positive definite B with even diagonal

TheoremJacobson's lemma for the adjoint representation#

In a finite-dimensional Lie algebra over a field of characteristic zero, if ⁅e, ⁅e, a⁆⁆ = 0 then ad ⁅e, a⁆ is nilpotent. In particular every element of ker (ad e) ⊓ [e, L] is ad-nilpotent.

TauCeti.isNilpotent_ad_lie_of_lie_lie_eq_zero.{u_1, u_2} {K : Type u_1} {L : Type u_2} [Field K]
  [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {e a : L}
  (h : ⁅e, ⁅e, a⁆⁆ = 0) : IsNilpotent ((LieAlgebra.ad K L) ⁅e, a⁆)
Lean

Formalized in Tau Ceti as TauCeti.isNilpotent_ad_lie_of_lie_lie_eq_zero.

Sources
LeanTauCeti.isNilpotent_ad_lie_of_lie_lie_eq_zero
Uses 1 · Used by 1
Proof usesJacobson's lemma on commutators
Used byKostant's conjugacy theorem

TheoremJordan–Chevalley decomposition of a derivation#

Over an algebraically closed field, the nilpotent and semisimple parts of a derivation of a finite-dimensional Lie algebra are derivations. They are polynomials in the original derivation.

LieDerivation.exists_isNilpotent_isSemisimple.{u_1, u_2} {K : Type u_1} {L : Type u_2} [Field K]
  [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [IsAlgClosed K] (D : LieDerivation K L L) :
  ∃ N S, ↑N ∈ K[↑D] ∧ ↑S ∈ K[↑D] ∧ IsNilpotent ↑N ∧ Module.End.IsSemisimple ↑S ∧ D = N + S
Lean

Formalized in Tau Ceti as LieDerivation.exists_isNilpotent_isSemisimple.

Other forms

Jordan–Chevalley decomposition of a split derivation. Formalized in Tau Ceti as LieDerivation.exists_isNilpotent_isSemisimple_of_iSup_maxGenEigenspace_eq_top.

LieDerivation.exists_isNilpotent_isSemisimple_of_iSup_maxGenEigenspace_eq_top.{u_1, u_2}
  {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L]
  (D : LieDerivation K L L) (hD : ⨆ μ, Module.End.maxGenEigenspace (↑D) μ = ⊤) :
  ∃ N S, ↑N ∈ K[↑D] ∧ ↑S ∈ K[↑D] ∧ IsNilpotent ↑N ∧ Module.End.IsSemisimple ↑S ∧ D = N + S
Sources
LeanLieDerivation.exists_isNilpotent_isSemisimple · LieDerivation.exists_isNilpotent_isSemisimple_of_iSup_maxGenEigenspace_eq_top
Used by 1
Used byAbstract Jordan decomposition, existence

TheoremKostant's multiplicity formula#

The multiplicity of the weight mu in a finite-dimensional module generated by a highest weight vector of weight lam is the alternating sum ∑_{w ∈ W} sgn(w) P(w(lam + ρ) - (mu + ρ)) of values of the Kostant partition function.

TauCeti.finrank_weightSpace_eq_kostantMultiplicity.{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]
  [Fintype ↥(LieAlgebra.IsKilling.rootSystem H).weylGroup]
  {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} = ⊤)
  (mu : Module.Dual K ↥H) :
  ↑(Module.finrank K ↥(LieModule.weightSpace M ⇑mu)) =
    (LieAlgebra.IsKilling.rootSystem H).kostantMultiplicity b lam mu
Lean

Formalized in Tau Ceti as TauCeti.finrank_weightSpace_eq_kostantMultiplicity.

Other forms

Kostant's multiplicity formula, read off the formal character. Formalized in Tau Ceti as TauCeti.formalCharacter_coeff_eq_kostantMultiplicity.

TauCeti.formalCharacter_coeff_eq_kostantMultiplicity.{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]
  [Fintype ↥(LieAlgebra.IsKilling.rootSystem H).weylGroup]
  {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} = ⊤)
  (mu : Module.Dual K ↥H) :
  (TauCeti.formalCharacter K (↥H) M).coeff mu =
    (LieAlgebra.IsKilling.rootSystem H).kostantMultiplicity b lam mu
Sources
LeanTauCeti.finrank_weightSpace_eq_kostantMultiplicity · TauCeti.formalCharacter_coeff_eq_kostantMultiplicity
Uses 2
Proof usesKostant's multiplicity formula, stated before any module is named · The Weyl character formula

TheoremThe lattice form of Weyl's theorem#

the Lie submodules of a finite-dimensional module over a Lie algebra with nondegenerate Killing form form a complemented lattice.

TauCeti.complementedLattice_lieSubmodule_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] : ComplementedLattice (LieSubmodule K L M)
Lean

Formalized in Tau Ceti as TauCeti.complementedLattice_lieSubmodule_of_isKilling.

Sources
LeanTauCeti.complementedLattice_lieSubmodule_of_isKilling
Uses 1 · Used by 2
Proof usesWeyl's complete reducibility theorem
Used byThe Brauer–Klimyk formula, in group-algebra form · Weyl's theorem as a decomposition

TheoremThe Leibniz form of the Jacobi identity, for a positive definite B with even diagonal# 

Matrix.FullShellLieAlgebra.leibniz_lie.{u_1, u_2} {I : Type u_1} [Fintype I] {B : Matrix I I ℤ}
  {Y : Type u_2} [AddCommGroup Y] {D : B.ShellCartanDatum Y} [LinearOrder I] (hB : B.PosDef)
  (hdiag : ∀ (i : I), Even (B i i)) (x y z : Matrix.FullShellLieAlgebra D) :
  ⁅x, ⁅y, z⁆⁆ = ⁅⁅x, y⁆, z⁆ + ⁅y, ⁅x, z⁆⁆
Lean

Formalized in Tau Ceti as Matrix.FullShellLieAlgebra.leibniz_lie.

Other forms

The Leibniz form of the Jacobi identity, for a positive definite B with even diagonal. Formalized in Tau Ceti as Matrix.ShellLieAlgebra.leibniz_lie.

Matrix.ShellLieAlgebra.leibniz_lie.{u_1} {I : Type u_1} [Fintype I] {B : Matrix I I ℤ}
  [LinearOrder I] (hB : B.PosDef) (hdiag : ∀ (i : I), Even (B i i)) (x y z : B.ShellLieAlgebra) :
  ⁅x, ⁅y, z⁆⁆ = ⁅⁅x, y⁆, z⁆ + ⁅y, ⁅x, z⁆⁆
Sources
LeanMatrix.FullShellLieAlgebra.leibniz_lie · Matrix.ShellLieAlgebra.leibniz_lie
Uses 1
Proof usesThe Jacobi identity, for a positive definite B with even diagonal

TheoremThe Levi decomposition#

Over a field of characteristic zero, a finite-dimensional Lie algebra is the semidirect sum of its solvable radical and a semisimple Lie subalgebra acting on the radical by the adjoint action.

TauCeti.exists_leviDecomposition.{u, v} (K : Type u) [Field K] (L : Type v) [LieRing L]
  [LieAlgebra K L] [CharZero K] [FiniteDimensional K L] :
  ∃ S ψ, LieAlgebra.IsSemisimple K ↥S ∧ Nonempty (L ≃ₗ⁅K⁆ ↥(LieAlgebra.radical K L) ⋊⁅ψ⁆ ↥S)
Lean

Formalized in Tau Ceti as TauCeti.exists_leviDecomposition.

Sources
LeanTauCeti.exists_leviDecomposition
Uses 1
Proof usesLevi's theorem

TheoremLevi's theorem#

Over a field of characteristic zero, the solvable radical of a finite-dimensional Lie algebra has a complementary Lie subalgebra, a Levi complement.

TauCeti.exists_leviComplement.{u, v} (K : Type u) [Field K] (L : Type v) [LieRing L]
  [LieAlgebra K L] [CharZero K] [FiniteDimensional K L] :
  ∃ S, IsCompl (↑(LieAlgebra.radical K L)) S.toSubmodule
Lean

Formalized in Tau Ceti as TauCeti.exists_leviComplement.

Sources
LeanTauCeti.exists_leviComplement
Uses 2 · Used by 3
Proof usesThe first isomorphism theorem for a surjective homomorphism of Lie algebras · Weyl's theorem as a decomposition
Used byThe Levi decomposition · Ado's theorem in characteristic zero · Hochschild's strengthening of Ado's theorem in characteristic zero

TheoremThe linear-independence half of the Poincaré--Birkhoff--Witt theorem#

The canonical map Sym(L) → gr U(L) is injective when L is a free module.

TauCeti.UniversalEnvelopingAlgebra.pbwAssociatedGradedMap_injective.{u, v} (R : Type u) (L : Type v)
  [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Free R L] :
  Function.Injective ⇑(TauCeti.UniversalEnvelopingAlgebra.pbwAssociatedGradedMap R L)
Lean

Formalized in Tau Ceti as TauCeti.UniversalEnvelopingAlgebra.pbwAssociatedGradedMap_injective.

Sources
LeanTauCeti.UniversalEnvelopingAlgebra.pbwAssociatedGradedMap_injective
Used by 6
Used byThe Poincaré--Birkhoff--Witt theorem · Harish-Chandra surjectivity with a degree bound · Harish-Chandra's theorem on central characters · The linear Harish-Chandra isomorphism Z(U(L)) ≃ₐ[K] S(H)^W · Ado's theorem in characteristic zero · Hochschild's strengthening of the Ado–Iwasawa theorem

DefinitionThe Poincaré--Birkhoff--Witt theorem#

For a Lie algebra that is free as a module, the symmetric algebra is isomorphic to the associated graded of the PBW filtration of the enveloping algebra, by the algebra map sending x ∈ L to the degree-one class of ι(x).

TauCeti.UniversalEnvelopingAlgebra.pbwAssociatedGradedEquiv.{u, v} (R : Type u) (L : Type v)
  [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Free R L] :
  SymmetricAlgebra R L ≃ₐ[R] TauCeti.UniversalEnvelopingAlgebra.PBWAssociatedGraded R L
Lean

Formalized in Tau Ceti as TauCeti.UniversalEnvelopingAlgebra.pbwAssociatedGradedEquiv.

Sources
LeanTauCeti.UniversalEnvelopingAlgebra.pbwAssociatedGradedEquiv
Uses 1 · Used by 6
Proof usesThe linear-independence half of the Poincaré--Birkhoff--Witt theorem
Used byHarish-Chandra surjectivity with a degree bound · Harish-Chandra's theorem on central characters · TauCeti.UniversalEnvelopingAlgebra.reesZeroFiberEquiv · The linear Harish-Chandra isomorphism Z(U(L)) ≃ₐ[K] S(H)^W · Ado's theorem in characteristic zero · Hochschild's strengthening of the Ado–Iwasawa theorem

TheoremThe positive-simple-root Chevalley collection formula over 𝔽₃#

The four factors have roots α₁+α₂, 2α₁+α₂, 3α₁+α₂, and 3α₁+2α₂, with their parameters normalized by the displayed conjugating words. The formula includes nonreduced coefficient algebras.

TauCeti.G2ShortRoot.PrimeField.commutatorElement_positive_simple_eq_root_product.{v} (A : Type v)
  [CommRing A] [Algebra (ZMod 3) A] (a b : A) :
  have x := fun i t =>
    (TauCeti.G2ShortRoot.PrimeField.rootSubgroupPoints (Sum.inl i) A) (Multiplicative.ofAdd t);
  have n := fun i =>
    x i 1 *
        (TauCeti.G2ShortRoot.PrimeField.rootSubgroupPoints (Sum.inr i) A)
          (Multiplicative.ofAdd (-1)) *
      x i 1;
  ⁅x 0 a, x 1 b⁆ =
    n 1 * x 0 (-a * b) * (n 1)⁻¹ * (n 0 * n 1 * x 0 (a ^ 2 * b) * (n 0 * n 1)⁻¹) *
        (n 0 * x 1 (a ^ 3 * b) * (n 0)⁻¹) *
      (n 1 * n 0 * x 1 (2 * a ^ 3 * b ^ 2) * (n 1 * n 0)⁻¹)
Lean

Formalized in Tau Ceti as TauCeti.G2ShortRoot.PrimeField.commutatorElement_positive_simple_eq_root_product.

Other forms

The positive-simple-root Chevalley collection formula in type G₂. Formalized in Tau Ceti as TauCeti.G2ShortRoot.IntegralToralClosure.commutatorElement_positive_simple_eq_root_product.

TauCeti.G2ShortRoot.IntegralToralClosure.commutatorElement_positive_simple_eq_root_product.{v}
  (A : Type v) [CommRing A] (a b : A) :
  have x := fun i t =>
    (TauCeti.G2ShortRoot.IntegralToralClosure.rootSubgroupPoints (Sum.inl i) A)
      (Multiplicative.ofAdd t);
  have n := fun i =>
    x i 1 *
        (TauCeti.G2ShortRoot.IntegralToralClosure.rootSubgroupPoints (Sum.inr i) A)
          (Multiplicative.ofAdd (-1)) *
      x i 1;
  ⁅x 0 a, x 1 b⁆ =
    n 1 * x 0 (-a * b) * (n 1)⁻¹ * (n 0 * n 1 * x 0 (a ^ 2 * b) * (n 0 * n 1)⁻¹) *
        (n 0 * x 1 (a ^ 3 * b) * (n 0)⁻¹) *
      (n 1 * n 0 * x 1 (2 * a ^ 3 * b ^ 2) * (n 1 * n 0)⁻¹)
Sources
LeanTauCeti.G2ShortRoot.PrimeField.commutatorElement_positive_simple_eq_root_product · TauCeti.G2ShortRoot.IntegralToralClosure.commutatorElement_positive_simple_eq_root_product

TheoremThe Racah–Speiser formula, in group-algebra form#

for dominant integral weights lam, mu, and nu, the tensor multiplicity c^nu_{lam mu} of L(nu) in L(lam) ⊗ L(mu) is the coefficient at nu of ch L(mu) · N(lam).

This is the Brauer–Klimyk formula TauCeti.isotypicMultiplicity_tensor_eq_coeff_formalCharacter_mul_weylNumerator for M = L(mu).

TauCeti.tensorMultiplicity_eq_coeff_formalCharacter_mul_weylNumerator.{u, v} {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]
  (b : (LieAlgebra.IsKilling.rootSystem H).Base)
  [Fintype ↥(LieAlgebra.IsKilling.rootSystem H).weylGroup] {lam mu nu : Module.Dual K ↥H}
  (hlam : TauCeti.IsDominantIntegral b lam) (hmu : TauCeti.IsDominantIntegral b mu)
  (hnu : TauCeti.IsDominantIntegral b nu) :
  ↑(TauCeti.tensorMultiplicity b lam mu nu) =
    (TauCeti.formalCharacter K (↥H) (TauCeti.irreducibleQuotient b mu) *
          TauCeti.weylNumerator (LieAlgebra.IsKilling.rootSystem H) b lam).coeff
      nu
Lean

Formalized in Tau Ceti as TauCeti.tensorMultiplicity_eq_coeff_formalCharacter_mul_weylNumerator.

Other forms

The Racah–Speiser formula, expanded over the Weyl group. Formalized in Tau Ceti as TauCeti.tensorMultiplicity_eq_sum_weylSign_mul_formalCharacter_coeff.

TauCeti.tensorMultiplicity_eq_sum_weylSign_mul_formalCharacter_coeff.{u, v} {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]
  (b : (LieAlgebra.IsKilling.rootSystem H).Base)
  [Fintype ↥(LieAlgebra.IsKilling.rootSystem H).weylGroup] {lam mu nu : Module.Dual K ↥H}
  (hlam : TauCeti.IsDominantIntegral b lam) (hmu : TauCeti.IsDominantIntegral b mu)
  (hnu : TauCeti.IsDominantIntegral b nu) :
  ↑(TauCeti.tensorMultiplicity b lam mu nu) =
    ∑ w,
      ↑((TauCeti.weylSign (LieAlgebra.IsKilling.rootSystem H) b) w) *
        (TauCeti.formalCharacter K (↥H) (TauCeti.irreducibleQuotient b mu)).coeff
          (nu - TauCeti.dotAction (LieAlgebra.IsKilling.rootSystem H) b w lam)
Sources
LeanTauCeti.tensorMultiplicity_eq_coeff_formalCharacter_mul_weylNumerator · TauCeti.tensorMultiplicity_eq_sum_weylSign_mul_formalCharacter_coeff
Uses 1
Proof usesThe Brauer–Klimyk formula, in group-algebra form

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.