Documentation

TauCeti.LinearAlgebra.RootSystem.RootLength

Long and short simple roots of a Dynkin type #

A Cartan matrix records more than an unoriented diagram: the ratio of a transposed pair of its off-diagonal entries is the ratio of the squared lengths of the two simple roots. This file reads that information off the standard Cartan matrices of TauCeti.DynkinType, pinning for each type which of its nodes carry long simple roots and which carry short ones, and then proves that the reading is correct against Mathlib's RootPairing.RootPositiveForm.rootLength.

Two pieces of data are attached to a type, both read off family by family. TauCeti.DynkinType.rootLength gives the relative squared length of each simple root, normalised for a valid type so that a shortest one has length 1; it symmetrises the standard Cartan matrix on the right, A i j * ℓ j = A j i * ℓ i, so it is integral where the symmetriser d asked for by TauCeti.IsFiniteType, which scales the matrix on the left, is rational: that one is the reciprocal d i = (ℓ i)⁻¹. TauCeti.DynkinType.IsLongSimpleRoot then singles out the long nodes. Away from the degenerate B 1 those are exactly the nodes of maximal length (TauCeti.DynkinType.isLongSimpleRoot_iff), in particular for a valid type.

A handful of degenerate types stand between the family-wise reading and its intended meaning, and each of the four statements below that meets one is proved first in its exact form, naming the types it excludes, and then specialised to a valid type for the downstream consumers, which reach a type through TauCeti.HasCartanType and so have validity and nothing else. The sole node of C 1 is the last node of the Cₙ family, hence long, of length 2: nothing shorter sits beside it to normalise against, so rootLength is off by the factor 2 there. The sole node of B 1 is the last node of the Bₙ family, hence short, while being of maximal length for want of competition: that is the one type where the family-wise reading and the maximality reading of IsLongSimpleRoot part company. Finally the rank-zero types A 0, B 0, C 0 and D 0 have no node at all. A statement quantified over the nodes cannot see that, but an existential one can.

The Bourbaki numbering #

Everything here is stated against the node numbering of TauCeti.DynkinType.cartanMatrix, which is Bourbaki's with node i at Fin index i - 1. Zero-based Fin indices against one-based Bourbaki labels are the standing trap, so the numbering is pinned explicitly: the Aₙ chain runs 0, 1, …, n - 1 in order; Bₙ and Cₙ continue that chain with the double edge between n - 2 and n - 1, the short simple root being the last node of Bₙ and the long one the last node of Cₙ; Dₙ forks at n - 3; Eₙ follows Bourbaki with index 1 the branch node; F₄ has 0, 1 long and 2, 3 short; and G₂ is short then long, so TauCeti.DynkinType.IsLongSimpleRoot selects index 1 there.

G₂ is the one place where Mathlib's convention differs from Bourbaki's, and TauCeti.DynkinType.cartanMatrix follows Bourbaki: Mathlib's CartanMatrix.G₂ = !![2, -3; -1, 2] is documented as the transpose of Bourbaki's plate IX matrix, so the standard matrix pinned here is CartanMatrix.G₂ᵀ = !![2, -1; -3, 2], whose short simple root comes first. That orientation is what TauCeti.DynkinType.cartanMatrix_mul_rootLength forces: reading the lengths off the transposed matrix instead would make that identity false.

Main definitions #

Main results #

References #

See Bourbaki, Lie Groups and Lie Algebras, Chapters 4-6, plates I-IX, for the numbering and the root lengths, and Kac, Infinite Dimensional Lie Algebras, Chapter 2, for symmetrisable Cartan matrices.

source
def TauCeti.DynkinType.rootLength (t : DynkinType) :
Fin t.rank → ℤ

The relative squared length of the simple roots of a Dynkin type, in the Bourbaki numbering of TauCeti.DynkinType.cartanMatrix, given family by family and normalised, for a valid type, so that a shortest simple root has length 1.

"Length" is squared length, as in Mathlib's RootPairing.RootPositiveForm.rootLength: it is the value of an invariant form on a root with itself. The vector symmetrises the standard Cartan matrix on the right (TauCeti.DynkinType.cartanMatrix_mul_rootLength), the symmetriser d that scales it on the left, as in TauCeti.IsFiniteType, being the reciprocal d i = (ℓ i)⁻¹. Either way the matrix alone determines the vector up to a positive factor once the diagram is connected; the normalisation fixes that factor.

