Integral lattices, discriminant forms, and overlattices

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

DefinitionThe E₈ root lattice is isometric to the spinor glue lattice D₈⁺#

The underlying rational equivalence sends the i-th simple root of E₈ to the i-th vector of Bourbaki's plate VII in Conway--Sloane coordinates.

TauCeti.IntegralLattice.typeE₈IsometryD8Plus :
  TauCeti.IntegralLattice.typeE₈RootLattice.Isometry
    (TauCeti.IntegralLattice.checkerboardPlusLattice 8
      TauCeti.IntegralLattice.typeE₈IsometryD8Plus._proof_1)
Lean

Formalized in Tau Ceti as TauCeti.IntegralLattice.typeE₈IsometryD8Plus.

Sources
LeanTauCeti.IntegralLattice.typeE₈IsometryD8Plus
Uses 3 · Used by 2
Statement usesTauCeti.IntegralLattice
Proof usesTauCeti.FiniteQuadraticModule · TauCeti.IntegralLattice.discriminantQuadraticModule
Used byE₈ is the unique even unimodular positive definite lattice of rank eight · Positive definite unimodular lattices of rank at most nine

DefinitionEven overlattices correspond to quadratic-isotropic subgroups#

For an even lattice, the intermediate-carrier order isomorphism restricts to the even carriers on one side and the quadratic-isotropic subgroups of the discriminant group on the other.

