Isometry classes of integral lattices

The isometry classes of integral lattices in a rational vector space V form the quotient IsometryQuotient V of IntegralLattice V by isometry. Transport along a rational linear equivalence V ≃ W identifies the isometry classes in V with those in W.

Main definitions

• TauCeti.IntegralLattice.isometrySetoid: isometry of integral lattices in V.
• TauCeti.IntegralLattice.IsometryQuotient: the isometry classes of integral lattices in V.
• TauCeti.IntegralLattice.isometryClass: the class cls L of a lattice.
• TauCeti.IntegralLattice.isometryQuotientEquiv: transport of classes along an ambient linear equivalence.

References

• O. T. O'Meara, Introduction to Quadratic Forms, §102A, for classes of lattices.

def TauCeti.IntegralLattice.isometrySetoid (V : Type u) [AddCommGroup V] [Module ℚ V] : Setoid (IntegralLattice V)

Isometry of integral lattices in a fixed rational space, as an equivalence relation.

theorem TauCeti.IntegralLattice.isometrySetoid_apply {V : Type u} [AddCommGroup V] [Module ℚ V] {L M : IntegralLattice V} : (isometrySetoid V) L M ↔ Nonempty (L.Isometry M)

Two lattices are related by isometrySetoid exactly when they are isometric.

@[reducible, inline]

abbrev TauCeti.IntegralLattice.IsometryQuotient (V : Type u) [AddCommGroup V] [Module ℚ V] : Type u

The isometry classes of integral lattices in a rational space V.

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

The isometry class cls L of an integral lattice.

@[simp]

theorem TauCeti.IntegralLattice.isometryClass_eq_isometryClass_iff {V : Type u} [AddCommGroup V] [Module ℚ V] {L M : IntegralLattice V} : L.isometryClass = M.isometryClass ↔ Nonempty (L.Isometry M)

Two lattices have the same isometry class exactly when they are isometric.

theorem TauCeti.IntegralLattice.Isometry.isometryClass_eq {V : Type u} [AddCommGroup V] [Module ℚ V] {L M : IntegralLattice V} (e : L.Isometry M) : L.isometryClass = M.isometryClass

Isometric lattices have the same isometry class.

theorem TauCeti.IntegralLattice.isometryClass_surjective {V : Type u} [AddCommGroup V] [Module ℚ V] : Function.Surjective isometryClass

Every isometry class is the class of a lattice.

@[simp]

theorem TauCeti.IntegralLattice.isometryClass_out {V : Type u} [AddCommGroup V] [Module ℚ V] (c : IsometryQuotient V) : (Quotient.out c).isometryClass = c

A chosen representative of an isometry class has that class.

theorem TauCeti.IntegralLattice.IsometryQuotient.eq_of_isometry_out {V : Type u} [AddCommGroup V] [Module ℚ V] {c d : IsometryQuotient V} (e : (Quotient.out c).Isometry (Quotient.out d)) : c = d

An isometry between the chosen representatives of two isometry classes shows that the classes are equal.

noncomputable def TauCeti.IntegralLattice.isometryQuotientEquiv {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (f : V ≃ₗ[ℚ] W) : IsometryQuotient V ≃ IsometryQuotient W

Transport along a rational linear equivalence V ≃ W identifies the isometry classes of integral lattices in V with those in W.

@[simp]

theorem TauCeti.IntegralLattice.isometryQuotientEquiv_isometryClass {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (f : V ≃ₗ[ℚ] W) (M : IntegralLattice V) : (isometryQuotientEquiv f) M.isometryClass = (M.transport f).isometryClass

isometryQuotientEquiv f sends the class of M to the class of its transport along f.

@[simp]

theorem TauCeti.IntegralLattice.isometryQuotientEquiv_symm_isometryClass {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (f : V ≃ₗ[ℚ] W) (M : IntegralLattice W) : (isometryQuotientEquiv f).symm M.isometryClass = (M.transport f.symm).isometryClass

The inverse of isometryQuotientEquiv f sends the class of M to the class of its transport along f.symm.

theorem TauCeti.IntegralLattice.IsometryQuotient.nonempty_isometry_transport_out {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (c : IsometryQuotient V) (f : V ≃ₗ[ℚ] W) : Nonempty (((Quotient.out c).transport f).Isometry (Quotient.out ((isometryQuotientEquiv f) c)))

The transport along f of the representative of a class is isometric to the representative of the transported class.