structure IsOrder (A : Type u_1) [Ring A] [Algebra ℚ A] (O : Subring A) : Prop

A subring O of a ℚ-algebra A is an order if it is finitely generated as a ℤ-module and its ℚ-span fills A (cf. Definition 12.22 of "Elliptic Curves").

• fg_zmul : (AddSubgroup.toIntSubmodule O.toAddSubgroup).FG
• span_eq_top : Submodule.span ℚ ↑O = ⊤

theorem ringOfIntegers_isOrder (K : Type u_1) [Field K] [NumberField K] : IsOrder K (integralClosure ℤ K).toSubring

The ring of integers 𝓞_K of a number field K is an order in K (Definition 12.22 / Theorem about 𝓞_K being a free ℤ-module of rank [K:ℚ]).

def ConductorOrder.conductorOrder (d : ℤ) (f : ℕ) : Subring (ℤ√d)

The order of conductor f in ℤ[√d]: the subring consisting of all elements whose imaginary part is divisible by f.

@[simp]

theorem ConductorOrder.mem_conductorOrder_iff {d : ℤ} {f : ℕ} {z : ℤ√d} : z ∈ conductorOrder d f ↔ ↑f ∣ z.im

Membership criterion for the conductor order: z ∈ conductorOrder d f iff f divides z.im.

theorem ConductorOrder.conductorOrder_le_of_dvd {d : ℤ} {f₁ f₂ : ℕ} (h : f₂ ∣ f₁) : conductorOrder d f₁ ≤ conductorOrder d f₂

Divisibility of conductors gives a reverse inclusion of orders: if f₂ ∣ f₁ then conductorOrder d f₁ ≤ conductorOrder d f₂.

theorem ConductorOrder.conductorOrder_fg {d : ℤ} (f : ℕ) : (AddSubgroup.toIntSubmodule (conductorOrder d f).toAddSubgroup).FG

The conductor order is finitely generated as a ℤ-module, with basis {1, f·√d}.

def ConductorOrder.imAddHom (d : ℤ) : ℤ√d →+ ℤ

The "imaginary part" homomorphism ℤ[√d] →+ ℤ sending a + b√d ↦ b.

theorem ConductorOrder.intCast_mem_subring {d : ℤ} (S : Subring (ℤ√d)) (n : ℤ) : ↑n ∈ S

Every integer cast n : ℤ → ℤ[√d] lies inside any subring S of ℤ[√d].

theorem ConductorOrder.mem_subring_of_dvd_im {d : ℤ} (S : Subring (ℤ√d)) {a : ℤ} (ha : { re := 0, im := a } ∈ S) {z : ℤ√d} (hdvd : a ∣ z.im) : z ∈ S

If a subring S contains the pure-imaginary element (0, a) and a divides the imaginary part of z, then z ∈ S.

theorem ConductorOrder.conductorOrder_isOrder {d : ℤ} {f : ℕ} (hf : 0 < f) : (AddSubgroup.toIntSubmodule (conductorOrder d f).toAddSubgroup).FG ∧ ∃ z ∈ conductorOrder d f, z.im ≠ 0

The conductor order with positive conductor f satisfies the two structural conditions to be an order: finite generation as a ℤ-module, and containing an element with nonzero imaginary part.

theorem ConductorOrder.exists_conductor_of_subring {d : ℤ} (S : Subring (ℤ√d)) (hS : ∃ z ∈ S, z.im ≠ 0) : ∃ (f : ℕ), 0 < f ∧ S = conductorOrder d f

Conversely, any subring S of ℤ[√d] that contains some element with nonzero imaginary part is itself a conductor order for a unique positive integer f.

theorem ConductorOrder.orders_eq_conductorOrders {d : ℤ} (S : Subring (ℤ√d)) : ((AddSubgroup.toIntSubmodule S.toAddSubgroup).FG ∧ ∃ z ∈ S, z.im ≠ 0) ↔ ∃ (f : ℕ), 0 < f ∧ S = conductorOrder d f

Classification of orders in ℤ[√d]: a subring S is an order (finitely generated with at least one element having nonzero imaginary part) iff it equals conductorOrder d f for some positive conductor f.

def ConductorOrder.orderDiscriminant (d : ℤ) (f : ℕ) : ℤ

The discriminant of the conductor f order in ℤ[√d], defined as 4 · f² · d.

def ConductorOrder.maximalDiscriminant (d : ℤ) : ℤ

