Function-field pullbacks of isogenies

This file proves that the coordinate pullback of an isogeny is injective and extends it uniquely to the function fields. Both rest on one nonconstancy statement: the pulled-back target coordinate is transcendental over the base field, since otherwise pointedness would make the source coordinate algebraic as well, against its transcendence. Injectivity is then the observation that a nonzero element of the kernel has a nonzero norm over the target's polynomial subring, and that norm is a polynomial relation killing the pulled-back coordinate.

That extension is what lets isogenies be composed: a coordinate pullback lands in a function field, so composing two of them needs the outer one extended across the inner one's fraction field. TauCeti.Isogeny.comp therefore lives here rather than beside TauCeti.Isogeny.id in Isogeny/Basic.lean — this is the first file where it can be stated.

Main results

• TauCeti.Isogeny.transcendental_pullback_X: the pullback of the affine coordinate x is transcendental over the base field. This is the nonconstancy step, and the source of a transcendental element inside the pulled-back function field.
• TauCeti.Isogeny.pullback_injective: a coordinate pullback satisfying MapsInfinity is injective.
• TauCeti.Isogeny.fieldPullback: the induced embedding of function fields.
• TauCeti.Isogeny.comap_fieldPullback_apply_algebraMap: a valuation restricted along the pullback, evaluated on an affine function of the target, is the valuation of its coordinate pullback.
• TauCeti.Isogeny.comp: composition of isogenies, with TauCeti.Isogeny.comp_fieldPullback its function-field law and TauCeti.Isogeny.id_comp, TauCeti.Isogeny.comp_id, TauCeti.Isogeny.comp_assoc the unit and associativity laws. The pointedness obligation is discharged privately when comp is defined.
• TauCeti.Isogeny.isScalarTower_fieldPullback: the three pullbacks of a composite make F(W₃) ⊆ F(W₂) ⊆ F(W₁) a scalar tower — the shared opening of the multiplicativity-under- composition proofs in Isogeny/Degree.lean and Isogeny/Separability.lean.
• TauCeti.Isogeny.comp_right_injective and TauCeti.Isogeny.comp_right_inj: precomposition by a fixed isogeny is injective. Equivalently, a factorisation ψ = λ.comp φ through a fixed φ determines its factor λ uniquely — the uniqueness half of factoring an isogeny, reached without the group structure on Hom that Silverman's subtraction argument uses.

Adapted 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/EC/IsogenyAG/CanonicalDual.lean, declaration Isogeny.compose_right_cancel. The source states it for an isogeny structure that carries the point map as an independent field, so its proof passes through ext_toCurveMap; here an isogeny is determined by its pullback, so pullback extensionality suffices.

The degree of an isogeny — the dimension of W₁.FunctionField over the image of fieldPullback — is TauCeti.Isogeny.degree, in Isogeny/Degree.lean; it is stated there rather than here because the finiteness that makes it honest is proved from transcendental_pullback_X together with the degree of the function field over the rational function field.

The construction is the coordinate-ring form of D. Angdinata's function-field definition of an isogeny and follows the nonconstancy argument described in the elliptic-curves roadmap. The composition definition follows the seed in TauCetiRoadmap/EllipticCurves/Suggested.lean, discharging the mapsInfinity obligation the seed leaves open. The geometric interpretation is Silverman, The Arithmetic of Elliptic Curves, II.2.4.

theorem TauCeti.Isogeny.transcendental_pullback_X {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) : Transcendental F (φ.pullback ((algebraMap (Polynomial F) W₂.CoordinateRing) Polynomial.X))

The pullback of the affine coordinate is transcendental. If φ^*x₂ were algebraic over F, then every pullback would be integral over F, because the target coordinate ring is integral over F[x₂]; pointedness would carry that to the source coordinate x₁, which is transcendental.

This is the nonconstancy of an isogeny, in the form later files consume: it exhibits a transcendental element of the pulled-back function field, which is what makes the extension it sits under finite.

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

The coordinate pullback of any isogeny of affine Weierstrass curves over a field is injective, by the general criterion CoordinateRing.algHom_injective: the pullback of the coordinate x is transcendental.

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

