structure Multigraph (V : Type u_1) : Type u_1

A multigraph on vertex set V: each unordered pair (v, w) carries a multiplicity edgeMult v w : ℕ, required to be symmetric in v, w.

• edgeMult : V → V → ℕ
• symm (v w : V) : self.edgeMult v w = self.edgeMult w v

def Multigraph.Adj {V : Type u_1} (G : Multigraph V) (v w : V) : Prop

Two vertices v, w are adjacent in G iff their edge multiplicity is positive.

def Multigraph.degree {V : Type u_1} (G : Multigraph V) [Fintype V] (v : V) : ℕ

The (multi)degree of a vertex v: the sum of edge multiplicities to all vertices of V.

def Multigraph.degreeOn {V : Type u_1} (G : Multigraph V) [Fintype V] (v : V) (P : V → Prop) [DecidablePred P] : ℕ

The partial degree of v restricted to neighbours satisfying the predicate P.

def Multigraph.Connected {V : Type u_1} (G : Multigraph V) (v w : V) : Prop

v and w are connected in G iff there is a finite path (a reflexive- transitive closure of adjacency) from v to w.

def Multigraph.IsConnected {V : Type u_1} (G : Multigraph V) : Prop

The multigraph G is connected iff every pair of vertices is connected.

theorem Multigraph.degreeOn_compl {V : Type u_1} (G : Multigraph V) [Fintype V] (v : V) (P : V → Prop) [DecidablePred P] : G.degree v = G.degreeOn v P + G.degreeOn v fun (w : V) => ¬P w

The total degree decomposes as the partial degree over P plus the partial degree over ¬P.

theorem Multigraph.degreeOn_congr {V : Type u_1} (G : Multigraph V) [Fintype V] (v : V) (P Q : V → Prop) [DecidablePred P] [DecidablePred Q] (h : ∀ (w : V), G.edgeMult v w > 0 → (P w ↔ Q w)) : G.degreeOn v P = G.degreeOn v Q

Two predicates P, Q that agree on all neighbours of v (vertices with positive edge multiplicity) give the same partial degree at v.

noncomputable def modularPolynomialSpec (k : Type u_1) [CommRing k] (ℓ : ℕ) (j₁ : k) : Polynomial k

The classical modular polynomial Φ_ℓ(X, Y) specialized to Y = j₁: a univariate polynomial in X over k whose roots over an algebraic closure are the j-invariants of elliptic curves ℓ-isogenous to a curve with j-invariant j₁.

noncomputable def IsogenyGraph.edgeMult (k : Type u_1) [CommRing k] (ℓ : ℕ) (j₁ j₂ : k) : ℕ

The multiplicity of j₂ as a root of Φ_ℓ(j₁, Y), equal to the number of ℓ-isogenies (with multiplicity) from a curve with j-invariant j₁ to one with j-invariant j₂.

def IsogenyGraph.hasEdge (k : Type u_1) [CommRing k] (ℓ : ℕ) (j₁ j₂ : k) : Prop

There is an edge from j₁ to j₂ in the ℓ-isogeny graph iff j₂ is a root of the modular polynomial Φ_ℓ(j₁, Y).

@[reducible, inline]

abbrev IsogenyGraph.𝔽_p_jInvariants (p : ℕ) : Type

The set of possible j-invariants over 𝔽_p, identified with ZMod p.

theorem IsogenyGraph.modularPolynomial_symm_edge (k : Type u_1) [CommRing k] (ℓ : ℕ) (j₁ j₂ : k) : hasEdge k ℓ j₁ j₂ → hasEdge k ℓ j₂ j₁

Edges in the ℓ-isogeny graph are symmetric: an ℓ-isogeny from j₁ to j₂ gives rise to a dual ℓ-isogeny from j₂ to j₁.

def IsogenyGraph.isogenyGraph (p ℓ : ℕ) [Fact (Nat.Prime p)] [Fact (Nat.Prime ℓ)] (_hne : p ≠ ℓ) : SimpleGraph (𝔽_p_jInvariants p)

The ℓ-isogeny graph over 𝔽_p as a SimpleGraph on j-invariants (Definition 22.1): two distinct j-values are adjacent iff there is an ℓ-isogeny between them.

noncomputable def IsogenyGraph.isogenyGraph_locallyFinite (p ℓ : ℕ) [Fact (Nat.Prime p)] [Fact (Nat.Prime ℓ)] (hne : p ≠ ℓ) : (isogenyGraph p ℓ hne).LocallyFinite

The ℓ-isogeny graph over 𝔽_p is locally finite.

theorem IsogenyGraph.isogenyGraph_regular (p ℓ : ℕ) [Fact (Nat.Prime p)] [Fact (Nat.Prime ℓ)] (hne : p ≠ ℓ) : (isogenyGraph p ℓ hne).IsRegularOfDegree (ℓ + 1)

The ℓ-isogeny graph over 𝔽_p is regular of degree ℓ + 1: every vertex has exactly ℓ + 1 outgoing ℓ-isogenies (counted with multiplicity).

@[simp]