The discriminant of the maximal order in ℤ[√d] (conductor 1), which is 4d.

def IsQuaternionAlgebra (k : Type u_1) [Field k] (H : Type u_2) [Ring H] [Algebra k H] : Prop

A k-algebra H is a quaternion algebra (Definition 12.12) if it has a basis of the form {1, α, β, αβ} with α², β² ∈ k× and αβ = -βα, equivalently encoded here via the existence of anticommuting elements with nonzero scalar squares and finrank k H = 4.

@[reducible, inline]

abbrev QAlgebra (k : Type u_1) [Field k] (a b : k) : a ≠ 0 → b ≠ 0 → Type u_1

Convenient abbreviation for the quaternion algebra ℍ[k, a, b] with both nonvanishing parameters a, b ∈ k×.

@[reducible, inline]

abbrev qI {k : Type u_1} [Field k] (a b : k) : QuaternionAlgebra k a 0 b

The standard basis element i of the quaternion algebra ℍ[k, a, b].

@[reducible, inline]

abbrev qJ {k : Type u_1} [Field k] (a b : k) : QuaternionAlgebra k a 0 b

The standard basis element j of the quaternion algebra ℍ[k, a, b].

@[reducible, inline]

abbrev qK {k : Type u_1} [Field k] (a b : k) : QuaternionAlgebra k a 0 b

The standard basis element k = i·j of the quaternion algebra ℍ[k, a, b].

theorem qI_mul_qI {k : Type u_1} [Field k] (a b : k) : qI a b * qI a b = ↑a

In ℍ[k, a, b], i² = a.

theorem qJ_mul_qJ {k : Type u_1} [Field k] (a b : k) : qJ a b * qJ a b = ↑b

In ℍ[k, a, b], j² = b.

theorem qI_mul_qJ {k : Type u_1} [Field k] (a b : k) : qI a b * qJ a b = qK a b

In ℍ[k, a, b], i · j = k.

theorem qJ_mul_qI {k : Type u_1} [Field k] (a b : k) : qJ a b * qI a b = -qK a b

In ℍ[k, a, b], j · i = -k.

theorem qI_mul_qJ_eq_neg_qJ_mul_qI {k : Type u_1} [Field k] (a b : k) : qI a b * qJ a b = -(qJ a b * qI a b)

The defining anticommutation relation i · j = -(j · i) in ℍ[k, a, b].

@[implicit_reducible]

instance instRingQuaternionAlgebraOfNat_atlas {k : Type u_1} [Field k] (a b : k) : Ring (QuaternionAlgebra k a 0 b)

Synonym: ℍ[k, a, b] is a ring (recorded for use later).

@[implicit_reducible]

instance instAlgebraQuaternionAlgebraOfNat_atlas {k : Type u_1} [Field k] (a b : k) : Algebra k (QuaternionAlgebra k a 0 b)

Synonym: ℍ[k, a, b] is a k-algebra.

theorem finrank_eq_four {k : Type u_1} [Field k] (a b : k) : Module.finrank k (QuaternionAlgebra k a 0 b) = 4

A quaternion algebra has k-dimension exactly 4 (cf. Definition 12.12).

def reducedTrace {k : Type u_2} [Field k] (a b : k) (γ : QuaternionAlgebra k a 0 b) : k

The reduced trace T γ = 2 · Re γ on the quaternion algebra ℍ[k, a, b] (Definition 12.6).

theorem reducedTrace_mk {k : Type u_2} [Field k] (a b r x y z : k) : reducedTrace a b { re := r, imI := x, imJ := y, imK := z } = 2 * r

The reduced trace of a quaternion ⟨r, x, y, z⟩ equals 2r.

theorem reducedTrace_coe {k : Type u_1} [Field k] (a b c : k) : reducedTrace a b ↑c = 2 * c

The reduced trace of a scalar c : k, viewed in ℍ[k, a, b], equals 2c.

noncomputable def basis {k : Type u_1} [Field k] (a b : k) : Module.Basis (Fin 4) k (QuaternionAlgebra k a 0 b)

The standard k-basis {1, i, j, k} of the quaternion algebra ℍ[k, a, b].

def quatBasis {k : Type u_1} [Field k] (a b : k) : QuaternionAlgebra.Basis (QuaternionAlgebra k a 0 b) a 0 b

The packaged QuaternionAlgebra.Basis structure for ℍ[k, a, b] itself.

