def Elliptic_Curves.IsImagQuadDiscriminant (D : ℤ) : Prop

An integer D is the discriminant of an imaginary quadratic order if it is negative and congruent to 0 or 1 modulo 4.

noncomputable def Elliptic_Curves.IdealClassGroup' (D : ℤ) : IsImagQuadDiscriminant D → Type

The ideal class group of the imaginary quadratic order of discriminant D, abstractly defined as a type (concrete construction left unspecified).

@[implicit_reducible]

noncomputable instance Elliptic_Curves.IdealClassGroup'.instCommGroup (D : ℤ) (hD : IsImagQuadDiscriminant D) : CommGroup (IdealClassGroup' D hD)

The ideal class group IdealClassGroup' D hD is a commutative group.

@[implicit_reducible]

noncomputable instance Elliptic_Curves.IdealClassGroup'.instFintype (D : ℤ) (hD : IsImagQuadDiscriminant D) : Fintype (IdealClassGroup' D hD)

The ideal class group IdealClassGroup' D hD is finite (so admits a Fintype structure), reflecting the classical finiteness of class number.

noncomputable def Elliptic_Curves.classNumber (D : ℤ) (hD : IsImagQuadDiscriminant D) : ℕ

The class number h(D) of the imaginary quadratic order of discriminant D, defined as the cardinality of its ideal class group.

theorem Elliptic_Curves.classNumber_pos (D : ℤ) (hD : IsImagQuadDiscriminant D) : 0 < classNumber D hD

The class number of an imaginary quadratic discriminant is positive.

structure Elliptic_Curves.RingClassField (D : ℤ) (hD : IsImagQuadDiscriminant D) : Type (max (u_1 + 1) (u_2 + 1))

A bundle of data witnessing the existence of the ring class field of discriminant D: the imaginary quadratic field K = ℚ(√D), an abelian extension K_D / K whose degree equals the class number, and the requisite algebra/number field/Galois structures.

• K : Type u_1
• K_D : Type u_2
• instFieldK : Field self.K
• instFieldKD : Field self.K_D
• instAlgebraQK : Algebra ℚ self.K
• instNumberFieldK : NumberField self.K
• instAlgebraKKD : Algebra self.K self.K_D
• instAlgebraQKD : Algebra ℚ self.K_D
• instIsScalarTower : IsScalarTower ℚ self.K self.K_D
• instNumberFieldKD : NumberField self.K_D
• instFiniteDimKKD : FiniteDimensional self.K self.K_D
• instIsGalois : IsGalois self.K self.K_D
• finrankK : Module.finrank ℚ self.K = 2
• degree_eq_classNumber : Module.finrank self.K self.K_D = classNumber D hD
• galoisGroupComm (σ τ : Gal(self.K_D/self.K)) : σ.trans τ = τ.trans σ

theorem Elliptic_Curves.RingClassField.nonempty (D : ℤ) (hD : IsImagQuadDiscriminant D) : Nonempty (RingClassField D hD)

The ring class field of an imaginary quadratic discriminant exists.

def Elliptic_Curves.NormEquation (D : ℤ) (p : ℕ) (t v : ℤ) : Prop

The Cornacchia-type norm equation 4p = t^2 - v^2 D with t, v integers, underlying Theorem 21.5(iv).

def Elliptic_Curves.SatisfiesNormEquation (D : ℤ) (p : ℕ) : Prop

The prime p satisfies the Cornacchia norm equation for discriminant D if there exist integers t, v with 4p = t^2 - v^2 D and p ∤ t.

noncomputable def Elliptic_Curves.hilbertClassPolynomialZ (D : ℤ) : Polynomial ℤ

The Hilbert class polynomial H_D(X) of discriminant D realized over ℤ (1 outside the imaginary quadratic discriminant range).

def Elliptic_Curves.IsNormOfPrincipalIdeal (D : ℤ) (p : ℕ) : Prop

p is the norm of a principal ideal in the order of discriminant D iff there exist integers t, v with 4p = t^2 - v^2 D and 2 ∣ t - vD. This is condition (i) in Theorem 21.5 of Sutherland.

def Elliptic_Curves.LegendreOneAndHDSplits (D : ℤ) (p : ℕ) : Prop

Condition (ii) of Theorem 21.5: the Legendre symbol (D/p) = 1 and the Hilbert class polynomial H_D splits into linear factors over 𝔽_p.

def Elliptic_Curves.SplitsCompletelyInRCF (D : ℤ) (p : ℕ) : Prop

Condition (iii) of Theorem 21.5: p splits completely in the ring class field of discriminant D, expressed as: there is a number field L over which H_D splits and all maximal ideals above p have absolute norm p.

theorem Elliptic_Curves.theorem_21_5_i_iff_ii (D : ℤ) (p : ℕ) (hD : IsImagQuadDiscriminant D) (hp : Nat.Prime p) (hp_odd : p ≠ 2) (hp_ndvd : ¬↑p ∣ D) : IsNormOfPrincipalIdeal D p ↔ LegendreOneAndHDSplits D p

Theorem 21.5, equivalence (i) ↔ (ii) of Sutherland: for p ∤ D odd prime, p is the norm of a principal 𝒪-ideal iff (D/p) = 1 and H_D(X) splits over 𝔽_p.