theorem IsogenyGraph.isogenyGraph_adj {p ℓ : ℕ} [Fact (Nat.Prime p)] [Fact (Nat.Prime ℓ)] {hne : p ≠ ℓ} {j₁ j₂ : 𝔽_p_jInvariants p} : (isogenyGraph p ℓ hne).Adj j₁ j₂ ↔ j₁ ≠ j₂ ∧ hasEdge (ZMod p) ℓ j₁ j₂

The defining adjacency relation of the ℓ-isogeny graph: j₁ and j₂ are adjacent iff they are distinct and there is an edge between them.

structure IsogenyVolcano (ℓ : ℕ) : Type (u_1 + 1)

An ℓ-volcano: a connected multigraph organized into levels (the surface is level 0, the floor is level depth). Vertices off the floor have degree ℓ + 1, surface vertices have a prescribed surface degree (≤ 2), and non-surface vertices have a unique parent at the level above. Edges can only join the surface to itself or adjacent levels.

• V : Type u_1
• instFintype : Fintype self.V
• instDecEq : DecidableEq self.V
• graph : Multigraph self.V
• depth : ℕ
• level : self.V → Fin (self.depth + 1)
• level_surj : Function.Surjective self.level
• surfaceDegree : ℕ
• surfaceDegree_le : self.surfaceDegree ≤ 2
• surface_regular (v : self.V) : self.level v = ⟨0, ⋯⟩ → (self.graph.degreeOn v fun (w : self.V) => self.level w = ⟨0, ⋯⟩) = self.surfaceDegree
• unique_parent (v : self.V) : ↑(self.level v) > 0 → (self.graph.degreeOn v fun (w : self.V) => ↑(self.level w) + 1 = ↑(self.level v)) = 1
• edges_between_levels (v w : self.V) : self.graph.edgeMult v w > 0 → ↑(self.level v) = 0 ∧ ↑(self.level w) = 0 ∨ ↑(self.level w) + 1 = ↑(self.level v) ∨ ↑(self.level v) + 1 = ↑(self.level w)
• degree_eq (v : self.V) : ↑(self.level v) < self.depth → self.graph.degree v = ℓ + 1
• connected : self.graph.IsConnected

def IsogenyVolcano.isSurface {ℓ : ℕ} (vol : IsogenyVolcano ℓ) (v : vol.V) : Prop

A vertex of the volcano is on the surface (or crater) iff its level is 0.

def IsogenyVolcano.isFloor {ℓ : ℕ} (vol : IsogenyVolcano ℓ) (v : vol.V) : Prop

A vertex of the volcano is on the floor iff its level is the maximal one (depth).

def IsogenyVolcano.volcanoDepth {ℓ : ℕ} (vol : IsogenyVolcano ℓ) : ℕ

The depth of the volcano (the maximal level index).

def IsogenyVolcano.IsHorizontalEdge {ℓ : ℕ} (vol : IsogenyVolcano ℓ) (v w : vol.V) : Prop

An edge (v, w) is horizontal iff it has positive multiplicity and both endpoints lie on the surface.

def IsogenyVolcano.IsDescendingEdge {ℓ : ℕ} (vol : IsogenyVolcano ℓ) (v w : vol.V) : Prop

An edge (v, w) is descending iff w is one level below v (level v + 1 = level w).

def IsogenyVolcano.IsAscendingEdge {ℓ : ℕ} (vol : IsogenyVolcano ℓ) (v w : vol.V) : Prop

An edge (v, w) is ascending iff w is one level above v (level w + 1 = level v).

def IsogenyVolcano.IsVerticalEdge {ℓ : ℕ} (vol : IsogenyVolcano ℓ) (v w : vol.V) : Prop

An edge is vertical iff it is either descending or ascending.

theorem IsogenyVolcano.descending_iff_ascending_symm {ℓ : ℕ} (vol : IsogenyVolcano ℓ) (v w : vol.V) : vol.IsDescendingEdge v w ↔ vol.IsAscendingEdge w v

An edge (v, w) is descending iff the reverse edge (w, v) is ascending.

theorem IsogenyVolcano.ascending_iff_descending_symm {ℓ : ℕ} (vol : IsogenyVolcano ℓ) (v w : vol.V) : vol.IsAscendingEdge v w ↔ vol.IsDescendingEdge w v

An edge (v, w) is ascending iff the reverse edge (w, v) is descending.

theorem CMConductorTrichotomy.coprime_dvd_prime {ℓ a b : ℕ} (hℓ : Nat.Prime ℓ) (hab : a.Coprime b) (ha : a ∣ ℓ) (hb : b ∣ ℓ) : a = 1 ∧ b = 1 ∨ a = 1 ∧ b = ℓ ∨ a = ℓ ∧ b = 1

If two coprime natural numbers a, b both divide a prime ℓ, then either both are 1, or one is 1 and the other is ℓ.