Validity is what the normalisation needs, and among the types of positive rank C 1 is the one that lacks it (the rank-zero types have no node to normalise against): its sole node is the last node of the Cₙ family, hence of length 2, with no shorter node beside it, so every length there is twice what the normalisation would ask. That type is excluded by TauCeti.DynkinType.Valid, and rootLength keeps the family-wise reading on it.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.DynkinType.rootLength_A (n : ℕ) :
    (A n).rootLength = fun (x : Fin (A n).rank) => 1
    source
    @[simp]
    theorem TauCeti.DynkinType.rootLength_D (n : ℕ) :
    (D n).rootLength = fun (x : Fin (D n).rank) => 1
    source
    @[simp]
    theorem TauCeti.DynkinType.rootLength_E6 :
    E6.rootLength = fun (x : Fin E6.rank) => 1
    source
    @[simp]
    theorem TauCeti.DynkinType.rootLength_E7 :
    E7.rootLength = fun (x : Fin E7.rank) => 1
    source
    @[simp]
    theorem TauCeti.DynkinType.rootLength_E8 :
    E8.rootLength = fun (x : Fin E8.rank) => 1
    source
    @[simp]
    theorem TauCeti.DynkinType.rootLength_B (n : ℕ) :
    (B n).rootLength = fun (i : Fin (B n).rank) => if ↑i + 1 = n then 1 else 2
    source
    @[simp]
    theorem TauCeti.DynkinType.rootLength_C (n : ℕ) :
    (C n).rootLength = fun (i : Fin (C n).rank) => if ↑i + 1 = n then 2 else 1
    source
    @[simp]
    theorem TauCeti.DynkinType.rootLength_F4 :
    F4.rootLength = fun (i : Fin F4.rank) => if ↑i < 2 then 2 else 1
    source
    @[simp]
    theorem TauCeti.DynkinType.rootLength_G2 :
    G2.rootLength = fun (i : Fin G2.rank) => if ↑i = 0 then 1 else 3
    source
    theorem TauCeti.DynkinType.rootLength_pos (t : DynkinType) (i : Fin t.rank) :
    0 < t.rootLength i

    Every simple root has positive length.

    source
    theorem TauCeti.DynkinType.exists_rootLength_eq_one_iff (t : DynkinType) :
    (∃ (i : Fin t.rank), t.rootLength i = 1) ↔ 0 < t.rank ∧ t ≠ C 1

    A Dynkin type has a simple root of length 1 exactly when it has a node at all and is not C 1. With TauCeti.DynkinType.rootLength_pos this is the normalisation that TauCeti.DynkinType.rootLength is stated up to: away from the two exceptions the shortest simple roots are exactly those of length 1.

    Both exceptions are degenerate. The rank-zero types A 0, B 0, C 0 and D 0 have no simple root at all to exhibit; and the sole node of C 1 is the last node of the Cₙ family, which that family calls long and gives length 2.

    source
    theorem TauCeti.DynkinType.exists_rootLength_eq_one {t : DynkinType} (ht : t.Valid) :
    ∃ (i : Fin t.rank), t.rootLength i = 1

    A valid Dynkin type has a simple root of length 1. This is TauCeti.DynkinType.exists_rootLength_eq_one_iff for a valid type, which excludes both of its exceptions: the rank-zero types and C 1.

    source
    theorem TauCeti.DynkinType.rootLength_eq_one_of_isSimplyLaced {t : DynkinType} (ht : t.IsSimplyLaced) (i : Fin t.rank) :
    t.rootLength i = 1

    A simply-laced type has all its simple roots of length 1.

    source
    theorem TauCeti.DynkinType.cartanMatrix_mul_rootLength (t : DynkinType) (i j : Fin t.rank) :
    t.cartanMatrix i j * t.rootLength j = t.cartanMatrix j i * t.rootLength i

    The standard Cartan matrix of a Dynkin type is symmetrised on the right by rootLength. Writing A = t.cartanMatrix and ℓ = t.rootLength, the products A i j * ℓ j are symmetric in i and j, so ℓ i / ℓ j = A i j / A j i whenever the two nodes are joined. This is what fixes the relative lengths, and with TauCeti.DynkinType.rootLength_pos it exhibits the rational symmetriser d i = (ℓ i)⁻¹ that TauCeti.IsFiniteType asks for, which scales the matrix on the left rather than on the right as ℓ does.

    No validity hypothesis is needed: the identity holds for the degenerate low-rank types too.

    source
    def TauCeti.DynkinType.IsLongSimpleRoot (t : DynkinType) :
    Fin t.rank → Prop

    A simple root of a Dynkin type is long when its type's family calls that node long, in the Bourbaki numbering of TauCeti.DynkinType.cartanMatrix: simply-laced types have all their simple roots of the same length, hence all long; Bₙ is short at its last node, Cₙ long only at its last node, F₄ long at its first two nodes and G₂ long at its second, following Bourbaki's numbering as TauCeti.DynkinType.cartanMatrix pins it.

    Away from the degenerate B 1 this is exactly maximality of length among the simple roots (TauCeti.DynkinType.isLongSimpleRoot_iff), in particular for a valid type (TauCeti.DynkinType.isLongSimpleRoot_iff_of_valid). B 1 really is an exception: it has a single node, of maximal length, that this predicate calls short as the short node of the Bₙ family.

    Equations
    Instances For
      source
      @[instance_reducible]
      instance TauCeti.DynkinType.instDecidablePredFinRankIsLongSimpleRoot (t : DynkinType) :
      DecidablePred t.IsLongSimpleRoot
      Equations
      source
      theorem TauCeti.DynkinType.isLongSimpleRoot_congr {t u : DynkinType} (h : t = u) (i : Fin t.rank) :
      t.IsLongSimpleRoot i ↔ u.IsLongSimpleRoot ((finCongr ⋯) i)

      The long-root predicate transports along an equality of diagrams. Transporting the statement together with its index type avoids dependent rewriting through DynkinType.rank.

      source
      @[simp]
      theorem TauCeti.DynkinType.isLongSimpleRoot_A (n : ℕ) :
      (A n).IsLongSimpleRoot = fun (x : Fin (A n).rank) => True
      source
      @[simp]
      theorem TauCeti.DynkinType.isLongSimpleRoot_D (n : ℕ) :
      (D n).IsLongSimpleRoot = fun (x : Fin (D n).rank) => True
      source
      @[simp]
      theorem TauCeti.DynkinType.isLongSimpleRoot_E6 :
      E6.IsLongSimpleRoot = fun (x : Fin E6.rank) => True
      source
      @[simp]
      theorem TauCeti.DynkinType.isLongSimpleRoot_E7 :
      E7.IsLongSimpleRoot = fun (x : Fin E7.rank) => True
      source
      @[simp]
      theorem TauCeti.DynkinType.isLongSimpleRoot_E8 :
      E8.IsLongSimpleRoot = fun (x : Fin E8.rank) => True
      source
      @[simp]
      theorem TauCeti.DynkinType.isLongSimpleRoot_B (n : ℕ) :
      (B n).IsLongSimpleRoot = fun (i : Fin (B n).rank) => ↑i + 1 < n
      source
      @[simp]
      theorem TauCeti.DynkinType.isLongSimpleRoot_C (n : ℕ) :
      (C n).IsLongSimpleRoot = fun (i : Fin (C n).rank) => ↑i + 1 = n
      source
      @[simp]
      theorem TauCeti.DynkinType.isLongSimpleRoot_F4 :
      F4.IsLongSimpleRoot = fun (i : Fin F4.rank) => ↑i < 2
      source
      @[simp]
      theorem TauCeti.DynkinType.isLongSimpleRoot_G2 :
      G2.IsLongSimpleRoot = fun (i : Fin G2.rank) => ↑i = 1
      source
      theorem TauCeti.DynkinType.isLongSimpleRoot_iff {t : DynkinType} (ht : t ≠ B 1) (i : Fin t.rank) :
      t.IsLongSimpleRoot i ↔ ∀ (j : Fin t.rank), t.rootLength j ≤ t.rootLength i

      A node of a Dynkin type other than B 1 is long exactly when its simple root has maximal length.

      The exception is not decoration. The degenerate type B 1 has a single node, necessarily of maximal length, but TauCeti.DynkinType.IsLongSimpleRoot calls it short because it is the short node of the Bₙ family; that node is the only counterexample among all the types.

      source
      theorem TauCeti.DynkinType.isLongSimpleRoot_iff_of_valid {t : DynkinType} (ht : t.Valid) (i : Fin t.rank) :
      t.IsLongSimpleRoot i ↔ ∀ (j : Fin t.rank), t.rootLength j ≤ t.rootLength i

      A node of a valid Dynkin type is long exactly when its simple root has maximal length. This is TauCeti.DynkinType.isLongSimpleRoot_iff for a valid type, which excludes its one exception B 1.

      source
      theorem TauCeti.DynkinType.isLongSimpleRoot_of_isSimplyLaced {t : DynkinType} (ht : t.IsSimplyLaced) (i : Fin t.rank) :
      t.IsLongSimpleRoot i

      Every simple root of a simply-laced type is long: all its simple roots have the same length.

      source
      theorem TauCeti.DynkinType.forall_isLongSimpleRoot_iff (t : DynkinType) :
      (∀ (i : Fin t.rank), t.IsLongSimpleRoot i) ↔ t.IsSimplyLaced ∨ t.rank = 0 ∨ t = C 1

      A Dynkin type has all its simple roots long exactly when it is simply laced, has no node at all, or is C 1. The multiply-laced types Bₙ, Cₙ, F₄ and G₂ each have a short simple root, save in the two degenerate cases the right-hand side names: the rank-zero B 0 and C 0, which have no node at all to be short, and C 1, whose sole node the Cₙ family calls long. The remaining degenerate type B 1 is no exception, its sole node being short.

      source
      theorem TauCeti.DynkinType.forall_isLongSimpleRoot_iff_isSimplyLaced {t : DynkinType} (ht : t.Valid) :
      (∀ (i : Fin t.rank), t.IsLongSimpleRoot i) ↔ t.IsSimplyLaced

      A valid Dynkin type has all its simple roots long exactly when it is simply laced. This is TauCeti.DynkinType.forall_isLongSimpleRoot_iff for a valid type, which excludes both of its degenerate cases: the rank-zero B 0 and C 0, and C 1.

      source
      theorem TauCeti.DynkinType.exists_isLongSimpleRoot_iff (t : DynkinType) :
      (∃ (i : Fin t.rank), t.IsLongSimpleRoot i) ↔ 0 < t.rank ∧ t ≠ B 1

      A Dynkin type has a long simple root exactly when it has a node at all and is not B 1. Both exceptions are degenerate: the rank-zero types have no node to be long, and the sole node of B 1 is the short last node of the Bₙ family.

      source
      theorem TauCeti.DynkinType.exists_isLongSimpleRoot {t : DynkinType} (ht : t.Valid) :
      ∃ (i : Fin t.rank), t.IsLongSimpleRoot i

      Every valid Dynkin type has a long simple root. This is TauCeti.DynkinType.exists_isLongSimpleRoot_iff for a valid type, which excludes both of its exceptions: the rank-zero types and B 1.

      source
      theorem TauCeti.DynkinType.isLongSimpleRoot_C_iff_not_isLongSimpleRoot_B (n : ℕ) (i : Fin n) :
      (C n).IsLongSimpleRoot i ↔ ¬(B n).IsLongSimpleRoot i

      Types Bₙ and Cₙ have the same diagram with long and short exchanged. Their standard Cartan matrices are transposes of one another (CartanMatrix.B_transpose), and this is that duality read at the level of root lengths: a node long in one type is short in the other.

      source
      theorem RootPairing.RootPositiveForm.rootLength_le_iff_pairingIn_le {ι : 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] {S : Type u_5} [CommRing S] [LinearOrder S] [IsStrictOrderedRing S] [Algebra S R] [FaithfulSMul S R] [Module S M] [IsScalarTower S R M] {P : RootPairing ι R M N} [P.IsValuedIn S] (B : RootPositiveForm S P) {i j : ι} (h : P.pairingIn S i j < 0) :
      B.rootLength i ≤ B.rootLength j ↔ P.pairingIn S j i ≤ P.pairingIn S i j

      Two roots meeting at a strictly negative pairing compare in length exactly as their transposed pair of pairings compares. This is the content behind reading root lengths off a Cartan matrix: ⟨αᵢ, αⱼ^∨⟩ / ⟨αⱼ, αᵢ^∨⟩ is the ratio ‖αᵢ‖² / ‖αⱼ‖², so the more negative entry belongs to the longer root.

      The negativity hypothesis is what pins the direction. It is automatic for two distinct simple roots of a base, whose pairings are nonpositive, once they are not orthogonal; for a pair with positive pairings the comparison is reversed.

      source
      theorem RootPairing.RootPositiveForm.rootLength_le_iff_dynkinRootLength_le {ι : 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] [CharZero R] {P : RootPairing ι R M N} [P.IsCrystallographic] {b : P.Base} {t : TauCeti.DynkinType} {e : ↥b.support ≃ Fin t.rank} (he : ∀ (i j : ↥b.support), b.cartanMatrix i j = t.cartanMatrix (e i) (e j)) (B : RootPositiveForm ℤ P) {i j : ↥b.support} (h : b.cartanMatrix i j < 0) :
      B.rootLength ↑i ≤ B.rootLength ↑j ↔ t.rootLength (e i) ≤ t.rootLength (e j)

      A base matched to a Dynkin type has its adjacent simple roots comparing in length exactly as TauCeti.DynkinType.rootLength says. The matching e is taken as data rather than through TauCeti.HasCartanType so that the statement names the node the comparison is made at; any witness of TauCeti.HasCartanType supplies one, and since the left-hand side does not mention e, the comparison read off the type is the same for every witness.

      The hypothesis that the two nodes are joined is necessary: two simple roots that are orthogonal are constrained by nothing, and in Cₙ for instance the first node is short although no neighbour of it is longer.