Documentation

TauCeti.LinearAlgebra.IntegralLattice.RootLattice.TypeD.SimpleRoots

The simple-root basis of the checkerboard lattice #

TauCeti.LinearAlgebra.IntegralLattice.RootLattice.TypeD.Basic builds the checkerboard lattice Dₙ = {x ∈ ℤⁿ | ∑ xᵢ even} in the Conway--Sloane coordinate model and computes its discriminant group. That model is the one the glue calculations need, but it does not by itself exhibit the lattice as the root lattice of type Dₙ: nothing so far relates it to the Bourbaki simple roots or to the Cartan matrix CartanMatrix.D n.

This file supplies that bridge, for 4 ≤ n. The Bourbaki-numbered simple roots

αᵢ = eᵢ - eᵢ₊₁   (i + 1 < n),      α_{n-1} = e_{n-2} + e_{n-1},

are already pinned in classical orthogonal coordinates by TauCeti.LinearAlgebra.RootSystem.ClassicalTypeD, together with their Gram matrix and their linear independence. Read in the rational ambient space ℚⁿ they lie in the checkerboard carrier, and they are proved here to be a ℤ-basis of it. Consequently the Gram matrix of the checkerboard lattice in that basis is exactly CartanMatrix.D n, which is what makes the name "type Dₙ root lattice" a theorem rather than a convention.

Spanning comes from the classical expansion: the integral span of the simple roots is exactly the lattice of integer vectors of even coordinate sum (TauCeti.DynkinType.mem_span_range_typeDSimpleRoot_iff).

Two numerical consequences close the loop with the discriminant computation of the base file. The basis-free signed determinant of the checkerboard lattice is the determinant of the Cartan matrix, and, since the discriminant group has order four and the Cartan matrix is a Gram matrix of a positive form, (CartanMatrix.D n).det = 4. This derives the determinant of CartanMatrix.D from the lattice.

Main declarations #

References #

The simple roots in the rational ambient space #

source
def TauCeti.IntegralLattice.checkerboardSimpleRoot (n : ℕ) (hn : 4 ≤ n) (i : Fin n) :
Fin n → ℚ

The i-th Bourbaki-numbered simple root of type Dₙ, read in the rational ambient space of the checkerboard lattice: the chain roots are eᵢ - eᵢ₊₁ and the fork root is e_{n-2} + e_{n-1}.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.IntegralLattice.checkerboardSimpleRoot_apply {n : ℕ} (hn : 4 ≤ n) (i j : Fin n) :
    checkerboardSimpleRoot n hn i j = ↑(DynkinType.typeDSimpleRoot n hn i j)
    source
    theorem TauCeti.IntegralLattice.checkerboardSimpleRoot_mem_checkerboardCarrier {n : ℕ} (hn : 4 ≤ n) (i : Fin n) :
    checkerboardSimpleRoot n hn i ∈ checkerboardCarrier n

    Every simple root lies in the checkerboard carrier: its coordinates are integers and their sum is 0 or 2.

    The Gram matrix #

    source
    theorem TauCeti.IntegralLattice.checkerboardLattice_form_checkerboardSimpleRoot_checkerboardSimpleRoot {n : ℕ} (hn : 4 ≤ n) (i j : Fin n) :
    ((checkerboardLattice n).form (checkerboardSimpleRoot n hn i)) (checkerboardSimpleRoot n hn j) = ↑(CartanMatrix.D n i j)

    The Gram matrix of the Bourbaki simple roots in the checkerboard lattice is the Cartan matrix of type Dₙ.

    Not a simp lemma: checkerboardLattice_form is @[simp], so simp rewrites the head of the left-hand side to Matrix.toBilin' 1 before this equation can fire. Every sibling checkerboardLattice_form_* lemma is untagged for the same reason.

    Spanning the checkerboard carrier #

    source
    theorem TauCeti.IntegralLattice.span_range_checkerboardSimpleRoot {n : ℕ} (hn : 4 ≤ n) :
    Submodule.span ℤ (Set.range (checkerboardSimpleRoot n hn)) = checkerboardCarrier n

    The Bourbaki simple roots of type Dₙ span the checkerboard carrier over ℤ.

    source
    theorem TauCeti.IntegralLattice.linearIndependent_checkerboardSimpleRoot {n : ℕ} (hn : 4 ≤ n) :
    LinearIndependent ℤ (checkerboardSimpleRoot n hn)

    The Bourbaki simple roots of type Dₙ are ℤ-linearly independent in the rational ambient space of the checkerboard lattice.

    source
    noncomputable def TauCeti.IntegralLattice.checkerboardSimpleRootBasis (n : ℕ) (hn : 4 ≤ n) :
    Module.Basis (Fin n) ℤ ↥(checkerboardLattice n).carrier

    The Bourbaki simple roots of type Dₙ are a ℤ-basis of the checkerboard lattice. This is what identifies the Conway--Sloane checkerboard model with the root lattice of type Dₙ.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.IntegralLattice.coe_checkerboardSimpleRootBasis_apply {n : ℕ} (hn : 4 ≤ n) (i : Fin n) :
      ↑((checkerboardSimpleRootBasis n hn) i) = checkerboardSimpleRoot n hn i

      The Gram matrix and the determinant #

      source
      @[simp]
      theorem TauCeti.IntegralLattice.gramMatrix_checkerboardSimpleRootBasis {n : ℕ} (hn : 4 ≤ n) :
      (checkerboardLattice n).gramMatrix (checkerboardSimpleRootBasis n hn) = CartanMatrix.D n

      The Gram matrix of the checkerboard lattice in the simple-root basis is the Cartan matrix of type Dₙ.

      source
      theorem TauCeti.IntegralLattice.determinant_checkerboardLattice_eq_det_cartanMatrixD {n : ℕ} (hn : 4 ≤ n) :
      (checkerboardLattice n).determinant = (CartanMatrix.D n).det

      The signed determinant of the checkerboard lattice is the determinant of the Cartan matrix of type Dₙ.

      source
      theorem CartanMatrix.D_det {n : ℕ} (hn : 2 ≤ n) :
      (D n).det = 4

      The determinant of the Cartan matrix of type Dₙ is 4.

      For 4 ≤ n the argument is lattice-theoretic rather than a direct expansion: the Cartan matrix is the Gram matrix of the checkerboard lattice in its simple-root basis, so its determinant is a square, and its absolute value is the order of the checkerboard discriminant group, which is four. The two smaller ranks follow from Mathlib's explicit matrices.

      source
      @[simp]
      theorem TauCeti.IntegralLattice.determinant_checkerboardLattice {n : ℕ} (hn : 4 ≤ n) :
      (checkerboardLattice n).determinant = 4

      The signed determinant of the checkerboard lattice is 4.