The Cartan-Killing classification of finite-type Cartan matrices

This file proves the central theorem of Layer 5 of the root systems roadmap: every nonempty connected finite-type Cartan matrix reindexes to the standard Cartan matrix of a unique valid DynkinType, and every base of an irreducible reduced crystallographic finite root system has a unique valid DynkinType (TauCeti.existsUnique_dynkinType).

The proof assembles the four geometric branches established in the subdiagram modules:

1. Triple edge: TauCeti.IsFiniteType.exists_equiv_cartanMatrix_eq_G2_of_apply_mul_apply_eq_three in TauCeti.LinearAlgebra.RootSystem.FiniteType.TripleEdge isolates the exceptional type G₂.
2. Double edge: TauCeti.IsFiniteType.existsUnique_dynkinType_of_apply_mul_apply_eq_two in TauCeti.LinearAlgebra.RootSystem.FiniteType.DoubleEdge.Classification classifies the families Bₙ, Cₙ, and the exceptional type F₄.
3. Simply-laced branching: TauCeti.IsFiniteType.existsUnique_dynkinType_of_isSimplyLaced_of_degree_eq_three in TauCeti.LinearAlgebra.RootSystem.FiniteType.Star.Reindex classifies the forks Dₙ and the exceptional types E₆, E₇, E₈.
4. Simply-laced chain: TauCeti.IsFiniteType.exists_equiv_forall_eq_cartanMatrix_A in TauCeti.LinearAlgebra.RootSystem.FiniteType.TypeA classifies the linear chains Aₙ.

Uniqueness among valid types is supplied by TauCeti.DynkinType.eq_of_valid_of_forall_eq in TauCeti.LinearAlgebra.RootSystem.Classification.

Main results

• TauCeti.IsFiniteType.existsUnique_dynkinType: every nonempty connected finite-type Cartan matrix has a unique valid Dynkin type.
• TauCeti.existsUnique_dynkinType: the Cartan-Killing classification for irreducible reduced crystallographic finite root systems.
• TauCeti.classifiedDynkinType: the selected type as data, with TauCeti.valid_classifiedDynkinType, TauCeti.hasCartanType_classifiedDynkinType and TauCeti.hasCartanType_iff_eq_classifiedDynkinType characterizing it. This is what a consumer names instead of rechoosing a witness out of the existence statement.
• RootPairing.Base.classifiedDynkinType_eq_classifiedDynkinType: the Dynkin type does not depend on the base, because the Cartan type does not (TauCeti.HasCartanType.of_base), the Weyl group acting transitively on the bases.
• TauCeti.nonempty_equiv_of_classifiedDynkinType_eq: two root systems whose bases have the same Dynkin type are isomorphic, the classification combined with the rigidity theorem TauCeti.nonempty_equiv_of_hasCartanType.
• RootPairing.Equiv.classifiedDynkinType_map and RootPairing.Base.nonempty_equiv_iff_classifiedDynkinType_eq: conversely the Dynkin type is invariant under isomorphism, so two irreducible reduced crystallographic finite root systems are isomorphic exactly when their Dynkin types agree.

The Dynkin type is therefore a complete isomorphism invariant. The existence half of the classification, the realization of each valid type by a model root system, is combined with these statements in TauCeti.LinearAlgebra.RootSystem.FiniteType.RationalClassification.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Ch. VI, §1.5 and §4.
• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, Ch. III, §11.
• TauCetiRoadmap/RepresentationTheory/RootSystems/README.md, Layer 5.

theorem TauCeti.IsFiniteType.existsUnique_dynkinType {B : Type u_1} {A : Matrix B B ℤ} (h : IsFiniteType A) (hconn : (diagramGraph A).Connected) : ∃! t : DynkinType, t.Valid ∧ ∃ (e : B ≃ Fin t.rank), ∀ (i j : B), A i j = t.cartanMatrix (e i) (e j)

The classification of finite-type Cartan matrices. Every nonempty connected finite-type matrix agrees with the standard Cartan matrix of a unique valid Dynkin type after a simultaneous relabelling of its rows and columns.

