The intermediate ring of an isogeny

The integral closure of the target coordinate ring inside the source function field, taken along an isogeny's pullback. This is the normalization that CoordinatePullback.MapsInfinity names, and it receives both coordinate rings: the target's through the pullback, and the source's because mapsInfinity is precisely the assertion that it lands there.

Main definitions

• TauCeti.Isogeny.intermediateRing: the integral closure of W₂.CoordinateRing in W₁.FunctionField along φ.pullback.
• TauCeti.Isogeny.toIntermediateRing and TauCeti.Isogeny.pullbackToIntermediateRing: the two coordinate rings corestricted into it, along which ideals are extended and the relative norm is taken.

Main results

• TauCeti.Isogeny.algebraMap_mem_intermediateRing: the source coordinate ring lands in it.
• TauCeti.Isogeny.pullback_mem_intermediateRing: so does the target coordinate ring.
• TauCeti.Isogeny.toIntermediateRing_injective and TauCeti.Isogeny.pullbackToIntermediateRing_injective: both coordinate rings embed in it, through the corestricted algebraMap and the corestricted pullback respectively.
• TauCeti.Isogeny.isIntegralClosure_intermediateRing: it really is the integral closure, in Mathlib's IsIntegralClosure sense.
• TauCeti.Isogeny.isScalarTower_intermediateRing: the corestricted pullback puts it in a scalar tower under W₂.CoordinateRing, which is the other half of a consumer's setup.
• TauCeti.Isogeny.id_intermediateRing: an identity isogeny's intermediate ring is the coordinate ring itself, sitting inside its own fraction field, and TauCeti.Isogeny.id_pullbackToIntermediateRing: its two corestrictions into that ring coincide.
• TauCeti.Isogeny.id_algebraMap_eq_pullback: the identity isogeny's pullback is the coordinate ring's own embedding into its function field, in the form the consumers above take.

Design

The result is a Subring W₁.FunctionField, not a Subalgebra. The algebra structure that φ.pullback induces on W₁.FunctionField is deliberately not a global instance — different isogenies induce different ones, so registering any would be a diamond, as Isogeny/Basic.lean explains. A Subalgebra would put that structure into the type, forcing every statement about the object to fix a choice of it; a Subring keeps it inside the definition, exactly where MapsInfinity already keeps it.

The two corestrictions are plain RingHoms rather than an Algebra W₂.CoordinateRing instance on the intermediate ring. An algebra instance would reintroduce the diamond the Subring choice exists to avoid, since the structure it would register is the pullback-induced one; a bundled map carries the same information to consumers without registering anything.

Nothing here assumes separability, so purely inseparable isogenies such as Frobenius are covered. id_intermediateRing is stated for an integrally closed coordinate ring rather than an elliptic one, which is all its proof uses; the elliptic case is that hypothesis discharged by WeierstrassCurve.Affine.isIntegrallyClosed_coordinateRing, and is not given a separate name because nothing would consume it.

The structural theory of this ring is not proved here. Module-finiteness over W₂.CoordinateRing is in the sibling IntermediateRing/Finite.lean as moduleFinite_intermediateRing, with no separability hypothesis; Dedekindness is in IntermediateRing/Dedekind.lean as isDedekindDomain_intermediateRing and integral closedness in IntermediateRing/IntegrallyClosed.lean as isIntegrallyClosed_intermediateRing. Its fraction field, rank, projectivity, and prime-counting theory are in IntermediateRing/Rank.lean.

This opens the "points come along" milestone of Layer 1 of TauCetiRoadmap/EllipticCurves/README.md, which names this object as "the intermediate ring — the integral closure of W₂.CoordinateRing in W₁.FunctionField, the normalization mapsInfinity names", receiving both coordinate rings on the way to pushClass and toPointHom. It follows Silverman, The Arithmetic of Elliptic Curves, II.2.

Provenance

⚠ mathlib-track. TauCetiRoadmap/EllipticCurves/README.md:1092 lists the IntermediateRing, and pushClass by ideal extension and relative norm (ClassGroup.extendedRelNormHom), among the components of D. Angdinata's shared isogeny development, on the way to toPointHom; the two embeddings added here are what that relative-norm step requires of the intermediate ring, since ideal extension along a non-injective map loses the information the class-group route needs. The siblings Finite.lean, Dedekind.lean, IntegrallyClosed.lean, and Rank.lean carry the same flag for the same object.

