def IsImaginaryQuadraticDiscriminant (D : ℤ) : Prop

An integer D is an imaginary quadratic discriminant iff D < 0 and D ≡ 0 or 1 (mod 4). These are exactly the discriminants of orders in imaginary quadratic fields.

noncomputable def imaginaryQuadraticOrder (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) : Subring ℂ

The imaginary quadratic order in ℂ associated with an imaginary quadratic discriminant D: it is generated as a subring of ℂ by ω_D = (D + √|D| · i)/2, the standard generator of the unique order of discriminant D in ℚ(√D).

noncomputable def CMjInvariants (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) : Finset ℂ

The finite set Ell_𝒪(ℂ) = {j(E) : End(E) ≃ 𝒪} of j-invariants of complex elliptic curves with CM by the order 𝒪 of discriminant D. These are the roots of the Hilbert class polynomial H_D(X), indexed by the ideal class group of 𝒪.

theorem CMjInvariants_nonempty (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) : (CMjInvariants D hD).Nonempty

The set Ell_𝒪(ℂ) of CM j-invariants is nonempty (every imaginary quadratic order has at least one ideal class, so it has at least one CM j-invariant).

noncomputable def hilbertClassPoly (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) : Polynomial ℂ

The Hilbert class polynomial H_D(X) := ∏_{j ∈ Ell_𝒪(ℂ)} (X - j) ∈ ℂ[X] of an imaginary quadratic discriminant D. Its roots are precisely the j-invariants of complex elliptic curves with CM by the order of discriminant D. (Cf. Theorem 20.12: the coefficients are actually integers.)

theorem hilbertClassPoly_monic (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) : (hilbertClassPoly D hD).Monic

The Hilbert class polynomial H_D is monic, being a product of monic linear factors X - j.

theorem hilbertClassPoly_natDegree (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) : (hilbertClassPoly D hD).natDegree = (CMjInvariants D hD).card

The natural degree of the Hilbert class polynomial equals the number of CM j-invariants of discriminant D (which equals the class number h(D)).

noncomputable def classicalModularPoly (N : ℕ) : Polynomial (Polynomial ℤ)

The classical modular polynomial Φ_N(X, Y) ∈ ℤ[X][Y] (Definition 19.15 / Theorem 19.17): the minimal polynomial of j_N(τ) := j(Nτ) over ℂ(j), viewed as a bivariate polynomial with integer coefficients.

noncomputable def classicalModularPolyDiag (N : ℕ) : Polynomial ℤ

The diagonal Φ_N(X, X) of the classical modular polynomial, obtained by substituting X for the outer variable. For prime N this is a polynomial whose leading term is -X^{2N} (Lemma 20.9).

theorem classicalModularPolyDiag_natDegree_eq (N : ℕ) (hN : Nat.Prime N) : (classicalModularPolyDiag N).natDegree = 2 * N

For prime N, the diagonal Φ_N(X, X) has natural degree 2N (corresponds to Lemma 20.9: the leading term is -X^{2N}).

theorem classicalModularPolyDiag_leadingCoeff_eq (N : ℕ) (hN : Nat.Prime N) : (classicalModularPolyDiag N).leadingCoeff = -1

For prime N, the leading coefficient of Φ_N(X, X) is -1 (Lemma 20.9).

theorem neg_classicalModularPolyDiag_monic (N : ℕ) (hN : Nat.Prime N) : (-classicalModularPolyDiag N).Monic

For prime N, the negation -Φ_N(X, X) is monic. Direct consequence of Lemma 20.9 (leading coefficient is -1).

theorem CMjInvariant_root_of_negModularPolyDiag (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) (j : ℂ) (hj : j ∈ CMjInvariants D hD) : ∃ (p : ℕ) (_ : Nat.Prime p), Polynomial.eval₂ (algebraMap ℤ ℂ) j (-classicalModularPolyDiag p) = 0

Every CM j-invariant j ∈ Ell_𝒪(ℂ) is a root of -Φ_p(X, X) for some prime p. This expresses each CM j-invariant as a root of a monic integer polynomial (supporting the proof that CM j-invariants are algebraic integers).

