Documentation

TauCeti.NumberTheory.IntegralLattice.Binary.Orientation

Oriented proper classes of binary lattices #

The basis matrix of an oriented integral change has determinant one. Its inverse acts on the binary norm form through the existing left SL₂(ℤ) action. Primitive normalization commutes with that action, so the proper class binaryProperClass depends only on the lattice and its fixed orientation. The characteristic lemma computes it using any carrier basis of that orientation.

Reversing the second basis vector realizes the determinant-minus-one substitution (x, y) ↦ (x, -y). It negates the middle coefficient of both the norm form and its primitive part. A basis with the opposite orientation gives a properly equivalent representative of that reflected form.

References #

source
theorem TauCeti.IntegralLattice.binaryNormForm_eq_inv_smul {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (b b' : Module.Basis (Fin 2) ℤ ↥L.carrier) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (h : b.toMatrix ⇑b' = ↑γ) :
L.binaryNormForm b' = γ⁻¹ • L.binaryNormForm b

A determinant-one basis matrix acts on the norm form through the inverse, matching the existing left action.

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

Every form properly equivalent to a norm form of L is again a norm form of L: for each γ : SL(2, ℤ) some carrier basis has norm form γ • L.binaryNormForm b.

source
theorem TauCeti.IntegralLattice.exists_binaryNormForm_eq_smul_of_orientation_eq {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (b b' : Module.Basis (Fin 2) ℤ ↥L.carrier) (h : b.orientation = b'.orientation) :
∃ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ), L.binaryNormForm b' = γ • L.binaryNormForm b

Bases with the same orientation give properly equivalent norm forms.

source
theorem TauCeti.IntegralLattice.exists_primPart_eq_smul_of_orientation_eq {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (b b' : Module.Basis (Fin 2) ℤ ↥L.carrier) (h : b.orientation = b'.orientation) :
∃ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ), (L.binaryNormForm b').primPart = γ • (L.binaryNormForm b).primPart

Primitive parts in equally oriented bases are properly equivalent.

source
theorem TauCeti.IntegralLattice.binaryProperClass_eq_of_orientation_eq {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (b b' : Module.Basis (Fin 2) ℤ ↥L.carrier) (h : b.orientation = b'.orientation) :
Quotient.mk'' (L.binaryNormForm b').primPart = Quotient.mk'' (L.binaryNormForm b).primPart

Equally oriented bases give the same proper class of the primitive norm form.

source
noncomputable def TauCeti.IntegralLattice.binaryProperClass {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hV : Module.finrank ℚ V = 2) (o : Orientation ℤ (↥L.carrier) (Fin 2)) :
MulAction.orbitRel.Quotient (Matrix.SpecialLinearGroup (Fin 2) ℤ) (BinaryQuadraticForm ℤ)

The proper class of the primitive norm form for a rank-two lattice with a fixed orientation.

Instances For
    source
    theorem TauCeti.IntegralLattice.binaryProperClass_eq_mk {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (b : Module.Basis (Fin 2) ℤ ↥L.carrier) (hV : Module.finrank ℚ V = 2) (o : Orientation ℤ (↥L.carrier) (Fin 2)) (hb : b.orientation = o) :
    L.binaryProperClass hV o = Quotient.mk'' (L.binaryNormForm b).primPart

    Any carrier basis giving the chosen orientation represents the intrinsic proper class.

    source
    @[simp]
    theorem TauCeti.IntegralLattice.binaryNormForm_unitsSMul_neg {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (b : Module.Basis (Fin 2) ℤ ↥L.carrier) :
    L.binaryNormForm (b.unitsSMul (Function.update 1 1 (-1))) = (L.binaryNormForm b).reflected

    Reversing the second basis vector negates precisely the middle coefficient of the norm form.

    source
    @[simp]
    theorem TauCeti.IntegralLattice.primPart_binaryNormForm_unitsSMul_neg {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (b : Module.Basis (Fin 2) ℤ ↥L.carrier) :
    (L.binaryNormForm (b.unitsSMul (Function.update 1 1 (-1)))).primPart = (L.binaryNormForm b).primPart.reflected

    Reversing the second basis vector also negates precisely the primitive middle coefficient.

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

    Changing orientation gives a form properly equivalent to the reflection of the original primitive form. The reflection is the determinant-minus-one substitution (x, y) ↦ (x, -y).