Isometry groups of indefinite lattices are infinite

A nondegenerate indefinite integral lattice L of rank at least three has infinitely many isometries, in contrast with the finiteness of O(L) for definite lattices. The proof splits according to whether the rational norm form of L is isotropic. The isotropic case, in which the Eichler transvections already form an infinite group, is TauCeti.IntegralLattice.infinite_isometry_of_not_anisotropic. This file treats the anisotropic case and assembles the two.

Suppose the rational norm form is anisotropic and indefinite; no rank or nondegeneracy hypothesis is needed. Choose lattice vectors x and y of positive and negative norm. They span a binary sublattice M whose rational norm form is indefinite and anisotropic, so its primitive discriminant is positive and not a square, and O(M) is infinite by Pell's equation. Its rational form is nondegenerate, so every isometry of M extends to a rational isometry of L acting as the identity on the orthogonal complement of ℚ x + ℚ y (LinearMap.BilinForm.Isometry.isometryGroupExtend). Such an extension need not preserve L, but a nonzero integer d carries the orthogonal projection of L into M, and then every isometry of M acting trivially on M / d M extends to an isometry of L. These isometries form a subgroup of finite index in the infinite group O(M), and distinct ones have distinct extensions.

In rank two an indefinite lattice with isotropic norm form, such as the hyperbolic plane, can have a finite isometry group, so the rank hypothesis of the combined statement cannot be dropped.

Main results

• TauCeti.IntegralLattice.infinite_isometry_of_isIndefinite_of_anisotropic: an indefinite lattice with anisotropic rational norm form has infinite O(L), and TauCeti.IntegralLattice.infinite_specialOrthogonalGroup_of_isIndefinite_of_anisotropic infinite SO(L).
• TauCeti.IntegralLattice.infinite_isometry_of_isIndefinite and TauCeti.IntegralLattice.infinite_specialOrthogonalGroup_of_isIndefinite: a nondegenerate indefinite lattice of rank at least three has infinite O(L) and SO(L).

References

• J. W. S. Cassels, Rational Quadratic Forms, Chapter 13.
• M. Eichler, Quadratische Formen und orthogonale Gruppen, Springer (1952).

A binary sublattice of an indefinite lattice

Extending isometries of the binary sublattice

The anisotropic case

theorem TauCeti.IntegralLattice.infinite_isometry_of_isIndefinite_of_anisotropic {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsIndefinite) (haniso : QuadraticMap.Anisotropic L.norm) : Infinite (L.Isometry L)

The anisotropic case of the infiniteness of O(L). An indefinite integral lattice whose rational norm form is anisotropic has infinitely many isometries. No rank or nondegeneracy hypothesis is needed: anisotropy forces nondegeneracy, and in rank two this is the Pell case.

theorem TauCeti.IntegralLattice.infinite_specialOrthogonalGroup_of_isIndefinite_of_anisotropic {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsIndefinite) (haniso : QuadraticMap.Anisotropic L.norm) : Infinite ↥L.specialOrthogonalGroup

The anisotropic case of the infiniteness of SO(L). An indefinite integral lattice whose rational norm form is anisotropic has infinitely many proper isometries.

Indefinite lattices of rank at least three

theorem TauCeti.IntegralLattice.infinite_isometry_of_isIndefinite {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [L.IsNondegenerate] (hrank : 3 ≤ Module.finrank ℤ ↥L.carrier) (hL : L.IsIndefinite) : Infinite (L.Isometry L)

Indefinite lattices have infinite isometry groups. A nondegenerate indefinite integral lattice of rank at least three has infinitely many isometries.

theorem TauCeti.IntegralLattice.infinite_specialOrthogonalGroup_of_isIndefinite {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} [L.IsNondegenerate] (hrank : 3 ≤ Module.finrank ℤ ↥L.carrier) (hL : L.IsIndefinite) : Infinite ↥L.specialOrthogonalGroup

Indefinite lattices have infinite special isometry groups. A nondegenerate indefinite integral lattice of rank at least three has infinitely many proper isometries.