The function field along a homomorphism of the base field

Mathlib carries a Weierstrass curve along a ring homomorphism f : R →+* S (WeierstrassCurve.map) and carries its coordinate ring along with it (CoordinateRing.map, injective when f is). This file carries the function field: for f : F →+* K a homomorphism of fields, F(W) embeds into K(W.map f).

There is nothing to choose. F(W) is the fraction field of the domain F[W], and F[W] lands in the field K(W.map f) injectively, so the embedding is the unique extension of that composite across fractions — IsFractionRing.lift. What the file records is how the embedding meets everything else: the two coordinates, the scalars, and composition of base maps.

The scalar compatibility map_algebraMap is the load-bearing one. Read as an equality of ring homomorphisms out of F it says the square

    F  ──────────────▸  K
    │                   │
    ▾                   ▾
  F(W)  ────────────▸  K(W.map f)

commutes, and map_map_algebraMap is that square applied to the coefficients of a second curve: a curve W₂ over F base-changed to F(W₁) and then carried along the embedding is the same curve as W₂.map f base-changed to K(W₁.map f). That equality is what lets a point of W₂ over F(W₁) — equivalently, by the universal property in Isogeny/Basic.lean, a coordinate pullback — be pushed to a point of W₂.map f over K(W₁.map f).

The homomorphism of base fields is an arbitrary f : F →+* K, not an algebraMap. Base change along a field extension is the case f = algebraMap F K, while an automorphism f = σ gives the semilinear transport of F(W) to the function field of the conjugate curve W.map σ. The latter is the raw material for a Galois action but is not itself one: the target is K(W.map σ), not K(W), so an action would additionally need the identification W.map σ = W for a curve defined over the fixed field together with its coherence laws, and none of that is built into the statements here. A single map covers both readings, and neither is built in.

Main definitions

• WeierstrassCurve.Affine.FunctionField.map: the embedding F(W) → K(W.map f).

Main results

• WeierstrassCurve.Affine.FunctionField.map_algebraMap_coordinateRing: it restricts to CoordinateRing.map on the coordinate ring, which is what pins it down.
• WeierstrassCurve.Affine.FunctionField.map_algebraMap and WeierstrassCurve.Affine.FunctionField.map_comp_algebraMap: it is compatible with the scalars, in element and in composed form.
• WeierstrassCurve.Affine.FunctionField.map_genericX and WeierstrassCurve.Affine.FunctionField.map_genericY: it sends the generic point of W to the generic point of W.map f.
• WeierstrassCurve.Affine.FunctionField.map_id, WeierstrassCurve.Affine.FunctionField.map_map, and its homomorphism-level companion map_comp_map: functoriality in f.
• WeierstrassCurve.Affine.FunctionField.map_map_algebraMap: the commuting square above, at the level of a second curve base-changed to the function field.

Roadmap

TauCetiRoadmap/EllipticCurves/README.md, Layer 0.5 (README:369), whose first milestone (README:376-378) asks for "base change of Weierstrass equations, coordinate rings, function fields, points, and isogenies". This is the function-field entry of that list; the isogeny entry is Isogeny/BaseChange.lean, which is what consumes everything here.

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

The function field carried along a homomorphism of the base field. F(W) is the fraction field of F[W], which lands injectively in the field K(W.map f), so there is exactly one extension of that map across fractions.

Equations

• WeierstrassCurve.Affine.FunctionField.map W f = IsFractionRing.lift ⋯

@[simp]

theorem WeierstrassCurve.Affine.FunctionField.map_algebraMap_coordinateRing {F : Type u_1} {K : Type u_2} [Field F] [Field K] (W : Affine F) (f : F →+* K) (z : W.CoordinateRing) : (map W f) ((algebraMap W.CoordinateRing W.FunctionField) z) = (algebraMap (W.map f).CoordinateRing (W.map f).FunctionField) ((CoordinateRing.map W f) z)

FunctionField.map restricts to CoordinateRing.map, which is the property that determines it.

@[simp]

theorem WeierstrassCurve.Affine.FunctionField.map_algebraMap {F : Type u_1} {K : Type u_2} [Field F] [Field K] (W : Affine F) (f : F →+* K) (a : F) : (map W f) ((algebraMap F W.FunctionField) a) = (algebraMap K (W.map f).FunctionField) (f a)

FunctionField.map is compatible with the scalars: a constant of F goes to the corresponding constant of K.

theorem WeierstrassCurve.Affine.FunctionField.map_comp_algebraMap {F : Type u_1} {K : Type u_2} [Field F] [Field K] (W : Affine F) (f : F →+* K) : (map W f).comp (algebraMap F W.FunctionField) = (algebraMap K (W.map f).FunctionField).comp f

FunctionField.map is compatible with the scalars, in composed form: the square with f along the top and the two constant embeddings down the sides commutes.

@[simp]

theorem WeierstrassCurve.Affine.FunctionField.map_genericX {F : Type u_1} {K : Type u_2} [Field F] [Field K] (W : Affine F) (f : F →+* K) : (map W f) W.genericX = (W.map f).genericX

FunctionField.map sends the generic x-coordinate to the generic x-coordinate.

@[simp]

theorem WeierstrassCurve.Affine.FunctionField.map_genericY {F : Type u_1} {K : Type u_2} [Field F] [Field K] (W : Affine F) (f : F →+* K) : (map W f) W.genericY = (W.map f).genericY

FunctionField.map sends the generic y-coordinate to the generic y-coordinate.

@[simp]

theorem WeierstrassCurve.Affine.FunctionField.map_algebraMap_ratFunc {F : Type u_1} {K : Type u_2} [Field F] [Field K] (W : Affine F) (f : F →+* K) (z : RatFunc F) : (map W f) ((algebraMap (RatFunc F) W.FunctionField) z) = (algebraMap (RatFunc K) (W.map f).FunctionField) ((RatFunc.mapRingHom (Polynomial.mapRingHom f) ⋯) z)

Changing the coefficient field of a Weierstrass function field commutes with the embedding of its rational-function subfield.

@[simp]

theorem WeierstrassCurve.Affine.FunctionField.map_id {F : Type u_1} [Field F] (W : Affine F) : map W (RingHom.id F) = RingHom.id W.FunctionField

FunctionField.map along the identity is the identity.

theorem WeierstrassCurve.Affine.FunctionField.map_comp_map {F : Type u_1} {K : Type u_2} {L : Type u_3} [Field F] [Field K] [Field L] (W : Affine F) (f : F →+* K) (g : K →+* L) : (map (W.map f) g).comp (map W f) = map W (g.comp f)

FunctionField.map is functorial. As for CoordinateRing.map_comp_map, the curve equality (W.map f).map g = W.map (g.comp f) holds definitionally, so no transport appears.

@[simp]

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

Pointwise functoriality of FunctionField.map.

theorem WeierstrassCurve.Affine.FunctionField.map_map_algebraMap {F : Type u_1} {K : Type u_2} [Field F] [Field K] (W : Affine F) (f : F →+* K) (W₂ : Affine F) : (W₂.map (algebraMap F W.FunctionField)).map (map W f) = (W₂.map f).map (algebraMap K (W.map f).FunctionField)

The commuting square, carried on the coefficients of a second curve. A curve W₂ over F base-changed to the function field of W, then carried along FunctionField.map W f, is W₂.map f base-changed to the function field of W.map f.

This is what makes a point of W₂ over F(W) — equivalently a coordinate pullback — push forward along f.