theorem Elliptic_Curves.theorem_21_5_ii_iff_iii (D : ℤ) (p : ℕ) (hD : IsImagQuadDiscriminant D) (hp : Nat.Prime p) (hp_odd : p ≠ 2) (hp_ndvd : ¬↑p ∣ D) : LegendreOneAndHDSplits D p ↔ SplitsCompletelyInRCF D p

Theorem 21.5, equivalence (ii) ↔ (iii) of Sutherland: (D/p) = 1 with H_D splitting over 𝔽_p iff p splits completely in the ring class field.

theorem Elliptic_Curves.theorem_21_5_iii_iff_iv (D : ℤ) (p : ℕ) (hD : IsImagQuadDiscriminant D) (hp : Nat.Prime p) (hp_odd : p ≠ 2) (hp_ndvd : ¬↑p ∣ D) : SplitsCompletelyInRCF D p ↔ SatisfiesNormEquation D p

Theorem 21.5, equivalence (iii) ↔ (iv) of Sutherland: complete splitting of p in the ring class field iff 4p = t^2 - v^2 D for some t, v with p ∤ t.

theorem Elliptic_Curves.theorem_21_5_iv_iff_i (D : ℤ) (p : ℕ) (hD : IsImagQuadDiscriminant D) (hp : Nat.Prime p) (hp_odd : p ≠ 2) (hp_ndvd : ¬↑p ∣ D) : SatisfiesNormEquation D p ↔ IsNormOfPrincipalIdeal D p

Theorem 21.5, equivalence (iv) ↔ (i) of Sutherland: 4p = t^2 - v^2 D with p ∤ t iff p is the norm of a principal 𝒪-ideal.

theorem Elliptic_Curves.theorem_21_5 (D : ℤ) (p : ℕ) (hD : IsImagQuadDiscriminant D) (hp : Nat.Prime p) (hp_odd : p ≠ 2) (hp_ndvd : ¬↑p ∣ D) : (IsNormOfPrincipalIdeal D p ↔ LegendreOneAndHDSplits D p) ∧ (LegendreOneAndHDSplits D p ↔ SplitsCompletelyInRCF D p) ∧ (SplitsCompletelyInRCF D p ↔ SatisfiesNormEquation D p) ∧ (SatisfiesNormEquation D p ↔ IsNormOfPrincipalIdeal D p)

Theorem 21.5 (Sutherland): for an imaginary quadratic discriminant D and an odd prime p with p ∤ D unramified in the ring class field L, the four conditions (i)-(iv) are pairwise equivalent.

@[simp]

theorem Elliptic_Curves.normEquation_iff (D : ℤ) (p : ℕ) (t v : ℤ) : NormEquation D p t v ↔ 4 * ↑p = t ^ 2 - v ^ 2 * D

Definitional unfolding of NormEquation D p t v.

theorem Elliptic_Curves.normEquation_neg (D : ℤ) (p : ℕ) (t v : ℤ) : NormEquation D p t v ↔ NormEquation D p (-t) (-v)

The norm equation is symmetric under sign change of t, v.

theorem Elliptic_Curves.normEquation_sq_le {D : ℤ} {p : ℕ} {t v : ℤ} (hD : D < 0) (hne : NormEquation D p t v) : t ^ 2 ≤ 4 * ↑p

If D < 0 and NormEquation D p t v holds, then t^2 ≤ 4p.

noncomputable def Elliptic_Curves.kroneckerSymbol (p : ℕ) [hp : Fact (Nat.Prime p)] (D : ℤ) : ℤ

Definition 21.4 (Sutherland): the Kronecker symbol (D/p). For odd primes it agrees with the Legendre symbol; for p = 2 it is 0 if 2 ∣ D, +1 if D ≡ ±1 mod 8, and -1 if D ≡ ±3 mod 8.

theorem Elliptic_Curves.kroneckerSymbol_values {p : ℕ} [hp : Fact (Nat.Prime p)] (D : ℤ) : kroneckerSymbol p D = -1 ∨ kroneckerSymbol p D = 0 ∨ kroneckerSymbol p D = 1

The Kronecker symbol (D/p) always takes values in {-1, 0, 1}.

theorem Elliptic_Curves.kroneckerSymbol_odd_prime {p : ℕ} [hp : Fact (Nat.Prime p)] (hodd : p ≠ 2) (D : ℤ) : kroneckerSymbol p D = legendreSym p D

For an odd prime, the Kronecker symbol coincides with the Legendre symbol.

structure Elliptic_Curves.Deuring.RingClassFieldPrime (D : ℤ) : Type

A "ring class field prime" for Theorem 21.12 (Deuring): a positive integer q > 1 that is coprime to the discriminant D, intended to represent a prime power norm of a prime in the ring class field.

• q : ℕ
• q_pos : 1 < self.q
• coprime_q_D : self.q.Coprime D.natAbs

noncomputable def Elliptic_Curves.Deuring.hilbertClassPolynomial (D : ℤ) (F : Type u_1) [Field F] : Polynomial F