theorem CMConductorTrichotomy.isogeny_order_trichotomy {ℓ : ℕ} (hℓ : Nat.Prime ℓ) {f f' : ℕ} (hf : 0 < f) (h1 : f ∣ ℓ * f') (h2 : f' ∣ ℓ * f) : f = f' ∨ f = ℓ * f' ∨ f' = ℓ * f

Conductor trichotomy for ℓ-isogenies: if conductors f, f' satisfy f ∣ ℓ f' and f' ∣ ℓ f, then f = f' (horizontal), f = ℓ f' (ascending), or f' = ℓ f (descending). Encodes the index relation behind Theorem 22.3.

inductive CMConductorTrichotomy.IsogenyType : Type

Classification (Definition 22.4) of an ℓ-isogeny between CM elliptic curves by the relation between the source and target endomorphism orders: horizontal (𝒪 = 𝒪''), descending ([𝒪 : 𝒪''] = ℓ), or ascending ([𝒪'' : 𝒪] = ℓ).

• horizontal : IsogenyType
• descending : IsogenyType
• ascending : IsogenyType

@[implicit_reducible]

instance CMConductorTrichotomy.instDecidableEqIsogenyType : DecidableEq IsogenyType

def CMConductorTrichotomy.classifyIsogeny (ℓ f f' : ℕ) : IsogenyType

Classify an ℓ-isogeny by comparing source conductor f and target conductor f': f = f' is horizontal, f = ℓ f' is descending, otherwise ascending.

theorem CMConductorTrichotomy.classifyIsogeny_horizontal {ℓ f f' : ℕ} (h : f = f') : classifyIsogeny ℓ f f' = IsogenyType.horizontal

If f = f' then the isogeny is classified as horizontal.

theorem CMConductorTrichotomy.classifyIsogeny_descending {ℓ : ℕ} (hℓ : 1 < ℓ) {f f' : ℕ} (hf' : 0 < f') (h : f = ℓ * f') : classifyIsogeny ℓ f f' = IsogenyType.descending

If f = ℓ f' (with f' > 0 and ℓ > 1), the isogeny is classified as descending.

theorem CMConductorTrichotomy.classifyIsogeny_ascending {ℓ : ℕ} (hℓ : 1 < ℓ) {f f' : ℕ} (hf : 0 < f) (h : f' = ℓ * f) : classifyIsogeny ℓ f f' = IsogenyType.ascending

If f' = ℓ f (with f > 0 and ℓ > 1), the isogeny is classified as ascending.

def IsogenyVolcano.craterGraph {ℓ : ℕ} (vol : IsogenyVolcano ℓ) : Multigraph vol.V

The crater (surface) subgraph of an isogeny volcano: the multigraph induced on the surface (level 0) vertices, keeping only edges that lie entirely on the surface.

theorem IsogenyVolcano.crater_degree_surface {ℓ : ℕ} (vol : IsogenyVolcano ℓ) (v : vol.V) (hv : vol.level v = ⟨0, ⋯⟩) : vol.craterGraph.degree v = vol.surfaceDegree

For a surface vertex v, its degree in the crater subgraph equals the volcano's surfaceDegree.

theorem IsogenyVolcano.crater_is_regular {ℓ : ℕ} (vol : IsogenyVolcano ℓ) (v w : vol.V) : vol.isSurface v → vol.isSurface w → vol.craterGraph.degree v = vol.craterGraph.degree w

The crater subgraph is regular when restricted to surface vertices: any two surface vertices have the same crater-degree.

theorem IsogenyVolcano.crater_degree_le_two {ℓ : ℕ} (vol : IsogenyVolcano ℓ) (v : vol.V) (hv : vol.isSurface v) : vol.craterGraph.degree v ≤ 2

Surface vertices have crater-degree at most 2, reflecting the surface-degree bound ≤ 2.

theorem IsogenyVolcano.nonsurface_edges_adjacent {ℓ : ℕ} (vol : IsogenyVolcano ℓ) (v : vol.V) (hv : ↑(vol.level v) > 0) (w : vol.V) (hw : vol.graph.edgeMult v w > 0) : ↑(vol.level w) + 1 = ↑(vol.level v) ∨ ↑(vol.level v) + 1 = ↑(vol.level w)

For a non-surface vertex v, every neighbour w is either one level above or one level below v — there are no horizontal edges away from the surface.

theorem IsogenyVolcano.nonsurface_not_ascending_iff_descending {ℓ : ℕ} (vol : IsogenyVolcano ℓ) (v : vol.V) (hv : ↑(vol.level v) > 0) (w : vol.V) (hw : vol.graph.edgeMult v w > 0) : ¬↑(vol.level w) + 1 = ↑(vol.level v) ↔ ↑(vol.level v) + 1 = ↑(vol.level w)

For a non-surface vertex v with neighbour w, not being an ascending edge is equivalent to being a descending edge.

theorem IsogenyVolcano.nonsurface_descending_degree {ℓ : ℕ} (vol : IsogenyVolcano ℓ) (v : vol.V) (hv_pos : ↑(vol.level v) > 0) (hv_lt : ↑(vol.level v) < vol.depth) : (vol.graph.degreeOn v fun (w : vol.V) => ↑(vol.level v) + 1 = ↑(vol.level w)) = ℓ

For a non-surface vertex v strictly above the floor, the descending degree equals ℓ: there are exactly ℓ descending edges.

theorem IsogenyVolcano.surface_descending_degree {ℓ : ℕ} (vol : IsogenyVolcano ℓ) (v : vol.V) (hv : vol.isSurface v) (hd : 0 < vol.depth) : (vol.graph.degreeOn v fun (w : vol.V) => ¬vol.level w = ⟨0, ⋯⟩) = ℓ + 1 - vol.surfaceDegree

For a surface vertex v (when the volcano has positive depth), the number of edges leaving the surface equals ℓ + 1 - surfaceDegree.

theorem IsogenyVolcano.level_val_eq_zero_of_depth_zero {ℓ : ℕ} (vol : IsogenyVolcano ℓ) (hd : vol.depth = 0) (v : vol.V) : ↑(vol.level v) = 0

If the volcano has depth 0, every vertex has level value 0.

theorem IsogenyVolcano.floor_nonascending_degree_eq_zero {ℓ : ℕ} (vol : IsogenyVolcano ℓ) (v : vol.V) (hv : ↑(vol.level v) = vol.depth) (hd : 0 < vol.depth) : (vol.graph.degreeOn v fun (w : vol.V) => ¬↑(vol.level w) + 1 = ↑(vol.level v)) = 0

For a floor vertex (level equal to depth, with positive depth), the number of non-ascending edges is 0: floor vertices have only their unique ascending edge.

theorem IsogenyVolcano.floor_degree_eq_one {ℓ : ℕ} (vol : IsogenyVolcano ℓ) (v : vol.V) (hv : ↑(vol.level v) = vol.depth) (hd : 0 < vol.depth) : vol.graph.degree v = 1

A floor vertex of a positive-depth volcano has total degree exactly 1 — its single edge being the ascending one.

theorem IsogenyVolcano.degree_eq_surfaceDegree_of_depth_zero {ℓ : ℕ} (vol : IsogenyVolcano ℓ) (hd : vol.depth = 0) (v : vol.V) : vol.graph.degree v = vol.surfaceDegree

For a depth-zero volcano (no non-surface levels) every vertex has total degree equal to the surface degree.

theorem IsogenyVolcano.lemma_22_13 {ℓ : ℕ} (vol : IsogenyVolcano ℓ) (v : vol.V) : vol.graph.degree v ≤ 2 ∧ vol.isFloor v ∨ vol.graph.degree v = ℓ + 1 ∧ ¬vol.isFloor v

Lemma 22.13: for any vertex v in an ordinary component of depth d of G_ℓ(𝔽_q), either deg v ≤ 2 and v is on the floor, or deg v = ℓ + 1 and v is not on the floor.

structure CMIsogeny.CMIsogenyData : Type

Data attached to a CM ℓ-isogeny problem: an imaginary quadratic discriminant D < 0, a prime ℓ, and a positive conductor f of the source order.

• D : ℤ
• hD_neg : self.D < 0
• ℓ : ℕ
• hℓ_prime : Nat.Prime self.ℓ
• f : ℕ
• hf_pos : 0 < self.f

structure CMIsogeny.SurfaceIsogenyCounts (C : CMIsogenyData) : Type

Counts of ℓ-isogenies from a surface (ℓ ∤ f) CM elliptic curve, organized by type. Following Theorem 22.5, there are 1 + (D/ℓ) horizontal, ℓ - (D/ℓ) descending, and 0 ascending isogenies.

• hℓ_ndvd_f : ¬C.ℓ ∣ C.f
• numHorizontal : ℕ
• numDescending : ℕ
• numAscending : ℕ
• horizontal_eq : ↑self.numHorizontal = 1 + jacobiSym C.D C.ℓ
• descending_eq : ↑self.numDescending = ↑C.ℓ - jacobiSym C.D C.ℓ
• ascending_eq : self.numAscending = 0

structure CMIsogeny.NonSurfaceIsogenyCounts (C : CMIsogenyData) : Type

Counts of ℓ-isogenies from a non-surface (ℓ ∣ f) CM elliptic curve: 0 horizontal, ℓ descending, and 1 ascending.

• hℓ_dvd_f : C.ℓ ∣ C.f
• numHorizontal : ℕ
• numDescending : ℕ
• numAscending : ℕ
• horizontal_eq : self.numHorizontal = 0
• descending_eq : self.numDescending = C.ℓ
• ascending_eq : self.numAscending = 1

noncomputable def CMIsogeny.surface_isogeny_counts (C : CMIsogenyData) (hndvd : ¬C.ℓ ∣ C.f) : SurfaceIsogenyCounts C

Existence (with values prescribed by Theorem 22.5) of the surface isogeny counts when ℓ ∤ f.

noncomputable def CMIsogeny.nonsurface_isogeny_counts (C : CMIsogenyData) (hdvd : C.ℓ ∣ C.f) : NonSurfaceIsogenyCounts C

Existence of the non-surface isogeny counts when ℓ ∣ f.

theorem CMIsogeny.cm_isogeny_count_by_type (C : CMIsogenyData) : (¬C.ℓ ∣ C.f → ∃ (h : ℕ) (d : ℕ) (a : ℕ), ↑h = 1 + jacobiSym C.D C.ℓ ∧ ↑d = ↑C.ℓ - jacobiSym C.D C.ℓ ∧ a = 0) ∧ (C.ℓ ∣ C.f → ∃ (h : ℕ) (d : ℕ) (a : ℕ), h = 0 ∧ d = C.ℓ ∧ a = 1)

Combined statement of the CM isogeny count by type (Theorem 22.5 / Definition 22.4): the case analysis on ℓ ∣ f produces either the surface counts (when ℓ ∤ f) or the non-surface counts (when ℓ ∣ f).

theorem CMIsogeny.surface_total_count (C : CMIsogenyData) (S : SurfaceIsogenyCounts C) : ↑S.numHorizontal + ↑S.numDescending + ↑S.numAscending = ↑C.ℓ + 1

Total ℓ-isogeny count from a surface CM curve sums to ℓ + 1.

theorem CMIsogeny.nonsurface_total_count (C : CMIsogenyData) (N : NonSurfaceIsogenyCounts C) : ↑N.numHorizontal + ↑N.numDescending + ↑N.numAscending = ↑C.ℓ + 1

Total ℓ-isogeny count from a non-surface CM curve sums to ℓ + 1.

structure VolcanoStructure.OrdinaryIsogenyComponent : Type

Data for an ordinary component of the ℓ-isogeny graph over 𝔽_q: a prime ℓ coprime to q, the Hasse trace t (with t² < 4q), a fundamental imaginary quadratic discriminant D₀, a positive base conductor f₀, and the class number.

• q : ℕ
• ℓ : ℕ
• hℓ_prime : Nat.Prime self.ℓ
• hℓ_ndvd_q : ¬self.ℓ ∣ self.q
• t : ℤ
• hHasse : self.t ^ 2 < 4 * ↑self.q
• D₀ : ℤ
• hD₀_neg : self.D₀ < 0
• f₀ : ℕ
• hf₀_pos : 0 < self.f₀
• classOrder : ℕ
• hClassOrder_pos : 0 < self.classOrder

structure VolcanoStructure.KohelVolcano (C : OrdinaryIsogenyComponent) : Type 1

Kohel's structural data for an ordinary ℓ-volcano: an IsogenyVolcano of prime degree ℓ, equipped with a conductor function f₀ · ℓ^level on vertices, crater data tied to the Kronecker symbol (D₀/ℓ), and the depth-determining equation 4q = t² - ℓ^{2d} v² D₀.

• volcano : IsogenyVolcano C.ℓ
• conductor : self.volcano.V → ℕ
• conductor_eq_level (v : self.volcano.V) : self.conductor v = C.f₀ * C.ℓ ^ ↑(self.volcano.level v)
• surface_degree_eq : ↑self.volcano.surfaceDegree = 1 + jacobiSym C.D₀ C.ℓ
• surface_size_nonneg : 0 ≤ jacobiSym C.D₀ C.ℓ → Fintype.card { v : self.volcano.V // ↑(self.volcano.level v) = 0 } = C.classOrder
• surface_size_neg : jacobiSym C.D₀ C.ℓ = -1 → Fintype.card { v : self.volcano.V // ↑(self.volcano.level v) = 0 } = 1
• v_aux : ℤ
• depth_eq : 4 * ↑C.q = C.t ^ 2 - ↑C.ℓ ^ (2 * self.volcano.depth) * self.v_aux ^ 2 * C.D₀
• hℓ_ndvd_v : ¬↑C.ℓ ∣ self.v_aux
• hℓ_ndvd_f₀ : ¬C.ℓ ∣ C.f₀
• index_step (i : ℕ) : i < self.volcano.depth → ∀ (v w : self.volcano.V), ↑(self.volcano.level v) = i → ↑(self.volcano.level w) = i + 1 → self.conductor w = C.ℓ * self.conductor v

noncomputable def VolcanoStructure.ordinary_component_volcano (C : OrdinaryIsogenyComponent) : IsogenyVolcano C.ℓ

The underlying ℓ-volcano structure on the ordinary component (existence statement; the construction is left as a sorry).

theorem VolcanoStructure.ordinary_component_surface_degree_eq (C : OrdinaryIsogenyComponent) : ↑(ordinary_component_volcano C).surfaceDegree = 1 + jacobiSym C.D₀ C.ℓ

The surface degree of the ordinary component volcano equals 1 + (D₀/ℓ) (Theorem 22.11).

theorem VolcanoStructure.ordinary_component_surface_size_nonneg (C : OrdinaryIsogenyComponent) : 0 ≤ jacobiSym C.D₀ C.ℓ → Fintype.card { v : (ordinary_component_volcano C).V // ↑((ordinary_component_volcano C).level v) = 0 } = C.classOrder

Surface size formula (split/ramified case): when (D₀/ℓ) ≥ 0, the surface has size equal to the class number / class order.

theorem VolcanoStructure.ordinary_component_surface_size_neg (C : OrdinaryIsogenyComponent) : jacobiSym C.D₀ C.ℓ = -1 → Fintype.card { v : (ordinary_component_volcano C).V // ↑((ordinary_component_volcano C).level v) = 0 } = 1

Surface size formula (inert case): when (D₀/ℓ) = -1, the surface consists of a single vertex.

noncomputable def VolcanoStructure.ordinary_component_v_aux (C : OrdinaryIsogenyComponent) : ℤ

The auxiliary integer v appearing in the depth-determining norm equation 4q = t² - ℓ^{2d} v² D₀.

theorem VolcanoStructure.ordinary_component_depth_eq (C : OrdinaryIsogenyComponent) : 4 * ↑C.q = C.t ^ 2 - ↑C.ℓ ^ (2 * (ordinary_component_volcano C).depth) * ordinary_component_v_aux C ^ 2 * C.D₀

The depth equation tying the trace t, prime power ℓ^{2d}, auxiliary v, and discriminant D₀ to 4q.

theorem VolcanoStructure.ordinary_component_hℓ_ndvd_v (C : OrdinaryIsogenyComponent) : ¬↑C.ℓ ∣ ordinary_component_v_aux C

The auxiliary integer v from the depth equation is coprime to ℓ.

theorem VolcanoStructure.ordinary_component_hℓ_ndvd_f₀ (C : OrdinaryIsogenyComponent) : ¬C.ℓ ∣ C.f₀

The base conductor f₀ is coprime to ℓ.

theorem VolcanoStructure.kohel_index_step_aux (C : OrdinaryIsogenyComponent) (i : ℕ) : i < (ordinary_component_volcano C).depth → ∀ (v : (ordinary_component_volcano C).V) (w : (ordinary_component_volcano C).V) (hv : ↑((ordinary_component_volcano C).level v) = i) (hw : ↑((ordinary_component_volcano C).level w) = i + 1), C.f₀ * C.ℓ ^ ↑((ordinary_component_volcano C).level w) = C.ℓ * (C.f₀ * C.ℓ ^ ↑((ordinary_component_volcano C).level v))

Auxiliary algebraic step underlying Kohel's index_step: pushing a level-i conductor f₀ · ℓ^i up to a level-(i+1) conductor gives ℓ times the original.

noncomputable def VolcanoStructure.kohel_volcano_exists (C : OrdinaryIsogenyComponent) : KohelVolcano C

Kohel's existence theorem (Theorem 22.11): packaging the data computed above into a single KohelVolcano for an ordinary component.

theorem VolcanoStructure.surface_conductor_eq {C : OrdinaryIsogenyComponent} (K : KohelVolcano C) (v : K.volcano.V) (hv : ↑(K.volcano.level v) = 0) : K.conductor v = C.f₀

A surface vertex of the Kohel volcano has conductor equal to the base conductor f₀.

theorem VolcanoStructure.floor_conductor_eq {C : OrdinaryIsogenyComponent} (K : KohelVolcano C) (v : K.volcano.V) (hv : ↑(K.volcano.level v) = K.volcano.depth) : K.conductor v = C.f₀ * C.ℓ ^ K.volcano.depth

A floor vertex of the Kohel volcano has conductor f₀ · ℓ^depth.

theorem VolcanoStructure.conductor_increases_by_ℓ {C : OrdinaryIsogenyComponent} (K : KohelVolcano C) (v w : K.volcano.V) (hv : ↑(K.volcano.level v) + 1 = ↑(K.volcano.level w)) (_hlt : ↑(K.volcano.level v) < K.volcano.depth) : K.conductor w = C.ℓ * K.conductor v

Moving down one level in the Kohel volcano multiplies the conductor by ℓ.

theorem VolcanoStructure.surface_degree_le_two {C : OrdinaryIsogenyComponent} (K : KohelVolcano C) : K.volcano.surfaceDegree ≤ 2

Re-export: the surface degree of a Kohel volcano is at most 2.

theorem VolcanoStructure.crater_degree_eq_jacobiSym {C : OrdinaryIsogenyComponent} (K : KohelVolcano C) (v : K.volcano.V) (hv : K.volcano.isSurface v) : ↑(K.volcano.craterGraph.degree v) = 1 + jacobiSym C.D₀ C.ℓ

For a surface vertex, the crater degree equals 1 + (D₀/ℓ).

theorem VolcanoStructure.nonsurface_descending_eq_ℓ {C : OrdinaryIsogenyComponent} (K : KohelVolcano C) (v : K.volcano.V) (hv_pos : ↑(K.volcano.level v) > 0) (hv_lt : ↑(K.volcano.level v) < K.volcano.depth) : (K.volcano.graph.degreeOn v fun (w : K.volcano.V) => ↑(K.volcano.level v) + 1 = ↑(K.volcano.level w)) = C.ℓ

For a non-surface, non-floor vertex of the Kohel volcano, the descending degree equals ℓ.

theorem VolcanoStructure.surface_descending_eq {C : OrdinaryIsogenyComponent} (K : KohelVolcano C) (v : K.volcano.V) (hv : K.volcano.isSurface v) (hd : 0 < K.volcano.depth) : (K.volcano.graph.degreeOn v fun (w : K.volcano.V) => ¬K.volcano.level w = ⟨0, ⋯⟩) = C.ℓ + 1 - K.volcano.surfaceDegree

For a surface vertex of a positive-depth Kohel volcano, the number of edges leaving the surface equals ℓ + 1 - surfaceDegree.

theorem CMSetCardinality.ellCMSet_finite (D : ℤ) (F : Type u_1) [Field F] [Fintype F] : (Elliptic_Curves.Deuring.ellCMSet D F).Finite

The set ellCMSet D F of j-invariants of elliptic curves over a finite field F with CM by the order of discriminant D is finite.

theorem CMSetCardinality.ellCMSet_card_of_splits (D : ℤ) (hD : Elliptic_Curves.IsImagQuadDiscriminant D) (F : Type u_1) [Field F] [Fintype F] (hsplits : (Elliptic_Curves.Deuring.hilbertClassPolynomial D F).Splits) (hsep : (Elliptic_Curves.Deuring.hilbertClassPolynomial D F).Separable) (hroots : ∀ (x : F), (Elliptic_Curves.Deuring.hilbertClassPolynomial D F).IsRoot x ↔ x ∈ Elliptic_Curves.Deuring.ellCMSet D F) : ⋯.toFinset.card = Elliptic_Curves.classNumber D hD

If the Hilbert class polynomial of D splits and is separable over F with roots equal to ellCMSet D F, then the cardinality of ellCMSet D F equals the class number of D (an instance of Deuring's Theorem 21.12).

def CMSetCardinality.OrderContains (D D' : ℤ) : Prop

D is contained in D' (as orders) iff D = u² D' for some positive integer u and D' is itself an imaginary quadratic discriminant.

theorem CMSetCardinality.orderContains_isDisc (D D' : ℤ) (_hD : Elliptic_Curves.IsImagQuadDiscriminant D) (hcontains : OrderContains D D') : Elliptic_Curves.IsImagQuadDiscriminant D'

If D contains D' then D' is itself an imaginary quadratic discriminant.

theorem CMSetCardinality.coprime_of_orderContains (D D' : ℤ) (q : ℕ) (hcop : q.Coprime D.natAbs) (hcontains : OrderContains D D') : q.Coprime D'.natAbs

Coprimality with |D| descends to coprimality with |D'| along an order containment.

theorem CMSetCardinality.normEquation_of_orderContains (D D' : ℤ) (q : ℕ) (t v : ℤ) (hne : Elliptic_Curves.NormEquation D q t v) (hcontains : OrderContains D D') : ∃ (w : ℤ), Elliptic_Curves.NormEquation D' q t w

A norm-equation solution for D lifts to a norm-equation solution for any D' that D contains.

theorem CMSetCardinality.ellCMSet_nonempty_of_normEquation (D : ℤ) (hD : Elliptic_Curves.IsImagQuadDiscriminant D) (q : ℕ) (hq : 1 < q) (hcop : q.Coprime D.natAbs) (t v : ℤ) (hne : Elliptic_Curves.NormEquation D q t v) (ht : ¬↑q ∣ t) (F : Type u_1) [Field F] [Fintype F] (hcard : Fintype.card F = q) : (Elliptic_Curves.Deuring.ellCMSet D F).Nonempty

If (D, q) admits a norm-equation solution (t, v) with q ∤ t, then ellCMSet D F is nonempty for every field F of size q.

theorem CMSetCardinality.ellCMSet_nonempty_implies_normEquation (D : ℤ) (hD : Elliptic_Curves.IsImagQuadDiscriminant D) (q : ℕ) (hq : 1 < q) (hcop : q.Coprime D.natAbs) (F : Type u_1) [Field F] [Fintype F] (hcard : Fintype.card F = q) (hne : (Elliptic_Curves.Deuring.ellCMSet D F).Nonempty) : ∃ (t : ℤ) (v : ℤ), Elliptic_Curves.NormEquation D q t v ∧ ¬↑q ∣ t

Conversely, if ellCMSet D F is nonempty for some field F of size q, then the corresponding norm equation has a solution (t, v) with q ∤ t.

theorem CMSetCardinality.ellCMSet_empty_or_card_eq_classNumber (D : ℤ) (hD : Elliptic_Curves.IsImagQuadDiscriminant D) (q : ℕ) (hq : 1 < q) (hcop : q.Coprime D.natAbs) (F : Type u_1) [Field F] [Fintype F] (hcard : Fintype.card F = q) : Elliptic_Curves.Deuring.ellCMSet D F = ∅ ∨ ⋯.toFinset.card = Elliptic_Curves.classNumber D hD

For a field F of size q coprime to |D|, the CM set ellCMSet D F is either empty or has cardinality equal to the class number h(D).

structure IsogenyCount.CMCurveData : Type

Data for counting ℓ-isogenies from a CM elliptic curve over 𝔽_q: an imaginary quadratic discriminant D with class data, a prime ℓ ∤ q coprime to |D|, and a conductor f.

• D : ℤ
• hD : Elliptic_Curves.IsImagQuadDiscriminant self.D
• ℓ : ℕ
• hℓ_prime : Nat.Prime self.ℓ
• q : ℕ
• hq : 1 < self.q
• hℓ_ndvd_q : ¬self.ℓ ∣ self.q
• hcop : self.q.Coprime self.D.natAbs
• f : ℕ
• hf_pos : 0 < self.f

def IsogenyCount.CMCurveData.descendantDisc (C : CMCurveData) : ℤ

The discriminant of a descendant order, obtained by multiplying D by ℓ².

structure IsogenyCount.IsogenyCount (C : CMCurveData) (F : Type u_1) [Field F] [Fintype F] : Type

Counts of ℓ-isogenies from a CM elliptic curve over F (with |F| = q): horizontal, ascending, and descending counts, with the values prescribed by Theorem 22.5, and the descending count conditioned on whether descendant CM curves exist over F.

• hcard : Fintype.card F = C.q
• hne : (Elliptic_Curves.Deuring.ellCMSet C.D F).Nonempty
• numHorizontal : ℕ
• numAscending : ℕ
• numDescending : ℕ
• horizontal_eq : ↑self.numHorizontal = 1 + jacobiSym C.D C.ℓ
• ascending_eq : self.numAscending = if C.ℓ ∣ C.f then 1 else 0
• descending_zero_of_empty : Elliptic_Curves.Deuring.ellCMSet C.descendantDisc F = ∅ → self.numDescending = 0
• descending_eq_of_nonempty : (Elliptic_Curves.Deuring.ellCMSet C.descendantDisc F).Nonempty → ↑self.numDescending = ↑C.ℓ - jacobiSym C.D C.ℓ

noncomputable def IsogenyCount.isogeny_count_exists (C : CMCurveData) (F : Type u_1) [Field F] [Fintype F] (hcard : Fintype.card F = C.q) (hne : (Elliptic_Curves.Deuring.ellCMSet C.D F).Nonempty) : IsogenyCount C F

Existence of an IsogenyCount package for any CM data with a nonempty CM set over F.

structure CMTorsor.CMTorsorData : Type

Data for a CM torsor: an imaginary quadratic discriminant D and a prime power q coprime to |D|.

• D : ℤ
• hD : Elliptic_Curves.IsImagQuadDiscriminant self.D
• q : ℕ
• hq : 1 < self.q
• hcop : self.q.Coprime self.D.natAbs

noncomputable def CMTorsor.IdealClassRepresentedByNorm (D : ℤ) (ℓ : ℕ) {ClO : Type u_1} [CommGroup ClO] : ClO → Prop

Predicate that an ideal class in the class group of an order is represented by an ideal of norm equal to a given prime ℓ.

def CMTorsor.IsIdealClassOfPrimeNorm (D : ℤ) (ℓ : ℕ) {ClO : Type u_1} [CommGroup ClO] (g : ClO) : Prop

An ideal class g is "of prime norm ℓ" iff ℓ is prime and g is represented by an ideal of norm ℓ.

theorem CMTorsor.ideal_class_has_prime_norm (D : ℤ) (hD : Elliptic_Curves.IsImagQuadDiscriminant D) (hD₂ : IsImaginaryQuadraticDiscriminant D) (c : ImagQuadIdealClass D hD₂) (q : ℕ) : ∃ (a : ImagQuadProperIdeal D hD₂), a.idealClass = c ∧ Nat.Prime a.norm ∧ ¬a.norm ∣ q

Every ideal class in the imaginary quadratic class group contains a representative ideal of prime norm coprime to a given integer q.

structure CMTorsor.CMTorsor (C : CMTorsorData) (F : Type u_1) [Field F] [Fintype F] : Type (max (max u_1 (u_2 + 1)) (u_3 + 1))

A CM-torsor structure: the class group ClO acts freely and transitively on the set EllSet of CM elliptic curves over F, with the j-invariants identifying EllSet with ellCMSet D F. Action by an ideal class of prime norm ℓ corresponds to an ℓ-isogeny in both directions.

• hcard : Fintype.card F = C.q
• hne : (Elliptic_Curves.Deuring.ellCMSet C.D F).Nonempty
• ClO : Type u_2
• instCommGroup : CommGroup self.ClO
• instFintypeCl : Fintype self.ClO
• classGroup_card : Fintype.card self.ClO = Elliptic_Curves.classNumber C.D ⋯
• EllSet : Type u_3
• instFintypeEll : Fintype self.EllSet
• instNonemptyEll : Nonempty self.EllSet
• instDecEqEll : DecidableEq self.EllSet
• jInvariant : self.EllSet → F
• jInvariant_injective : Function.Injective self.jInvariant
• jInvariant_range : Set.range self.jInvariant = Elliptic_Curves.Deuring.ellCMSet C.D F
• instMulAction : MulAction self.ClO self.EllSet
• action_free (g : self.ClO) (x : self.EllSet) : g • x = x → g = 1
• action_transitive (x y : self.EllSet) : ∃ (g : self.ClO), g • x = y
• horizontal_isogeny (ℓ : ℕ) : Nat.Prime ℓ → ¬ℓ ∣ C.q → ∀ (g : self.ClO), IsIdealClassOfPrimeNorm C.D ℓ g → ∀ (x : self.EllSet), IsogenyGraph.hasEdge F ℓ (self.jInvariant x) (self.jInvariant (g • x))
• dual_isogeny (ℓ : ℕ) : Nat.Prime ℓ → ¬ℓ ∣ C.q → ∀ (g : self.ClO), IsIdealClassOfPrimeNorm C.D ℓ g → ∀ (x : self.EllSet), IsogenyGraph.hasEdge F ℓ (self.jInvariant (g • x)) (self.jInvariant x)

noncomputable def CMTorsor.cm_torsor_exists (C : CMTorsorData) (F : Type u_1) [Field F] [Fintype F] (hcard : Fintype.card F = C.q) (hne : (Elliptic_Curves.Deuring.ellCMSet C.D F).Nonempty) : CMTorsor C F

A CM torsor exists for any CM data with a nonempty CM set over a finite field F of the prescribed cardinality.