Documentation

TauCeti.NumberTheory.IntegralLattice.Binary.Isometry

Binary isometries and reflected proper classes #

An improper automorphism of an integral binary lattice exists exactly when its primitive norm form is properly equivalent to its reflection (a, -b, c). Consequently the special orthogonal group has index two exactly in this case, and otherwise has index one.

The comparison uses the actual lattice isometry group and the existing proper action on binary forms. It does not require an ideal-class correspondence.

Writing a proper isometry as its matrix in a carrier basis identifies the special orthogonal group with the stabilizer in SL(2, ℤ) of the binary norm form, that is, with its proper automorphs (specialOrthogonalGroupEquivStabilizer).

References #

source
theorem TauCeti.IntegralLattice.binaryNormForm_map_isometry {V : Type u_1} [AddCommGroup V] [Module ℚ V] {W : Type u_2} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} (b : Module.Basis (Fin 2) ℤ ↥L.carrier) {M : IntegralLattice W} (e : L.Isometry M) :
M.binaryNormForm ((e.carrierBasisEquiv (Fin 2)) b) = L.binaryNormForm b

Transporting a carrier basis between lattices by an isometry preserves its norm form.

source
theorem TauCeti.IntegralLattice.exists_isometry_map_basis_iff {V : Type u_1} [AddCommGroup V] [Module ℚ V] {W : Type u_2} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} (b : Module.Basis (Fin 2) ℤ ↥L.carrier) {M : IntegralLattice W} (b' : Module.Basis (Fin 2) ℤ ↥M.carrier) :
(∃ (e : L.Isometry M), (e.carrierBasisEquiv (Fin 2)) b = b') ↔ M.binaryNormForm b' = L.binaryNormForm b

Equal binary norm forms in two carrier bases determine a lattice isometry taking the first basis to the second.

source
theorem TauCeti.IntegralLattice.exists_improper_isometry_iff {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (b : Module.Basis (Fin 2) ℤ ↥L.carrier) :
(∃ (e : L.Isometry L), (Isometry.det L) e = -1) ↔ ∃ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ), (L.binaryNormForm b).primPart = γ • (L.binaryNormForm b).primPart.reflected

An improper lattice automorphism exists exactly when the primitive norm form is properly equivalent to its reflection.

source
theorem TauCeti.IntegralLattice.index_specialOrthogonalGroup_eq_two_iff_reflected {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (b : Module.Basis (Fin 2) ℤ ↥L.carrier) :
L.specialOrthogonalGroup.index = 2 ↔ ∃ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ), (L.binaryNormForm b).primPart = γ • (L.binaryNormForm b).primPart.reflected

The special orthogonal group has index two exactly when the primitive binary norm form is properly equivalent to its reflection.

source
noncomputable def TauCeti.IntegralLattice.specialOrthogonalGroupEquivStabilizer {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (b : Module.Basis (Fin 2) ℤ ↥L.carrier) :
↥L.specialOrthogonalGroup ≃* ↥(MulAction.stabilizer (Matrix.SpecialLinearGroup (Fin 2) ℤ) (L.binaryNormForm b))

Proper isometries are proper automorphs. In a carrier basis b of a rank-two lattice, the matrix of a proper isometry is an element of SL(2, ℤ) fixing the binary norm form, and every such automorph arises from exactly one proper isometry.

Instances For
    source
    @[simp]
    theorem TauCeti.IntegralLattice.coe_specialOrthogonalGroupEquivStabilizer_apply {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (b : Module.Basis (Fin 2) ℤ ↥L.carrier) (g : ↥L.specialOrthogonalGroup) :
    ↑↑((specialOrthogonalGroupEquivStabilizer b) g) = (LinearMap.toMatrix b b) ↑(↑g).carrierEquiv

    The automorph attached to a proper isometry is its matrix in the carrier basis.

    source
    @[simp]
    theorem TauCeti.IntegralLattice.toMatrix_specialOrthogonalGroupEquivStabilizer_symm_apply {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (b : Module.Basis (Fin 2) ℤ ↥L.carrier) (γ : ↥(MulAction.stabilizer (Matrix.SpecialLinearGroup (Fin 2) ℤ) (L.binaryNormForm b))) :
    (LinearMap.toMatrix b b) ↑(↑((specialOrthogonalGroupEquivStabilizer b).symm γ)).carrierEquiv = ↑↑γ

    The proper isometry attached to an automorph of the norm form has that automorph as its matrix in the carrier basis.