theorem TauCeti.existsUnique_dynkinType {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [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 : DynkinType, t.Valid ∧ HasCartanType P b t

The Cartan-Killing classification, existence and uniqueness of the Dynkin type. Every irreducible reduced crystallographic finite root system has a unique valid DynkinType.

noncomputable def TauCeti.classifiedDynkinType {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [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) : DynkinType

The Dynkin type of a base, the valid type that TauCeti.existsUnique_dynkinType selects, as data rather than as an existence statement. Its two defining properties are TauCeti.valid_classifiedDynkinType and TauCeti.hasCartanType_classifiedDynkinType, and TauCeti.hasCartanType_iff_eq_classifiedDynkinType says they pin it down.

It is noncomputable: the classification says which types occur and that the type of a base is unique, not how to read it off a root system.

The type is attached to a base, but it does not depend on the base: RootPairing.Base.classifiedDynkinType_eq_classifiedDynkinType.

theorem TauCeti.valid_classifiedDynkinType {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [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) : (classifiedDynkinType b).Valid

The Dynkin type of a base is valid: it is one of Aₙ (n ≥ 1), Bₙ (n ≥ 2), Cₙ (n ≥ 3), Dₙ (n ≥ 4), E₆, E₇, E₈, F₄, G₂.

theorem TauCeti.hasCartanType_classifiedDynkinType {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [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) : HasCartanType P b (classifiedDynkinType b)

The Cartan matrix of a base is the standard Cartan matrix of its Dynkin type, up to a relabelling of the simple roots by the nodes of that type.

theorem TauCeti.HasCartanType.classifiedDynkinType_eq {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [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 : DynkinType} (h : HasCartanType P b t) (ht : t.Valid) : classifiedDynkinType b = t

A valid Cartan type of a base is its Dynkin type. This is the uniqueness half of TauCeti.existsUnique_dynkinType, in the form that identifies a type produced elsewhere - by a coordinate model, say - with the selected one.

theorem TauCeti.hasCartanType_iff_eq_classifiedDynkinType {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [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 : DynkinType} (ht : t.Valid) : HasCartanType P b t ↔ t = classifiedDynkinType b

A base has a given valid Cartan type exactly when that type is its Dynkin type.

theorem TauCeti.rank_classifiedDynkinType {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [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) : (classifiedDynkinType b).rank = b.support.card

The rank of the Dynkin type of a base is the number of simple roots.

theorem RootPairing.Base.classifiedDynkinType_eq_classifiedDynkinType {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [Finite ι] [CharZero R] [IsDomain R] [P.IsRootSystem] [P.IsCrystallographic] [P.IsReduced] [P.IsIrreducible] [Nonempty ι] (b b' : P.Base) : TauCeti.classifiedDynkinType b = TauCeti.classifiedDynkinType b'

The Dynkin type of a root system does not depend on the base, the Weyl group acting transitively on the bases.

theorem TauCeti.nonempty_equiv_of_classifiedDynkinType_eq {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [Finite ι] [CharZero R] [IsDomain R] [P.IsRootSystem] [P.IsCrystallographic] [P.IsReduced] [P.IsIrreducible] [Nonempty ι] {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P₂ : RootPairing ι₂ R M₂ N₂} [Finite ι₂] [P₂.IsRootSystem] [P₂.IsCrystallographic] [P₂.IsReduced] [P₂.IsIrreducible] [Nonempty ι₂] (b : P.Base) (b₂ : P₂.Base) (h : classifiedDynkinType b = classifiedDynkinType b₂) : Nonempty (P.Equiv P₂)

Two root systems whose bases have the same Dynkin type are isomorphic. This is the classification and the rigidity theorem TauCeti.nonempty_equiv_of_hasCartanType in one statement: the Dynkin type of a base determines the root system it comes from, up to isomorphism. The converse is RootPairing.Base.nonempty_equiv_iff_classifiedDynkinType_eq.

@[simp]

theorem RootPairing.Equiv.classifiedDynkinType_map {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [Finite ι] [CharZero R] [IsDomain R] [P.IsRootSystem] [P.IsCrystallographic] [P.IsReduced] [P.IsIrreducible] [Nonempty ι] {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P₂ : RootPairing ι₂ R M₂ N₂} [Finite ι₂] [P₂.IsRootSystem] [P₂.IsCrystallographic] [P₂.IsReduced] [P₂.IsIrreducible] [Nonempty ι₂] (e : P.Equiv P₂) (b : P.Base) : TauCeti.classifiedDynkinType (b.map e) = TauCeti.classifiedDynkinType b

The Dynkin type is invariant under isomorphism: pushing a base forward along an equivalence of root systems does not change its Dynkin type.

theorem RootPairing.Base.nonempty_equiv_iff_classifiedDynkinType_eq {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [Finite ι] [CharZero R] [IsDomain R] [P.IsRootSystem] [P.IsCrystallographic] [P.IsReduced] [P.IsIrreducible] [Nonempty ι] {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P₂ : RootPairing ι₂ R M₂ N₂} [Finite ι₂] [P₂.IsRootSystem] [P₂.IsCrystallographic] [P₂.IsReduced] [P₂.IsIrreducible] [Nonempty ι₂] (b : P.Base) (b₂ : P₂.Base) : Nonempty (P.Equiv P₂) ↔ TauCeti.classifiedDynkinType b = TauCeti.classifiedDynkinType b₂

Two root systems are isomorphic exactly when they have the same Dynkin type. Either base of either root system may be used to read off the type, since it does not depend on the base.