theorem basis_i_mul_i {k : Type u_1} [Field k] (a b : k) : (quatBasis a b).i * (quatBasis a b).i = a • 1 + 0 • (quatBasis a b).i

Basis identity: i² = a·1 + 0·i in ℍ[k, a, b].

theorem basis_j_mul_j {k : Type u_1} [Field k] (a b : k) : (quatBasis a b).j * (quatBasis a b).j = b • 1

Basis identity: j² = b·1 in ℍ[k, a, b].

theorem basis_i_mul_j {k : Type u_1} [Field k] (a b : k) : (quatBasis a b).i * (quatBasis a b).j = (quatBasis a b).k

Basis identity: i · j = k in ℍ[k, a, b].

theorem basis_j_mul_i {k : Type u_1} [Field k] (a b : k) : (quatBasis a b).j * (quatBasis a b).i = 0 • (quatBasis a b).j - (quatBasis a b).k

Basis identity: j · i = 0·j - k = -k in ℍ[k, a, b].

theorem hamilton_eq : Quaternion ℝ = QuaternionAlgebra ℝ (-1) 0 (-1)

The classical Hamilton quaternions ℍ are defeq to ℍ[ℝ, -1, -1].

theorem hamilton_i_sq : qI (-1) (-1) * qI (-1) (-1) = -1

In Hamilton's quaternions, i² = -1.

theorem hamilton_j_sq : qJ (-1) (-1) * qJ (-1) (-1) = -1

In Hamilton's quaternions, j² = -1.

theorem hamilton_ij_eq_neg_ji : qI (-1) (-1) * qJ (-1) (-1) = -(qJ (-1) (-1) * qI (-1) (-1))

In Hamilton's quaternions, i · j = -(j · i).

theorem hamilton_finrank : Module.finrank ℝ (Quaternion ℝ) = 4

Hamilton's quaternions have ℝ-dimension 4.

theorem hamilton_not_commutative : ¬∀ (a b : Quaternion ℝ), a * b = b * a

Hamilton's quaternions are not commutative: i · j ≠ j · i.

def reducedNorm {k : Type u_2} [Field k] (a b : k) (γ : QuaternionAlgebra k a 0 b) : k

The reduced norm N γ = (γ · γ̄).re on the quaternion algebra ℍ[k, a, b] (Definition 12.6).

theorem reducedNorm_mk {k : Type u_2} [Field k] (a b r x y z : k) : reducedNorm a b { re := r, imI := x, imJ := y, imK := z } = r * r - a * (x * x) - b * (y * y) + a * b * (z * z)

Explicit formula: N ⟨r, x, y, z⟩ = r² - a x² - b y² + a b z².

theorem mul_star_eq_algebraMap_reducedNorm {k : Type u_2} [Field k] (a b : k) (γ : QuaternionAlgebra k a 0 b) : γ * star γ = (algebraMap k (QuaternionAlgebra k a 0 b)) (reducedNorm a b γ)

The product γ · γ̄ equals the scalar (N γ) viewed in ℍ[k, a, b].

theorem star_mul_eq_algebraMap_reducedNorm {k : Type u_2} [Field k] (a b : k) (γ : QuaternionAlgebra k a 0 b) : star γ * γ = (algebraMap k (QuaternionAlgebra k a 0 b)) (reducedNorm a b γ)

The product γ̄ · γ also equals the scalar (N γ).

instance quatAlg_nontrivial {k : Type u_2} [Field k] (a b : k) : Nontrivial (QuaternionAlgebra k a 0 b)

Every quaternion algebra ℍ[k, a, b] is nontrivial.

theorem isDivisionRing_iff_norm_anisotropic {k : Type u_2} [Field k] (a b : k) : (∀ (γ : QuaternionAlgebra k a 0 b), reducedNorm a b γ = 0 → γ = 0) ↔ ∀ (γ : QuaternionAlgebra k a 0 b), γ ≠ 0 → IsUnit γ

Lemma 12.13: a quaternion algebra is a division ring iff its reduced norm is anisotropic, i.e. N γ = 0 ⇒ γ = 0.

@[reducible]

noncomputable def toDivisionRing {k : Type u_2} [Field k] (a b : k) (h : ∀ (γ : QuaternionAlgebra k a 0 b), reducedNorm a b γ = 0 → γ = 0) : DivisionRing (QuaternionAlgebra k a 0 b)

