Class sets and class numbers of integral lattices

The classes in the genus of L form the subset L.genusClasses of the isometry classes IsometryQuotient V of integral lattices in the ambient space V of L, and the class number h(L) is its cardinality.

All lattices in one genus have the same rank, so they all live, up to isometry, in the ambient space of L: every lattice in the genus of L, in any rational space, is isometric to one in V (TauCeti.IntegralLattice.SameGenus.exists_isometry). Accordingly the class number depends only on the genus and not on the ambient space used to count it (TauCeti.IntegralLattice.SameGenus.classNumber_eq).

The class number is defined for every lattice, as a natural-number cardinality, and is 0 exactly when the genus contains infinitely many classes. Finiteness has different proofs for different kinds of lattices. This file proves it for definite lattices: for positive definite ones it is a consequence of reduction theory (TauCeti.IntegralLattice.finite_of_pairwise_isEmpty_isometry), and the negative definite case follows by negating the form. It also computes the class set directly in rank at most one, where the class number is 1 by the determinant classification TauCeti.IntegralLattice.nonempty_isometry_of_finrank_le_one.

Main definitions

• TauCeti.IntegralLattice.genusClasses: the classes in the genus of L.
• TauCeti.IntegralLattice.classNumber: the class number h(L).

Main results

• TauCeti.IntegralLattice.isometryClass_mem_genusClasses_iff: the class of M lies in the genus of L exactly when M has the same genus as L.
• TauCeti.IntegralLattice.SameGenus.classNumber_eq: lattices of the same genus, in possibly different ambient spaces, have the same class number.
• TauCeti.IntegralLattice.IsPosDef.finite_genusClasses and TauCeti.IntegralLattice.IsNegDef.finite_genusClasses: a definite genus contains finitely many classes.
• TauCeti.IntegralLattice.card_le_classNumber_of_pairwise_isEmpty_isometry and TauCeti.IntegralLattice.card_eq_classNumber_iff_of_pairwise_isEmpty_isometry: a family of pairwise non-isometric lattices in a genus with finitely many classes has at most h(L) members, with equality exactly when it represents every class.
• TauCeti.IntegralLattice.classNumber_eq_one_of_finrank_le_one: in rank at most one the genus is a single class.

References

• O. T. O'Meara, Introduction to Quadratic Forms, §102A, for classes, genera and class numbers.
• J. W. S. Cassels, Rational Quadratic Forms, Chapter 9, §1.

