The coordinate-ring map: surjectivity, the generators of XYIdeal, and the Galois action

Mathlib's WeierstrassCurve.Affine.CoordinateRing.map sends a ring homomorphism f : R →+* S to R[W] →+* S[W.map f]. Around it Mathlib proves map_mk, map_smul and injectivity (CoordinateRing.map_injective), and it separately defines the classes XClass, YClass and the ideal XYIdeal they span. This file fills the two gaps between those: map is also surjective when f is, and map commutes with all three of those constructions.

Neither gap is deep. Since R[W] is AdjoinRoot W.polynomial, the surjectivity argument lives at the AdjoinRoot level in TauCeti/RingTheory/AdjoinRoot/Basic.lean and the coordinate-ring statement follows in a line; the commutation statements unfold the classes and push map_mk through.

Main results

• WeierstrassCurve.Affine.CoordinateRing.map_surjective and WeierstrassCurve.Affine.CoordinateRing.map_bijective: the coordinate-ring specialisations, stated like Mathlib's CoordinateRing.map_injective for an arbitrary f : R →+* S.
• WeierstrassCurve.Affine.CoordinateRing.map_XClass and WeierstrassCurve.Affine.CoordinateRing.map_YClass: map W f sends the class of X - x to the class of X - f x, and the class of Y - y(X) to the class of Y - (y.map f)(X).
• WeierstrassCurve.Affine.CoordinateRing.map_XYIdeal: map W f carries XYIdeal W x y = ⟨XClass W x, YClass W y⟩ to XYIdeal (W.map f) (f x) (y.map f).
• WeierstrassCurve.Affine.CoordinateRing.map_of_X, WeierstrassCurve.Affine.CoordinateRing.map_root and WeierstrassCurve.Affine.CoordinateRing.map_algebraMap: map W f fixes the two coordinates and is compatible with the scalars — it is a map of R-algebras up to f itself.
• WeierstrassCurve.Affine.CoordinateRing.map_id, WeierstrassCurve.Affine.CoordinateRing.map_map, and its homomorphism-level companion map_comp_map: map is a functor in f. The curve equalities W.map (RingHom.id R) = W and (W.map f).map g = W.map (g.comp f) hold definitionally, so neither statement carries a transport.
• WeierstrassCurve.Affine.CoordinateRing.ringHom_ext: ring homomorphisms out of the coordinate ring are determined by the constants and the classes of x and y.
• WeierstrassCurve.coordinateRingGaloisAction and WeierstrassCurve.coordinateRingGaloisAction_mk: for W over R and an R-algebra A, the action of A ≃ₐ[R] A on the coordinate ring of W⁄A, applying an automorphism to the coefficients.

For a base equivalence e the first two give RingEquiv.ofBijective (map W e) (map_bijective W e.bijective) in one line at the use site, so no equivalence is defined here; Mathlib's generic AdjoinRoot.mapRingEquiv is the other route to the same object. The Galois action is the one case built here, because its target is the coordinate ring of W⁄A itself rather than of (W⁄A).map σ: it is AdjoinRoot.mapRingEquiv along the coefficientwise automorphism, which fixes the Weierstrass polynomial of a curve defined over R, so no transport along (W⁄A).map σ = W⁄A is needed.

XYIdeal W x y is the ideal generated by XClass W x and YClass W y for an arbitrary x : R and y : R[X], and that is all map_XYIdeal uses. Reading it as "the ideal of a point" needs hypotheses stated nowhere here — that (x, y) satisfy the curve equation — and reading it as a maximal ideal needs a field as well; Mathlib's XYIdeal' and XYIdeal_eq₂ are the statements that carry those. So this is a result about the generators, not about points.

Stated over arbitrary commutative rings; the curve need not be elliptic.

The commutation results serve 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, compatible with identity, composition, degree, separability, MapsInfinity, duals, and induced point maps": these are that compatibility for the coordinate ring and the distinguished elements Mathlib singles out in it. They do not on their own supply the "induced point maps" clause, which needs the curve equation these statements do not assume.

The surjectivity results support the Hasse strand of the same file, Layer 3. That roadmap's Layer-0 narrative makes the Frobenius "the key input to Layer 3", and the arithmetic Frobenius of the function field over a finite field is obtained by transporting the q-power map of the base to the coordinate ring, which needs exactly this bijectivity. The roadmap's §"What Mathlib already has (consume)" lists Affine.CoordinateRing as consumed infrastructure that "is load-bearing API here, not an implementation detail"; this is a complement to that API, not a reimplementation of it.

