The Cartan-Killing classification of rational root systems

Every irreducible reduced crystallographic finite root system over ℚ is isomorphic to the model root system TauCeti.DynkinType.rationalRootSystem t of exactly one valid Dynkin type t (RootPairing.existsUnique_nonempty_equiv_rationalRootSystem). So t ↦ t.rationalRootSystem is a bijection from the valid Dynkin types onto the isomorphism classes of such root systems.

The three ingredients are all available. The combinatorial classification attaches a valid Dynkin type to every base (TauCeti.classifiedDynkinType), and that type does not depend on the base (TauCeti.HasCartanType.of_base). The model root systems realize every valid type (TauCeti.DynkinType.hasCartanType_rationalRootSystem). Rigidity turns equal types into an isomorphism (TauCeti.nonempty_equiv_of_hasCartanType). A base to start from exists over any field of characteristic zero (RootPairing.nonempty_base).

Main results

• RootPairing.Base.nonempty_equiv_rationalRootSystem_iff: a rational root system is isomorphic to the model of a valid type t exactly when t is the Dynkin type of one, hence of every, base.
• RootPairing.existsUnique_nonempty_equiv_rationalRootSystem: the Cartan-Killing classification, every irreducible reduced crystallographic finite root system over ℚ is isomorphic to the model root system of a unique valid Dynkin type.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Ch. VI, §4.
• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, Ch. III, §11 and §12.

theorem RootPairing.Base.nonempty_equiv_rationalRootSystem_iff {ι : Type u_1} {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module ℚ M] [AddCommGroup N] [Module ℚ N] {P : RootPairing ι ℚ M N} [Finite ι] [Nonempty ι] [P.IsCrystallographic] [P.IsReduced] [P.IsIrreducible] (b : P.Base) {t : TauCeti.DynkinType} (ht : t.Valid) : Nonempty (P.Equiv (t.rationalRootSystem ht)) ↔ t = TauCeti.classifiedDynkinType b

A rational root system is isomorphic to the model of its Dynkin type, and to no other. The Dynkin type may be read off any base.

theorem RootPairing.existsUnique_nonempty_equiv_rationalRootSystem {ι : Type u_1} {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module ℚ M] [AddCommGroup N] [Module ℚ N] (P : RootPairing ι ℚ M N) [Finite ι] [Nonempty ι] [P.IsCrystallographic] [P.IsReduced] [P.IsIrreducible] : ∃! t : TauCeti.DynkinType, ∃ (ht : t.Valid), Nonempty (P.Equiv (t.rationalRootSystem ht))

The 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.