theorem CMjInvariant_isIntegral (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) (j : ℂ) (hj : j ∈ CMjInvariants D hD) : IsIntegral ℤ j

Corollary 20.13: every CM j-invariant is an algebraic integer over ℤ. Proved by exhibiting it as a root of the monic integer polynomial -Φ_p(X, X).

theorem galoisAction_coeffs_rational (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) (n : ℕ) : ∃ (q : ℚ), (∏ j ∈ CMjInvariants D hD, (Polynomial.X - Polynomial.C j)).coeff n = ↑q

Each coefficient of the Hilbert class polynomial H_D(X) is a rational number. Comes from Galois-equivariance of the coefficients (they are fixed by Gal(ℚ̄/ℚ)), and is one of the two ingredients in Theorem 20.12.

theorem hilbertClassPoly_coeff_rational (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) (n : ℕ) : ∃ (q : ℚ), (hilbertClassPoly D hD).coeff n = ↑q

Restated form of galoisAction_coeffs_rational: each coefficient of H_D(X) is rational.

theorem coeff_prod_X_sub_C_isIntegral (s : Finset ℂ) (hint : ∀ j ∈ s, IsIntegral ℤ j) (n : ℕ) : IsIntegral ℤ ((∏ j ∈ s, (Polynomial.X - Polynomial.C j)).coeff n)

For a finite set s ⊂ ℂ of algebraic integers, each coefficient of the monic product ∏_{j∈s} (X - j) is itself an algebraic integer. Used as a lemma toward proving H_D ∈ ℤ[X].

theorem hilbertClassPoly_int_coeffs (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) : hilbertClassPoly D hD ∈ Polynomial.lifts (Int.castRingHom ℂ)

Theorem 20.12: the Hilbert class polynomial H_D(X) has integer coefficients, i.e. lies in the image of ℤ[X] → ℂ[X]. Combines rationality of coefficients with the fact that they are algebraic integers.

def IsCMjInvariant (j : ℂ) : Prop

Predicate: a complex number j ∈ ℂ is a CM j-invariant iff it appears in Ell_𝒪(ℂ) for some imaginary quadratic order 𝒪 of discriminant D.

theorem hilbertClassPoly_eval_eq_zero (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) (j : ℂ) (hj : j ∈ CMjInvariants D hD) : Polynomial.eval j (hilbertClassPoly D hD) = 0

Every CM j-invariant of discriminant D is a root of the Hilbert class polynomial H_D (by construction, as H_D is the product over these roots).

theorem hilbertClassPoly_isRoot (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) (j : ℂ) (hj : j ∈ CMjInvariants D hD) : (hilbertClassPoly D hD).IsRoot j

IsRoot-form of hilbertClassPoly_eval_eq_zero: every CM j-invariant is a root of the Hilbert class polynomial.

theorem cm_j_invariant_isIntegral (j : ℂ) (hcm : IsCMjInvariant j) : IsIntegral ℤ j

Corollary 20.13 (general form): if j ∈ ℂ is the j-invariant of a complex elliptic curve with complex multiplication, then j is an algebraic integer.

noncomputable def imagQuadGen (D : ℤ) : ℂ

The standard generator ω_D := (D mod 2)/2 + i√|D|/2 ∈ ℂ of the imaginary quadratic order of discriminant D.

noncomputable def imagQuadOrder (D : ℤ) : Subring ℂ

Subring-of-ℂ version of the imaginary quadratic order of discriminant D: the subring of ℂ generated by imagQuadGen D.

def ImagQuadIdealClass (D : ℤ) (_hD : IsImaginaryQuadraticDiscriminant D) : Type

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

theorem CMjInvariants_card_eq_classNumber (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) : (CMjInvariants D hD).card = Nat.card (ImagQuadIdealClass D hD)

The number of CM j-invariants Ell_𝒪(ℂ) of discriminant D equals the class number |cl(𝒪)| (cardinality of the ideal class group).

noncomputable def ImagQuadProperIdeal (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) : Type

The type of proper (invertible) 𝒪-ideals for the imaginary quadratic order of discriminant D.

