The intermediate ring is module-finite over the target coordinate ring

φ.intermediateRing is a finite W₂.CoordinateRing-module, with no normality or separability hypothesis. This is the finiteness that the relative ideal norm — and through it pushClass and the induced map on points — needs, including for Frobenius.

The target coordinate ring is finite over F[X], and W₁.FunctionField is finite over the fraction field of F[X]: first through W₂.FunctionField, then through the finite extension an isogeny induces. Since φ.intermediateRing is the integral closure of W₂.CoordinateRing, it is also the integral closure of F[X]. The separability-free normalization theorem TauCeti.IsIntegralClosure.finite_polynomial makes it finite over F[X], hence over the target coordinate ring.

Main results

• TauCeti.Isogeny.moduleFinite_intermediateRing: φ.intermediateRing is module-finite over W₂.CoordinateRing for every isogeny.

Design

The result is stated for arbitrary algebra structures whose structure maps are the pullback, matching Isogeny.degree_eq_finrank, rather than for one fixed choice: registering such a structure globally would be a diamond, since different isogenies induce different ones. A consumer produces the W₂.CoordinateRing-structure on the intermediate ring from the bundled φ.pullbackToIntermediateRing — letI := φ.pullbackToIntermediateRing.toAlgebra — which is why IntermediateRing/Basic.lean corestricts the pullback rather than registering an instance.

That letI supplies the Algebra but not the IsScalarTower this theorem also takes, so it is not by itself the whole setup. Isogeny.isScalarTower_intermediateRing supplies the tower from the same corestriction, and the two together are what a caller needs.

Provenance

The conclusion follows D. K. Angdinata's Isogeny.lean, Apache-2.0, supplied by the author on 2026-09-07, declaration intermediateRingFinite. That proof chooses a separating coordinate on the source. The proof here instead uses the target's fixed coordinate line and the general separability-free finite-normalization theorem, so it needs no coordinate case split.

theorem TauCeti.Isogeny.moduleFinite_intermediateRing {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) [Algebra W₂.CoordinateRing W₁.FunctionField] [Algebra W₂.FunctionField W₁.FunctionField] [IsScalarTower W₂.CoordinateRing W₂.FunctionField W₁.FunctionField] [Algebra W₂.CoordinateRing ↥φ.intermediateRing] [IsScalarTower W₂.CoordinateRing (↥φ.intermediateRing) W₁.FunctionField] (h : ∀ (x : W₂.CoordinateRing), (algebraMap W₂.CoordinateRing W₁.FunctionField) x = φ.pullback x) : Module.Finite W₂.CoordinateRing ↥φ.intermediateRing

The intermediate ring is module-finite over the target coordinate ring. No normality or separability hypothesis is needed, so this includes inseparable isogenies such as Frobenius.