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

Surface vertices of an ordinary $\ell$-isogeny volcano have degree $1 + (D_0 / \ell)$ in the crater (Kohel's theorem, Theorem 22.11(ii)).

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

Vertices on the surface ($V_0$) of an ordinary $\ell$-volcano have endomorphism ring of conductor $f_0$ (Theorem 22.11(i), (v)).

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

Vertices on the floor ($V_d$) of an ordinary $\ell$-volcano of depth $d$ have endomorphism ring of conductor $f_0 \cdot \ell^d$ (Theorem 22.11(iv), (v)).