Documentation

TauCeti.LinearAlgebra.RootSystem.FiniteType.Star.Classification

Classification of finite three-arm stars #

The fork bound in TauCeti.LinearAlgebra.RootSystem.FiniteType.Star.Basic restricts an ordered three-arm star of finite type to the shapes underlying A, D, E₆, E₇, and E₈. This file identifies each surviving model star with its standard Cartan matrix and proves the converse, completing the classification of the model stars themselves.

This is the simply-laced fork assembly step in Layer 5 of the root-systems roadmap. Extracting such a star from an arbitrary connected finite-type diagram remains part of the assembly of the full Cartan--Killing classification.

Main definitions #

Main results #

References #

The classification follows N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Chapter VI, §4, and J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §11.4.

Chains #

Forks #

Exceptional forks #

source
theorem TauCeti.isFiniteType_starCartanMatrix_three_iff {a b c : ℕ} (hab : a ≤ b) (hbc : b ≤ c) :
IsFiniteType (starCartanMatrix ![a, b, c]) ↔ a = 0 ∨ a = 1 ∧ b = 1 ∨ a = 1 ∧ b = 2 ∧ c ≤ 4

An ordered three-arm star is of finite type exactly for the A, D, and exceptional E shapes. Arm lengths count vertices beyond the centre, so an empty first arm gives an A-chain, ![1, 1, c] gives D, and ![1, 2, 2], ![1, 2, 3], ![1, 2, 4] give E₆, E₇, E₈.

The forward implication is the fork bound. For the converse, the explicit reindexings above identify every surviving model with a principal submatrix of its standard Cartan matrix.

Cartan types of forks #

source
def TauCeti.StarHasCartanType {α : Type u_1} [DecidableEq α] (ℓ : α → ℕ) (t : DynkinType) :
Prop

The star with arms ℓ has Cartan type t when its vertices can be relabelled by the Bourbaki indices Fin t.rank so that its Cartan matrix becomes the standard one of type t. The same relabelling is applied simultaneously to rows and columns.

Instances For
    source
    theorem TauCeti.starHasCartanType_iff {α : Type u_1} [DecidableEq α] (ℓ : α → ℕ) (t : DynkinType) :
    StarHasCartanType ℓ t ↔ ∃ (e : StarIndex ℓ ≃ Fin t.rank), ∀ (v w : StarIndex ℓ), starCartanMatrix ℓ v w = t.cartanMatrix (e v) (e w)

    Having Cartan type t, unfolded to the simultaneous relabelling it asserts to exist. This is the interface through which consumers build and destructure TauCeti.StarHasCartanType.

    source
    theorem TauCeti.starHasCartanType_iff_reindex {α : Type u_1} [DecidableEq α] (ℓ : α → ℕ) (t : DynkinType) :
    StarHasCartanType ℓ t ↔ ∃ (e : StarIndex ℓ ≃ Fin t.rank), (Matrix.reindex e e) (starCartanMatrix ℓ) = t.cartanMatrix

    Having Cartan type t, expressed as a reindexing of matrices rather than entrywise.

    source
    theorem TauCeti.StarHasCartanType.eq_of_valid {α : Type u_1} [DecidableEq α] {ℓ : α → ℕ} {t t' : DynkinType} (h : StarHasCartanType ℓ t) (h' : StarHasCartanType ℓ t') (ht : t.Valid) (ht' : t'.Valid) :
    t = t'

    A star has at most one valid Cartan type.

    source
    theorem TauCeti.StarHasCartanType.comp {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {t : DynkinType} {m : β → ℕ} (h : StarHasCartanType m t) (e : α ≃ β) :
    StarHasCartanType (m ∘ ⇑e) t

    Having a Cartan type is invariant under relabelling the arms.

    source
    @[simp]
    theorem TauCeti.starHasCartanType_comp_iff {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {t : DynkinType} {m : β → ℕ} (e : α ≃ β) :
    StarHasCartanType (m ∘ ⇑e) t ↔ StarHasCartanType m t

    Having a Cartan type is invariant under relabelling the arms, in either direction.

    The fork (1, 1, c) and type D #

    source
    theorem TauCeti.starHasCartanType_D (c : ℕ) :
    StarHasCartanType ![1, 1, c] (DynkinType.D (c + 3))

    The fork of type D. The star with arms of one, one and c vertices has Cartan type D (c + 3). When 1 ≤ c, the branch node is Bourbaki index c, the two leaves of the fork are c + 1 and c + 2, and the long arm is the chain c - 1, …, 0. When c = 0, the third arm is empty and the same formula identifies the resulting chain with the degenerate type D 3.

    The exceptional shapes (1, 2, c) and the types E₆, E₇, E₈ #

    source
    theorem TauCeti.starHasCartanType_E6 :
    StarHasCartanType ![1, 2, 2] DynkinType.E6

    Type E₆. The star with arms of one, two and two vertices has Cartan type E₆.

    source
    theorem TauCeti.starHasCartanType_E7 :
    StarHasCartanType ![1, 2, 3] DynkinType.E7

    Type E₇. The star with arms of one, two and three vertices has Cartan type E₇.

    source
    theorem TauCeti.starHasCartanType_E8 :
    StarHasCartanType ![1, 2, 4] DynkinType.E8

    Type E₈. The star with arms of one, two and four vertices has Cartan type E₈.

    source
    theorem TauCeti.IsFiniteType.existsUnique_dynkinType_of_star {ℓ : Fin 3 → ℕ} (hℓ : ∀ (i : Fin 3), ℓ i ≠ 0) (h : IsFiniteType (starCartanMatrix ℓ)) :
    ∃! t : DynkinType, t.Valid ∧ StarHasCartanType ℓ t

    The classification of the three-armed forks of finite type. A finite star with three nonempty arms has a unique valid Cartan type: exactly one valid standard Cartan matrix agrees with the star after simultaneously relabelling its rows and columns.

    The fork bound leaves the shapes (1, 1, c), (1, 2, 2), (1, 2, 3), and (1, 2, 4) after the arms are sorted. The theorems TauCeti.starHasCartanType_D, TauCeti.starHasCartanType_E6, TauCeti.starHasCartanType_E7, and TauCeti.starHasCartanType_E8 identify those shapes as D or one of the exceptional E types. Uniqueness follows from TauCeti.DynkinType.eq_of_valid_of_forall_eq.