TauCeti.IntegralLattice.evenIntermediateCarrierOrderIsoIsotropicSubgroup.{u} {V : Type u}
  [AddCommGroup V] [_root_.Module ℚ V] (L : TauCeti.IntegralLattice V) [L.IsNondegenerate]
  (hL : L.IsEven) :
  { M // TauCeti.IntegralLattice.IntermediateCarrier.IsEven M } ≃o
    { H // (L.discriminantQuadraticModule hL).IsIsotropic H }
Lean

Formalized in Tau Ceti as TauCeti.IntegralLattice.evenIntermediateCarrierOrderIsoIsotropicSubgroup.

Sources
LeanTauCeti.IntegralLattice.evenIntermediateCarrierOrderIsoIsotropicSubgroup
Uses 3 · Used by 2
Statement usesTauCeti.FiniteQuadraticModule · TauCeti.IntegralLattice · TauCeti.IntegralLattice.discriminantQuadraticModule
Used byGluing along a code gives a unimodular lattice exactly when the code is Lagrangian · The Leech lattice is unimodular, being glued along a Lagrangian subgroup

DefinitionThe standard model is isometric to the discriminant quadratic module of an even-rank checkerboard lattice#

The standard model is isometric to the discriminant quadratic module of an even-rank checkerboard lattice, by the identification carrying (1, 0) to the vector class and (0, 1) to the spinor class.

This is the Dₙ row of the ADE table for even n: not only is the discriminant group (ℤ/2)², its quadratic form is the displayed one.

TauCeti.IntegralLattice.checkerboardDiscriminantQuadraticIsometry (n : ℕ) [NeZero n] (hn : Even n) :
  (TauCeti.IntegralLattice.checkerboardStandardQuadraticModule n hn).Isometry
    ((TauCeti.IntegralLattice.checkerboardLattice n).discriminantQuadraticModule ⋯)
Lean

Formalized in Tau Ceti as TauCeti.IntegralLattice.checkerboardDiscriminantQuadraticIsometry.

Sources
LeanTauCeti.IntegralLattice.checkerboardDiscriminantQuadraticIsometry
Uses 3
Statement usesTauCeti.FiniteQuadraticModule · TauCeti.IntegralLattice · TauCeti.IntegralLattice.discriminantQuadraticModule

TheoremPositive definite unimodular lattices of rank at most nine#

Such a lattice is the standard lattice Iₙ, the root lattice E₈, or I₁ ⊕ E₈.

TauCeti.IntegralLattice.IsPosDef.nonempty_isometry_of_isUnimodular_of_finrank_le_nine.{u}
  {V : Type u} [AddCommGroup V] [_root_.Module ℚ V] {L : TauCeti.IntegralLattice V}
  (hL : L.IsPosDef) (hU : L.IsUnimodular) (hn : Module.finrank ℤ ↥L.carrier ≤ 9) :
  Nonempty ((TauCeti.IntegralLattice.unitLattice (Fin (Module.finrank ℤ ↥L.carrier))).Isometry L) ∨
    Nonempty (TauCeti.IntegralLattice.typeE₈RootLattice.Isometry L) ∨
      Nonempty
        (((TauCeti.IntegralLattice.unitLattice (Fin 1)).orthogonalSum
              TauCeti.IntegralLattice.typeE₈RootLattice).Isometry
          L)
Lean

Formalized in Tau Ceti as TauCeti.IntegralLattice.IsPosDef.nonempty_isometry_of_isUnimodular_of_finrank_le_nine.

Sources
LeanTauCeti.IntegralLattice.IsPosDef.nonempty_isometry_of_isUnimodular_of_finrank_le_nine
Uses 6
Statement usesTauCeti.IntegralLattice
Proof usesThe E₈ root lattice is isometric to the spinor glue lattice D₈⁺ · A positive definite lattice is I_k plus a lattice without vectors of norm one · Hermite's inequality for the minimum · TauCeti.FiniteQuadraticModule · TauCeti.IntegralLattice.discriminantQuadraticModule

TheoremE₈ is the unique even unimodular positive definite lattice of rank eight# 

TauCeti.IntegralLattice.IsPosDef.nonempty_isometry_typeE₈RootLattice_of_isEven.{u} {V : Type u}
  [AddCommGroup V] [_root_.Module ℚ V] {L : TauCeti.IntegralLattice V} (hL : L.IsPosDef)
  (hU : L.IsUnimodular) (he : L.IsEven) (hn : Module.finrank ℤ ↥L.carrier = 8) :
  Nonempty (TauCeti.IntegralLattice.typeE₈RootLattice.Isometry L)
Lean

Formalized in Tau Ceti as TauCeti.IntegralLattice.IsPosDef.nonempty_isometry_typeE₈RootLattice_of_isEven.

Sources
LeanTauCeti.IntegralLattice.IsPosDef.nonempty_isometry_typeE₈RootLattice_of_isEven
Uses 6
Statement usesTauCeti.IntegralLattice
Proof usesThe E₈ root lattice is isometric to the spinor glue lattice D₈⁺ · A positive definite lattice is I_k plus a lattice without vectors of norm one · Hermite's inequality for the minimum · TauCeti.FiniteQuadraticModule · TauCeti.IntegralLattice.discriminantQuadraticModule

TheoremThe reflections in the 240 roots generate the isometry group of the E₈ lattice#

its Weyl group is the whole of O(E₈).

TauCeti.IntegralLattice.weylGroup_typeE₈RootLattice_eq_top :
  TauCeti.IntegralLattice.typeE₈RootLattice.weylGroup = ⊤
Lean

Formalized in Tau Ceti as TauCeti.IntegralLattice.weylGroup_typeE₈RootLattice_eq_top.

Sources
LeanTauCeti.IntegralLattice.weylGroup_typeE₈RootLattice_eq_top
Uses 1
Statement usesTauCeti.IntegralLattice

StructureTauCeti.IntegralLattice#

An integral symmetric lattice in a rational vector space.

The field le_dual says exactly that the form takes integer values on pairs of vectors in carrier.

TauCeti.IntegralLattice.{u} (V : Type u) [AddCommGroup V] [_root_.Module ℚ V] : Type u
Lean

Formalized in Tau Ceti as TauCeti.IntegralLattice.

Sources
LeanTauCeti.IntegralLattice
Used by 32
Used byGluing 2 ℤ²⁴ along the Golay code gives a unimodular lattice, because the glue is Lagrangian · Gluing 2 ℤ²⁴ along the Golay code gives an even lattice, because the glue is quadratic-isotropic · Gluing along a code gives a unimodular lattice exactly when the code is Lagrangian · Over ℤ/2^r with r ≥ 1, a self-orthogonal code has an even unimodular Construction A lattice exactly when it is a Type II code · The discriminant bilinear module of a Construction A lattice is C⊥ / C · The Golay root lattice is A₁²⁴ · Milgram's theorem · Minkowski's bound for the minimum · Minkowski's convex body theorem for a realized lattice · Minkowski's second theorem · A positive definite lattice is I_k plus a lattice without vectors of norm one · E₈ is the unique even unimodular positive definite lattice of rank eight · Even overlattices correspond to quadratic-isotropic subgroups · Positive definite unimodular lattices of rank at most nine · TauCeti.IntegralLattice.discriminantQuadraticModule · The E₈ root lattice is isometric to the spinor glue lattice D₈⁺ · The reflections in the 240 roots generate the isometry group of the E₈ lattice · The standard model is isometric to the discriminant quadratic module of an even-rank checkerboard lattice · Construction B · TauCeti.IntegralLattice.isLeast_form_self_orthogonalSum · The carrier decomposition of the Leech lattice · The Leech lattice · The Leech lattice is even · The Leech lattice is unimodular, being glued along a Lagrangian subgroup · The minimum norm of the discriminant class labelled a : ZMod (n + 1) · The positive root lattice of a simply-laced Dynkin type t · The root lattice of type Dₙ is the checkerboard lattice · A positive definite genus contains finitely many classes · E₈ ⊕ E₈ ⊕ U ≅ D₁₆⁺ ⊕ U · Hermite's inequality for the minimum · Indefinite lattices have infinite isometry groups · TauCeti.IntegralLattice.classNumber

DefinitionTauCeti.IntegralLattice.discriminantQuadraticModule#

The discriminant group of an even nondegenerate integral lattice, equipped with its canonical half-norm quadratic map and discriminant polar pairing.

TauCeti.IntegralLattice.discriminantQuadraticModule.{u} {V : Type u} [AddCommGroup V]
  [_root_.Module ℚ V] (L : TauCeti.IntegralLattice V) [L.IsNondegenerate] (hL : L.IsEven) :
  TauCeti.FiniteQuadraticModule
Lean

Formalized in Tau Ceti as TauCeti.IntegralLattice.discriminantQuadraticModule.

Sources
LeanTauCeti.IntegralLattice.discriminantQuadraticModule
Uses 2 · Used by 14
Statement usesTauCeti.FiniteQuadraticModule · TauCeti.IntegralLattice
Used byGluing 2 ℤ²⁴ along the Golay code gives a unimodular lattice, because the glue is Lagrangian · Gluing 2 ℤ²⁴ along the Golay code gives an even lattice, because the glue is quadratic-isotropic · Gluing along a code gives a unimodular lattice exactly when the code is Lagrangian · Milgram's theorem · E₈ is the unique even unimodular positive definite lattice of rank eight · Even overlattices correspond to quadratic-isotropic subgroups · Positive definite unimodular lattices of rank at most nine · The E₈ root lattice is isometric to the spinor glue lattice D₈⁺ · The standard model is isometric to the discriminant quadratic module of an even-rank checkerboard lattice · The carrier decomposition of the Leech lattice · The Leech lattice · The Leech lattice is even · The Leech lattice is unimodular, being glued along a Lagrangian subgroup · E₈ ⊕ E₈ ⊕ U ≅ D₁₆⁺ ⊕ U

DefinitionA positive definite lattice is I_k plus a lattice without vectors of norm one#

The standard lattice I_k is carried onto the unit-norm sublattice, with k its rank, and the second summand is the complement unitNormComplement L.

TauCeti.IntegralLattice.IsPosDef.unitNormDecomposition.{u} {V : Type u} [AddCommGroup V]
  [_root_.Module ℚ V] {L : TauCeti.IntegralLattice V} (hL : L.IsPosDef) :
  ((TauCeti.IntegralLattice.unitLattice (Fin (Module.finrank ℤ ↥L.unitNormSubmodule))).orthogonalSum
        L.unitNormComplement).Isometry
    L
Lean

Formalized in Tau Ceti as TauCeti.IntegralLattice.IsPosDef.unitNormDecomposition.

Sources
LeanTauCeti.IntegralLattice.IsPosDef.unitNormDecomposition
Uses 1 · Used by 2
Statement usesTauCeti.IntegralLattice
Used byE₈ is the unique even unimodular positive definite lattice of rank eight · Positive definite unimodular lattices of rank at most nine

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.