The function-field pullback induced by an isogeny. It is the unique extension of the coordinate pullback across the target fraction field.

Equations

• φ.fieldPullback = IsFractionRing.liftAlgHom ⋯

@[simp]

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

The function-field pullback restricts to the original coordinate pullback.

theorem TauCeti.Isogeny.comap_fieldPullback_apply_algebraMap {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) {Γ : Type u_2} [LinearOrderedCommGroupWithZero Γ] (v : Valuation W₁.FunctionField Γ) (c : W₂.CoordinateRing) : (Valuation.comap φ.fieldPullback.toRingHom v) ((algebraMap W₂.CoordinateRing W₂.FunctionField) c) = v (φ.pullback c)

A restricted valuation, evaluated on an affine function of the target: it is the value of the pullback of that function.

theorem TauCeti.Isogeny.ringHom_eq_fieldPullback {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) (f : W₂.FunctionField →+* W₁.FunctionField) (hf : ∀ (x : W₂.CoordinateRing), f ((algebraMap W₂.CoordinateRing W₂.FunctionField) x) = φ.pullback x) : f = ↑φ.fieldPullback

A ring homomorphism agreeing with an isogeny's coordinate pullback is its function-field pullback. W₂.FunctionField is a fraction field of W₂.CoordinateRing, so a map out of it is determined by its restriction.

Stated for a bare RingHom rather than an F-algebra homomorphism, because that is the form a caller holds: the algebraMap of an Algebra W₂.FunctionField W₁.FunctionField instance carries no F-structure of its own. fieldPullback_unique is the AlgHom corollary.

theorem TauCeti.Isogeny.fieldPullback_unique {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) (f : W₂.FunctionField →ₐ[F] W₁.FunctionField) (hf : ∀ (x : W₂.CoordinateRing), f ((algebraMap W₂.CoordinateRing W₂.FunctionField) x) = φ.pullback x) : f = φ.fieldPullback

A function-field algebra homomorphism agreeing with an isogeny's coordinate pullback is its function-field pullback, the AlgHom corollary of ringHom_eq_fieldPullback.

theorem TauCeti.Isogeny.algebraMap_functionField_eq_fieldPullback {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] (h : ∀ (x : W₂.CoordinateRing), (algebraMap W₂.CoordinateRing W₁.FunctionField) x = φ.pullback x) (z : W₂.FunctionField) : (algebraMap W₂.FunctionField W₁.FunctionField) z = φ.fieldPullback z

A coordinate-level structure map forces the field-level one. If an Algebra W₂.CoordinateRing W₁.FunctionField structure is the coordinate pullback, then any Algebra W₂.FunctionField W₁.FunctionField structure sitting in a tower over it is the function-field pullback.

This is the bridge every consumer needs that holds a coordinate-level witness but must transport a property of the extension across it — finite-dimensionality, separability, or integrality of an element over W₂.FunctionField. Properties intrinsic to a ring, IsIntegrallyClosed among them, do not depend on this structure map and are not what it carries.

@[simp]

theorem TauCeti.Isogeny.id_fieldPullback {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) : (id W).fieldPullback = AlgHom.id F W.FunctionField

The identity isogeny induces the identity pullback on the function field.

theorem TauCeti.Isogeny.isScalarTower_of_algebraMap_eq_fieldPullback {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) [Algebra W₂.FunctionField W₁.FunctionField] (h : ∀ (z : W₂.FunctionField), (algebraMap W₂.FunctionField W₁.FunctionField) z = φ.fieldPullback z) : IsScalarTower F W₂.FunctionField W₁.FunctionField

The pullback is a tower map over the base field: fieldPullback is an F-algebra map, so F(W₁) is an F(W₂)-algebra over F.

Not an instance — like the algebra structure it refines, it depends on φ — so a consumer installs it with haveI := φ.isScalarTower_of_algebraMap_eq_fieldPullback h. That is the opening of every argument that reads an invariant of F(W₁)/F(W₂) against the base field: the differential criterion for separability and the divisor pullback both begin with it.