The Hilbert class polynomial of discriminant D viewed as a polynomial over an arbitrary field F, obtained by base change from the integral form.

noncomputable def Elliptic_Curves.Deuring.ellCMSet (D : ℤ) (F : Type u_1) [Field F] [Fintype F] : Set F

Ell_𝒪(F): the set of j-invariants of elliptic curves over the finite field F whose endomorphism ring is the order of discriminant D.

theorem Elliptic_Curves.Deuring.theorem_21_12 (D : ℤ) (hD : IsImagQuadDiscriminant D) (𝔮 : RingClassFieldPrime D) (F : Type u_1) [Field F] [Fintype F] (hcard : Fintype.card F = 𝔮.q) : (hilbertClassPolynomial D F).Splits ∧ (hilbertClassPolynomial D F).Separable ∧ ∀ (x : F), (hilbertClassPolynomial D F).IsRoot x ↔ x ∈ ellCMSet D F

Theorem 21.12 (Deuring, Sutherland): for an imaginary quadratic order of discriminant D with ring class field L, and q the norm of a prime ideal of 𝒪_L with q ⊥ D, the Hilbert class polynomial H_D(X) splits into distinct linear factors over 𝔽_q, with roots equal to Ell_𝒪(𝔽_q).

opaque DeuringLifting.IsReductionOfCurve {F : Type} [Field F] [DecidableEq F] [Fintype F] {L : Type} [Field L] [DecidableEq L] [NumberField L] (E : WeierstrassCurve.Affine F) (E_star : WeierstrassCurve.Affine L) (𝔮 : Ideal (NumberField.RingOfIntegers L)) [𝔮.IsMaximal] (e : F ≃+* NumberField.RingOfIntegers L ⧸ 𝔮) : Prop

IsReductionOfCurve E E_star 𝔮 e is the predicate stating that the curve E_star over the number field L has good reduction modulo the prime 𝔮 identifying with E via the ring isomorphism e : F ≃+* 𝒪_L/𝔮.

opaque DeuringLifting.IsReductionOfEndomorphism {F : Type} [Field F] [DecidableEq F] [Fintype F] {L : Type} [Field L] [DecidableEq L] [NumberField L] (E : WeierstrassCurve.Affine F) (E_star : WeierstrassCurve.Affine L) (φ : AddMonoid.End E.Point) (φ_star : AddMonoid.End E_star.Point) (𝔮 : Ideal (NumberField.RingOfIntegers L)) [𝔮.IsMaximal] (e : F ≃+* NumberField.RingOfIntegers L ⧸ 𝔮) (hcurve : IsReductionOfCurve E E_star 𝔮 e) : Prop

IsReductionOfEndomorphism states that the endomorphism φ_star of the lift E_star reduces to the endomorphism φ of E modulo 𝔮, given that E_star is a good reduction lift of E.

theorem DeuringLifting.deuring_lifting_theorem {F : Type} [Field F] [DecidableEq F] [Fintype F] (E : WeierstrassCurve.Affine F) (φ : AddMonoid.End E.Point) (hφ : φ ≠ 0) : ∃ (L : Type) (x : Field L) (x_1 : DecidableEq L) (x_2 : NumberField L) (E_star : WeierstrassCurve.Affine L) (φ_star : AddMonoid.End E_star.Point) (𝔮 : Ideal (NumberField.RingOfIntegers L)) (x_3 : 𝔮.IsMaximal) (e : F ≃+* NumberField.RingOfIntegers L ⧸ 𝔮) (hcurve : IsReductionOfCurve E E_star 𝔮 e), IsReductionOfEndomorphism E E_star φ φ_star 𝔮 e hcurve

Theorem 21.13 (Deuring lifting theorem, Sutherland): every nonzero endomorphism φ of an elliptic curve E/𝔽_q lifts to a characteristic-zero endomorphism φ_star of an elliptic curve E_star over a number field L with good reduction at a prime 𝔮 of residue field 𝔽_q.

structure RingClassField.IsImagQuadDisc (D : ℤ) : Prop

Predicate (in Prop) form of "D is the discriminant of an imaginary quadratic order": D < 0 and D ≡ 0 or 1 mod 4.

• neg : D < 0
• cong : D % 4 = 0 ∨ D % 4 = 1

noncomputable def RingClassField.ImagQuadField (D : ℤ) : Type

The imaginary quadratic field K = ℚ(√D), abstractly defined as a type.

@[implicit_reducible]

noncomputable instance RingClassField.ImagQuadField.instField (D : ℤ) : Field (ImagQuadField D)

The imaginary quadratic field ImagQuadField D has a Field structure.

@[implicit_reducible]

noncomputable instance RingClassField.ImagQuadField.instAlgebra (D : ℤ) : Algebra ℚ (ImagQuadField D)

ImagQuadField D is a ℚ-algebra.

theorem RingClassField.ImagQuadField.instNumberField (D : ℤ) (hD : IsImagQuadDisc D) : NumberField (ImagQuadField D)

For an imaginary quadratic discriminant D, ImagQuadField D is a number field.

theorem RingClassField.ImagQuadField.finrank_eq_two (D : ℤ) (hD : IsImagQuadDisc D) : Module.finrank ℚ (ImagQuadField D) = 2

