Documentation

TauCeti.LinearAlgebra.RootSystem.FiniteType.DoubleEdge.Classification

Classification of finite double-edge chains #

The double-edge bound in TauCeti.LinearAlgebra.RootSystem.FiniteType.DoubleEdge.Basic leaves exactly three possible shapes for two nonempty chains joined by a double edge: one chain has one vertex, giving the families B_n and C_n, or both chains have two vertices, giving F_4. That file realizes the two infinite families and deliberately leaves the exceptional case to the assembly step of the classification.

This file supplies that step. The equivalence TauCeti.doubleEdgeF4Equiv reads the second chain towards the double edge, followed by the first chain away from it. Under this ordering the matrix TauCeti.doubleEdgeCartanMatrix 2 2 is Mathlib's Bourbaki-numbered CartanMatrix.F₄. Its finite type follows from TauCeti.DynkinType.isFiniteType_cartanMatrix_F4, and combining this with the double-edge bound gives a complete characterization of when the model diagram is of finite type.

This file classifies the model double-edge chains themselves, and combines this with the no-branch extraction theorem to establish the double-edge branch of the classification: every connected finite-type Cartan matrix carrying a double edge has a unique valid Dynkin type (Bₙ, Cₙ, or F₄).

Main results #

References #

This is the double-edge assembly step in the "classification of finite-type Cartan matrices" target of Layer 5 of TauCetiRoadmap/RepresentationTheory/RootSystems/README.md. The numbering of F₄ is Bourbaki's; see Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Ch. VI, §4 and plate VIII, or J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §11.4.

source
def TauCeti.doubleEdgeF4Equiv :
Fin 2 ⊕ Fin 2 ≃ Fin 4

The ordering of a double-edge chain with two vertices on each side that identifies it with the Bourbaki-numbered F₄ diagram. It reads the second chain from its outer vertex to the double edge, then the first chain from the double edge to its outer vertex. Thus inr 0, inr 1, inl 1, inl 0 become nodes 0, 1, 2, 3.

Instances For
    source
    @[simp]
    theorem TauCeti.doubleEdgeF4Equiv_inl_zero :
    doubleEdgeF4Equiv (Sum.inl 0) = 3

    The outer vertex of the first chain is node 3 under doubleEdgeF4Equiv.

    source
    @[simp]
    theorem TauCeti.doubleEdgeF4Equiv_inl_one :
    doubleEdgeF4Equiv (Sum.inl 1) = 2

    The inner vertex of the first chain is node 2 under doubleEdgeF4Equiv.

    source
    @[simp]
    theorem TauCeti.doubleEdgeF4Equiv_inr_zero :
    doubleEdgeF4Equiv (Sum.inr 0) = 0

    The outer vertex of the second chain is node 0 under doubleEdgeF4Equiv.

    source
    @[simp]
    theorem TauCeti.doubleEdgeF4Equiv_inr_one :
    doubleEdgeF4Equiv (Sum.inr 1) = 1

    The inner vertex of the second chain is node 1 under doubleEdgeF4Equiv.

    source
    theorem TauCeti.doubleEdgeCartanMatrix_two_two :
    doubleEdgeCartanMatrix 2 2 = DynkinType.F4.cartanMatrix.submatrix ⇑doubleEdgeF4Equiv ⇑doubleEdgeF4Equiv

    The exceptional double-edge chain is F₄. After ordering its four vertices from one outer end to the other, with the double edge in the middle, doubleEdgeCartanMatrix 2 2 is the standard Bourbaki-numbered Cartan matrix of the Dynkin type F₄.

    source
    theorem TauCeti.isFiniteType_doubleEdgeCartanMatrix_two_two :
    IsFiniteType (doubleEdgeCartanMatrix 2 2)

    The double-edge chain with two vertices on each side is of finite type, since it is the standard Cartan matrix of type F₄ after reindexing.

    source
    def TauCeti.doubleEdgeBEquiv (q : ℕ) :
    Fin 1 ⊕ Fin q ≃ Fin (q + 1)

    The equivalence identifying the double-edge chain with one vertex on the first chain with the standard Bourbaki-numbered B_{q+1} diagram. It puts the q vertices of the second chain first, followed by the lone vertex of the first chain.

    Instances For
      source
      @[simp]
      theorem TauCeti.doubleEdgeBEquiv_inl_val (q : ℕ) (i : Fin 1) :
      ↑((doubleEdgeBEquiv q) (Sum.inl i)) = q
      source
      @[simp]
      theorem TauCeti.doubleEdgeBEquiv_inr_val (q : ℕ) (i : Fin q) :
      ↑((doubleEdgeBEquiv q) (Sum.inr i)) = ↑i
      source
      theorem TauCeti.doubleEdgeCartanMatrix_one_left (q : ℕ) :
      doubleEdgeCartanMatrix 1 q = (CartanMatrix.B (q + 1)).submatrix ⇑(doubleEdgeBEquiv q) ⇑(doubleEdgeBEquiv q)

      A double-edge chain whose first chain is a single vertex is of type Bₙ.

      source
      @[simp]
      theorem TauCeti.isFiniteType_doubleEdgeCartanMatrix_iff {p q : ℕ} (hp : 0 < p) (hq : 0 < q) :
      IsFiniteType (doubleEdgeCartanMatrix p q) ↔ q = 1 ∨ p = 1 ∨ p = 2 ∧ q = 2

      Classification of finite double-edge chains. Suppose both chains are nonempty. Their double-edge diagram is of finite type exactly when the second chain is a single vertex (type C_n), the first chain is a single vertex (type B_n), or both chains have two vertices (type F₄).

      source
      theorem TauCeti.IsFiniteType.existsUnique_dynkinType_of_apply_mul_apply_eq_two {B : Type u_1} {A : Matrix B B ℤ} (h : IsFiniteType A) (hconn : (diagramGraph A).Preconnected) {u v : B} (huv : A u v * A v u = 2) :
      ∃! t : DynkinType, t.Valid ∧ ∃ (e : B ≃ Fin t.rank), ∀ (i j : B), A i j = t.cartanMatrix (e i) (e j)

      The double-edge branch of the finite-type classification. A connected finite-type matrix containing a double edge has a unique valid Dynkin type. It is one of Bₙ, Cₙ, or F₄.

      source
      theorem TauCeti.existsUnique_dynkinType_of_apply_mul_apply_eq_two {ι : 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] (b : P.Base) {u v : ↥b.support} (huv : b.cartanMatrix u v * b.cartanMatrix v u = 2) :
      ∃! t : DynkinType, t.Valid ∧ HasCartanType P b t

      An irreducible root system with a double edge has a unique valid Dynkin type. The type is one of Bₙ, Cₙ, or F₄.