noncomputable def TauCeti.Isogeny.comp {F : Type u_1} [Field F] {W₁ W₂ W₃ : WeierstrassCurve.Affine F} (ψ : Isogeny W₂ W₃) (φ : Isogeny W₁ W₂) : Isogeny W₁ W₃

Composition of isogenies: pull back along ψ into W₂.FunctionField, then carry that across to W₁.FunctionField by φ.fieldPullback.

Equations

• ψ.comp φ = { pullback := φ.fieldPullback.comp ψ.pullback, mapsInfinity := ⋯ }

@[simp]

theorem TauCeti.Isogeny.comp_pullback {F : Type u_1} [Field F] {W₁ W₂ W₃ : WeierstrassCurve.Affine F} (ψ : Isogeny W₂ W₃) (φ : Isogeny W₁ W₂) : (ψ.comp φ).pullback = φ.fieldPullback.comp ψ.pullback

The equation lemma for comp's coordinate pullback: the definition's body is not exposed across the module boundary, so this is how downstream modules compute with it.

@[simp]

theorem TauCeti.Isogeny.comp_fieldPullback {F : Type u_1} [Field F] {W₁ W₂ W₃ : WeierstrassCurve.Affine F} (ψ : Isogeny W₂ W₃) (φ : Isogeny W₁ W₂) : (ψ.comp φ).fieldPullback = φ.fieldPullback.comp ψ.fieldPullback

The function-field pullback of a composite is the composite of the function-field pullbacks.

theorem TauCeti.Isogeny.isScalarTower_fieldPullback {F : Type u_1} [Field F] {W₁ W₂ W₃ : WeierstrassCurve.Affine F} (ψ : Isogeny W₂ W₃) (φ : Isogeny W₁ W₂) : IsScalarTower W₃.FunctionField W₂.FunctionField W₁.FunctionField

The pullbacks of a composite isogeny form a scalar tower: F(W₃) ⊆ F(W₂) ⊆ F(W₁), the inclusions being the three function-field pullbacks. This is comp_fieldPullback read as a statement about algebra structures — the composite's pullback is the composite of the two, which is exactly the compatibility IsScalarTower asks for.

The three letIs are part of the statement, because these algebra structures come from AlgHoms rather than from instances: a consumer installs the same three lets and this lemma then applies. It is the shared opening of every proof that an invariant is multiplicative under composition — degree_comp, separableDegree_comp and inseparableDegree_comp each begin with it.

@[simp]

theorem TauCeti.Isogeny.id_comp {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) : (id W₂).comp φ = φ

The identity isogeny is a left unit for composition.

@[simp]

theorem TauCeti.Isogeny.comp_id {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) : φ.comp (id W₁) = φ

The identity isogeny is a right unit for composition.

@[simp]

theorem TauCeti.Isogeny.comp_assoc {F : Type u_1} [Field F] {W₁ W₂ W₃ W₄ : WeierstrassCurve.Affine F} (χ : Isogeny W₃ W₄) (ψ : Isogeny W₂ W₃) (φ : Isogeny W₁ W₂) : (χ.comp ψ).comp φ = χ.comp (ψ.comp φ)

Composition of isogenies is associative; the right-associated form is the simp-normal one, as for CategoryTheory.Category.assoc.

theorem TauCeti.Isogeny.comp_right_injective {F : Type u_1} [Field F] {W₁ W₂ W₃ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) : Function.Injective fun (ψ : Isogeny W₂ W₃) => ψ.comp φ

Precomposition by a fixed isogeny is injective.

@[simp]

theorem TauCeti.Isogeny.comp_right_inj {F : Type u_1} [Field F] {W₁ W₂ W₃ : WeierstrassCurve.Affine F} {φ : Isogeny W₁ W₂} {ψ₁ ψ₂ : Isogeny W₂ W₃} : ψ₁.comp φ = ψ₂.comp φ ↔ ψ₁ = ψ₂

Two isogenies agree exactly when they agree after precomposition by a fixed isogeny. So a factorisation through a fixed φ determines its factor uniquely.