The imaginary quadratic field has degree 2 over ℚ.

noncomputable def RingClassField.ImagQuadOrder (D : ℤ) : Type

The order 𝒪 = ℤ[(D + √D)/2] (or ℤ[√D]) of discriminant D, abstractly defined as a type.

@[implicit_reducible]

noncomputable instance RingClassField.ImagQuadOrder.instCommRing (D : ℤ) : CommRing (ImagQuadOrder D)

The imaginary quadratic order is a commutative ring.

noncomputable def RingClassField.IdealClassGroup (D : ℤ) : Type

The ideal class group cl(𝒪) of the order of discriminant D.

@[implicit_reducible]

noncomputable instance RingClassField.IdealClassGroup.instCommGroup (D : ℤ) : CommGroup (IdealClassGroup D)

The ideal class group is a commutative group.

@[implicit_reducible]

noncomputable instance RingClassField.IdealClassGroup.instFintype (D : ℤ) (hD : IsImagQuadDisc D) : Fintype (IdealClassGroup D)

For an imaginary quadratic discriminant D, the ideal class group is finite.

noncomputable def RingClassField.classNumber (D : ℤ) (hD : IsImagQuadDisc D) : ℕ

The class number h(D) = #cl(𝒪).

theorem RingClassField.classNumber_pos (D : ℤ) (hD : IsImagQuadDisc D) : 0 < classNumber D hD

The class number of an imaginary quadratic discriminant is positive.

noncomputable def RingClassField.hilbertClassPoly (D : ℤ) : Polynomial (ImagQuadField D)

The Hilbert class polynomial H_D(X) viewed as a polynomial over the imaginary quadratic field K = ℚ(√D).

theorem RingClassField.hilbertClassPoly_monic (D : ℤ) (hD : IsImagQuadDisc D) : (hilbertClassPoly D).Monic

The Hilbert class polynomial is monic.

theorem RingClassField.hilbertClassPoly_natDegree (D : ℤ) (hD : IsImagQuadDisc D) : (hilbertClassPoly D).natDegree = classNumber D hD

The Hilbert class polynomial has degree equal to the class number.

theorem RingClassField.hilbertClassPoly_ne_zero (D : ℤ) (hD : IsImagQuadDisc D) : hilbertClassPoly D ≠ 0

The Hilbert class polynomial is nonzero.

theorem RingClassField.hilbertClassPoly_lifts_int (D : ℤ) (hD : IsImagQuadDisc D) : hilbertClassPoly D ∈ Polynomial.lifts (algebraMap ℤ (ImagQuadField D))

The Hilbert class polynomial is in the image of ℤ-coefficient polynomials: it has integer coefficients.

@[reducible, inline]

abbrev RingClassField.RingClassFieldType (D : ℤ) : Type

Definition 21.3 (Sutherland): the ring class field of discriminant D, defined as the splitting field of the Hilbert class polynomial H_D over K = ℚ(√D).

@[implicit_reducible]

noncomputable instance RingClassField.instFieldRingClassFieldType (D : ℤ) : Field (RingClassFieldType D)

The ring class field is a field.

@[implicit_reducible]

noncomputable instance RingClassField.instAlgebraImagQuadFieldRingClassFieldType (D : ℤ) : Algebra (ImagQuadField D) (RingClassFieldType D)

The ring class field is an algebra over the imaginary quadratic base field.

theorem RingClassField.ringClassField_isGalois (D : ℤ) (hD : IsImagQuadDisc D) : IsGalois (ImagQuadField D) (RingClassFieldType D)

The ring class field is Galois over the imaginary quadratic base field.

noncomputable def RingClassField.EllO (D : ℤ) : Set (RingClassFieldType D)

Ell_𝒪: the set of j-invariants in the ring class field corresponding to elliptic curves with CM by the order of discriminant D.

theorem RingClassField.EllO_subset_roots (D : ℤ) (j : RingClassFieldType D) (hj : j ∈ EllO D) : (Polynomial.aeval j) (hilbertClassPoly D) = 0

Every j ∈ Ell_𝒪(D) is a root of the Hilbert class polynomial.

theorem RingClassField.roots_subset_EllO (D : ℤ) (j : RingClassFieldType D) (hj : j ∈ (hilbertClassPoly D).rootSet (RingClassFieldType D)) : j ∈ EllO D

Every root of the Hilbert class polynomial in the ring class field belongs to Ell_𝒪(D).

theorem RingClassField.EllO_nonempty (D : ℤ) (hD : IsImagQuadDisc D) : (EllO D).Nonempty

The set Ell_𝒪(D) is nonempty for an imaginary quadratic discriminant.

noncomputable def RingClassField.cmAction (D : ℤ) : IdealClassGroup D → ↑(EllO D) → ↑(EllO D)

The action of the ideal class group on Ell_𝒪(D): given a class α ∈ cl(𝒪) and j ∈ Ell_𝒪(D), we produce α · j ∈ Ell_𝒪(D).

theorem RingClassField.cmAction_transitive (D : ℤ) (hD : IsImagQuadDisc D) (j₁ j₂ : ↑(EllO D)) : ∃ (α : IdealClassGroup D), cmAction D α j₁ = j₂

