Proper ideals of primitive binary quadratic forms

The fractional ideal of a primitive integral form of nonsquare discriminant is proper and invertible over the associated quadratic number-field order. Its multiplier ring is the order itself. These invertible ideals define ideal classes in the form-ideal correspondence.

References

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

theorem TauCeti.BinaryQuadraticForm.IsPrimitive.fractionalIdeal_isProper {f : BinaryQuadraticForm ℤ} (hprim : f.IsPrimitive) (D : ℤ) (hf : f.discrim = D) [Fact ¬IsSquare D] : (QuadraticOrder.numberFieldOrder D ⋯).IsProperFractionalIdeal (f.fractionalIdeal D hf)

The ideal of a primitive form is proper in the actual quadratic number-field order.

noncomputable def TauCeti.BinaryQuadraticForm.properFractionalIdeal (f : BinaryQuadraticForm ℤ) (D : ℤ) (hf : f.discrim = D) [Fact ¬IsSquare D] (hprim : f.IsPrimitive) : (QuadraticOrder.numberFieldOrder D ⋯).properFractionalIdeals

The proper fractional ideal associated with a primitive form.

@[simp]

theorem TauCeti.BinaryQuadraticForm.coe_properFractionalIdeal (f : BinaryQuadraticForm ℤ) (D : ℤ) (hf : f.discrim = D) [Fact ¬IsSquare D] (hprim : f.IsPrimitive) : ↑(f.properFractionalIdeal D hf hprim) = f.fractionalIdeal D hf

The raw proper form ideal has the original fractional ideal as its value.

theorem TauCeti.BinaryQuadraticForm.IsPrimitive.fractionalIdeal_isUnit {f : BinaryQuadraticForm ℤ} (hprim : f.IsPrimitive) (D : ℤ) (hf : f.discrim = D) [Fact ¬IsSquare D] : IsUnit (f.fractionalIdeal D hf)

The fractional ideal of a primitive form is invertible.

noncomputable def TauCeti.BinaryQuadraticForm.invertibleFractionalIdeal (f : BinaryQuadraticForm ℤ) (D : ℤ) (hf : f.discrim = D) [Fact ¬IsSquare D] (hprim : f.IsPrimitive) : (QuadraticOrder.numberFieldOrder D ⋯).invertibleProperFractionalIdeals

The invertible fractional ideal associated with a primitive form.

@[simp]

theorem TauCeti.BinaryQuadraticForm.coe_invertibleFractionalIdeal (f : BinaryQuadraticForm ℤ) (D : ℤ) (hf : f.discrim = D) [Fact ¬IsSquare D] (hprim : f.IsPrimitive) : ↑(f.invertibleFractionalIdeal D hf hprim) = f.fractionalIdeal D hf

The invertible form ideal has the original fractional ideal as its value.

theorem TauCeti.BinaryQuadraticForm.invertibleFractionalIdeal_eq_one_of_isUnit_a (f : BinaryQuadraticForm ℤ) (D : ℤ) (hf : f.discrim = D) [Fact ¬IsSquare D] (hprim : f.IsPrimitive) (ha : IsUnit f.a) : f.invertibleFractionalIdeal D hf hprim = 1

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