The ideal attached to an integral binary quadratic form

A form (a, b, c) of discriminant D gives the two-generator order module aℤ + ((-b + √D)/2)ℤ in the rational quadratic algebra. The construction first works as a module over the actual quadratic order in either the field or split case. In the nonsquare case it gives a fractional ideal of the existing number-field order.

References

• D. A. Cox, Primes of the Form x² + ny², §7, Theorem 7.7.

def TauCeti.BinaryQuadraticForm.idealGenerator (f : BinaryQuadraticForm ℤ) (D : ℤ) : QuadraticAlgebra ℚ (↑D) 0

The second ideal generator (-b + √D)/2.

@[simp]

theorem TauCeti.BinaryQuadraticForm.idealGenerator_re (f : BinaryQuadraticForm ℤ) (D : ℤ) : (f.idealGenerator D).re = -↑f.b / 2

The rational coefficient of the second ideal generator.

@[simp]

theorem TauCeti.BinaryQuadraticForm.idealGenerator_im (f : BinaryQuadraticForm ℤ) (D : ℤ) : (f.idealGenerator D).im = 1 / 2

The square-root coefficient of the second ideal generator.

theorem TauCeti.BinaryQuadraticForm.eq_of_idealGenerator_mul_a_eq {g h : BinaryQuadraticForm ℤ} {D : ℤ} (hg : g.discrim = D) (hh : h.discrim = D) (hga : g.a ≠ 0) (heq : g.idealGenerator D * ↑h.a = h.idealGenerator D * ↑g.a) : g = h

A form of discriminant D with nonzero leading coefficient is determined by the quotient of its two ideal generators: if β_g a_h = β_h a_g, then g = h.

theorem TauCeti.BinaryQuadraticForm.generator_eq_idealGenerator_add (f : BinaryQuadraticForm ℤ) (D : ℤ) (hf : f.discrim = D) : QuadraticOrder.generator D = f.idealGenerator D + ((D + f.b) / 2) • 1

A form's second ideal generator differs integrally from the order generator.

theorem TauCeti.BinaryQuadraticForm.idealGenerator_mem_order (f : BinaryQuadraticForm ℤ) (D : ℤ) (hf : f.discrim = D) : f.idealGenerator D ∈ QuadraticOrder.toSubalgebra D ⋯

The second generator belongs to the actual quadratic order.

@[simp]

theorem TauCeti.BinaryQuadraticForm.idealGenerator_mul_self (f : BinaryQuadraticForm ℤ) (D : ℤ) (hf : f.discrim = D) : f.idealGenerator D * f.idealGenerator D = -f.b • f.idealGenerator D - (f.a * f.c) • 1

The quadratic relation of the second ideal generator.

def TauCeti.BinaryQuadraticForm.orderIdeal (f : BinaryQuadraticForm ℤ) (D : ℤ) (hf : f.discrim = D) : Submodule (↥(QuadraticOrder.toSubalgebra D ⋯)) (QuadraticAlgebra ℚ (↑D) 0)

The order module aℤ + ((-b + √D)/2)ℤ, over the actual quadratic order.

@[simp]

theorem TauCeti.BinaryQuadraticForm.coe_orderIdeal (f : BinaryQuadraticForm ℤ) (D : ℤ) (hf : f.discrim = D) : ↑(f.orderIdeal D hf) = ↑(Submodule.span ℤ {↑f.a, f.idealGenerator D})

The order ideal has the defining two-generator lattice as its carrier.

theorem TauCeti.BinaryQuadraticForm.mem_orderIdeal_iff (f : BinaryQuadraticForm ℤ) (D : ℤ) (hf : f.discrim = D) (z : QuadraticAlgebra ℚ (↑D) 0) : z ∈ f.orderIdeal D hf ↔ ∃ (m : ℤ) (n : ℤ), m • ↑f.a + n • f.idealGenerator D = z

Ideal membership is an integral combination of its two generators.

theorem TauCeti.BinaryQuadraticForm.orderIdeal_restrictScalars (f : BinaryQuadraticForm ℤ) (D : ℤ) (hf : f.discrim = D) : Submodule.restrictScalars ℤ (f.orderIdeal D hf) = Submodule.span ℤ {↑f.a, f.idealGenerator D}

Restriction to the integers recovers the defining two-generator lattice.