The ideal class group action on Ell_𝒪(D) is transitive.

theorem RingClassField.cmAction_free (D : ℤ) (hD : IsImagQuadDisc D) (α : IdealClassGroup D) (j : ↑(EllO D)) (h : cmAction D α j = j) : α = 1

The ideal class group action on Ell_𝒪(D) is free: only the identity class fixes a point.

theorem RingClassField.galAction_preserves_EllO (D : ℤ) (σ : Gal(RingClassFieldType D/ImagQuadField D)) (j : RingClassFieldType D) (hj : j ∈ EllO D) : σ j ∈ EllO D

The Galois action on the ring class field preserves the subset Ell_𝒪(D).

theorem RingClassField.galAction_cmAction_compat (D : ℤ) (hD : IsImagQuadDisc D) (σ : Gal(RingClassFieldType D/ImagQuadField D)) (j₁ j₂ : ↑(EllO D)) (α₁ : IdealClassGroup D) (hα₁ : cmAction D α₁ j₁ = ⟨σ ↑j₁, ⋯⟩) (α₂ : IdealClassGroup D) (hα₂ : cmAction D α₂ j₂ = ⟨σ ↑j₂, ⋯⟩) : α₁ = α₂

Compatibility of the Galois action with the ideal class group action: if σ sends j₁ to α₁ · j₁ and j₂ to α₂ · j₂, then α₁ = α₂, i.e. σ acts uniformly through a single ideal class.

noncomputable def RingClassField.galToClassGroupAux (D : ℤ) (hD : IsImagQuadDisc D) (σ : Gal(RingClassFieldType D/ImagQuadField D)) (j₀ : ↑(EllO D)) : IdealClassGroup D

Auxiliary construction: from a Galois automorphism σ and a base point j₀ ∈ Ell_𝒪(D), pick the ideal class taking j₀ to σ(j₀).

noncomputable def RingClassField.galToClassGroupHom (D : ℤ) (hD : IsImagQuadDisc D) : Gal(RingClassFieldType D/ImagQuadField D) →* IdealClassGroup D

The group homomorphism Gal(L/K) → cl(𝒪) underlying Corollary 21.2.

theorem RingClassField.galToClassGroupHom_spec (D : ℤ) (hD : IsImagQuadDisc D) (σ : Gal(RingClassFieldType D/ImagQuadField D)) (j₀ : ↑(EllO D)) : cmAction D ((galToClassGroupHom D hD) σ) j₀ = ⟨σ ↑j₀, ⋯⟩

Characterizing property of galToClassGroupHom: it sends σ to the ideal class α such that α · j₀ = σ(j₀).

theorem RingClassField.galToClassGroupHom_injective (D : ℤ) (hD : IsImagQuadDisc D) : Function.Injective ⇑(galToClassGroupHom D hD)

The natural map Gal(L/K) → cl(𝒪) is injective.

theorem RingClassField.galToClassGroupHom_surjective (D : ℤ) (hD : IsImagQuadDisc D) : Function.Surjective ⇑(galToClassGroupHom D hD)

The natural map Gal(L/K) → cl(𝒪) is surjective.

noncomputable def RingClassField.galToClassGroup_mulEquiv (D : ℤ) (hD : IsImagQuadDisc D) : Gal(RingClassFieldType D/ImagQuadField D) ≃* IdealClassGroup D

The group isomorphism Gal(L/K) ≃* cl(𝒪) from Corollary 21.2, constructed via the bijective hom galToClassGroupHom.

theorem RingClassField.corollary_21_2_irreducible (D : ℤ) (hD : IsImagQuadDisc D) : Irreducible (hilbertClassPoly D)

Corollary 21.2 (irreducibility part, Sutherland): the Hilbert class polynomial H_D(X) is irreducible over K = ℚ(√D).

theorem RingClassField.corollary_21_2_degree (D : ℤ) (hD : IsImagQuadDisc D) : Module.finrank (ImagQuadField D) (RingClassFieldType D) = classNumber D hD

Corollary 21.2 (degree part, Sutherland): the ring class field K(j(E))/K has degree equal to the class number h(D).

noncomputable def RingClassField.corollary_21_2_galois_iso (D : ℤ) (hD : IsImagQuadDisc D) : Gal(RingClassFieldType D/ImagQuadField D) ≃* IdealClassGroup D

Corollary 21.2 (Galois isomorphism part, Sutherland): the Galois group Gal(K(j(E))/K) is isomorphic to the ideal class group cl(𝒪).

noncomputable def CMMethod.HasJInvariant {F : Type u_1} [Field F] (E : WeierstrassCurve.Affine F) (j₀ : F) : Prop

Predicate saying that the elliptic curve E/F has prescribed j-invariant j₀ ∈ F.