noncomputable def ImagQuadProperIdeal.norm {D : ℤ} {hD : IsImaginaryQuadraticDiscriminant D} (a : ImagQuadProperIdeal D hD) : ℕ

The (absolute) norm N(𝔞) of a proper 𝒪-ideal 𝔞, viewed as a natural number.

noncomputable def ImagQuadProperIdeal.idealClass {D : ℤ} {hD : IsImaginaryQuadraticDiscriminant D} (a : ImagQuadProperIdeal D hD) : ImagQuadIdealClass D hD

The ideal class in cl(𝒪) of a proper 𝒪-ideal 𝔞.

theorem ImagQuadProperIdeal.norm_pos {D : ℤ} {hD : IsImaginaryQuadraticDiscriminant D} (a : ImagQuadProperIdeal D hD) : 0 < a.norm

The norm of any proper 𝒪-ideal is a positive natural number.

theorem ImagQuadIdealClass.infinite_prime_norm (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) (c : ImagQuadIdealClass D hD) : {a : ImagQuadProperIdeal D hD | a.idealClass = c ∧ Nat.Prime a.norm}.Infinite

Theorem 20.11: every ideal class in cl(𝒪) of an imaginary quadratic order contains infinitely many proper ideals of prime norm.

@[reducible]

noncomputable def instCommGroupImagQuadIdealClass (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) : CommGroup (ImagQuadIdealClass D hD)

The commutative group structure on the ideal class group cl(𝒪) of an imaginary quadratic order.

@[implicit_reducible]

noncomputable instance instCommGroupImagQuadIdealClass_1 (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) : CommGroup (ImagQuadIdealClass D hD)

Typeclass-level commutative group instance on cl(𝒪).

noncomputable def classGroupToCMjInvariantsBijection (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) : ImagQuadIdealClass D hD ≃ ↥(CMjInvariants D hD)

The bijection between the ideal class group cl(𝒪) and the set of CM j-invariants Ell_𝒪(ℂ) of discriminant D (the action of cl(𝒪) is simply transitive on Ell_𝒪(ℂ)).

noncomputable def classGroupActionHom (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) : ImagQuadIdealClass D hD →* Equiv.Perm ↥(CMjInvariants D hD)

The action homomorphism cl(𝒪) → Sym(Ell_𝒪(ℂ)) arising from the simply transitive action by left multiplication, transported across the bijection cl(𝒪) ≃ Ell_𝒪(ℂ).

noncomputable def SplittingFieldGaloisSubgroup (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) : Subgroup (Equiv.Perm ↥(CMjInvariants D hD))

The image of Gal(L/K) in Sym(Ell_𝒪(ℂ)), where L is the splitting field of H_D(X) over K = ℚ(√D) (i.e. the ring class field). The Galois group acts on the roots of H_D, which are the CM j-invariants.

theorem galoisSubgroup_le_classGroupRange (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) : SplittingFieldGaloisSubgroup D hD ≤ (classGroupActionHom D hD).range

Theorem 20.14 (containment): the Galois group Gal(L/K) (acting on CM j-invariants) lands inside the image of the class group action.

@[reducible, inline]

abbrev SplittingFieldGaloisGroup (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) : Type

Abbreviation for the Galois group of the splitting field of H_D(X) over K = ℚ(√D), realized as the subgroup of Sym(Ell_𝒪(ℂ)).

@[implicit_reducible]

noncomputable instance instGroupSplittingFieldGaloisGroup (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) : Group (SplittingFieldGaloisGroup D hD)

The group structure on the Galois group Gal(L/K), inherited from Equiv.Perm.

theorem classGroupAction_transitive (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) (j₁ j₂ : ↥(CMjInvariants D hD)) : ∃ (α : ImagQuadIdealClass D hD), ((classGroupActionHom D hD) α) j₁ = j₂

Transitivity of the class group action on CM j-invariants: for any pair of CM j-invariants j₁, j₂ there is α ∈ cl(𝒪) sending j₁ to j₂.

theorem classGroupActionHom_injective (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) : Function.Injective ⇑(classGroupActionHom D hD)

