Integral quadratic forms and lattices

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

TheoremHermite's inequality for the minimum#

A positive definite integral lattice of rank n satisfies min L ≤ (4 / 3) ^ ((n - 1) / 2) · (det L) ^ (1 / n).

TauCeti.IntegralLattice.IsPosDef.minimum_le_rpow_mul_determinant_rpow.{u} {V : Type u}
  [AddCommGroup V] [_root_.Module ℚ V] {L : TauCeti.IntegralLattice V} (hL : L.IsPosDef) :
  ↑L.minimum ≤
    (4 / 3) ^ ((↑(Module.finrank ℤ ↥L.carrier) - 1) / 2) *
      ↑L.determinant ^ (1 / ↑(Module.finrank ℤ ↥L.carrier))
Lean

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

Other forms

Hermite's inequality for the minimum, without roots. Formalized in Tau Ceti as TauCeti.IntegralLattice.IsPosDef.three_pow_mul_minimum_pow_le.

TauCeti.IntegralLattice.IsPosDef.three_pow_mul_minimum_pow_le.{u} {V : Type u} [AddCommGroup V]
  [_root_.Module ℚ V] {L : TauCeti.IntegralLattice V} (hL : L.IsPosDef) :
  3 ^ (Module.finrank ℤ ↥L.carrier).choose 2 * ↑L.minimum ^ Module.finrank ℤ ↥L.carrier ≤
    4 ^ (Module.finrank ℤ ↥L.carrier).choose 2 * L.determinant
Sources
LeanTauCeti.IntegralLattice.IsPosDef.minimum_le_rpow_mul_determinant_rpow · TauCeti.IntegralLattice.IsPosDef.three_pow_mul_minimum_pow_le
Uses 2 · Used by 2
Statement usesTauCeti.IntegralLattice
Proof usesHermite's inequality
Used byE₈ is the unique even unimodular positive definite lattice of rank eight · Positive definite unimodular lattices of rank at most nine

TheoremA positive definite genus contains finitely many classes#

The lattices of the genus all have the rank and determinant of L, so this is the finiteness of positive definite classes of given rank and bounded determinant.

TauCeti.IntegralLattice.IsPosDef.finite_genusClasses.{u} {V : Type u} [AddCommGroup V]
  [_root_.Module ℚ V] {L : TauCeti.IntegralLattice V} (hL : L.IsPosDef) : L.genusClasses.Finite
Lean

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

Sources
LeanTauCeti.IntegralLattice.IsPosDef.finite_genusClasses
Uses 2
Statement usesTauCeti.IntegralLattice
Proof usesHermite's inequality

TheoremE₈ ⊕ E₈ ⊕ U ≅ D₁₆⁺ ⊕ U#

Adding the hyperbolic plane U makes the two non-isometric even unimodular lattices of rank sixteen isometric.

TauCeti.IntegralLattice.nonempty_isometry_orthogonalSum_hyperbolicPlane_e8PowLattice :
  Nonempty
    (((TauCeti.IntegralLattice.e8PowLattice 2).orthogonalSum
          TauCeti.IntegralLattice.hyperbolicPlane).Isometry
      ((TauCeti.IntegralLattice.checkerboardPlusLattice (8 * 2) ⋯).orthogonalSum
        TauCeti.IntegralLattice.hyperbolicPlane))
Lean

Formalized in Tau Ceti as TauCeti.IntegralLattice.nonempty_isometry_orthogonalSum_hyperbolicPlane_e8PowLattice.

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

TheoremIndefinite lattices have infinite isometry groups#

A nondegenerate indefinite integral lattice of rank at least three has infinitely many isometries.

TauCeti.IntegralLattice.infinite_isometry_of_isIndefinite.{u_1} {V : Type u_1} [AddCommGroup V]
  [_root_.Module ℚ V] {L : TauCeti.IntegralLattice V} [L.IsNondegenerate]
  (hrank : 3 ≤ Module.finrank ℤ ↥L.carrier) (hL : L.IsIndefinite) : Infinite (L.Isometry L)
Lean

Formalized in Tau Ceti as TauCeti.IntegralLattice.infinite_isometry_of_isIndefinite.