Provenance

The need for these statements is from the AINTLIB HasseWeil project (github.com/CBirkbeck/AINTLIB, Apache-2.0, pinned by that roadmap at dev/hasse-weil @ 513e83879e2f), HasseWeil/WeilPairing/FrobeniusFunctionFieldEquiv.lean, declaration coordRingMap_bijective. There they are bundled as bijectivity of one map, for a ring equivalence only — surjectivity being obtained by lifting along e.symm — inside a 267-line file that also constructs the function-field Frobenius. Here there is no inverse to lift along: the statement is for an arbitrary surjective f : R →+* S, matching the generality of Mathlib's CoordinateRing.map_injective, and preimages come from Polynomial.map_surjective. The argument itself lives one level down, in TauCeti/RingTheory/AdjoinRoot/Basic.lean; the equivalence the source bundled it for is left to the use site.

map_XClass, map_YClass and map_XYIdeal are adapted from the same project's HasseWeil/WeilPairing/DivisorGalois.lean (declarations of the same names), where they are stated for a WeierstrassCurve.Affine and its image under a ring homomorphism. The proofs are that file's.

theorem WeierstrassCurve.Affine.CoordinateRing.ringHom_ext {R : Type u_1} [CommRing R] (W : Affine R) {T : Type u_3} [Semiring T] {f g : W.CoordinateRing →+* T} (hc : ∀ (a : R), f ((algebraMap R W.CoordinateRing) a) = g ((algebraMap R W.CoordinateRing) a)) (hx : f ((AdjoinRoot.of W.polynomial) Polynomial.X) = g ((AdjoinRoot.of W.polynomial) Polynomial.X)) (hy : f (AdjoinRoot.root W.polynomial) = g (AdjoinRoot.root W.polynomial)) : f = g

Ring homomorphisms out of the coordinate ring are determined by the constants and the classes of x and y.

theorem WeierstrassCurve.Affine.CoordinateRing.map_surjective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (W : Affine R) {f : R →+* S} (hf : Function.Surjective ⇑f) : Function.Surjective ⇑(map W f)

CoordinateRing.map is surjective when the base map is, the companion of Mathlib's CoordinateRing.map_injective.

theorem WeierstrassCurve.Affine.CoordinateRing.map_bijective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (W : Affine R) {f : R →+* S} (hf : Function.Bijective ⇑f) : Function.Bijective ⇑(map W f)

CoordinateRing.map is bijective when the base map is.

@[simp]