The class group action homomorphism cl(𝒪) → Sym(Ell_𝒪(ℂ)) is injective. This is the freeness half of the simple transitivity of the action.

noncomputable def GalToClassGroup_fun (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) (σ : SplittingFieldGaloisGroup D hD) : ImagQuadIdealClass D hD

Underlying function Ψ_fun : Gal(L/K) → cl(𝒪) of the homomorphism Ψ appearing in Theorem 20.14: given σ ∈ Gal(L/K), pick a base CM j-invariant j₀ and define Ψ(σ) to be the unique class group element sending j₀ ↦ σ(j₀).

theorem GalToClassGroup_fun_compatible (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) (σ : SplittingFieldGaloisGroup D hD) : ↑σ = (classGroupActionHom D hD) (GalToClassGroup_fun D hD σ)

Compatibility lemma: the action of σ ∈ Gal(L/K) on Ell_𝒪(ℂ) agrees with the action of the class group element Ψ_fun(σ), not just on a single base point but as a permutation.

noncomputable def GalToClassGroup_hom (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) : SplittingFieldGaloisGroup D hD →* ImagQuadIdealClass D hD

The group homomorphism Ψ : Gal(L/K) → cl(𝒪) of Theorem 20.14, packaging GalToClassGroup_fun together with the multiplicative structure (map_one, map_mul are derived from compatibility).

theorem GalToClassGroup_compatible (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) (σ : SplittingFieldGaloisGroup D hD) : ↑σ = (classGroupActionHom D hD) ((GalToClassGroup_hom D hD) σ)

Restated compatibility through the bundled homomorphism Ψ: the action of σ on Ell_𝒪(ℂ) is the same as the action of Ψ(σ) ∈ cl(𝒪).

theorem GalToClassGroup_injective (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) : Function.Injective ⇑(GalToClassGroup_hom D hD)

Injectivity half of Theorem 20.14: the homomorphism Ψ : Gal(L/K) → cl(𝒪) is injective.

theorem hilbertClassPoly_isRoot_iff (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) (z : ℂ) : (hilbertClassPoly D hD).IsRoot z ↔ z ∈ CMjInvariants D hD

Characterization of roots of H_D: z ∈ ℂ is a root of the Hilbert class polynomial iff z ∈ Ell_𝒪(ℂ). Direct from the factored form ∏_{j} (X - j).

noncomputable def evalClassicalModularPoly (N : ℕ) (j₁ j₂ : ℂ) : ℂ

Evaluation Φ_N(j₁, j₂) of the classical modular polynomial at a pair of complex j-invariants (j₁, j₂).

def AreCyclicNIsogenous (j₁ j₂ : ℂ) (N : ℕ) : Prop

Predicate: complex j-invariants j₁, j₂ are related by a cyclic N-isogeny. Equivalently (by Theorem 20.3) one of Φ_N(j₁, j₂) = 0 characterizations.

theorem modularPoly_characterizes_cyclicIsogeny (N : ℕ) (j₁ j₂ : ℂ) : evalClassicalModularPoly N j₁ j₂ = 0 ↔ AreCyclicNIsogenous j₁ j₂ N

Theorem 20.3 (over ℂ): Φ_N(j₁, j₂) = 0 iff j₁, j₂ are the j-invariants of complex elliptic curves related by a cyclic isogeny of degree N.

theorem classicalModularPoly_symmetric (N : ℕ) (hN : 1 < N) : Polynomial.Bivariate.swap (classicalModularPoly N) = classicalModularPoly N

Theorem 20.7: the classical modular polynomial is symmetric in its two variables, i.e. Φ_N(X, Y) = Φ_N(Y, X).

theorem evalClassicalModularPoly_eq_aevalAeval (N : ℕ) (j₁ j₂ : ℂ) : evalClassicalModularPoly N j₁ j₂ = (Polynomial.aevalAeval j₁ j₂) (classicalModularPoly N)

Coercion of evalClassicalModularPoly to the aevalAeval API: both compute Φ_N(j₁, j₂) in ℂ via the same iterated evaluation, so they agree.

