The isometry group of an integral lattice

The self-isometries of an integral lattice L form a group O(L) = Isometry L L under composition, with f * g the isometry g followed by f, as for LinearEquiv.automorphismGroup. Restricting a self-isometry to the carrier is a group homomorphism into the automorphism group of the carrier, and composing with the determinant gives the determinant of a self-isometry, a unit of ℤ, hence ±1. Its kernel is the special isometry group SO(L), a subgroup of index at most two. Negation is a self-isometry of every lattice, the element -1 of O(L), and its determinant is (-1) ^ rank L; so SO(L) is a proper subgroup in odd rank.

Main definitions

• The Group instance on Isometry L L: composition, identity and inversion of self-isometries.
• TauCeti.IntegralLattice.Isometry.carrierEquivHom: restriction to the carrier as a group homomorphism O(L) →* (L ≃ₗ[ℤ] L).
• TauCeti.IntegralLattice.Isometry.det: the determinant O(L) →* ℤˣ.
• TauCeti.IntegralLattice.specialOrthogonalGroup: the subgroup SO(L) of determinant one.
• TauCeti.IntegralLattice.Isometry.neg: negation, the element -1 of O(L).

Main results

• TauCeti.IntegralLattice.Isometry.carrierEquivHom_injective: a self-isometry is determined by its restriction to the carrier.
• TauCeti.IntegralLattice.index_specialOrthogonalGroup_le_two: SO(L) has index at most two.
• TauCeti.IntegralLattice.Isometry.det_neg: the determinant of negation is (-1) ^ rank L.

References

• W. Ebeling, Lattices and Codes, Chapter 1
• J. H. Conway and N. J. A. Sloane, Sphere Packings, Lattices and Groups, Chapter 3, §4

@[instance_reducible]

instance TauCeti.IntegralLattice.Isometry.instGroup {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} : Group (L.Isometry L)

The self-isometries of an integral lattice form a group under composition: f * g is g followed by f, the identity is refl and the inverse is symm, as for LinearEquiv.automorphismGroup.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.IntegralLattice.Isometry.one_def {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} : 1 = refl L

theorem TauCeti.IntegralLattice.Isometry.mul_def {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (f g : L.Isometry L) : f * g = g.trans f

theorem TauCeti.IntegralLattice.Isometry.inv_def {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (f : L.Isometry L) : f⁻¹ = f.symm

@[simp]

theorem TauCeti.IntegralLattice.Isometry.one_apply {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (x : V) : 1 x = x

@[simp]

theorem TauCeti.IntegralLattice.Isometry.mul_apply {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (f g : L.Isometry L) (x : V) : (f * g) x = f (g x)

@[simp]

theorem TauCeti.IntegralLattice.Isometry.inv_apply {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (f : L.Isometry L) (x : V) : f⁻¹ x = f.symm x

def TauCeti.IntegralLattice.Isometry.carrierEquivHom {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.Isometry L →* ↥L.carrier ≃ₗ[ℤ] ↥L.carrier

Restriction of a self-isometry to the carrier, as a group homomorphism from O(L) to the automorphism group of the carrier.

Equations

• TauCeti.IntegralLattice.Isometry.carrierEquivHom L = { toFun := fun (e : L.Isometry L) => e.carrierEquiv, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.IntegralLattice.Isometry.carrierEquivHom_apply {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (e : L.Isometry L) : (carrierEquivHom L) e = e.carrierEquiv

theorem TauCeti.IntegralLattice.Isometry.carrierEquivHom_injective {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : Function.Injective ⇑(carrierEquivHom L)

A self-isometry is determined by its restriction to the carrier.

noncomputable def TauCeti.IntegralLattice.Isometry.det {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.Isometry L →* ℤˣ

The determinant of a self-isometry of an integral lattice: the determinant of its restriction to the carrier, a unit of ℤ.

Equations

• TauCeti.IntegralLattice.Isometry.det L = LinearEquiv.det.comp (TauCeti.IntegralLattice.Isometry.carrierEquivHom L)

theorem TauCeti.IntegralLattice.Isometry.det_apply {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (e : L.Isometry L) : (det L) e = LinearEquiv.det e.carrierEquiv

@[simp]

theorem TauCeti.IntegralLattice.Isometry.coe_det {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (e : L.Isometry L) : ↑((det L) e) = LinearMap.det ↑e.carrierEquiv

theorem TauCeti.IntegralLattice.Isometry.det_eq_one_or_neg_one {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (e : L.Isometry L) : (det L) e = 1 ∨ (det L) e = -1

The determinant of a self-isometry is 1 or -1.

def TauCeti.IntegralLattice.Isometry.neg {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.Isometry L

Negation is a self-isometry of every integral lattice: the element -1 of O(L).

Equations

• TauCeti.IntegralLattice.Isometry.neg L = { toIsometryEquiv := let __LinearEquiv := LinearEquiv.neg ℚ; { toLinearEquiv := __LinearEquiv, map_app' := ⋯ }, map_carrier := ⋯ }

@[simp]

theorem TauCeti.IntegralLattice.Isometry.neg_apply {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x : V) : (neg L) x = -x

@[simp]

theorem TauCeti.IntegralLattice.Isometry.carrierEquiv_neg {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : (neg L).carrierEquiv = LinearEquiv.neg ℤ

Negation restricts to negation of the carrier.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.neg_mul_neg {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : neg L * neg L = 1

Negation is an involution of O(L).

@[simp]

theorem TauCeti.IntegralLattice.Isometry.det_neg {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : (det L) (neg L) = (-1) ^ Module.finrank ℤ ↥L.carrier

The determinant of negation is (-1) ^ rank L.

noncomputable def TauCeti.IntegralLattice.specialOrthogonalGroup {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : Subgroup (L.Isometry L)

The special isometry group SO(L): the subgroup of the isometry group O(L) = Isometry L L of self-isometries of determinant one.

Equations

• L.specialOrthogonalGroup = (TauCeti.IntegralLattice.Isometry.det L).ker

@[simp]

theorem TauCeti.IntegralLattice.mem_specialOrthogonalGroup_iff {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {e : L.Isometry L} : e ∈ L.specialOrthogonalGroup ↔ (Isometry.det L) e = 1

theorem TauCeti.IntegralLattice.index_specialOrthogonalGroup_le_two {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.specialOrthogonalGroup.index ≤ 2

SO(L) has index at most two in O(L), the determinant taking values in ℤˣ = {±1}.

theorem TauCeti.IntegralLattice.neg_mem_specialOrthogonalGroup_iff {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : Isometry.neg L ∈ L.specialOrthogonalGroup ↔ Even (Module.finrank ℤ ↥L.carrier)

Negation lies in SO(L) exactly when the rank of L is even.