Form ideals under proper changes of variables

For the left action γ • f = f ∘ γ⁻¹, write γ = !![p,q;r,s] and β = (-b + √D)/2. The transformed ideal is the original ideal multiplied by star (a s + r β) / a. This factor has norm a'/a, where a' is the transformed leading coefficient. The two basis-vector identities require a nonzero original leading coefficient and also cover square discriminants and a zero transformed leading coefficient. The norm formula holds even when the original leading coefficient is zero, when both sides vanish. Positivity of the norm is equivalent to positivity of a * a', the comparison needed for the oriented narrow class. The canonical norm statements use QuadraticAlgebra.norm; the existing algebra-norm bridge also simplifies Algebra.norm expressions. The factor is nonzero whenever the original leading coefficient is nonzero, at any quadratic parameter. The native fractional-ideal statements use the nonsquare hypothesis.

Conversely, a positive-norm homothety between the fractional ideals of positive-leading forms gives a proper equivalence, for either sign of nonsquare discriminant (exists_smul_eq_of_fractionalIdeal_eq_of_norm_pos). The orientation of their two ideal bases determines the sign of the integral change-of-basis determinant, independently of any Picard-class construction.

References

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

def TauCeti.BinaryQuadraticForm.idealChangeFactor (f : BinaryQuadraticForm ℤ) (D : ℤ) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : QuadraticAlgebra ℚ (↑D) 0

The ideal-scaling factor for the left proper-equivalence action, defined using the rational inverse of the leading coefficient at any discriminant.

@[simp]

theorem TauCeti.BinaryQuadraticForm.idealChangeFactor_mul_first (f : BinaryQuadraticForm ℤ) (D : ℤ) (hf : f.discrim = D) (ha : f.a ≠ 0) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : f.idealChangeFactor D γ * (↑(↑γ 1 1) * ↑f.a + ↑(↑γ 1 0) * f.idealGenerator D) = ↑(γ • f).a

Scaling the first changed basis vector gives the new leading coefficient.

@[simp]

theorem TauCeti.BinaryQuadraticForm.idealChangeFactor_mul_second (f : BinaryQuadraticForm ℤ) (D : ℤ) (hf : f.discrim = D) (ha : f.a ≠ 0) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : f.idealChangeFactor D γ * (↑(↑γ 0 1) * ↑f.a + ↑(↑γ 0 0) * f.idealGenerator D) = (γ • f).idealGenerator D

Scaling the second changed basis vector gives the new second ideal generator.

@[simp]

theorem TauCeti.BinaryQuadraticForm.norm_idealChangeFactor (f : BinaryQuadraticForm ℤ) (D : ℤ) (hf : f.discrim = D) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : QuadraticAlgebra.norm (f.idealChangeFactor D γ) = ↑(γ • f).a / ↑f.a

The scaling factor has norm equal to the ratio of leading coefficients, including a zero original leading coefficient, when both sides vanish.

theorem TauCeti.BinaryQuadraticForm.norm_idealChangeFactor_pos_iff (f : BinaryQuadraticForm ℤ) (D : ℤ) (hf : f.discrim = D) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : 0 < QuadraticAlgebra.norm (f.idealChangeFactor D γ) ↔ 0 < f.a * (γ • f).a

The change factor has positive norm exactly when the old and new leading coefficients have positive product.

theorem TauCeti.BinaryQuadraticForm.idealChangeFactor_ne_zero (f : BinaryQuadraticForm ℤ) (D : ℤ) (ha : f.a ≠ 0) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : f.idealChangeFactor D γ ≠ 0

The change factor is nonzero when the original leading coefficient is nonzero, for every quadratic parameter.

theorem TauCeti.BinaryQuadraticForm.fractionalIdeal_smul (f : BinaryQuadraticForm ℤ) (D : ℤ) (hf : f.discrim = D) [Fact ¬IsSquare D] (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : (γ • f).fractionalIdeal D ⋯ = (FractionalIdeal.spanSingleton (nonZeroDivisors ↥(QuadraticOrder.numberFieldOrder D ⋯).toSubalgebra)) (f.idealChangeFactor D γ) * f.fractionalIdeal D hf

Properly equivalent forms have fractional ideals differing by the explicit principal factor.

theorem TauCeti.BinaryQuadraticForm.invertibleFractionalIdeal_smul (f : BinaryQuadraticForm ℤ) (D : ℤ) [Fact ¬IsSquare D] (hf : f.discrim = D) (hprim : f.IsPrimitive) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : (γ • f).invertibleFractionalIdeal D ⋯ ⋯ = (toPrincipalIdeal (↥(QuadraticOrder.numberFieldOrder D ⋯).toSubalgebra) (QuadraticAlgebra ℚ (↑D) 0)) (Units.mk0 (f.idealChangeFactor D γ) ⋯) * f.invertibleFractionalIdeal D hf hprim

The native invertible form ideals differ by the explicit proper-change principal factor.

The orientation of a pair of ideal elements

theorem TauCeti.BinaryQuadraticForm.exists_smul_eq_of_fractionalIdeal_eq_of_norm_pos (f g : BinaryQuadraticForm ℤ) (D : ℤ) [Fact ¬IsSquare D] (hfD : f.discrim = D) (hgD : g.discrim = D) (hfa : 0 < f.a) (hga : 0 < g.a) (μ : QuadraticAlgebra ℚ (↑D) 0) (hμ : 0 < (Algebra.norm ℚ) μ) (hI : g.fractionalIdeal D hgD = (FractionalIdeal.spanSingleton (nonZeroDivisors ↥(QuadraticOrder.numberFieldOrder D ⋯).toSubalgebra)) μ * f.fractionalIdeal D hfD) : ∃ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ), γ • f = g

Positive-leading forms with homothetic ideals are properly equivalent when the scaling factor has positive norm. This applies to either sign of nonsquare discriminant.