theorem frobeniusElement_exists (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) (α : ImagQuadIdealClass D hD) : ∃ (σ : SplittingFieldGaloisGroup D hD), ↑σ = (classGroupActionHom D hD) α

Existence of Frobenius-type elements: for every ideal class α ∈ cl(𝒪), some Galois element σ ∈ Gal(L/K) acts on Ell_𝒪(ℂ) exactly via α under the class group action. (Surjectivity of Ψ follows.)

theorem frobeniusElement_mapsTo (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) (σ : SplittingFieldGaloisGroup D hD) (α : ImagQuadIdealClass D hD) (hσ : ↑σ = (classGroupActionHom D hD) α) : (GalToClassGroup_hom D hD) σ = α

Compatibility: if σ ∈ Gal(L/K) acts as the class group element α, then Ψ(σ) = α.

theorem GalToClassGroup_surjective (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) : Function.Surjective ⇑(GalToClassGroup_hom D hD)

Surjectivity half of Theorem 20.14 / Theorem 21.1: every class group element is hit by some Galois element under Ψ : Gal(L/K) → cl(𝒪).

theorem GalToClassGroup_bijective (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) : Function.Bijective ⇑(GalToClassGroup_hom D hD)

Theorem 21.1: the homomorphism Ψ : Gal(L/K) → cl(𝒪) is a bijection.

noncomputable def GalToClassGroup_mulEquiv (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) : SplittingFieldGaloisGroup D hD ≃* ImagQuadIdealClass D hD

Theorem 21.1 (packaged): the multiplicative equivalence Gal(L/K) ≃* cl(𝒪) obtained by promoting Ψ to an iso.

theorem galoisAction_transitive_on_roots (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) (j₁ j₂ : ↥(CMjInvariants D hD)) : ∃ (σ : SplittingFieldGaloisGroup D hD), ↑σ j₁ = j₂

Galois transitivity on the roots of H_D: for any two CM j-invariants j₁, j₂, there exists σ ∈ Gal(L/K) with σ(j₁) = j₂. Follows from transitivity of the class group action together with surjectivity of Ψ.

theorem splittingFieldGaloisGroup_mul_comm (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) (σ₁ σ₂ : SplittingFieldGaloisGroup D hD) : σ₁ * σ₂ = σ₂ * σ₁

The Galois group Gal(L/K) is abelian: it is isomorphic to the ideal class group cl(𝒪), which is abelian (Corollary 21.2).

@[reducible]

noncomputable def instCommGroupSplittingFieldGaloisGroup' (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) : CommGroup (SplittingFieldGaloisGroup D hD)

The commutative-group instance on Gal(L/K): extending the group structure with commutativity proved in splittingFieldGaloisGroup_mul_comm.

theorem hilbertClassPoly_irreducible_and_abelian_galois (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) : (∀ (j₁ j₂ : ↥(CMjInvariants D hD)), ∃ (σ : SplittingFieldGaloisGroup D hD), ↑σ j₁ = j₂) ∧ ∃ (x : CommGroup (SplittingFieldGaloisGroup D hD)), Nonempty (SplittingFieldGaloisGroup D hD ≃* ImagQuadIdealClass D hD)

Corollary 21.2 (formal content): the Hilbert class polynomial H_D(X) is irreducible over K = ℚ(√D) (encoded as transitivity of the Galois action on its roots) and K(j(E))/K is a finite abelian extension with Galois group isomorphic to cl(𝒪).

noncomputable def HilbertClassPolynomial.intPoly (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) : Polynomial ℤ

Theorem 20.12 (computational form): an integer polynomial intPoly D whose image in ℂ[X] equals the Hilbert class polynomial H_D(X), and which is monic of the same degree. Chosen using Polynomial.lifts_and_natDegree_eq_and_monic.

theorem HilbertClassPolynomial.intPoly_natDegree (D : ℤ) (hD : IsImaginaryQuadraticDiscriminant D) : (intPoly D hD).natDegree = (hilbertClassPoly D hD).natDegree

The integer-coefficient form intPoly D has the same natural degree as H_D(X) (i.e. the class number h(D)).