Documentation

TauCeti.LinearAlgebra.IntegralLattice.Unit

The standard unit integral lattice #

For a finite index type ι, the lattice unitLattice ι is the standard lattice I_ι = ℤ^ι in ℚ^ι, with the dot-product form. Its Gram matrix in the standard basis is the identity matrix. Consequently it is positive definite, unimodular, and has determinant and discriminant one. It is odd whenever ι is nonempty, and its signature is (#ι, 0, 0).

The lattices I_n are the basic odd unimodular lattices: they serve as the standard comparison objects in integral-lattice calculations, for instance as the odd positive definite unimodular lattices against which even lattices such as E_8 are contrasted.

The empty-index case is retained: I_∅ is the rank-zero even unimodular lattice. This is why the parity and level results below separate empty and nonempty index types.

Main declarations #

References #

source
noncomputable def TauCeti.IntegralLattice.unitLattice (ι : Type u) [Fintype ι] :
IntegralLattice (ι → ℚ)

The standard unit lattice I_ι: the integer coordinate lattice ℤ^ι inside ℚ^ι, with the dot-product form and identity Gram matrix.

Instances For
    source
    theorem TauCeti.IntegralLattice.unitLattice_carrier_eq_span_basisFun (ι : Type u) [Fintype ι] :
    (unitLattice ι).carrier = Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℚ ι))

    The standard unit lattice is the integral span of the coordinate basis.

    source
    @[simp]
    theorem TauCeti.IntegralLattice.mem_unitLattice_carrier_iff (ι : Type u) [Fintype ι] (x : ι → ℚ) :
    x ∈ (unitLattice ι).carrier ↔ ∀ (i : ι), ∃ (z : ℤ), ↑z = x i

    A vector belongs to the standard unit lattice exactly when all its coordinates are integers.

    source
    @[simp]
    theorem TauCeti.IntegralLattice.unitLattice_form_apply (ι : Type u) [Fintype ι] (x y : ι → ℚ) :
    ((unitLattice ι).form x) y = ∑ i : ι, x i * y i

    The form of the standard unit lattice is the ordinary dot product.

    source
    @[simp]
    theorem TauCeti.IntegralLattice.unitLattice_norm_apply (ι : Type u) [Fintype ι] (x : ι → ℚ) :
    (unitLattice ι).norm x = ∑ i : ι, x i ^ 2

    The norm of a vector in the standard unit lattice is the sum of its coordinate squares.

    source
    noncomputable def TauCeti.IntegralLattice.unitLatticeBasis (ι : Type u) [Fintype ι] :
    Module.Basis ι ℤ ↥(unitLattice ι).carrier

    The coordinate vectors form the standard integral basis of I_ι.

    Instances For
      source
      @[simp]
      theorem TauCeti.IntegralLattice.coe_unitLatticeBasis_apply (ι : Type u) [Fintype ι] (i : ι) :
      ↑((unitLatticeBasis ι) i) = (Pi.basisFun ℚ ι) i

      The standard integral basis vector has the corresponding unit coordinate vector in ℚ^ι.

      source
      theorem TauCeti.IntegralLattice.single_one_mem_unitLattice_carrier (ι : Type u) [Fintype ι] [DecidableEq ι] (i : ι) :
      Pi.single i 1 ∈ (unitLattice ι).carrier

      The coordinate vector eᵢ lies in the standard unit lattice.

      source
      @[simp]
      theorem TauCeti.IntegralLattice.gramMatrix_unitLatticeBasis (ι : Type u) [Fintype ι] [DecidableEq ι] :
      (unitLattice ι).gramMatrix (unitLatticeBasis ι) = 1

      The Gram matrix of the standard integral basis is the identity matrix.

      source
      @[simp]
      theorem TauCeti.IntegralLattice.finrank_unitLattice (ι : Type u) [Fintype ι] :
      Module.finrank ℤ ↥(unitLattice ι).carrier = Fintype.card ι

      The rank of I_ι is the cardinality of its index type.

      source
      @[simp]
      theorem TauCeti.IntegralLattice.unitLattice_determinant (ι : Type u) [Fintype ι] :
      (unitLattice ι).determinant = 1

      The signed determinant of the standard unit lattice is one.

      source
      @[simp]
      theorem TauCeti.IntegralLattice.unitLattice_discriminant (ι : Type u) [Fintype ι] :
      (unitLattice ι).discriminant = 1

      The discriminant of the standard unit lattice is one.

      source
      instance TauCeti.IntegralLattice.instIsNondegenerateUnitLattice (ι : Type u) [Fintype ι] :
      (unitLattice ι).IsNondegenerate

      The standard unit lattice is nondegenerate.

      source
      theorem TauCeti.IntegralLattice.isPosDef_unitLattice (ι : Type u) [Fintype ι] :
      (unitLattice ι).IsPosDef

      The standard unit lattice is positive definite.

      source
      @[simp]
      theorem TauCeti.IntegralLattice.unitLattice_signature (ι : Type u) [Fintype ι] :
      (unitLattice ι).signature = (Fintype.card ι, 0, 0)

      The standard unit lattice has signature (#ι, 0, 0).

      source
      theorem TauCeti.IntegralLattice.isUnimodular_unitLattice (ι : Type u) [Fintype ι] :
      (unitLattice ι).IsUnimodular

      The standard unit lattice is unimodular.

      source
      @[simp]
      theorem TauCeti.IntegralLattice.isEven_unitLattice_iff (ι : Type u) [Fintype ι] :
      (unitLattice ι).IsEven ↔ Fintype.card ι = 0

      The standard unit lattice is even exactly when it has rank zero.

      source
      theorem TauCeti.IntegralLattice.not_isEven_unitLattice (ι : Type u) [Fintype ι] [Nonempty ι] :
      ¬(unitLattice ι).IsEven

      A positive-rank standard unit lattice is odd.

      source
      @[simp]
      theorem TauCeti.IntegralLattice.level_unitLattice_of_isEmpty (ι : Type u) [Fintype ι] [IsEmpty ι] :
      (unitLattice ι).level = 1

      The rank-zero standard unit lattice has level one.

      source
      @[simp]
      theorem TauCeti.IntegralLattice.level_unitLattice (ι : Type u) [Fintype ι] [Nonempty ι] :
      (unitLattice ι).level = 2

      A positive-rank standard unit lattice has level two.