Base change of an isogeny

An isogeny is a coordinate pullback W₂.CoordinateRing →ₐ[F] W₁.FunctionField sending the point at infinity to the point at infinity. This file carries one along a homomorphism f : F →+* K of the base field, producing an isogeny W₁.map f → W₂.map f, and records that the construction is functorial in both arguments.

The mechanism is the coordinate-ring universal property in Affine/Eval.lean. The images of the two coordinate functions under a pullback are a point of W₂ over W₁.FunctionField, and WeierstrassCurve.Affine.CoordinateRing.evalAlgHom constructs a pullback from such a point. A point of a curve is carried along any ring homomorphism by WeierstrassCurve.Affine.Equation.map, so the base-changed pullback is the point (f^*x, f^*y), read through the identification WeierstrassCurve.Affine.FunctionField.map_map_algebraMap of the two ways of getting W₂ over K(W₁.map f). No tensor product appears, and nothing about W₂.CoordinateRing beyond its being generated by the two coordinates is used.

Pointedness survives for the same reason it holds: MapsInfinity is integrality of F[W₁] over the pulled-back F[W₂], an integral dependence is a monic polynomial identity, and a ring homomorphism carries such an identity to another one. The two coordinates therefore stay integral, and WeierstrassCurve.Affine.algebraMap_mem_adjoin_genericX_genericY — the coordinate ring, inside the function field, lies in the subalgebra they generate — propagates that to the whole coordinate ring.

The base map is an arbitrary homomorphism of fields, so f = algebraMap F K is base change along a field extension, while f = σ an automorphism is the semilinear transport of an isogeny to the conjugate isogeny W₁.map σ → W₂.map σ. That transport is the raw material for a Galois action on isogenies rather than an action itself: it lands on the conjugate curves, so an action would first need the identifications Wᵢ.map σ = Wᵢ available for curves defined over the fixed field. Both readings are uses of one construction.

What is not here

The degree. deg (φ.map f) = deg φ is a true and wanted statement — it is flat base change of a finite morphism — but it is not a formal consequence of anything above: it compares [K(W₁.map f) : (φ.map f)^*K(W₂.map f)] with [F(W₁) : φ^*F(W₂)], which needs the function field of the base-changed curve to be recognised as a localisation of K ⊗_F F[W₁]. That comparison, and with it the invariance of the separable and inseparable degrees, is its own development.

Main definitions

• TauCeti.CoordinatePullback.map: the base-changed coordinate pullback.
• TauCeti.Isogeny.map: the base-changed isogeny.

Main results

• TauCeti.CoordinatePullback.map_coordinateRingMap: the defining commuting square — the base-changed pullback agrees with the original one after CoordinateRing.map on the source and FunctionField.map on the target.
• TauCeti.CoordinatePullback.MapsInfinity.map: pointedness survives base change, which is what makes Isogeny.map well defined.
• TauCeti.Isogeny.map_fieldPullback_map: the pointwise commuting square at the level of function fields, where an isogeny is usually met; map_fieldPullback_comp_map is its homomorphism-level companion.
• TauCeti.Isogeny.id_map, TauCeti.Isogeny.comp_map: base change preserves the identity isogeny and composition.
• TauCeti.Isogeny.map_id, TauCeti.Isogeny.map_map: functoriality in the base map itself.

Roadmap

TauCetiRoadmap/EllipticCurves/README.md, Layer 0.5 (README:369). Its first milestone (README:376-378) asks for "base change of Weierstrass equations, coordinate rings, function fields, points, and isogenies, compatible with identity, composition, degree, separability, MapsInfinity, duals, and induced point maps"; this file is the isogeny entry, with the identity, composition and MapsInfinity clauses. Layer 1's dual-isogeny milestone (README:529-531) opens "for the separable part, base change to Kˢᵉᵖ, where Kˢᵉᵖ(W₁)/φ^*Kˢᵉᵖ(W₂) is Galois", and Isogeny.map is the arrow that base change names there.

Mathlib's WeierstrassCurve.map_id and WeierstrassCurve.map_map are proved by rfl. Their affine specialisations are therefore definitional equalities too, so the identity and composition laws below need no explicit transports between mapped curves.

noncomputable def TauCeti.CoordinatePullback.map {F : Type u_1} {K : Type u_2} [Field F] [Field K] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : CoordinatePullback W₁ W₂) (f : F →+* K) : CoordinatePullback (W₁.map f) (W₂.map f)

Base change of a coordinate pullback along a homomorphism f of the base field: the pullback whose two coordinate functions are those of φ, carried along f.

Equations

• φ.map f = WeierstrassCurve.Affine.CoordinateRing.evalAlgHom ⋯

@[simp]

theorem TauCeti.CoordinatePullback.map_of_X {F : Type u_1} {K : Type u_2} [Field F] [Field K] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : CoordinatePullback W₁ W₂) (f : F →+* K) : (φ.map f) ((AdjoinRoot.of (W₂.map f).polynomial) Polynomial.X) = (WeierstrassCurve.Affine.FunctionField.map W₁ f) (φ ((AdjoinRoot.of W₂.polynomial) Polynomial.X))

The base-changed pullback sends the class of X to the carried x-coordinate.

@[simp]

theorem TauCeti.CoordinatePullback.map_root {F : Type u_1} {K : Type u_2} [Field F] [Field K] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : CoordinatePullback W₁ W₂) (f : F →+* K) : (φ.map f) (AdjoinRoot.root (W₂.map f).polynomial) = (WeierstrassCurve.Affine.FunctionField.map W₁ f) (φ (AdjoinRoot.root W₂.polynomial))

