Finiteness in a definite lattice: bounded-norm sets, shells and isometries

A positive definite integral lattice has only finitely many vectors of norm at most any given bound, and hence only finitely many vectors of any given norm. This is what makes the minimum, the shells and the representation numbers of a positive definite lattice finite quantities. A negative definite lattice likewise has only finitely many vectors of norm at least any given bound, and finite shells.

Finite shells make the isometry group finite: an isometry L → M is determined by the images of a ℤ-basis of L, and each of these lies in the shell of M of the corresponding norm. Hence there are only finitely many isometries into a definite lattice, and in particular the isometry group O(L) = Isometry L L of a definite lattice L is finite.

Definiteness is load-bearing: the hyperbolic plane is nondegenerate, yet its isotropic vectors form an infinite shell of norm zero (TauCeti.IntegralLattice.infinite_vectorsOfNorm_zero_hyperbolicPlane).

Main results

• TauCeti.IntegralLattice.IsPosSemidef.integralNorm_nonneg and TauCeti.IntegralLattice.IsPosDef.posDef_integralNorm: the integral norm form of a positive semidefinite lattice is nonnegative, and that of a positive definite lattice is positive definite.
• TauCeti.IntegralLattice.IsPosDef.finite_setOf_norm_le: only finitely many lattice vectors have norm at most a given rational bound.
• TauCeti.IntegralLattice.IsPosDef.finite_vectorsOfNorm and TauCeti.IntegralLattice.IsNegDef.finite_vectorsOfNorm: every shell of a definite lattice is finite.
• TauCeti.IntegralLattice.finite_isometry_of_forall_finite_vectorsOfNorm: there are only finitely many isometries into a lattice all of whose shells are finite.
• TauCeti.IntegralLattice.IsPosDef.finite_isometry and TauCeti.IntegralLattice.IsNegDef.finite_isometry: there are only finitely many isometries into a definite lattice; in particular the isometry group of a definite lattice is finite.

References

• O. T. O'Meara, Introduction to Quadratic Forms, §102.
• J. H. Conway and N. J. A. Sloane, Sphere Packings, Lattices and Groups, Chapter 1, §2.

theorem TauCeti.IntegralLattice.IsPosSemidef.integralNorm_nonneg {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosSemidef) (x : ↥L.carrier) : 0 ≤ L.integralNorm x

The integral norm of a positive semidefinite lattice is nonnegative.

theorem TauCeti.IntegralLattice.IsPosDef.posDef_integralNorm {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) : QuadraticMap.PosDef L.integralNorm

The integral norm form of a positive definite lattice is positive definite.

theorem TauCeti.IntegralLattice.IsPosDef.finite_setOf_norm_le {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) (C : ℚ) : {x : ↥L.carrier | L.norm ↑x ≤ C}.Finite

Bounded-norm sets of a positive definite lattice are finite. Only finitely many vectors of a positive definite integral lattice have norm at most a given rational bound.

theorem TauCeti.IntegralLattice.IsPosDef.finite_vectorsOfNorm {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) (n : ℚ) : (L.vectorsOfNorm n).Finite

Every shell of a positive definite lattice is finite.

theorem TauCeti.IntegralLattice.IsNegDef.posDef_neg_integralNorm {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsNegDef) : QuadraticMap.PosDef (-L.integralNorm)

The negated integral norm form of a negative definite lattice is positive definite.

theorem TauCeti.IntegralLattice.IsNegDef.finite_setOf_le_norm {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsNegDef) (C : ℚ) : {x : ↥L.carrier | C ≤ L.norm ↑x}.Finite

Sets of bounded norm in a negative definite lattice are finite. Only finitely many vectors of a negative definite integral lattice have norm at least a given rational bound.

theorem TauCeti.IntegralLattice.IsNegDef.finite_vectorsOfNorm {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsNegDef) (n : ℚ) : (L.vectorsOfNorm n).Finite

Every shell of a negative definite lattice is finite.

theorem TauCeti.IntegralLattice.finite_isometry_of_forall_finite_vectorsOfNorm {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {W : Type u_1} [AddCommGroup W] [Module ℚ W] {M : IntegralLattice W} (h : ∀ (n : ℚ), (M.vectorsOfNorm n).Finite) : Finite (L.Isometry M)

Finite shells give finitely many isometries. An isometry L → M is determined by the images of a ℤ-basis of L, each of which lies in the shell of M of the corresponding norm; so if every shell of M is finite, there are only finitely many isometries from L to M.

theorem TauCeti.IntegralLattice.IsPosDef.finite_isometry {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {W : Type u_1} [AddCommGroup W] [Module ℚ W] {M : IntegralLattice W} (hM : M.IsPosDef) : Finite (L.Isometry M)

The isometry group of a positive definite lattice is finite. More generally, there are only finitely many isometries into a positive definite lattice.

theorem TauCeti.IntegralLattice.IsNegDef.finite_isometry {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {W : Type u_1} [AddCommGroup W] [Module ℚ W] {M : IntegralLattice W} (hM : M.IsNegDef) : Finite (L.Isometry M)

The isometry group of a negative definite lattice is finite. More generally, there are only finitely many isometries into a negative definite lattice.