Sources
LeanTauCeti.IntegralLattice.infinite_isometry_of_isIndefinite
Uses 2
Statement usesTauCeti.IntegralLattice
Proof usesCayley–Hamilton in size two

TheoremClassification of odd unimodular forms over ℤ_[2]#

Let B and C be symmetric forms over ℤ_[2] with unit Gram determinants in bases of the same size, each representing a unit, and let w and w' be characteristic vectors for B and C. Then B and C are isometric exactly when the product of their Gram determinants is a square and B w w ≡ C w' w' modulo 8.

The second condition says that the oddities of B and C agree.

LinearMap.BilinForm.IsSymm.equivalent_iff_isSquare_det_mul_det_and_eight_dvd_of_odd.{u_1, u_2}
  {M : Type u_1} {N : Type u_2} [AddCommGroup M] [_root_.Module ℤ_[2] M] [AddCommGroup N]
  [_root_.Module ℤ_[2] N] {B : LinearMap.BilinForm ℤ_[2] M} {C : LinearMap.BilinForm ℤ_[2] N}
  (hB : B.IsSymm) (hC : C.IsSymm) {n : ℕ} (b : Module.Basis (Fin n) ℤ_[2] M)
  (c : Module.Basis (Fin n) ℤ_[2] N) (hBdet : IsUnit ((LinearMap.BilinForm.toMatrix b) B).det)
  (hCdet : IsUnit ((LinearMap.BilinForm.toMatrix c) C).det) (hBodd : ∃ x, IsUnit ((B x) x))
  (hCodd : ∃ y, IsUnit ((C y) y)) {w : M} {w' : N} (hw : B.IsCharacteristic w)
  (hw' : C.IsCharacteristic w') :
  B.Equivalent C ↔
    IsSquare (((LinearMap.BilinForm.toMatrix b) B).det * ((LinearMap.BilinForm.toMatrix c) C).det) ∧
      8 ∣ (C w') w' - (B w) w
Lean

Formalized in Tau Ceti as LinearMap.BilinForm.IsSymm.equivalent_iff_isSquare_det_mul_det_and_eight_dvd_of_odd.

Sources
LeanLinearMap.BilinForm.IsSymm.equivalent_iff_isSquare_det_mul_det_and_eight_dvd_of_odd

StructureTauCeti.FiniteQuadraticModule#

A finite abelian group equipped with a quadratic map to ℚ/ℤ.

The associated bilinear pairing is required to be the polar form, so the quadratic map determines all pairing values.

TauCeti.FiniteQuadraticModule.{u_1} : Type (u_1 + 1)
Lean

Formalized in Tau Ceti as TauCeti.FiniteQuadraticModule.

Sources
LeanTauCeti.FiniteQuadraticModule
Used by 20
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 · Nikulin's comparison theorem · Nikulin's decomposition of nondegenerate quadratic modules of odd order · Nikulin's generator decomposition · 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 · TauCeti.IntegralLattice.discriminantQuadraticModule · 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 · TauCeti.FiniteQuadraticModule.orthogonalGroup

AbbreviationTauCeti.FiniteQuadraticModule.orthogonalGroup#

The orthogonal group O(A) of a finite quadratic module A.

TauCeti.FiniteQuadraticModule.orthogonalGroup.{u_1} (A : TauCeti.FiniteQuadraticModule) :
  Subgroup (A.carrier ≃ₗ[ℤ] A.carrier)
Lean

Formalized in Tau Ceti as TauCeti.FiniteQuadraticModule.orthogonalGroup.

Sources
LeanTauCeti.FiniteQuadraticModule.orthogonalGroup
Uses 1
Statement usesTauCeti.FiniteQuadraticModule

DefinitionTauCeti.IntegralLattice.classNumber#

The class number h(L): the number of isometry classes in the genus of L. It is 0 when the genus contains infinitely many classes.

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

Formalized in Tau Ceti as TauCeti.IntegralLattice.classNumber.

Sources
LeanTauCeti.IntegralLattice.classNumber
Uses 1
Statement usesTauCeti.IntegralLattice

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.