Root System
Results named in Tau Ceti's TauCeti.LinearAlgebra.RootSystem modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.
TheoremThe Cartan-Killing classification#
Every irreducible reduced crystallographic finite root
system over ℚ is isomorphic to the model root system TauCeti.DynkinType.rationalRootSystem t of
a unique valid Dynkin type t.
RootPairing.existsUnique_nonempty_equiv_rationalRootSystem.{u_1, u_2, u_3} {ι : Type u_1}
{M : Type u_2} {N : Type u_3} [AddCommGroup M] [_root_.Module ℚ M] [AddCommGroup N]
[_root_.Module ℚ N] (P : RootPairing ι ℚ M N) [Finite ι] [Nonempty ι] [P.IsCrystallographic]
[P.IsReduced] [P.IsIrreducible] :
∃! t, ∃ (ht : t.Valid), Nonempty (P.Equiv (t.rationalRootSystem ht))
Lean
Formalized in Tau Ceti as RootPairing.existsUnique_nonempty_equiv_rationalRootSystem.
Other forms
The Cartan-Killing classification, existence and uniqueness of the Dynkin type. Formalized in Tau Ceti as TauCeti.existsUnique_dynkinType.
TauCeti.existsUnique_dynkinType.{u_1, u_2, u_3, u_4} {ι : Type u_1} {R : Type u_2} {M : Type u_3}
{N : Type u_4} [CommRing R] [AddCommGroup M] [_root_.Module R M] [AddCommGroup N]
[_root_.Module R N] {P : RootPairing ι R M N} [Finite ι] [CharZero R] [IsDomain R]
[P.IsRootSystem] [P.IsCrystallographic] [P.IsReduced] [P.IsIrreducible] [Nonempty ι]
(b : P.Base) : ∃! t, t.Valid ∧ TauCeti.HasCartanType P b t
Sources
TheoremChevalley's theorem on structure constants#
If α + β is a root, then
N_{α,β} = ±(r + 1), where r = chainBotCoeff α β is the largest integer with β - r α a root
of the pinned datum.
TauCeti.DynkinType.structureConstant_eq_natCast_or_eq_neg_natCast {t : TauCeti.DynkinType}
{ht : t.Valid} {α β : Fin t.numRoots}
(h :
(t.simplyConnectedRootDatum ht).root α + (t.simplyConnectedRootDatum ht).root β ∈
Set.range ⇑(t.simplyConnectedRootDatum ht).root) :
t.structureConstant ht α β = ↑(RootPairing.chainBotCoeff α β + 1) ∨
t.structureConstant ht α β = -↑(RootPairing.chainBotCoeff α β + 1)
Lean
Formalized in Tau Ceti as TauCeti.DynkinType.structureConstant_eq_natCast_or_eq_neg_natCast.
Sources
TheoremKostant's multiplicity formula, stated before any module is named#
an element of ℤ[M]
whose product with the Weyl denominator is the Weyl numerator of λ has μ-th coefficient
∑_{w ∈ W} sgn(w) P(w ⬝ λ - μ).
The hypothesis is exactly the Weyl character formula, so this turns that formula into a closed expression for one weight multiplicity at a time.
RootPairing.coeff_eq_kostantMultiplicity_of_mul_weylDenominator_eq_weylNumerator.{u, v, w, x}
{ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M]
[_root_.Module R M] [AddCommGroup N] [_root_.Module R N] [CharZero R] (P : RootPairing ι R M N)
[Finite ι] (b : P.Base) [IsDomain R] [Invertible 2] [P.IsCrystallographic] [P.IsReduced]
[Fintype ↥P.weylGroup] {f : AddMonoidAlgebra ℤ M} {lam : M}
(hf : f * TauCeti.weylDenominator P b = TauCeti.weylNumerator P b lam) (mu : M) :
f.coeff mu = P.kostantMultiplicity b lam mu
Lean
Formalized in Tau Ceti as RootPairing.coeff_eq_kostantMultiplicity_of_mul_weylDenominator_eq_weylNumerator.
Sources
Used by 1
TheoremTits' theorem: the braid relations are the only relations among the simple reflections#
The canonical homomorphism from the Coxeter group of a base to the Weyl group is injective.
TauCeti.weylCoxeterHom_injective.{u, v, w, x} {ι : Type u} {R : Type v} {M : Type w} {N : Type x}
[CommRing R] [AddCommGroup M] [_root_.Module R M] [AddCommGroup N] [_root_.Module R N]
(P : RootPairing ι R M N) [Finite ι] [CharZero R] [IsDomain R] [P.IsCrystallographic] (b : P.Base)
[P.IsReduced] : Function.Injective ⇑(TauCeti.weylCoxeterHom P b)
TheoremThe Weyl denominator identity#
the Weyl denominator is the Weyl numerator of the weight
0,
∏_{α > 0} (1 - e^{-α}) = ∑_{w ∈ W} sgn(w) e^{w ⬝ 0},
an identity in the integral group algebra of the weight space. Written without the dot action, the
right-hand side is ∑_{w ∈ W} sgn(w) e^{w(ρ) - ρ}.
This is the case λ = 0 of the Weyl character formula, in which the character of the trivial
module is 1.
TauCeti.weylDenominator_eq_weylNumerator_zero.{u, v, w, x} {ι : Type u} {R : Type v} {M : Type w}
{N : Type x} [CommRing R] [AddCommGroup M] [_root_.Module R M] [AddCommGroup N]
[_root_.Module R N] (P : RootPairing ι R M N) [Finite ι] [CharZero R] (b : P.Base) [LinearOrder R]
[IsStrictOrderedRing R] [Invertible 2] [P.IsCrystallographic] [P.IsReduced] [P.IsRootSystem]
[Fintype ↥P.weylGroup] : TauCeti.weylDenominator P b = TauCeti.weylNumerator P b 0
Lean
Formalized in Tau Ceti as TauCeti.weylDenominator_eq_weylNumerator_zero.
Other forms
The Weyl denominator identity for a root datum. Formalized in Tau Ceti as RootPairing.dotAlternatization_one.
RootPairing.dotAlternatization_one.{u_1, u_2, u_3} {ι : Type u_1} {M : Type u_2} {N : Type u_3}
[AddCommGroup M] [AddCommGroup N] (P : RootPairing ι ℤ M N) [Finite ι] (b : P.Base) [P.IsReduced]
[Fintype ↥P.weylGroup] : (P.dotAlternatization b) 1 = TauCeti.weylDenominator P b
Sources
Used by 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.