The choice of object is taken from the AINTLIB project (github.com/CBirkbeck/AINTLIB, at revision 2baa76f742bdb4fb8ee323fabba41203bd390e08, Apache 2.0 per the source file's header, by Chris Birkbeck): projects/HasseWeil/HasseWeil/Curves/NormConormIntegralClosure.lean, which introduces B := integralClosure C₂.CoordinateRing C₁.FunctionField and carries its structural instances instDedekindB, instModuleFiniteB, instFractionRingB and instTorsionFreeB, proved in projects/HasseWeil/HasseWeil/Curves/RamificationFinite.lean.

What is adapted here is the object and the observation that the integral closure over the coordinate ring — rather than over a localization — is the right home for the norm and class-group route to the induced map on points. Of the structural instances, module-finiteness and Dedekindness are ported, in the siblings IntermediateRing/Finite.lean and IntermediateRing/Dedekind.lean rather than here, both without separability: the former uses separability-free finite normalization, and the latter uses TauCeti.IsIntegralClosure.isDedekindDomain in place of the Mathlib route the source uses. IntermediateRing/IntegrallyClosed.lean proves integral closedness without it either. instFractionRingB is ported in IntermediateRing/Rank.lean as isFractionRing_intermediateRing, with the pullback-induced algebra structures installed locally and no separability assumption. Only instTorsionFreeB is not ported. None of the declarations below is a transcription of a source declaration.

instTorsionFreeB is unported but not missing, and should stay unported. Its content is available from the two embeddings below composed with Mathlib's Module.isTorsionFree_iff_algebraMap_injective: a consumer holding the corestricted algebra structures writes

Module.isTorsionFree_iff_algebraMap_injective.mpr φ.toIntermediateRing_injective
Module.isTorsionFree_iff_algebraMap_injective.mpr φ.pullbackToIntermediateRing_injective

for the source and target sides. Named isTorsionFree_intermediateRing lemmas of exactly that shape were written and then deleted in review, as one-step wrappers of that iff with no in-repo consumer: a theorem carrying an explicit pointwise hypothesis can never be selected by instance search, so it saves a caller nothing over the one-liner. Read "not ported" as "deliberately absent, content reachable in one step" rather than as a gap to be filled.

References

• J. Silverman, The Arithmetic of Elliptic Curves, II.2.

noncomputable def TauCeti.Isogeny.intermediateRing {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) : Subring W₁.FunctionField

The intermediate ring of an isogeny: the integral closure of the target coordinate ring inside the source function field, along the isogeny's pullback.

Equations

• φ.intermediateRing = (integralClosure W₂.CoordinateRing W₁.FunctionField).toSubring

theorem TauCeti.Isogeny.mem_intermediateRing_iff {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) (z : W₁.FunctionField) : z ∈ φ.intermediateRing ↔ IsIntegral W₂.CoordinateRing z

Membership in the intermediate ring is integrality over the target coordinate ring acting through the pullback. The definition's body is not exposed across the module boundary, so this is how downstream modules compute with it.

Deliberately not @[simp]: it would rewrite every z ∈ φ.intermediateRing into the IsIntegral form, which is exactly the left-hand side of the two membership lemmas below, so tagging it would stop those firing. The simp-normal form of a membership goal is discharge by one of them; this lemma is the escape hatch for the goals they do not cover.

@[simp]

theorem TauCeti.Isogeny.algebraMap_mem_intermediateRing {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) (x : W₁.CoordinateRing) : (algebraMap W₁.CoordinateRing W₁.FunctionField) x ∈ φ.intermediateRing

The source coordinate ring lands in the intermediate ring. This is mapsInfinity read as a statement about that ring: pointedness of the isogeny says exactly that the source coordinates are integral over the pulled-back target coordinate ring.

@[simp]

theorem TauCeti.Isogeny.pullback_mem_intermediateRing {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) (x : W₂.CoordinateRing) : φ.pullback x ∈ φ.intermediateRing

The target coordinate ring lands in the intermediate ring, through the pullback: each element of the image is integral over the ring it is the image of.

noncomputable def TauCeti.Isogeny.toIntermediateRing {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) : W₁.CoordinateRing →+* ↥φ.intermediateRing

The source coordinate ring, corestricted into the intermediate ring. Extending an ideal of W₁.CoordinateRing into the intermediate ring is done along this map.

Equations

• φ.toIntermediateRing = (algebraMap W₁.CoordinateRing W₁.FunctionField).codRestrict φ.intermediateRing ⋯

@[simp]

theorem TauCeti.Isogeny.coe_toIntermediateRing {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) (x : W₁.CoordinateRing) : ↑(φ.toIntermediateRing x) = (algebraMap W₁.CoordinateRing W₁.FunctionField) x

theorem TauCeti.Isogeny.toIntermediateRing_injective {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) : Function.Injective ⇑φ.toIntermediateRing

The source coordinate ring embeds in the intermediate ring. The corestricted map is algebraMap W₁.CoordinateRing W₁.FunctionField, injective because the function field is by definition the fraction field of the coordinate ring, and corestriction preserves that.

noncomputable def TauCeti.Isogeny.pullbackToIntermediateRing {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) : W₂.CoordinateRing →+* ↥φ.intermediateRing

The target coordinate ring, corestricted into the intermediate ring along the pullback. The relative ideal norm back down to W₂.CoordinateRing is taken over this map.

Equations

• φ.pullbackToIntermediateRing = φ.pullback.codRestrict φ.intermediateRing ⋯

@[simp]

theorem TauCeti.Isogeny.coe_pullbackToIntermediateRing {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) (x : W₂.CoordinateRing) : ↑(φ.pullbackToIntermediateRing x) = φ.pullback x

theorem TauCeti.Isogeny.pullbackToIntermediateRing_injective {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) : Function.Injective ⇑φ.pullbackToIntermediateRing

The target coordinate ring embeds in the intermediate ring, through the pullback. This is pullback_injective corestricted; the pullback of an isogeny is injective because φ^*x₂ is transcendental over the base field. The source-side companion is toIntermediateRing_injective above.

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

The corestricted pullback puts the intermediate ring in a scalar tower. With letI := φ.pullbackToIntermediateRing.toAlgebra, the target coordinate ring acts on W₁.FunctionField through the intermediate ring exactly as it does directly.

This is the second half of the one-line setup a consumer needs: pullbackToIntermediateRing supplies the Algebra, and this supplies the IsScalarTower that every downstream statement over the intermediate ring also asks for.

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

The intermediate ring really is the integral closure, in Mathlib's IsIntegralClosure sense: an element of W₁.FunctionField lies in it exactly when it is integral over W₂.CoordinateRing.

Stated for an arbitrary W₂.CoordinateRing-algebra structure on W₁.FunctionField whose structure map is the pullback, so that a caller's own structure is accepted rather than only the locally-built one intermediateRing is defined against. Nothing here assumes separability.

@[simp]

theorem TauCeti.Isogeny.id_intermediateRing {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) [IsIntegrallyClosed W.CoordinateRing] : (id W).intermediateRing = (algebraMap W.CoordinateRing W.FunctionField).range

The identity isogeny's intermediate ring is the coordinate ring itself, embedded in its own fraction field: nothing in the function field beyond an integrally closed coordinate ring is integral over it. For an elliptic curve the hypothesis is WeierstrassCurve.Affine.isIntegrallyClosed_coordinateRing.

theorem TauCeti.Isogeny.id_algebraMap_eq_pullback {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) (x : W.CoordinateRing) : (algebraMap W.CoordinateRing W.FunctionField) x = (id W).pullback x

The identity isogeny's pullback is the coordinate ring's own embedding into its function field. This is the form in which Isogeny.isScalarTower_intermediateRing and its fellow consumers take their pinning hypothesis, so it is stated once here rather than reproved at each use.

@[simp]

theorem TauCeti.Isogeny.id_pullbackToIntermediateRing {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) : (id W).pullbackToIntermediateRing = (id W).toIntermediateRing

The identity isogeny corestricts both coordinate rings the same way. Its pullback is the coordinate ring's own embedding in its fraction field, so the map along which ideals are extended and the map along which the relative norm is taken are one and the same.