Binary norm forms of integral lattices

In a rank-two carrier basis, a lattice with Gram matrix !![A, B; B, C] has binary norm form A x² + 2B x y + C y². Its discriminant is -4 * determinant. Dividing by its content produces a primitive form when the ambient form is nonzero. The content and primitive discriminant are basis-independent, although the polynomial depends on the basis.

The intrinsic nonnegative content binaryContent and the primitive discriminant binaryDiscriminant are characterized by computation in any carrier basis. The content is also the nonnegative generator of the norm ideal. Nondegeneracy gives positive content and nonzero primitive discriminant. The latter is zero or one modulo four, negative for either definite sign, and positive for an indefinite lattice. It is not a square when the rational norm form is anisotropic, since a square discriminant factors the norm form over ℚ. A separate integer twist of the form multiplies its content by the absolute scalar.

References

• D. A. Cox, Primes of the Form x² + ny², Sections 1 and 2.

noncomputable def TauCeti.IntegralLattice.binaryNormForm {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (b : Module.Basis (Fin 2) ℤ ↥L.carrier) : BinaryQuadraticForm ℤ

The integral norm in a rank-two carrier basis, with twice the off-diagonal Gram entry as its middle coefficient.

@[simp]

theorem TauCeti.IntegralLattice.binaryNormForm_a {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (b : Module.Basis (Fin 2) ℤ ↥L.carrier) : (L.binaryNormForm b).a = L.gramMatrix b 0 0

The leading coefficient is the first diagonal Gram entry.

@[simp]

theorem TauCeti.IntegralLattice.binaryNormForm_b {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (b : Module.Basis (Fin 2) ℤ ↥L.carrier) : (L.binaryNormForm b).b = 2 * L.gramMatrix b 0 1

The middle coefficient is twice the off-diagonal Gram entry.

@[simp]

theorem TauCeti.IntegralLattice.binaryNormForm_c {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (b : Module.Basis (Fin 2) ℤ ↥L.carrier) : (L.binaryNormForm b).c = L.gramMatrix b 1 1

The last coefficient is the second diagonal Gram entry.

@[simp]

theorem TauCeti.IntegralLattice.eval_binaryNormForm {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (b : Module.Basis (Fin 2) ℤ ↥L.carrier) (x y : ℤ) : (L.binaryNormForm b).eval x y = L.integralNorm (x • b 0 + y • b 1)

The binary form evaluates to the integral norm of the vector with the given coordinates.

theorem TauCeti.IntegralLattice.norm_eq_binaryNormForm {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (b : Module.Basis (Fin 2) ℤ ↥L.carrier) (z : V) : L.norm z = ↑(L.binaryNormForm b).a * ((Module.Basis.extendOfIsLattice ℚ b).repr z) 0 ^ 2 + ↑(L.binaryNormForm b).b * ((Module.Basis.extendOfIsLattice ℚ b).repr z) 0 * ((Module.Basis.extendOfIsLattice ℚ b).repr z) 1 + ↑(L.binaryNormForm b).c * ((Module.Basis.extendOfIsLattice ℚ b).repr z) 1 ^ 2

The same polynomial computes the rational norm in the extended basis.

@[simp]

theorem TauCeti.IntegralLattice.discrim_binaryNormForm {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (b : Module.Basis (Fin 2) ℤ ↥L.carrier) : (L.binaryNormForm b).discrim = -4 * L.determinant

The discriminant of the norm form is minus four times the lattice determinant.

theorem TauCeti.IntegralLattice.dvd_content_binaryNormForm_iff {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (b : Module.Basis (Fin 2) ℤ ↥L.carrier) (n : ℕ) : n ∣ (L.binaryNormForm b).content ↔ ∀ (z : ↥L.carrier), ↑n ∣ L.integralNorm z

An integer divides the content exactly when it divides every integral norm.

theorem TauCeti.IntegralLattice.content_binaryNormForm_eq {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (b b' : Module.Basis (Fin 2) ℤ ↥L.carrier) : (L.binaryNormForm b).content = (L.binaryNormForm b').content

Changing the carrier basis preserves the content of the norm form.

theorem TauCeti.IntegralLattice.discrim_binaryNormForm_primPart_eq {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (b b' : Module.Basis (Fin 2) ℤ ↥L.carrier) : (L.binaryNormForm b).primPart.discrim = (L.binaryNormForm b').primPart.discrim

The discriminant of the primitive part is independent of the carrier basis.

theorem TauCeti.IntegralLattice.discrim_binaryNormForm_ne_zero {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (b : Module.Basis (Fin 2) ℤ ↥L.carrier) [L.IsNondegenerate] : (L.binaryNormForm b).discrim ≠ 0

A nondegenerate rank-two lattice has a nonzero norm-form discriminant.

@[simp]

theorem TauCeti.IntegralLattice.binaryNormForm_eq_zero_iff {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (b : Module.Basis (Fin 2) ℤ ↥L.carrier) : L.binaryNormForm b = 0 ↔ L.form = 0

The binary norm form vanishes exactly when the ambient lattice form vanishes.

theorem TauCeti.IntegralLattice.binaryNormForm_ne_zero {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (b : Module.Basis (Fin 2) ℤ ↥L.carrier) (hL : L.form ≠ 0) : L.binaryNormForm b ≠ 0

A nonzero ambient form has a nonzero binary norm form, including the degenerate case.

theorem TauCeti.IntegralLattice.content_binaryNormForm_pos {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (b : Module.Basis (Fin 2) ℤ ↥L.carrier) (hL : L.form ≠ 0) : 0 < (L.binaryNormForm b).content

A nonzero ambient form has a binary norm form of positive content.

theorem TauCeti.IntegralLattice.isPrimitive_binaryNormForm_primPart {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (b : Module.Basis (Fin 2) ℤ ↥L.carrier) (hL : L.form ≠ 0) : (L.binaryNormForm b).primPart.IsPrimitive

Dividing the norm form by its content gives a primitive form whenever the ambient form is nonzero.

noncomputable def TauCeti.IntegralLattice.binaryContent {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hV : Module.finrank ℚ V = 2) : ℕ

The basis-independent nonnegative content of a rank-two lattice; it is positive for a nonzero ambient form.

noncomputable def TauCeti.IntegralLattice.binaryDiscriminant {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hV : Module.finrank ℚ V = 2) : ℤ

The basis-independent discriminant of the primitive norm form of a rank-two lattice.

theorem TauCeti.IntegralLattice.binaryContent_eq_content_binaryNormForm {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (b : Module.Basis (Fin 2) ℤ ↥L.carrier) (hV : Module.finrank ℚ V = 2) : L.binaryContent hV = (L.binaryNormForm b).content

The intrinsic content can be computed in any carrier basis.

theorem TauCeti.IntegralLattice.normIdeal_eq_span_binaryContent {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hV : Module.finrank ℚ V = 2) : L.normIdeal = Ideal.span {↑(L.binaryContent hV)}

The content generates the norm ideal. The values B(x, x) of a rank-two lattice generate the ideal of ℤ spanned by its content, so the content is the nonnegative generator of the norm ideal.

theorem TauCeti.IntegralLattice.binaryDiscriminant_eq_discrim_primPart {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (b : Module.Basis (Fin 2) ℤ ↥L.carrier) (hV : Module.finrank ℚ V = 2) : L.binaryDiscriminant hV = (L.binaryNormForm b).primPart.discrim

The intrinsic primitive discriminant can be computed in any carrier basis.

theorem TauCeti.IntegralLattice.binaryContent_sq_mul_binaryDiscriminant {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hV : Module.finrank ℚ V = 2) : ↑(L.binaryContent hV) ^ 2 * L.binaryDiscriminant hV = -4 * L.determinant

The primitive discriminant times the squared content is minus four times the determinant.

theorem TauCeti.IntegralLattice.binaryContent_pos {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hV : Module.finrank ℚ V = 2) (hL : L.form ≠ 0) : 0 < L.binaryContent hV

A rank-two lattice with nonzero ambient form has positive content.

theorem TauCeti.IntegralLattice.binaryDiscriminant_ne_zero {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hV : Module.finrank ℚ V = 2) [L.IsNondegenerate] : L.binaryDiscriminant hV ≠ 0

The primitive discriminant of a nondegenerate rank-two lattice is nonzero.

theorem TauCeti.IntegralLattice.form_ne_zero_of_binaryDiscriminant_ne_zero {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hV : Module.finrank ℚ V = 2) (h : L.binaryDiscriminant hV ≠ 0) : L.form ≠ 0

A rank-two lattice with nonzero primitive discriminant has nonzero form.

theorem TauCeti.IntegralLattice.isNondegenerate_of_binaryDiscriminant_ne_zero {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hV : Module.finrank ℚ V = 2) (h : L.binaryDiscriminant hV ≠ 0) : L.IsNondegenerate

A rank-two lattice with nonzero primitive discriminant is nondegenerate.

theorem TauCeti.IntegralLattice.binaryDiscriminant_emod_four_eq_zero_or_one {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hV : Module.finrank ℚ V = 2) : L.binaryDiscriminant hV % 4 = 0 ∨ L.binaryDiscriminant hV % 4 = 1

An integral primitive discriminant is zero or one modulo four.

@[simp]

theorem TauCeti.IntegralLattice.binaryNormForm_smul {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (b : Module.Basis (Fin 2) ℤ ↥L.carrier) (n : ℤ) : (n • L).binaryNormForm b = n • L.binaryNormForm b

Twisting the lattice form by an integer scales the associated binary form by that integer.

@[simp]

theorem TauCeti.IntegralLattice.binaryContent_smul {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (n : ℤ) (hV : Module.finrank ℚ V = 2) : (n • L).binaryContent hV = n.natAbs * L.binaryContent hV

A form twist multiplies the lattice content by the absolute scalar.

theorem TauCeti.IntegralLattice.binaryDiscriminant_neg_of_isPosDef {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hV : Module.finrank ℚ V = 2) (hL : L.IsPosDef) : L.binaryDiscriminant hV < 0

The primitive discriminant of a positive definite rank-two lattice is negative.

@[simp]

theorem TauCeti.IntegralLattice.binaryDiscriminant_neg {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hV : Module.finrank ℚ V = 2) : (-L).binaryDiscriminant hV = L.binaryDiscriminant hV

Negating the lattice form preserves the primitive discriminant.

theorem TauCeti.IntegralLattice.binaryDiscriminant_neg_of_isNegDef {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hV : Module.finrank ℚ V = 2) (hL : L.IsNegDef) : L.binaryDiscriminant hV < 0

The primitive discriminant of a negative definite rank-two lattice is negative.

theorem TauCeti.IntegralLattice.binaryDiscriminant_pos_of_isIndefinite {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hV : Module.finrank ℚ V = 2) (hL : L.IsIndefinite) : 0 < L.binaryDiscriminant hV

The primitive discriminant of an indefinite rank-two lattice is positive.

theorem TauCeti.IntegralLattice.not_isSquare_binaryDiscriminant_of_anisotropic {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (hV : Module.finrank ℚ V = 2) (hL : QuadraticMap.Anisotropic L.norm) : ¬IsSquare (L.binaryDiscriminant hV)

The primitive discriminant of a rank-two lattice with anisotropic rational norm form is not a square: a square discriminant would let the norm form factor over ℚ and vanish on a nonzero vector.