The determinant of a full sublattice

Whenever two integral lattices share their ambient rational form and the carrier of one lies inside the carrier of the other, their invariants differ by the square of the index:

det(L) = det(M) · [M : L]²,      disc(L) = disc(M) · [M : L]².

Nondegeneracy is not needed: in the degenerate case both determinants vanish and the equalities are 0 = 0.

Extending carrier bases of the two lattices to bases of the ambient rational space, the index is the absolute determinant of the change-of-basis matrix by AddSubgroup.relIndex_eq_abs_det, while the Gram determinants differ by the square of that same determinant because a bilinear form's matrix transforms by congruence.

Main results

• TauCeti.IntegralLattice.determinant_eq_mul_relIndex_sq and TauCeti.IntegralLattice.discriminant_eq_mul_relIndex_sq: the determinant and the discriminant of a full sublattice scale by the square of the index.

References

• V. V. Nikulin, Integral symmetric bilinear forms and some of their applications, §1.4.
• W. Ebeling, Lattices and Codes, Chapter 1.
• TauCetiRoadmap/IntegralLattices/README.md, Layer 4.

theorem TauCeti.IntegralLattice.determinant_eq_mul_relIndex_sq {V : Type u} [AddCommGroup V] [Module ℚ V] (L M : IntegralLattice V) (hform : L.form = M.form) (hle : L.carrier ≤ M.carrier) : L.determinant = M.determinant * ↑(L.carrier.toAddSubgroup.relIndex M.carrier.toAddSubgroup) ^ 2

The signed determinant of a full sublattice scales by the square of the index. If two integral lattices share their ambient rational form and one carrier lies inside the other, the determinant of the smaller carrier L.carrier is the determinant of the larger carrier M.carrier times the square of the index [M : L].

theorem TauCeti.IntegralLattice.discriminant_eq_mul_relIndex_sq {V : Type u} [AddCommGroup V] [Module ℚ V] (L M : IntegralLattice V) (hform : L.form = M.form) (hle : L.carrier ≤ M.carrier) : L.discriminant = M.discriminant * L.carrier.toAddSubgroup.relIndex M.carrier.toAddSubgroup ^ 2

The discriminant of a full sublattice scales by the square of the index.