The determinant and the discriminant group of a lattice #
Let L be a full ℤ-lattice in a finite-dimensional real inner product space E, with the
volume measure of the inner product. This file defines the determinant and the discriminant
group of L, using that the covolume of the dual lattice L^∨ = ZLattice.dual L is the inverse
of the covolume of L (ZLattice.covolume_dual).
The determinant of L is ZLattice.det L = covolume L ^ 2, the Gram determinant of any
ℤ-basis of L (ZLattice.det_eq_det_gram). The discriminant group is the quotient
ZLattice.DiscriminantGroup L = L^∨ ⧸ (L ∩ L^∨); it is defined for every lattice, and for an
integral lattice, where L ≤ L^∨, it is the quotient L^∨ ⧸ L. For an integral lattice the
discriminant group is finite of order det L = [L^∨ : L]
(ZLattice.IsIntegral.det_eq_card_discriminantGroup); in particular det L is then a positive
integer. Without integrality the discriminant group need not be finite: for c ℤ ⊆ ℝ with c²
irrational (such as L = 2^{1/4} ℤ), the dual c⁻¹ ℤ meets c ℤ only at 0, so the discriminant
group and every quotient L^∨ ⧸ (L^∨ ∩ a L^∨ ∩ L) are infinite
(ZLattice.infinite_discriminantGroup_span_singleton_of_irrational_sq,
ZLattice.infinite_quotient_smul_dual_inf_of_irrational_sq). For an integral full lattice of rank
n and a natural number c ≠ 0, the quotient L^∨ / cL of the dual by the scaled lattice
cL = (c : ℝ) • L is finite with cⁿ |L^∨ / L| elements.
For an integral lattice, unimodularity L = L^∨ is equivalent to each of covolume L = 1,
det L = 1 and the triviality of the discriminant group. A unimodular lattice is automatically
discrete and full, and has covolume one with no further assumption
(ZLattice.IsUnimodular.covolume_eq_one).
For an even lattice of even rank 2k, the signed determinant (-1)^k det L is congruent to 0
or 1 modulo 4, because the Gram matrix of a ℤ-basis is a symmetric integer matrix with even
diagonal (Matrix.IsSymm.neg_one_pow_mul_det_modEq_zero_or_one).
Main definitions #
ZLattice.det L: the determinantcovolume L ^ 2of a lattice.ZLattice.DiscriminantGroup L: the discriminant groupL^∨ ⧸ (L ∩ L^∨).ZLattice.discriminantGroupComapEquiv L e: theℤ-linear equivalence of discriminant groups induced by a linear isometry equivalencee.
Main statements #
ZLattice.det_eq_det_gram:det Lis the Gram determinant of anyℤ-basis ofL.ZLattice.det_dual:det L^∨ = (det L)⁻¹.ZLattice.card_discriminantGroup_comap: the order of the discriminant group is invariant under linear isometry equivalences.ZLattice.IsIntegral.det_eq_card_discriminantGroup: for integralL,det L = |L^∨ ⧸ L|.ZLattice.IsIntegral.finite_discriminantGroup: for integralL,L^∨ ⧸ Lis finite.ZLattice.IsIntegral.one_le_det: for integralL,1 ≤ det L.ZLattice.IsIntegral.det_toMatrix_integralForm: for integralL, the integer Gram matrix of anyℤ-basis has determinant|L^∨ ⧸ L|.ZLattice.IsIntegral.card_quotient_smul_submoduleOf_dual,ZLattice.IsIntegral.finite_quotient_smul_submoduleOf_dual: for an integral full latticeLof ranknandc ≠ 0, the quotientL^∨ / cLis finite withcⁿ |L^∨ / L|elements.ZLattice.infinite_quotient_smul_dual_inf_of_irrational_sq,ZLattice.infinite_discriminantGroup_span_singleton_of_irrational_sq: whenc²is irrational, the discriminant group ofc ℤ ⊆ ℝand every quotientL^∨ ⧸ (L^∨ ∩ a L^∨ ∩ L)are infinite.ZLattice.rank_discriminantGroup_le: the discriminant group of a full lattice of ranknis generated bynelements.ZLattice.IsUnimodular.subsingleton_discriminantGroup,ZLattice.IsUnimodular.card_discriminantGroup_eq_one: a unimodular lattice has trivial discriminant group of order1.ZLattice.IsIntegral.isUnimodular_iff_covolume_eq_one,ZLattice.IsIntegral.isUnimodular_iff_det_eq_one,ZLattice.IsIntegral.isUnimodular_iff_subsingleton_discriminantGroup: the forms of unimodularity for an integral lattice.ZLattice.IsEven.neg_one_pow_mul_card_discriminantGroup_modEq_zero_or_one: for an even lattice of rank2k,(-1)^k det L ≡ 0or1modulo4.
References #
- W. Ebeling, Lattices and Codes, 3rd ed., Springer, 2013, Chapter 1.
The discriminant group #
The discriminant group L^∨ ⧸ (L ∩ L^∨) of a lattice L, as the quotient of the dual lattice
by the vectors of L in it. For an integral lattice, where L ≤ L^∨, this is L^∨ ⧸ L, a finite
group of order det L (IsIntegral.det_eq_card_discriminantGroup).
Instances For
A vector of the dual lattice represents the zero class of the discriminant group exactly when
it lies in L.
Two vectors of the dual lattice represent the same class of the discriminant group exactly
when their difference lies in L.
The order of the discriminant group is the index of L ∩ L^∨ in L^∨.
The discriminant group is trivial exactly when the dual lattice is contained in L.
An integral lattice is unimodular exactly when its discriminant group is trivial.
A unimodular lattice has trivial discriminant group.
The discriminant group of a unimodular lattice has order 1.
A linear isometry equivalence e : F ≃ₗᵢ[ℝ] E identifies the discriminant group of the
pullback of L with the discriminant group of L.
Instances For
discriminantGroupComapEquiv L e acts on quotient classes via dualComapEquiv L e.
The order of the discriminant group is invariant under linear isometry equivalences.
The discriminant group of a full lattice is finitely generated, as a quotient of the dual lattice.
The discriminant group of a full lattice of rank n is generated by n elements: the classes
of a ℤ-basis of the dual lattice.
The determinant #
The determinant of a lattice L: the square of its covolume. For a full lattice it is the Gram
determinant of any ℤ-basis of L (det_eq_det_gram), and for an integral lattice it is the
order of the discriminant group (IsIntegral.det_eq_card_discriminantGroup).
Instances For
The determinant of a lattice is the square of its covolume.
The determinant of a full lattice is positive.
The inverse covolume is the inverse square root of the determinant. This is the normalization in the finite Fourier sum of lattice theta series.
The determinant of a full lattice is the determinant of the Gram matrix of any of its
ℤ-bases.
The determinant of the dual of a full lattice is the inverse of its determinant.
The determinant is invariant under linear isometry equivalences.
For an integral lattice L, the determinant is the index of L in its dual.
For an integral lattice L, the determinant is the order of the discriminant group
L^∨ ⧸ L. In particular it is a positive integer.
For an integral lattice the inverse covolume is the inverse square root of the discriminant group's order.
For an integral lattice the covolume is the square root of the discriminant group's order.
The discriminant group of an integral lattice is finite.
The determinant of an integral lattice is at least one: it is the order of the discriminant group, a positive integer.
For an integral full lattice L, the Gram matrix of a ℤ-basis b in the integer-valued
inner product IsIntegral.integralForm has determinant |L^∨ / L| = det L.
The signed determinant of an even lattice is a discriminant. For an even lattice L of
even rank 2k, the signed determinant (-1)^k det L is an integer congruent to 0 or 1
modulo 4. Here det L appears as the order of the discriminant group, which it equals
(ZLattice.IsIntegral.det_eq_card_discriminantGroup).
Unimodular lattices #
A unimodular lattice has covolume one.
A unimodular lattice has determinant one.
An integral lattice is unimodular exactly when its determinant is one.
An integral lattice is unimodular exactly when its covolume is one.
For an integral full lattice L of rank n, Nat.card (L^∨ / cL) = cⁿ |L^∨ / L|: the tower
cL ≤ L ≤ L^∨ has indices cⁿ and |L^∨ / L| = det L. For c ≠ 0 the quotient is therefore
finite with cⁿ |L^∨ / L| elements; for c = 0 and positive rank both sides are 0, the value
Nat.card gives an infinite type.
For an integral full lattice L and c ≠ 0, the quotient L^∨ / cL is finite.
When c² is irrational, the discriminant group of c ℤ ⊆ ℝ is infinite.