A simply-laced finite-type diagram without a branch node is of type Aₙ

The classification of finite-type Cartan matrices eliminates every shape outside the Dynkin list and is then left with the task of naming the shapes that survive: a diagram known to be a chain of single edges has to be reindexed onto the standard Cartan matrix DynkinType.cartanMatrix (.A n) before it can be said to have that Cartan type. This file performs that reindexing for the type Aₙ branch, where the surviving shape is a connected simply-laced diagram whose vertices all have at most two neighbours.

The reindexing is the identification of the diagram with a path graph: a connected finite-type diagram is a tree (TauCeti.IsFiniteType.isTree_diagramGraph), a finite tree of maximum degree two is a path graph (SimpleGraph.IsTree.nonempty_iso_pathGraph_of_degree_le_two), and a simply-laced matrix is determined by its diagram, its entries being 2 on the diagonal, -1 along the edges, and 0 elsewhere. Those are exactly the entries of CartanMatrix.A n at consecutive and non-consecutive indices, which is what TauCeti.chainEntry_eq_cartanMatrix_A records.

Both hypotheses do work. Without simple lacing the surviving shapes are Bₙ, Cₙ, F₄ and G₂, whose diagrams are also paths, and without the degree bound they are Dₙ and E₆, E₇, E₈.

Main results

• TauCeti.apply_eq_chainEntry_of_iso_pathGraph: a simply-laced normalized matrix equals chainEntry along any diagram isomorphism to pathGraph n.
• TauCeti.exists_equiv_forall_eq_cartanMatrix_A_of_isTree_of_isSimplyLaced_of_degree_le_two: a simply-laced matrix with diagonal entries 2 and a tree diagram of maximum degree two is the standard Cartan matrix of type Aₙ after a relabelling of its index type.
• TauCeti.IsFiniteType.exists_equiv_forall_eq_cartanMatrix_A: a connected simply-laced finite-type matrix whose diagram has maximum degree two is the standard Cartan matrix of type Aₙ after a relabelling of its index type.
• TauCeti.hasCartanType_A_of_isSimplyLaced_of_degree_le_two: the same statement for the base of an irreducible root system, in the form TauCeti.HasCartanType.
• TauCeti.existsUnique_dynkinType_of_isSimplyLaced_of_degree_le_two: such a base has exactly one valid Dynkin type, which is the classification statement itself on these diagrams.

References

This is the type Aₙ case of the reindexing step of the classification of finite-type Cartan matrices, Layer 5 of TauCetiRoadmap/RepresentationTheory/RootSystems/README.md. See J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §11.4, and Bourbaki, Lie Groups and Lie Algebras, Chapters 4-6, Ch. VI §4.

theorem TauCeti.apply_eq_chainEntry_of_iso_pathGraph {B : Type u_2} {A : Matrix B B ℤ} (hdiag : ∀ (i : B), A i i = 2) (hsl : A.IsSimplyLaced) {G : SimpleGraph B} (hadj : ∀ (i j : B), G.Adj i j ↔ i ≠ j ∧ A i j ≠ 0) {n : ℕ} (iso : G ≃g SimpleGraph.pathGraph n) (i j : B) : A i j = chainEntry ↑(iso i) ↑(iso j)

A simply-laced normalized matrix equals chainEntry along any diagram isomorphism to pathGraph n.

theorem TauCeti.exists_equiv_forall_eq_cartanMatrix_A_of_isTree_of_isSimplyLaced_of_degree_le_two {B : Type u_1} [Fintype B] [DecidableEq B] {A : Matrix B B ℤ} (htree : (diagramGraph A).IsTree) (hdiag : ∀ (i : B), A i i = 2) (hzero : ∀ (i j : B), A i j = 0 ↔ A j i = 0) (hsl : A.IsSimplyLaced) (hdeg : ∀ (i : B), (diagramGraph A).degree i ≤ 2) : ∃ (e : B ≃ Fin (Fintype.card B)), ∀ (i j : B), A i j = (DynkinType.A (Fintype.card B)).cartanMatrix (e i) (e j)

A simply-laced matrix with diagonal entries 2 whose diagram is a tree of maximum degree two is the standard Cartan matrix of type Aₙ, after a relabelling of its index type by the vertices of a path.

Only the Cartan-matrix normalization and symmetric vanishing pattern are needed here, rather than positive definiteness or the other finite-type hypotheses.

theorem TauCeti.IsFiniteType.exists_equiv_forall_eq_cartanMatrix_A {B : Type u_1} [Fintype B] [DecidableEq B] {A : Matrix B B ℤ} (h : IsFiniteType A) (hconn : (diagramGraph A).Connected) (hsl : A.IsSimplyLaced) (hdeg : ∀ (i : B), (diagramGraph A).degree i ≤ 2) : ∃ (e : B ≃ Fin (Fintype.card B)), ∀ (i j : B), A i j = (DynkinType.A (Fintype.card B)).cartanMatrix (e i) (e j)

A connected simply-laced finite-type matrix whose diagram has maximum degree two is the standard Cartan matrix of type Aₙ, after a relabelling of its index type by the vertices of a path.

The relabelling is simultaneous on rows and columns, which is what TauCeti.HasCartanType asks for; the type Aₙ matrix being symmetric, the orientation it fixes carries no information here.

theorem TauCeti.hasCartanType_A_of_isSimplyLaced_of_degree_le_two {ι : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [Finite ι] [CharZero R] [IsDomain R] [DecidableEq ι] [P.IsRootSystem] [P.IsCrystallographic] [P.IsReduced] [P.IsIrreducible] [Nonempty ι] (b : P.Base) (hsl : b.cartanMatrix.IsSimplyLaced) (hdeg : ∀ (i : ↥b.support), (diagramGraph b.cartanMatrix).degree i ≤ 2) : HasCartanType P b (DynkinType.A b.support.card)

An irreducible root system whose Dynkin diagram is simply laced and has no branch node has Cartan type Aₙ, for n the number of its simple roots. This is the type Aₙ half of the existence of a Dynkin type; TauCeti.HasCartanType.eq_of_valid supplies its uniqueness. Reducedness is used to deduce connectedness of the Dynkin diagram from irreducibility.

theorem TauCeti.existsUnique_dynkinType_of_isSimplyLaced_of_degree_le_two {ι : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [Finite ι] [CharZero R] [IsDomain R] [DecidableEq ι] [P.IsRootSystem] [P.IsCrystallographic] [P.IsReduced] [P.IsIrreducible] [Nonempty ι] (b : P.Base) (hsl : b.cartanMatrix.IsSimplyLaced) (hdeg : ∀ (i : ↥b.support), (diagramGraph b.cartanMatrix).degree i ≤ 2) : ∃! t : DynkinType, t.Valid ∧ HasCartanType P b t

An irreducible root system whose Dynkin diagram is simply laced and has no branch node has exactly one valid Dynkin type. Existence is the identification with type Aₙ above and uniqueness is TauCeti.HasCartanType.eq_of_valid, so this is the classification target existsUnique_dynkinType on the diagrams this file names.