theorem TauCeti.BinaryQuadraticForm.orderIdeal_le_order (f : BinaryQuadraticForm ℤ) (D : ℤ) (hf : f.discrim = D) : Submodule.restrictScalars ℤ (f.orderIdeal D hf) ≤ Subalgebra.toSubmodule (QuadraticOrder.toSubalgebra D ⋯)

Every member of the form ideal belongs to the order.

noncomputable def TauCeti.BinaryQuadraticForm.fractionalIdeal (f : BinaryQuadraticForm ℤ) (D : ℤ) (hf : f.discrim = D) [Fact ¬IsSquare D] : FractionalIdeal (nonZeroDivisors ↥(QuadraticOrder.numberFieldOrder D ⋯).toSubalgebra) (QuadraticAlgebra ℚ (↑D) 0)

The form ideal as a fractional ideal of the existing quadratic number-field order.

@[simp]

theorem TauCeti.BinaryQuadraticForm.coe_fractionalIdeal (f : BinaryQuadraticForm ℤ) (D : ℤ) (hf : f.discrim = D) [Fact ¬IsSquare D] : ↑(f.fractionalIdeal D hf) = ↑(f.orderIdeal D hf)

The fractional ideal has the same carrier as the order ideal.

theorem TauCeti.BinaryQuadraticForm.fractionalIdeal_restrictScalars (f : BinaryQuadraticForm ℤ) (D : ℤ) (hf : f.discrim = D) [Fact ¬IsSquare D] : Submodule.restrictScalars ℤ ↑(f.fractionalIdeal D hf) = Submodule.restrictScalars ℤ (f.orderIdeal D hf)

Restriction of the fractional ideal to the integers recovers the defining lattice.

@[simp]

theorem TauCeti.BinaryQuadraticForm.a_mem_orderIdeal (f : BinaryQuadraticForm ℤ) (D : ℤ) (hf : f.discrim = D) : ↑f.a ∈ f.orderIdeal D hf

The first ideal generator is a member of the ideal.

@[simp]

theorem TauCeti.BinaryQuadraticForm.idealGenerator_mem_orderIdeal (f : BinaryQuadraticForm ℤ) (D : ℤ) (hf : f.discrim = D) : f.idealGenerator D ∈ f.orderIdeal D hf

The second ideal generator is a member of the ideal.

theorem TauCeti.BinaryQuadraticForm.orderIdeal_ne_bot (f : BinaryQuadraticForm ℤ) (D : ℤ) (hf : f.discrim = D) : f.orderIdeal D hf ≠ ⊥

The form order ideal is nonzero, in both field and split quadratic algebras.

theorem TauCeti.BinaryQuadraticForm.linearIndependent_idealGenerators (f : BinaryQuadraticForm ℤ) (D : ℤ) (ha : f.a ≠ 0) : LinearIndependent ℤ ![↑f.a, f.idealGenerator D]

The two ideal generators are independent if the leading coefficient is nonzero.

noncomputable def TauCeti.BinaryQuadraticForm.idealBasis (f : BinaryQuadraticForm ℤ) (D : ℤ) (hf : f.discrim = D) (ha : f.a ≠ 0) : Module.Basis (Fin 2) ℤ ↥(f.orderIdeal D hf)

The integral basis a, (-b + √D)/2 of the form ideal.

theorem TauCeti.BinaryQuadraticForm.coe_idealBasis_apply (f : BinaryQuadraticForm ℤ) (D : ℤ) (hf : f.discrim = D) (ha : f.a ≠ 0) (i : Fin 2) : ↑((f.idealBasis D hf ha) i) = ![↑f.a, f.idealGenerator D] i

The ideal basis maps to its defining two-generator family in the quadratic algebra.

@[simp]

theorem TauCeti.BinaryQuadraticForm.coe_idealBasis_zero (f : BinaryQuadraticForm ℤ) (D : ℤ) (hf : f.discrim = D) (ha : f.a ≠ 0) : ↑((f.idealBasis D hf ha) 0) = ↑f.a

The first ideal basis vector is the leading coefficient.

@[simp]

theorem TauCeti.BinaryQuadraticForm.coe_idealBasis_one (f : BinaryQuadraticForm ℤ) (D : ℤ) (hf : f.discrim = D) (ha : f.a ≠ 0) : ↑((f.idealBasis D hf ha) 1) = f.idealGenerator D

