Documentation

TauCeti.LinearAlgebra.IntegralLattice.RationalInvariants

Rational form invariants of an integral lattice #

A nondegenerate integral lattice has two determinant invariants: its signed integral Gram determinant and the square-class discriminant of its ambient rational quadratic form. This file identifies them. It also records the signed square-class invariant, whose additional factor is determined solely by the rank.

The comparison lets arithmetic invariants of the rational quadratic space be read directly from an integral Gram matrix. It is the bridge between the determinant theory of integral lattices and the regular-form invariants used in local and global classification.

Main definition #

Main results #

source
noncomputable def TauCeti.IntegralLattice.rationalFormClass {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] :
RegularFormClass ℚ

The regular isometry class of the ambient rational norm form of a nondegenerate integral lattice.

Instances For
    source
    theorem TauCeti.IntegralLattice.rationalFormClass_def {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] :
    L.rationalFormClass = formClass L.norm ⋯

    Unfolding the rational form class to the class of the ambient norm quadratic form.

    source
    @[simp]
    theorem TauCeti.IntegralLattice.rank_rationalFormClass {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] :
    L.rationalFormClass.rank = Module.finrank ℤ ↥L.carrier

    The rank of the rational form class is the rank of the lattice carrier.

    source
    theorem TauCeti.IntegralLattice.toMatrix_norm_rationalBasis {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) :
    QuadraticForm.toMatrix L.rationalBasis L.norm = (L.gramMatrix (Module.Free.chooseBasis ℤ ↥L.carrier)).map ⇑(algebraMap ℤ ℚ)

    The matrix of the ambient norm form in the rationalized carrier basis is the cast of the integral Gram matrix.

    source
    theorem TauCeti.IntegralLattice.discr_rationalFormClass {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] :
    L.rationalFormClass.discr = squareClass L.determinantUnit

    The discriminant of the ambient rational form is the square class of the signed integral Gram determinant.

    source
    theorem TauCeti.IntegralLattice.signedDiscr_rationalFormClass {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] :
    L.rationalFormClass.signedDiscr = (Module.finrank ℤ ↥L.carrier).choose 2 • squareClass (-1) + squareClass L.determinantUnit

    The signed discriminant of the ambient rational form is the determinant square class with the standard rank-dependent sign correction.

    source
    theorem TauCeti.IntegralLattice.Isometry.rationalFormClass_eq {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type w} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) [L.IsNondegenerate] [M.IsNondegenerate] :
    L.rationalFormClass = M.rationalFormClass

    An integral-lattice isometry preserves the regular class of the ambient rational form.