structure OrdinaryVolcanoStructure.OrdinaryCurveData : Type

Combinatorial input for the $\ell$-isogeny volcano of an ordinary elliptic curve $E/\mathbb{F}_q$ (Kohel's Theorem 22.11). It records the prime $\ell \nmid q$, the trace of Frobenius $t$ (satisfying the strict Hasse bound), the fundamental discriminant $D_0 < 0$ of the CM order, the prime-to-$\ell$ conductor $f_0$, the global conductor $f = f_0 \cdot \ell^h$, and the order of the class group acting on the surface.

• 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₀
• f : ℕ
• hf_pos : 0 < self.f
• h : ℕ
• conductor_factorization : self.f = self.f₀ * self.ℓ ^ self.h
• hℓ_ndvd_f₀ : ¬self.ℓ ∣ self.f₀
• classOrder : ℕ
• hClassOrder_pos : 0 < self.classOrder

def OrdinaryVolcanoStructure.OrdinaryCurveData.toComponent (C : OrdinaryCurveData) : VolcanoStructure.OrdinaryIsogenyComponent

Forget the volcano depth $h$ and conductor factorization in OrdinaryCurveData to recover the underlying OrdinaryIsogenyComponent data used by the abstract volcano formalism.

structure OrdinaryVolcanoStructure.OrdinaryVolcano (C : OrdinaryCurveData) : Type 1

Existence statement for the $\ell$-isogeny volcano of an ordinary elliptic curve: a KohelVolcano over the underlying isogeny component whose depth coincides with the exponent $h$ in the conductor factorization $f = f_0 \cdot \ell^h$.

• kohelVolcano : VolcanoStructure.KohelVolcano C.toComponent
• depth_eq_h : self.kohelVolcano.volcano.depth = C.h

noncomputable def OrdinaryVolcanoStructure.ordinary_volcano_exists (C : OrdinaryCurveData) : OrdinaryVolcano C

Existence of the Kohel $\ell$-isogeny volcano for any ordinary elliptic curve satisfying the input data: there is a KohelVolcano whose depth equals the conductor $\ell$-exponent $h$ (Theorem 22.11).

theorem OrdinaryVolcanoStructure.conductor_at_level {C : OrdinaryCurveData} (V : OrdinaryVolcano C) (v : V.kohelVolcano.volcano.V) : V.kohelVolcano.conductor v = C.f₀ * C.ℓ ^ ↑(V.kohelVolcano.volcano.level v)

The conductor of any vertex $v$ in the $\ell$-volcano equals $f_0 \cdot \ell^{\mathrm{lvl}(v)}$ where $\mathrm{lvl}(v)$ is its level. This is the level-conductor correspondence at the heart of Kohel's volcano structure.

theorem OrdinaryVolcanoStructure.surface_conductor {C : OrdinaryCurveData} (V : OrdinaryVolcano C) (v : V.kohelVolcano.volcano.V) (hv : ↑(V.kohelVolcano.volcano.level v) = 0) : V.kohelVolcano.conductor v = C.f₀

Vertices on the surface (level $0$) of the volcano have conductor exactly $f_0$, the prime-to-$\ell$ part of the global conductor.

theorem OrdinaryVolcanoStructure.floor_conductor {C : OrdinaryCurveData} (V : OrdinaryVolcano C) (v : V.kohelVolcano.volcano.V) (hv : ↑(V.kohelVolcano.volcano.level v) = V.kohelVolcano.volcano.depth) : V.kohelVolcano.conductor v = C.f₀ * C.ℓ ^ C.h

Vertices at the floor of the volcano (maximum level $h$) have the maximum conductor $f_0 \cdot \ell^h = f$.

theorem OrdinaryVolcanoStructure.surface_degree_eq {C : OrdinaryCurveData} (V : OrdinaryVolcano C) : ↑V.kohelVolcano.volcano.surfaceDegree = 1 + jacobiSym C.D₀ C.ℓ

The degree of the surface graph equals $1 + \left(\tfrac{D_0}{\ell}\right)$ where the right-hand factor is the Jacobi/Kronecker symbol. This dichotomy distinguishes split ($+2$), inert ($0$), and ramified ($1$) primes in the CM field.