The second ideal basis vector is (-b + √D)/2.

theorem TauCeti.BinaryQuadraticForm.mem_fractionalIdeal_iff (f : BinaryQuadraticForm ℤ) (D : ℤ) (hf : f.discrim = D) [Fact ¬IsSquare D] (z : QuadraticAlgebra ℚ (↑D) 0) : z ∈ f.fractionalIdeal D hf ↔ ∃ (m : ℤ) (n : ℤ), m • ↑f.a + n • f.idealGenerator D = z

Fractional-ideal membership is the same integral two-generator formula.

@[simp]

theorem TauCeti.BinaryQuadraticForm.a_mem_fractionalIdeal (f : BinaryQuadraticForm ℤ) (D : ℤ) (hf : f.discrim = D) [Fact ¬IsSquare D] : ↑f.a ∈ f.fractionalIdeal D hf

The leading coefficient belongs to the fractional form ideal.

@[simp]

theorem TauCeti.BinaryQuadraticForm.idealGenerator_mem_fractionalIdeal (f : BinaryQuadraticForm ℤ) (D : ℤ) (hf : f.discrim = D) [Fact ¬IsSquare D] : f.idealGenerator D ∈ f.fractionalIdeal D hf

The second generator belongs to the fractional form ideal.

theorem TauCeti.BinaryQuadraticForm.fractionalIdeal_le_one (f : BinaryQuadraticForm ℤ) (D : ℤ) (hf : f.discrim = D) [Fact ¬IsSquare D] : f.fractionalIdeal D hf ≤ 1

The fractional ideal is integral, hence contained in the unit fractional ideal.

theorem TauCeti.BinaryQuadraticForm.fractionalIdeal_eq_one_of_isUnit_a (f : BinaryQuadraticForm ℤ) (D : ℤ) (hf : f.discrim = D) [Fact ¬IsSquare D] (ha : IsUnit f.a) : f.fractionalIdeal D hf = 1

A form whose leading coefficient is a unit has the unit ideal.

theorem TauCeti.BinaryQuadraticForm.fractionalIdeal_le_iff (f : BinaryQuadraticForm ℤ) (D : ℤ) (hf : f.discrim = D) [Fact ¬IsSquare D] {J : FractionalIdeal (nonZeroDivisors ↥(QuadraticOrder.numberFieldOrder D ⋯).toSubalgebra) (QuadraticAlgebra ℚ (↑D) 0)} : f.fractionalIdeal D hf ≤ J ↔ ↑f.a ∈ J ∧ f.idealGenerator D ∈ J

A fractional ideal contains the form ideal exactly when it contains both generators.

theorem TauCeti.BinaryQuadraticForm.fractionalIdeal_mul_fractionalIdeal_le_iff (f g : BinaryQuadraticForm ℤ) (D : ℤ) (hf : f.discrim = D) (hg : g.discrim = D) [Fact ¬IsSquare D] {J : FractionalIdeal (nonZeroDivisors ↥(QuadraticOrder.numberFieldOrder D ⋯).toSubalgebra) (QuadraticAlgebra ℚ (↑D) 0)} : f.fractionalIdeal D hf * g.fractionalIdeal D hg ≤ J ↔ ↑f.a * ↑g.a ∈ J ∧ ↑f.a * g.idealGenerator D ∈ J ∧ f.idealGenerator D * ↑g.a ∈ J ∧ f.idealGenerator D * g.idealGenerator D ∈ J

A fractional ideal contains the product of two form ideals of the same discriminant exactly when it contains the four products of their generators.

theorem TauCeti.BinaryQuadraticForm.fractionalIdeal_ne_zero (f : BinaryQuadraticForm ℤ) (D : ℤ) (hf : f.discrim = D) [Fact ¬IsSquare D] : f.fractionalIdeal D hf ≠ 0

The form ideal is nonzero.

theorem TauCeti.BinaryQuadraticForm.norm_idealGenerators (f : BinaryQuadraticForm ℤ) (D : ℤ) (hf : f.discrim = D) (m n : ℤ) : QuadraticAlgebra.norm (m • ↑f.a + n • f.idealGenerator D) = ↑f.a * ↑(f.eval m (-n))

Norm on the ideal generators recovers the original form, with the second coordinate negated.