Promote a quaternion algebra ℍ[k, a, b] with anisotropic reduced norm to a DivisionRing, by inverting nonzero elements via the conjugate.

theorem algebraMap_mul_eq_smul {R : Type u_1} {K : Type u_2} [CommRing R] [Field K] [Algebra R K] (r : R) (k : K) : (algebraMap R K) r * k = r • k

Algebra-map multiplication coincides with scalar action: (algebraMap R K) r * k = r • k.

theorem TensorProduct.exists_tmul_inv_algebraMap {R : Type u_1} [CommRing R] [IsDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {A : Type u_3} [AddCommGroup A] [Module R A] (x : TensorProduct R A K) : ∃ (a : A) (s : ↥(nonZeroDivisors R)), x = a ⊗ₜ[R] ((algebraMap R K) ↑s)⁻¹

A key step in Lemma 12.5: every element of A ⊗_R K, where K = Frac R, can be written as a ⊗ ((algebraMap R K) s)⁻¹ for some a ∈ A and s ∈ R⁰.

theorem TensorProduct.exists_pure_tensor_fractionRing {R : Type u_1} [CommRing R] [IsDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {A : Type u_3} [AddCommGroup A] [Module R A] (x : TensorProduct R A K) : ∃ (a : A) (b : K), x = a ⊗ₜ[R] b

Lemma 12.5: every element of A ⊗_R K (where K = Frac R) can be written as a single pure tensor a ⊗ b.

theorem TensorProduct.exists_pure_tensor_int_rat {M : Type u_1} [AddCommGroup M] [Module ℤ M] (x : TensorProduct ℤ M ℚ) : ∃ (m : M) (n : ℤ), n ≠ 0 ∧ x = m ⊗ₜ[ℤ] (↑n)⁻¹

Specialization of Lemma 12.5 to R = ℤ, K = ℚ: every element of M ⊗_ℤ ℚ is a pure tensor m ⊗ n⁻¹ with n ∈ ℤ \ {0}.

noncomputable def IsogenyEndRing {F : Type v} [Field F] [DecidableEq F] (E : WeierstrassCurve.Affine F) : Subring (EndRing E)

The subring of "isogeny endomorphisms" of E inside the full endomorphism ring; this is the subring relevant for Corollary 12.20.

theorem IsogenyEndRing_torsionFree {F : Type v} [Field F] [DecidableEq F] (E : WeierstrassCurve.Affine F) : Module.IsTorsionFree ℤ ↥(IsogenyEndRing E)

The isogeny endomorphism ring of E is torsion-free as a ℤ-module, a step in proving it is a free ℤ-module of rank 1, 2 or 4.

theorem IsogenyEndRing_finite {F : Type v} [Field F] [DecidableEq F] (E : WeierstrassCurve.Affine F) : Module.Finite ℤ ↥(IsogenyEndRing E)

The isogeny endomorphism ring of E is a finitely generated ℤ-module (Corollary 12.20).

theorem IsogenyEndRing_finrank_mem {F : Type v} [Field F] [DecidableEq F] (E : WeierstrassCurve.Affine F) : Module.finrank ℤ ↥(IsogenyEndRing E) ∈ {1, 2, 4}

The ℤ-rank of the isogeny endomorphism ring of E is one of 1, 2, or 4 (Corollary 12.20).

instance IsogenyEndRing_free {F : Type v} [Field F] [DecidableEq F] (E : WeierstrassCurve.Affine F) : Module.Free ℤ ↥(IsogenyEndRing E)

The isogeny endomorphism ring of E is a free ℤ-module, derived from torsion- freeness and finite generation.

theorem IsogenyEndRing_free_rank_1_2_or_4 {F : Type v} [Field F] [DecidableEq F] (E : WeierstrassCurve.Affine F) : Module.Free ℤ ↥(IsogenyEndRing E) ∧ (Module.finrank ℤ ↥(IsogenyEndRing E) = 1 ∨ Module.finrank ℤ ↥(IsogenyEndRing E) = 2 ∨ Module.finrank ℤ ↥(IsogenyEndRing E) = 4)

Corollary 12.20: the endomorphism ring End(E) is a free ℤ-module of rank r ∈ {1, 2, 4}, the dimension of End⁰(E) over ℚ.

def WeierstrassCurve.Affine.HasCM {F : Type w} [Field F] [DecidableEq F] (E : Affine F) : Prop

Definition 12.21: an elliptic curve E has complex multiplication if End(E) ≇ ℤ.