theorem CMMethod.corollary_21_9 (D : ℤ) (p : ℕ) (t v : ℤ) (hD : Elliptic_Curves.IsImagQuadDiscriminant D) (hp : Nat.Prime p) (hp_odd : p ≠ 2) (hp_ndvd : ¬↑p ∣ D) (hne : Elliptic_Curves.NormEquation D p t v) (ht : ¬↑p ∣ t) (F : Type u_1) [Field F] [Fintype F] [DecidableEq F] (hcard : Fintype.card F = p) (E : WeierstrassCurve.Affine F) (j₀ : F) (hj₀_ne0 : j₀ ≠ 0) (hj₀_ne1728 : j₀ ≠ 1728) (hj₀_root : (Elliptic_Curves.Deuring.hilbertClassPolynomial D F).IsRoot j₀) (hj_E : HasJInvariant E j₀) : Hasse.traceFrobenius E = t ∨ Hasse.traceFrobenius E = -t

Corollary 21.9 (Sutherland): for an imaginary quadratic discriminant D, an odd prime p ∤ D with 4p = t^2 - v^2 D and p ∤ t, and an elliptic curve E/𝔽_p whose j-invariant j₀ ∉ {0, 1728} is a root of H_D(X) mod p, the trace of Frobenius of E equals ±t.

theorem CMMethod.corollary_21_9_trace_not_dvd (D : ℤ) (p : ℕ) (t v : ℤ) (hD : Elliptic_Curves.IsImagQuadDiscriminant D) (hp : Nat.Prime p) (hp_odd : p ≠ 2) (hp_ndvd : ¬↑p ∣ D) (hne : Elliptic_Curves.NormEquation D p t v) (ht : ¬↑p ∣ t) (F : Type u_1) [Field F] [Fintype F] [DecidableEq F] (hcard : Fintype.card F = p) (E : WeierstrassCurve.Affine F) (j₀ : F) (hj₀_ne0 : j₀ ≠ 0) (hj₀_ne1728 : j₀ ≠ 1728) (hj₀_root : (Elliptic_Curves.Deuring.hilbertClassPolynomial D F).IsRoot j₀) (hj_E : HasJInvariant E j₀) : ¬↑p ∣ Hasse.traceFrobenius E

Companion to Corollary 21.9: under the same hypotheses, the Frobenius trace of E is not divisible by p (equivalently, E is ordinary).

structure CMMethod.CMOutput (F : Type u_1) [Field F] [Fintype F] [DecidableEq F] : Type u_1

The output of the CM method: a curve over a finite field F together with its Frobenius trace witnessing the relation trace = ±t.

• curve : WeierstrassCurve.Affine F
• trace : ℤ
• frob_trace_eq : Hasse.traceFrobenius self.curve = self.trace ∨ Hasse.traceFrobenius self.curve = -self.trace

noncomputable def ProperIdealNormCount.conductor (D : ℤ) : Elliptic_Curves.IsImagQuadDiscriminant D → ℕ

The conductor [𝒪_K : 𝒪] of the order of discriminant D in its maximal order, as a natural number.

theorem ProperIdealNormCount.conductor_pos (D : ℤ) (hD : Elliptic_Curves.IsImagQuadDiscriminant D) : 0 < conductor D hD

The conductor of an imaginary quadratic order is positive.

noncomputable def ProperIdealNormCount.numProperIdealsOfNorm (D : ℤ) (p : ℕ) : ℕ

The number of proper 𝒪-ideals of norm p.

theorem ProperIdealNormCount.corollary_21_7_conductor_divides (D : ℤ) (p : ℕ) (hD : Elliptic_Curves.IsImagQuadDiscriminant D) [hp : Fact (Nat.Prime p)] (hdvd : ↑p ∣ ↑(conductor D hD)) : numProperIdealsOfNorm D p = 0

Corollary 21.7 (Sutherland), case p ∣ conductor: if the prime p divides the conductor of the order 𝒪, there are no proper 𝒪-ideals of norm p.

theorem ProperIdealNormCount.corollary_21_7_conductor_coprime (D : ℤ) (p : ℕ) (hD : Elliptic_Curves.IsImagQuadDiscriminant D) [hp : Fact (Nat.Prime p)] (hndvd : ¬↑p ∣ ↑(conductor D hD)) : ↑(numProperIdealsOfNorm D p) = 1 + Elliptic_Curves.kroneckerSymbol p D

Corollary 21.7 (Sutherland), case p coprime to the conductor: when p does not divide the conductor of 𝒪, the number of proper 𝒪-ideals of norm p is 1 + (D/p).

noncomputable def RingClassFieldRamification.IsUnramifiedInRCF (D : ℤ) (p : ℕ) : Prop

Predicate: the rational prime p is unramified in the ring class field of discriminant D.

theorem RingClassFieldRamification.corollary_21_8_conductor_coprime (D : ℤ) (p : ℕ) (hD : Elliptic_Curves.IsImagQuadDiscriminant D) (hp : Nat.Prime p) (hndvd : ¬↑p ∣ ↑(ProperIdealNormCount.conductor D hD)) : IsUnramifiedInRCF D p

Corollary 21.8 (Sutherland): the ring class field of discriminant D is unramified at every rational prime p that does not divide the conductor of 𝒪.

theorem RingClassFieldRamification.conductor_dvd_disc (D : ℤ) (hD : Elliptic_Curves.IsImagQuadDiscriminant D) : ↑(ProperIdealNormCount.conductor D hD) ∣ D

