Documentation

TauCeti.LinearAlgebra.IntegralLattice.Unimodular

Unimodular integral lattices #

An integral lattice is unimodular when its carrier is equal to its dual carrier. For a nondegenerate lattice this file identifies that condition with each of the standard criteria: the discriminant group is trivial, its cardinality is one, the Gram determinant is a unit, the discriminant is one, and the restricted integral pairing is a linear equivalence. Unimodularity also forces nondegeneracy of the rational form.

The cardinality of the discriminant group is also computed as the absolute value of the Gram determinant. The proof uses Mathlib's determinant/index formula for a full-rank submodule rather than reproving Smith normal form.

Main declarations #

References #

source
def TauCeti.IntegralLattice.IsUnimodular {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) :
Prop

An integral lattice is unimodular when it is equal to its dual lattice inside the common rational ambient space.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.IntegralLattice.isUnimodular_def {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) :
    L.IsUnimodular ↔ L.carrier = L.dualCarrier

    Unimodularity unfolded as equality with the dual carrier.

    source
    theorem TauCeti.IntegralLattice.IsUnimodular.nondegenerate {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsUnimodular) :
    L.form.Nondegenerate

    A unimodular integral lattice has a nondegenerate rational form.

    source
    theorem TauCeti.IntegralLattice.isUnimodular_iff_dualCarrier_le {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) :
    L.IsUnimodular ↔ L.dualCarrier ≤ L.carrier

    Unimodularity is equivalent to every vector in the dual carrier already belonging to the original carrier.

    source
    theorem TauCeti.IntegralLattice.isUnimodular_iff_carrierInDual_eq_top {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) :
    L.IsUnimodular ↔ L.carrierInDual = ⊤

    Unimodularity is equivalent to the embedded carrier filling the dual carrier.

    source
    theorem TauCeti.IntegralLattice.isUnimodular_iff_subsingleton_discriminantGroup {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) :
    L.IsUnimodular ↔ Subsingleton L.DiscriminantGroup

    Unimodularity is equivalent to triviality of the discriminant group.

    source
    theorem TauCeti.IntegralLattice.isUnimodular_iff_natCard_discriminantGroup_eq_one {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) :
    L.IsUnimodular ↔ Nat.card L.DiscriminantGroup = 1

    Unimodularity is equivalent to the discriminant group having one element.

    source
    theorem TauCeti.IntegralLattice.Isometry.isUnimodular_iff {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) :
    L.IsUnimodular ↔ M.IsUnimodular

    Unimodularity is preserved and reflected by an integral-lattice isometry.

    source
    theorem TauCeti.IntegralLattice.integralForm_eq_dualPairingEquiv_comp {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] :
    L.integralForm = ↑L.dualPairingEquiv ∘ₗ Submodule.inclusion ⋯

    The restricted integral form factors as carrier inclusion followed by the perfect dual pairing.

    source
    theorem TauCeti.IntegralLattice.isUnimodular_iff_integralForm_bijective {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] :
    L.IsUnimodular ↔ Function.Bijective ⇑L.integralForm

    A nondegenerate integral lattice is unimodular exactly when its restricted pairing with the module dual is bijective.

    source
    noncomputable def TauCeti.IntegralLattice.integralPairingEquiv {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] (hL : L.IsUnimodular) :
    ↥L.carrier ≃ₗ[ℤ] Module.Dual ℤ ↥L.carrier

    For a unimodular lattice, the restricted integral pairing is a linear equivalence with the module dual.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.IntegralLattice.integralPairingEquiv_toLinearMap {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] (hL : L.IsUnimodular) :
      ↑(L.integralPairingEquiv hL) = L.integralForm

      The underlying linear map of integralPairingEquiv is the restricted integral form.

      source
      theorem TauCeti.IntegralLattice.isUnimodular_iff_discriminant_eq_one {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] :
      L.IsUnimodular ↔ L.discriminant = 1

      A nondegenerate integral lattice is unimodular exactly when its basis-independent discriminant is one.

      source
      theorem TauCeti.IntegralLattice.isUnimodular_iff_isUnit_determinant {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] :
      L.IsUnimodular ↔ IsUnit L.determinant

      A nondegenerate integral lattice is unimodular exactly when its signed determinant is a unit of ℤ.

      source
      theorem TauCeti.IntegralLattice.isUnimodular_iff_natAbs_gramDet_eq_one {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] {ι : Type v} [Fintype ι] [DecidableEq ι] (e : Module.Basis ι ℤ ↥L.carrier) :
      L.IsUnimodular ↔ (L.gramDet e).natAbs = 1

      In every carrier basis, unimodularity is equivalent to the Gram determinant having absolute value one.

      source
      theorem TauCeti.IntegralLattice.isUnimodular_iff_isUnit_gramDet {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] {ι : Type v} [Fintype ι] [DecidableEq ι] (e : Module.Basis ι ℤ ↥L.carrier) :
      L.IsUnimodular ↔ IsUnit (L.gramDet e)

      In every carrier basis, unimodularity is equivalent to the signed Gram determinant being a unit of ℤ; in particular, determinant -1 is allowed.