The base-changed pullback sends the class of Y to the carried y-coordinate.

@[simp]

theorem TauCeti.CoordinatePullback.map_coordinateRingMap {F : Type u_1} {K : Type u_2} [Field F] [Field K] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : CoordinatePullback W₁ W₂) (f : F →+* K) (z : W₂.CoordinateRing) : (φ.map f) ((WeierstrassCurve.Affine.CoordinateRing.map W₂ f) z) = (WeierstrassCurve.Affine.FunctionField.map W₁ f) (φ z)

The defining commuting square of the base change. Carrying a function of W₂ along f and then pulling it back is pulling it back and then carrying it along f.

theorem TauCeti.CoordinatePullback.map_comp_coordinateRingMap {F : Type u_1} {K : Type u_2} [Field F] [Field K] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : CoordinatePullback W₁ W₂) (f : F →+* K) : (φ.map f).comp (WeierstrassCurve.Affine.CoordinateRing.map W₂ f) = (WeierstrassCurve.Affine.FunctionField.map W₁ f).comp φ.toRingHom

The commuting square as an equality of ring homomorphisms.

@[simp]

theorem TauCeti.CoordinatePullback.id_map {F : Type u_1} {K : Type u_2} [Field F] [Field K] (W : WeierstrassCurve.Affine F) (f : F →+* K) : (id W).map f = id (W.map f)

Base change fixes the identity coordinate pullback.

@[simp]

theorem TauCeti.CoordinatePullback.map_id {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : CoordinatePullback W₁ W₂) : φ.map (RingHom.id F) = φ

Base change of a coordinate pullback along the identity is the original pullback.

@[simp]

theorem TauCeti.CoordinatePullback.map_map {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : CoordinatePullback W₁ W₂) (f : F →+* K) (g : K →+* L) : (φ.map f).map g = φ.map (g.comp f)

Base change of a coordinate pullback is functorial in the base map.

theorem TauCeti.CoordinatePullback.isIntegral_map {F : Type u_1} {K : Type u_2} [Field F] [Field K] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : CoordinatePullback W₁ W₂) (f : F →+* K) {z : W₁.FunctionField} (hz : IsIntegral W₂.CoordinateRing z) : IsIntegral (W₂.map f).CoordinateRing ((WeierstrassCurve.Affine.FunctionField.map W₁ f) z)

Integral dependence over the pulled-back coordinate ring survives base change. An integral dependence is a monic polynomial identity, and map_comp_coordinateRingMap carries such an identity along f.

theorem TauCeti.CoordinatePullback.MapsInfinity.map {F : Type u_1} {K : Type u_2} [Field F] [Field K] {W₁ W₂ : WeierstrassCurve.Affine F} {φ : CoordinatePullback W₁ W₂} (hφ : φ.MapsInfinity) (f : F →+* K) : (φ.map f).MapsInfinity

Pointedness survives base change: a coordinate pullback that maps infinity to infinity still does so after base change along a homomorphism of the base field.

noncomputable def TauCeti.Isogeny.map {F : Type u_1} {K : Type u_2} [Field F] [Field K] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) (f : F →+* K) : Isogeny (W₁.map f) (W₂.map f)

Base change of an isogeny along a homomorphism f of the base field.

Equations

• φ.map f = { pullback := φ.pullback.map f, mapsInfinity := ⋯ }

@[simp]

theorem TauCeti.Isogeny.map_pullback {F : Type u_1} {K : Type u_2} [Field F] [Field K] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) (f : F →+* K) : (φ.map f).pullback = φ.pullback.map f

theorem TauCeti.Isogeny.map_fieldPullback_comp_map {F : Type u_1} {K : Type u_2} [Field F] [Field K] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) (f : F →+* K) : (↑(φ.map f).fieldPullback).comp (WeierstrassCurve.Affine.FunctionField.map W₂ f) = (WeierstrassCurve.Affine.FunctionField.map W₁ f).comp ↑φ.fieldPullback

The commuting square at the level of function fields, as an equality of ring homomorphisms.

@[simp]

theorem TauCeti.Isogeny.map_fieldPullback_map {F : Type u_1} {K : Type u_2} [Field F] [Field K] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) (f : F →+* K) (z : W₂.FunctionField) : (φ.map f).fieldPullback ((WeierstrassCurve.Affine.FunctionField.map W₂ f) z) = (WeierstrassCurve.Affine.FunctionField.map W₁ f) (φ.fieldPullback z)

The pointwise commuting square at the level of function fields.

@[simp]

theorem TauCeti.Isogeny.id_map {F : Type u_1} {K : Type u_2} [Field F] [Field K] (W : WeierstrassCurve.Affine F) (f : F →+* K) : (id W).map f = id (W.map f)

Base change fixes the identity isogeny.

@[simp]

theorem TauCeti.Isogeny.comp_map {F : Type u_1} {K : Type u_2} [Field F] [Field K] {W₁ W₂ W₃ : WeierstrassCurve.Affine F} (ψ : Isogeny W₂ W₃) (φ : Isogeny W₁ W₂) (f : F →+* K) : (ψ.comp φ).map f = (ψ.map f).comp (φ.map f)

Base change respects composition.

@[simp]

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

Base change along the identity is the identity.

@[simp]

theorem TauCeti.Isogeny.map_map {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] {W₁ W₂ : WeierstrassCurve.Affine F} (φ : Isogeny W₁ W₂) (f : F →+* K) (g : K →+* L) : (φ.map f).map g = φ.map (g.comp f)

Base change is functorial in the base map.