The conductor of an order in an imaginary quadratic field divides the discriminant.

noncomputable def ImagQuadPrimeSplitting.rootsMinPolyMod (D : ℤ) (p : ℕ) [Fact (Nat.Prime p)] : Finset (ZMod p)

Roots in ZMod p of the minimal polynomial of ω = (D + √D)/2 (or √D) for the imaginary quadratic discriminant D.

noncomputable def ImagQuadPrimeSplitting.numIdealsOfNorm (D : ℤ) (p : ℕ) [Fact (Nat.Prime p)] : ℤ

The number of 𝒪_K-ideals of norm p, counted by the roots of the minimal polynomial of ω modulo p.

theorem ImagQuadPrimeSplitting.card_filter_sq_add_eq_zero_ZMod2 (c : ZMod 2) : {x : ZMod 2 | x ^ 2 + c = 0}.card = 1

In ZMod 2, for any constant c, the equation x^2 + c = 0 has exactly one solution.

theorem ImagQuadPrimeSplitting.card_filter_sq_sub_x_add_ZMod2 (c : ZMod 2) : {x : ZMod 2 | x ^ 2 - x + c = 0}.card = if c = 0 then 2 else 0

In ZMod 2, the equation x^2 - x + c = 0 has 2 solutions if c = 0 and none otherwise.

theorem ImagQuadPrimeSplitting.numIdealsOfNorm_eq_one_add_kroneckerSymbol (D : ℤ) (p : ℕ) [hp : Fact (Nat.Prime p)] (hD : Elliptic_Curves.IsImagQuadDiscriminant D) : numIdealsOfNorm D p = 1 + Elliptic_Curves.kroneckerSymbol p D

Lemma 21.6 (Sutherland, ideal-counting version): the number of 𝒪_K-ideals of norm p equals 1 + (D/p).

def ImagQuadPrimeFactorization.primeIdealAbove {d : ℤ} (p : ℕ) (r : ℤ) : Ideal (ℤ√d)

The prime ideal 𝔭 = (p, ω - r) in ℤ[√d] above a rational prime p and a root r of x² + d ≡ 0 mod p, used in Lemma 21.6.

theorem ImagQuadPrimeFactorization.primeIdeal_of_norm_eq_span_infrastructure {d : ℤ} (hd : d < 0) [IsDomain (ℤ√d)] (p : ℕ) [Fact (Nat.Prime p)] (𝔭 : Ideal (ℤ√d)) (h𝔭 : 𝔭 ≠ ⊥) (hnorm : ProperIdealInvertible.idealNormZsqrtd 𝔭 = p) : ∃ (r : ℤ), (r ^ 2 + d) % ↑p = 0 ∧ 𝔭 = primeIdealAbove p r

Infrastructure form: in ℤ[√d] with d < 0, every prime ideal 𝔭 ≠ ⊥ of norm p has the form (p, ω - r) for some r with r² + d ≡ 0 mod p.

theorem ImagQuadPrimeFactorization.principal_ideal_prime_split_infrastructure {d : ℤ} (hd : d < 0) [IsDomain (ℤ√d)] (p : ℕ) [Fact (Nat.Prime p)] (r : ℤ) (hroot : (r ^ 2 + d) % ↑p = 0) (hdistinct : 2 * r % ↑p ≠ 0) : primeIdealAbove p r * ProperIdealInvertible.conjIdeal (primeIdealAbove p r) = Ideal.span {↑p} ∧ primeIdealAbove p r ≠ ProperIdealInvertible.conjIdeal (primeIdealAbove p r)

Infrastructure form (split case): when r is a root of x² + d ≡ 0 mod p with 2r ≢ 0 mod p, the principal ideal (p) in ℤ[√d] factors as 𝔭 · 𝔭̄ with 𝔭 ≠ 𝔭̄.

theorem ImagQuadPrimeFactorization.principal_ideal_prime_ramified_infrastructure {d : ℤ} (hd : d < 0) [IsDomain (ℤ√d)] (p : ℕ) [Fact (Nat.Prime p)] (r : ℤ) (hroot : (r ^ 2 + d) % ↑p = 0) (hramified : 2 * r % ↑p = 0) : primeIdealAbove p r ^ 2 = Ideal.span {↑p}

Infrastructure form (ramified case): when r is a root of x² + d ≡ 0 mod p with 2r ≡ 0 mod p, the principal ideal (p) in ℤ[√d] is 𝔭².

theorem ImagQuadPrimeFactorization.principal_ideal_prime_inert_infrastructure {d : ℤ} (hd : d < 0) [IsDomain (ℤ√d)] (p : ℕ) [Fact (Nat.Prime p)] (hD : Elliptic_Curves.IsImagQuadDiscriminant (4 * d)) (hkron : Elliptic_Curves.kroneckerSymbol p (4 * d) = -1) : (Ideal.span {↑p}).IsPrime

Infrastructure form (inert case): if the Kronecker symbol (4d/p) = -1, then the principal ideal (p) in ℤ[√d] is prime.