def TauCeti.IntegralLattice.genusClasses {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : Set (IsometryQuotient V)

The classes in the genus of L: the isometry classes of the lattices in the ambient space of L which have the same genus as L.

@[simp]

theorem TauCeti.IntegralLattice.isometryClass_mem_genusClasses_iff {V : Type u} [AddCommGroup V] [Module ℚ V] {L M : IntegralLattice V} : M.isometryClass ∈ L.genusClasses ↔ L.SameGenus M

The class of M lies in the genus of L exactly when M has the same genus as L.

theorem TauCeti.IntegralLattice.isometryClass_mem_genusClasses {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.isometryClass ∈ L.genusClasses

The genus of L contains the class of L.

theorem TauCeti.IntegralLattice.genusClasses_nonempty {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.genusClasses.Nonempty

The genus of a lattice contains at least one class.

theorem TauCeti.IntegralLattice.mem_genusClasses_iff {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {c : IsometryQuotient V} : c ∈ L.genusClasses ↔ L.SameGenus (Quotient.out c)

A class lies in the genus of L exactly when its chosen representative has the same genus as L.

theorem TauCeti.IntegralLattice.genusClasses_eq_genusClasses_iff {V : Type u} [AddCommGroup V] [Module ℚ V] {L M : IntegralLattice V} : L.genusClasses = M.genusClasses ↔ L.SameGenus M

Two lattices in V have the same classes in their genus exactly when they have the same genus.

theorem TauCeti.IntegralLattice.SameGenus.genusClasses_eq {V : Type u} [AddCommGroup V] [Module ℚ V] {L M : IntegralLattice V} (h : L.SameGenus M) : L.genusClasses = M.genusClasses

Lattices of the same genus have the same classes in their genus.

theorem TauCeti.IntegralLattice.isometryQuotientEquiv_mem_genusClasses_iff {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (f : V ≃ₗ[ℚ] W) {L : IntegralLattice V} {L' : IntegralLattice W} (h : L.SameGenus L') (c : IsometryQuotient V) : (isometryQuotientEquiv f) c ∈ L'.genusClasses ↔ c ∈ L.genusClasses

Transport along f : V ≃ W carries the classes in the genus of L onto the classes in the genus of any lattice in W with the same genus as L.

theorem TauCeti.IntegralLattice.SameGenus.exists_isometry {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (h : L.SameGenus M) : ∃ (N : IntegralLattice V), L.SameGenus N ∧ Nonempty (M.Isometry N)

Every lattice of the same genus as L, in any rational space, is isometric to a lattice in the ambient space of L of that genus. So L.genusClasses accounts for every class in the genus of L.

noncomputable def TauCeti.IntegralLattice.classNumber {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : ℕ

The class number h(L): the number of isometry classes in the genus of L. It is 0 when the genus contains infinitely many classes.

theorem TauCeti.IntegralLattice.classNumber_def {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.classNumber = Nat.card ↑L.genusClasses

The class number is the cardinality of the set of classes in the genus.

theorem TauCeti.IntegralLattice.classNumber_pos_iff {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} : 0 < L.classNumber ↔ L.genusClasses.Finite

The class number is positive exactly when the genus contains finitely many classes.

theorem TauCeti.IntegralLattice.SameGenus.classNumber_eq {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (h : L.SameGenus M) : L.classNumber = M.classNumber

The class number is an invariant of the genus. Lattices of the same genus have the same class number, even when they live in different ambient spaces.

theorem TauCeti.IntegralLattice.Isometry.classNumber_eq {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) : L.classNumber = M.classNumber

Isometric lattices have the same class number.

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

A positive definite genus contains finitely many classes. The lattices of the genus all have the rank and determinant of L, so this is the finiteness of positive definite classes of given rank and bounded determinant.

theorem TauCeti.IntegralLattice.IsPosDef.classNumber_pos {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) : 0 < L.classNumber

A positive definite lattice has positive class number.

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

A negative definite genus contains finitely many classes. Negating the form carries the classes in the genus of L injectively into the classes in the positive definite genus of -L.

theorem TauCeti.IntegralLattice.IsNegDef.classNumber_pos {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsNegDef) : 0 < L.classNumber

A negative definite lattice has positive class number.

theorem TauCeti.IntegralLattice.injective_isometryClass_comp {V : Type u} [AddCommGroup V] [Module ℚ V] {ι : Type u_1} {f : ι → IntegralLattice V} (hf : Pairwise fun (i j : ι) => IsEmpty ((f i).Isometry (f j))) : Function.Injective (isometryClass ∘ f)

Pairwise non-isometric lattices have distinct classes.

theorem TauCeti.IntegralLattice.range_isometryClass_comp_subset {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {ι : Type u_1} {f : ι → IntegralLattice V} (hgen : ∀ (i : ι), L.SameGenus (f i)) : Set.range (isometryClass ∘ f) ⊆ L.genusClasses

The classes of a family of lattices in the genus of L are classes in the genus of L.

theorem TauCeti.IntegralLattice.card_le_classNumber_of_pairwise_isEmpty_isometry {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {ι : Type u_1} {f : ι → IntegralLattice V} (hL : L.genusClasses.Finite) (hgen : ∀ (i : ι), L.SameGenus (f i)) (hf : Pairwise fun (i j : ι) => IsEmpty ((f i).Isometry (f j))) : Nat.card ι ≤ L.classNumber

A genus with finitely many classes contains at most h(L) pairwise non-isometric lattices. The bound concerns families in the ambient space of L; an infinite family has Nat.card ι = 0.

theorem TauCeti.IntegralLattice.card_eq_classNumber_iff_of_pairwise_isEmpty_isometry {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {ι : Type u_1} {f : ι → IntegralLattice V} (hL : L.genusClasses.Finite) (hgen : ∀ (i : ι), L.SameGenus (f i)) (hf : Pairwise fun (i j : ι) => IsEmpty ((f i).Isometry (f j))) : Nat.card ι = L.classNumber ↔ ∀ (M : IntegralLattice V), L.SameGenus M → ∃ (i : ι), Nonempty ((f i).Isometry M)

A family of pairwise non-isometric lattices in a genus with finitely many classes has exactly h(L) members if and only if it represents every class of the genus: every lattice in the ambient space of L with the genus of L is isometric to a member of the family.

theorem TauCeti.IntegralLattice.genusClasses_eq_singleton_of_finrank_le_one {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hle : Module.finrank ℤ ↥L.carrier ≤ 1) : L.genusClasses = {L.isometryClass}

In rank at most one the genus of L is the single class of L.

theorem TauCeti.IntegralLattice.classNumber_eq_one_of_finrank_le_one {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hle : Module.finrank ℤ ↥L.carrier ≤ 1) : L.classNumber = 1

In rank at most one the class number is 1 by the determinant classification TauCeti.IntegralLattice.nonempty_isometry_of_finrank_le_one.