theorem WeierstrassCurve.Affine.CoordinateRing.map_XClass {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (W : Affine R) (f : R →+* S) (x : R) : (map W f) (XClass W x) = XClass (W.map f) (f x)

CoordinateRing.map f commutes with XClass: the class of X - x goes to the class of X - f x on the mapped curve.

@[simp]

theorem WeierstrassCurve.Affine.CoordinateRing.map_YClass {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (W : Affine R) (f : R →+* S) (y : Polynomial R) : (map W f) (YClass W y) = YClass (W.map f) (Polynomial.map f y)

CoordinateRing.map f commutes with YClass: the class of Y - y(X) goes to the class of Y - (y.map f)(X) on the mapped curve.

@[simp]

theorem WeierstrassCurve.Affine.CoordinateRing.map_XYIdeal {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (W : Affine R) (f : R →+* S) (x : R) (y : Polynomial R) : Ideal.map (map W f) (XYIdeal W x y) = XYIdeal (W.map f) (f x) (Polynomial.map f y)

CoordinateRing.map f commutes with XYIdeal: the ideal generated by XClass W x and YClass W y pushes forward to the one generated by XClass (W.map f) (f x) and YClass (W.map f) (y.map f). No curve equation on (x, y) is assumed.

@[simp]

theorem WeierstrassCurve.Affine.CoordinateRing.map_of_X {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (W : Affine R) (f : R →+* S) : (map W f) ((AdjoinRoot.of W.polynomial) Polynomial.X) = (AdjoinRoot.of (W.map f).polynomial) Polynomial.X

CoordinateRing.map sends the class of X to the class of X.

@[simp]

theorem WeierstrassCurve.Affine.CoordinateRing.map_root {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (W : Affine R) (f : R →+* S) : (map W f) (AdjoinRoot.root W.polynomial) = AdjoinRoot.root (W.map f).polynomial

CoordinateRing.map sends the class of Y to the class of Y.

@[simp]

theorem WeierstrassCurve.Affine.CoordinateRing.map_algebraMap {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (W : Affine R) (f : R →+* S) (r : R) : (map W f) ((algebraMap R W.CoordinateRing) r) = (algebraMap S (W.map f).CoordinateRing) (f r)

CoordinateRing.map commutes with the scalars: it is a map of R-algebras up to the base change f itself.

@[simp]

theorem WeierstrassCurve.Affine.CoordinateRing.map_id {R : Type u_1} [CommRing R] (W : Affine R) : map W (RingHom.id R) = RingHom.id W.CoordinateRing

CoordinateRing.map along the identity is the identity.

theorem WeierstrassCurve.Affine.CoordinateRing.map_comp_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (W : Affine R) {T : Type u_3} [CommRing T] (f : R →+* S) (g : S →+* T) : (map (W.map f) g).comp (map W f) = map W (g.comp f)

CoordinateRing.map is functorial. The curve equality (W.map f).map g = W.map (g.comp f) holds definitionally, so the statement needs no transport.

@[simp]

theorem WeierstrassCurve.Affine.CoordinateRing.map_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (W : Affine R) {T : Type u_3} [CommRing T] (f : R →+* S) (g : S →+* T) (z : W.CoordinateRing) : (map (W.map f) g) ((map W f) z) = (map W (g.comp f)) z

Pointwise functoriality of CoordinateRing.map.

noncomputable def WeierstrassCurve.coordinateRingGaloisAction {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (W : WeierstrassCurve R) : (A ≃ₐ[R] A) →* (W.baseChange A).toAffine.CoordinateRing ≃+* (W.baseChange A).toAffine.CoordinateRing

The Galois action on the coordinate ring of a base-changed Weierstrass curve. An R-automorphism σ of A acts on A[W] by applying σ to the coefficients and fixing the classes of x and y: it is AdjoinRoot.mapRingEquiv along the coefficientwise σ, which fixes the Weierstrass polynomial because W is defined over R.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem WeierstrassCurve.coordinateRingGaloisAction_mk {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (W : WeierstrassCurve R) (σ : A ≃ₐ[R] A) (p : Polynomial (Polynomial A)) : (W.coordinateRingGaloisAction σ) ((Affine.CoordinateRing.mk (W.baseChange A).toAffine) p) = (Affine.CoordinateRing.mk (W.baseChange A).toAffine) (Polynomial.map (Polynomial.mapRingHom ↑σ) p)

The coordinate-ring Galois action on the class of a polynomial: it applies the automorphism to the coefficients, as Mathlib's CoordinateRing.map_mk does for map.

@[simp]

theorem WeierstrassCurve.coordinateRingGaloisAction_of {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (W : WeierstrassCurve R) (σ : A ≃ₐ[R] A) (p : Polynomial A) : (W.coordinateRingGaloisAction σ) ((AdjoinRoot.of (W.baseChange A).toAffine.polynomial) p) = (AdjoinRoot.of (W.baseChange A).toAffine.polynomial) (Polynomial.map (↑σ) p)

On the polynomial subring, the coordinate-ring Galois action maps coefficients and fixes x.

@[simp]

theorem WeierstrassCurve.coordinateRingGaloisAction_root {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (W : WeierstrassCurve R) (σ : A ≃ₐ[R] A) : (W.coordinateRingGaloisAction σ) (AdjoinRoot.root (W.baseChange A).toAffine.polynomial) = AdjoinRoot.root (W.baseChange A).toAffine.polynomial

The coordinate-ring Galois action fixes the class of y.

@[simp]

theorem WeierstrassCurve.coordinateRingGaloisAction_algebraMap {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (W : WeierstrassCurve R) (σ : A ≃ₐ[R] A) (a : A) : (W.coordinateRingGaloisAction σ) ((algebraMap A (W.baseChange A).toAffine.CoordinateRing) a) = (algebraMap A (W.baseChange A).toAffine.CoordinateRing) (σ a)

The coordinate-ring Galois action applies the automorphism to constants.