theorem ImagQuadPrimeFactorization.primeIdeal_of_norm_eq_span {d : ℤ} (hd : d < 0) [IsDomain (ℤ√d)] (p : ℕ) [Fact (Nat.Prime p)] (𝔭 : Ideal (ℤ√d)) (h𝔭 : 𝔭 ≠ ⊥) (hnorm : ProperIdealInvertible.idealNormZsqrtd 𝔭 = p) : ∃ (r : ℤ), (r ^ 2 + d) % ↑p = 0 ∧ 𝔭 = primeIdealAbove p r

User-facing version of primeIdeal_of_norm_eq_span_infrastructure.

theorem ImagQuadPrimeFactorization.principal_ideal_prime_split {d : ℤ} (hd : d < 0) [IsDomain (ℤ√d)] (p : ℕ) [hp : Fact (Nat.Prime p)] (r : ℤ) (hroot : (r ^ 2 + d) % ↑p = 0) (hdistinct : 2 * r % ↑p ≠ 0) : primeIdealAbove p r * ProperIdealInvertible.conjIdeal (primeIdealAbove p r) = Ideal.span {↑p} ∧ primeIdealAbove p r ≠ ProperIdealInvertible.conjIdeal (primeIdealAbove p r)

User-facing version of principal_ideal_prime_split_infrastructure.

theorem ImagQuadPrimeFactorization.principal_ideal_prime_ramified {d : ℤ} (hd : d < 0) [IsDomain (ℤ√d)] (p : ℕ) [hp : Fact (Nat.Prime p)] (r : ℤ) (hroot : (r ^ 2 + d) % ↑p = 0) (hramified : 2 * r % ↑p = 0) : primeIdealAbove p r ^ 2 = Ideal.span {↑p}

User-facing version of principal_ideal_prime_ramified_infrastructure.

theorem ImagQuadPrimeFactorization.principal_ideal_prime_inert {d : ℤ} (hd : d < 0) [IsDomain (ℤ√d)] (p : ℕ) [hp : Fact (Nat.Prime p)] (hD : Elliptic_Curves.IsImagQuadDiscriminant (4 * d)) (hkron : Elliptic_Curves.kroneckerSymbol p (4 * d) = -1) : (Ideal.span {↑p}).IsPrime

User-facing version of principal_ideal_prime_inert_infrastructure.

theorem ImagQuadPrimeSplitting.IdealRootBijection.primeIdealAbove_hasNorm {d : ℤ} (hd : d < 0) [IsDomain (ℤ√d)] (p : ℕ) [Fact (Nat.Prime p)] (r : ℤ) (hroot : (r ^ 2 + d) % ↑p = 0) : ImagQuadPrimeFactorization.primeIdealAbove p r ≠ ⊥ ∧ ProperIdealInvertible.idealNormZsqrtd (ImagQuadPrimeFactorization.primeIdealAbove p r) = p

The ideal (p, ω - r) in ℤ[√d] is nonzero and has norm p whenever r² + d ≡ 0 mod p.

theorem ImagQuadPrimeSplitting.IdealRootBijection.primeIdealAbove_injective {d : ℤ} (hd : d < 0) [IsDomain (ℤ√d)] (p : ℕ) [hp : Fact (Nat.Prime p)] (r s : ℤ) (hr : (r ^ 2 + d) % ↑p = 0) (hs : (s ^ 2 + d) % ↑p = 0) (heq : ImagQuadPrimeFactorization.primeIdealAbove p r = ImagQuadPrimeFactorization.primeIdealAbove p s) : ↑r = ↑s

Distinct roots r ≠ s (mod p) of x² + d ≡ 0 mod p give distinct prime ideals (p, ω - r) ≠ (p, ω - s).

theorem ImagQuadPrimeSplitting.IdealRootBijection.numIdealsOfNorm_eq_card_ideals_of_norm {d : ℤ} (hd : d < 0) [IsDomain (ℤ√d)] (p : ℕ) [hp : Fact (Nat.Prime p)] (hD : Elliptic_Curves.IsImagQuadDiscriminant (4 * d)) : numIdealsOfNorm (4 * d) p = ↑{r : ZMod p | ImagQuadPrimeFactorization.primeIdealAbove p ↑r.val ≠ ⊥ ∧ ProperIdealInvertible.idealNormZsqrtd (ImagQuadPrimeFactorization.primeIdealAbove p ↑r.val) = p}.card

The number of 𝒪_K-ideals of norm p in the imaginary quadratic field of discriminant 4d equals the number of roots r ∈ ZMod p for which (p, ω - r) is a nonzero ideal of norm p.

theorem CMMethod.TwistSelection.exists_curve_or_twist_with_order {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (E : WeierstrassCurve.Affine F) (t : ℤ) (hfrob : Hasse.traceFrobenius E = t ∨ Hasse.traceFrobenius E = -t) (hE : Hasse.numPoints E ≤ 2 * Fintype.card F + 2) : ↑(Hasse.numPoints E) = ↑(Fintype.card F) + 1 - t ∨ ↑(QuadraticTwist.twistNumPoints E) = ↑(Fintype.card F) + 1 - t

Given an elliptic curve E/F with Frobenius trace ±t, either E itself or its quadratic twist has exactly |F| + 1 - t points. This is the twist selection step in the CM method.