Picard classes of primitive binary quadratic forms

A primitive integral form f = (a, b, c) of nonsquare discriminant D has the invertible fractional ideal aℤ + ((-b + √D)/2)ℤ of the quadratic order O_D of discriminant D (TauCeti.BinaryQuadraticForm.invertibleFractionalIdeal). Its class in the Picard group Pic(O_D) is TauCeti.BinaryQuadraticForm.picClass. Properly equivalent forms have ideals differing by an explicit principal factor (invertibleFractionalIdeal_smul), so the class is constant on proper equivalence classes.

For negative D the converse holds on positive definite forms: two primitive forms with positive leading coefficients and the same Picard class are properly equivalent. Nonzero norms are positive, so exists_smul_eq_of_fractionalIdeal_eq_of_norm_pos turns equal Picard classes into proper equivalence. The general norm-positive comparison is proved in Ideal.Change.

Consequently the proper equivalence classes of primitive positive definite forms of discriminant -n inject into Pic(O_{-n}) (posDefProperClassToPic_injective). This is the injective half of the form-ideal correspondence of Cox, Theorem 7.7.

Main definitions and results

• TauCeti.BinaryQuadraticForm.picClass: the Picard class of a primitive form.
• TauCeti.BinaryQuadraticForm.picClass_smul: it is invariant under proper equivalence.
• TauCeti.BinaryQuadraticForm.picClass_eq_picClass_iff_of_neg: for D < 0 and positive leading coefficients, equal Picard classes are exactly proper equivalence.
• TauCeti.BinaryQuadraticForm.posDefProperClassToPic: the induced map on proper classes of primitive positive definite forms, and posDefProperClassToPic_injective.

References

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

noncomputable def TauCeti.BinaryQuadraticForm.picClass (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) [Fact ¬IsSquare D] (f : ↥(primitiveForms D)) : GlobalNumberFields.Pic (QuadraticOrder.numberFieldOrder D hD)

The Picard class of a primitive form. For a primitive form (a, b, c) of nonsquare discriminant D, the class of the invertible ideal aℤ + ((-b + √D)/2)ℤ in the Picard group of the quadratic order of discriminant D.

theorem TauCeti.BinaryQuadraticForm.picClass_def (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) [Fact ¬IsSquare D] (f : ↥(primitiveForms D)) : picClass D hD f = (QuadraticOrder.numberFieldOrder D hD).mkPic ((↑f).invertibleFractionalIdeal D ⋯ ⋯)

The Picard class of a primitive form is the class of its invertible form ideal.

theorem TauCeti.BinaryQuadraticForm.picClass_eq_one_of_isUnit_a (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) [Fact ¬IsSquare D] {f : ↥(primitiveForms D)} (ha : IsUnit (↑f).a) : picClass D hD f = 1

A form whose leading coefficient is a unit has trivial Picard class.

@[simp]

theorem TauCeti.BinaryQuadraticForm.picClass_smul (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) [Fact ¬IsSquare D] (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (f : ↥(primitiveForms D)) : picClass D hD (γ • f) = picClass D hD f

Properly equivalent forms have the same Picard class.

theorem TauCeti.BinaryQuadraticForm.picClass_eq_picClass_iff_of_neg (D : ℤ) (hD : D % 4 = 0 ∨ D % 4 = 1) [Fact ¬IsSquare D] (hneg : D < 0) {f g : ↥(primitiveForms D)} (hf : 0 < (↑f).a) (hg : 0 < (↑g).a) : picClass D hD f = picClass D hD g ↔ ∃ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ), γ • f = g

Equal Picard classes of positive definite forms. For negative D, two primitive forms of discriminant D with positive leading coefficients have the same Picard class exactly when they are properly equivalent.

noncomputable def TauCeti.BinaryQuadraticForm.posDefProperClassToPic (n : ℕ) [NeZero n] (hn : -↑n % 4 = 0 ∨ -↑n % 4 = 1) : PosDefProperClass n → GlobalNumberFields.Pic (QuadraticOrder.numberFieldOrder (-↑n) hn)

The Picard class of a proper class of primitive positive definite forms, the class of aℤ + ((-b + √(-n))/2)ℤ in the Picard group of the quadratic order of discriminant -n.

@[simp]

theorem TauCeti.BinaryQuadraticForm.posDefProperClassToPic_mk (n : ℕ) [NeZero n] (hn : -↑n % 4 = 0 ∨ -↑n % 4 = 1) (f : ↥(posDef n ⊓ primitiveForms (-↑n))) : posDefProperClassToPic n hn ⟦f⟧ = picClass (-↑n) hn ⟨↑f, ⋯⟩

The Picard class of the proper class of a form is the Picard class of the form.

theorem TauCeti.BinaryQuadraticForm.posDefProperClassToPic_injective (n : ℕ) [NeZero n] (hn : -↑n % 4 = 0 ∨ -↑n % 4 = 1) : Function.Injective (posDefProperClassToPic n hn)

Distinct proper classes of primitive positive definite forms have distinct Picard classes. This is the injective half of the correspondence between proper classes of primitive positive definite forms of discriminant -n and the Picard group of the order of discriminant -n.