Base change of the étale algebra, and the local condition of 2-descent

Let W : y² = f(x) = x³ + a₂x² + a₄x + a₆ be an elliptic curve in characteristic ≠ 2 normal form over a field K, with étale algebra A = K[X]⧸⟨f⟩ and descent map μ : W(K) → M = Aˣ/(Aˣ)², as set up in TauCeti/AlgebraicGeometry/EllipticCurve/MordellWeil/XSubT.lean.

Everything in that construction base-changes along a field extension L/K — in the arithmetic application L is a completion of K. This file builds that base change and uses it to define the local condition at L: the subgroup

W.localCondition L : Subgroup W.M

of square classes whose image in (W⁄L).M lies in the image of the local descent map μ_L. The 2-Selmer group of W is cut out of W.M by these conditions at all completions of K, so localCondition is the object every later descent statement is phrased in.

Main definitions

• WeierstrassCurve.Affine.mapA: the base-change homomorphism K[X]⧸⟨f⟩ →+* L[X]⧸⟨f⟩ of étale algebras.
• WeierstrassCurve.Affine.localRes: the induced map W.M →* (W⁄L).M on square classes.
• WeierstrassCurve.Affine.pointMap: the base-change homomorphism W(K) →+ W(L) on points.
• WeierstrassCurve.Affine.localCondition: the local 2-descent condition at L.

Main statements

• WeierstrassCurve.Affine.localRes_μX and WeierstrassCurve.Affine.localRes_comp_μ: the descent map is natural under base change — restricting square classes after the global μ is applying the local μ after the base change of points.
• WeierstrassCurve.Affine.range_μ_le_localCondition: the image of the global descent map satisfies the local condition at every extension field. This is what makes localCondition a condition: it is a constraint the classes coming from W(K) are known to satisfy, so the intersection of the local conditions bounds W(K)/2W(K) from above.
• WeierstrassCurve.Affine.card_range_μ_of_surjective_algebraMap: base change along an isomorphism preserves the size of the descent image, via WeierstrassCurve.Affine.range_μ_of_surjective_algebraMap, which identifies the two images. This is the transport step: a count of #(im μ) established over a concrete field carries to any field isomorphic to it. Its inputs are WeierstrassCurve.Affine.bijective_mapA_of_surjective_algebraMap and WeierstrassCurve.Affine.localRes_injective_of_surjective_algebraMap.

Implementation notes

Square classes are spelled W.M, the quotient of W.Aˣ by the range of powMonoidHom 2, following XSubT.lean; the source uses a local abbreviation Units.modPow for the same group, which is not a Mathlib declaration and which TauCeti deliberately does not carry, so that the repository has a single spelling of square classes. Accordingly localRes is built from QuotientGroup.map rather than from the source's Units.modPow.map.

pointMap is Mathlib's WeierstrassCurve.Affine.Point.map and is not a new construction: the only content is the alignment of W with W⁄K, which baseChange_self supplies and Mathlib's AddEquiv.cast transports along.

Provenance

Adapted, with the author's proofs, from Michael Stoll's EllipticCurves project (github.com/MichaelStollBayreuth/EllipticCurves, Apache-2.0, pinned by TauCetiRoadmap/EllipticCurves/README.md at 66889eada51a), EllipticCurves/SelmerGroup.lean lines 85-323 — that file's BaseChange section: lines 85-295 give the base change up to the local condition and its compatibility with μ, and lines 296-323 give the isomorphism-invariance block — range_μ_of_bijective_algebraMap and card_range_μ_of_bijective_algebraMap upstream, renamed here for the weaker hypothesis — plus the étale-algebra bijectivity at line 168.

One declaration is not adapted from the source: localRes_injective_of_surjective_algebraMap is re-derived here. The source obtains it from its local Units.modPow.bijective_map, which is in the square-class spelling this repository does not carry, and Mathlib has no QuotientGroup.map injectivity helper to appeal to instead.

This advances TauCetiRoadmap/EllipticCurves/README.md, Layer 6 (README:813-820), whose "Explicit 2-descent (core, this layer)" bullet names "the local conditions" as the first item to migrate.

@[simp]

theorem WeierstrassCurve.Affine.baseChange_self {R : Type u_1} [CommRing R] (W : Affine R) : toAffine (W.baseChange R) = W

Base changing along the identity algebra map returns the curve itself. Stated over a commutative ring: it is a formal map identity and uses nothing about R beyond its ring structure.

theorem WeierstrassCurve.Affine.map_f {R : Type u_1} [CommRing R] (W : Affine R) {S : Type u_2} [CommRing S] (σ : R →+* S) : (toAffine (W.map σ)).f = Polynomial.map σ W.f

theorem WeierstrassCurve.Affine.eval_map_f {R : Type u_1} [CommRing R] (W : Affine R) {S : Type u_2} [CommRing S] (σ : R →+* S) (x : R) : Polynomial.eval (σ x) (toAffine (W.map σ)).f = σ (Polynomial.eval x W.f)

theorem WeierstrassCurve.Affine.map_fCofactor {R : Type u_1} [CommRing R] (W : Affine R) {S : Type u_2} [CommRing S] (σ : R →+* S) (x : R) : Polynomial.map σ (W.fCofactor x) = (toAffine (W.map σ)).fCofactor (σ x)

theorem WeierstrassCurve.Affine.eval_baseChange_f {R : Type u_1} [CommRing R] (W : Affine R) (S : Type u_2) [CommRing S] [Algebra R S] (x : R) : Polynomial.eval ((algebraMap R S) x) (toAffine (W.baseChange S)).f = (algebraMap R S) (Polynomial.eval x W.f)

theorem WeierstrassCurve.Affine.baseChange_fCofactor {R : Type u_1} [CommRing R] (W : Affine R) (S : Type u_2) [CommRing S] [Algebra R S] (x : R) : Polynomial.map (algebraMap R S) (W.fCofactor x) = (toAffine (W.baseChange S)).fCofactor ((algebraMap R S) x)

theorem WeierstrassCurve.Affine.baseChange_f {R : Type u_1} [CommRing R] (W : Affine R) (S : Type u_2) [CommRing S] [Algebra R S] : (toAffine (W.baseChange S)).f = Polynomial.map (algebraMap R S) W.f

noncomputable def WeierstrassCurve.Affine.mapA {K : Type u_1} [Field K] (W : Affine K) (L : Type u_2) [Field L] [Algebra K L] : W.A →+* (toAffine (W.baseChange L)).A

The base-change homomorphism K[X]⧸⟨f⟩ →+* L[X]⧸⟨f⟩ of étale algebras, as an instance of AdjoinRoot.map (so that its API — map_of, map_root, map_comp_map, mapRingEquiv — applies directly).

Equations

• W.mapA L = AdjoinRoot.map (algebraMap K L) W.f (WeierstrassCurve.toAffine (W.baseChange L)).f ⋯

@[simp]

theorem WeierstrassCurve.Affine.mapA_mk {K : Type u_1} [Field K] (W : Affine K) (L : Type u_2) [Field L] [Algebra K L] (p : Polynomial K) : (W.mapA L) ((AdjoinRoot.mk W.f) p) = (AdjoinRoot.mk (toAffine (W.baseChange L)).f) (Polynomial.map (algebraMap K L) p)

noncomputable def WeierstrassCurve.Affine.localRes {K : Type u_1} [Field K] (W : Affine K) (L : Type u_2) [Field L] [Algebra K L] : M →* M

The base-change map on square classes of units of the étale algebra.

Equations

• W.localRes L = QuotientGroup.map (powMonoidHom 2).range (powMonoidHom 2).range (Units.map ↑(W.mapA L)) ⋯

@[simp]

theorem WeierstrassCurve.Affine.localRes_mk {K : Type u_1} [Field K] (W : Affine K) (L : Type u_2) [Field L] [Algebra K L] (u : W.Aˣ) : (W.localRes L) ↑u = ↑((Units.map ↑(W.mapA L)) u)

theorem WeierstrassCurve.Affine.localRes_unit {K : Type u_1} [Field K] (W : Affine K) (L : Type u_2) [Field L] [Algebra K L] {a : W.A} (ha : IsUnit a) : (W.localRes L) ↑ha.unit = ↑⋯.unit

The base-change map on square classes, on the class of a unit given as IsUnit a.

theorem WeierstrassCurve.Affine.bijective_mapA_of_surjective_algebraMap {K : Type u_1} [Field K] (W : Affine K) (L : Type u_2) [Field L] [Algebra K L] (h : Function.Surjective ⇑(algebraMap K L)) : Function.Bijective ⇑(W.mapA L)

Base change of the étale algebra along a surjective algebra map of fields is an isomorphism: mapA is AdjoinRoot.map, which AdjoinRoot.mapRingEquiv upgrades.

Surjectivity is the whole hypothesis: a ring homomorphism out of a field is automatically injective, so algebraMap K L is bijective as soon as it is onto.

theorem WeierstrassCurve.Affine.localRes_injective_of_surjective_algebraMap {K : Type u_1} [Field K] (W : Affine K) (L : Type u_2) [Field L] [Algebra K L] (h : Function.Surjective ⇑(algebraMap K L)) : Function.Injective ⇑(W.localRes L)

Along an isomorphism, the base-change map on square classes is injective: a square root of mapA a pulls back along the isomorphism to a square root of a.

noncomputable def WeierstrassCurve.Affine.pointMap {K : Type u_1} [Field K] (W : Affine K) (L : Type u_2) [Field L] [Algebra K L] : W.Point →+ (toAffine (W.baseChange L)).Point

The base-change homomorphism on points, W(K) →+ W(L): Mathlib's WeierstrassCurve.Affine.Point.map, aligned with the plain base change W⁄L via baseChange_self.

Equations

• W.pointMap L = (WeierstrassCurve.Affine.Point.map (Algebra.ofId K L)).comp (AddEquiv.cast ⋯).toAddMonoidHom

@[simp]

theorem WeierstrassCurve.Affine.pointMap_some {K : Type u_1} [Field K] (W : Affine K) (L : Type u_2) [Field L] [Algebra K L] {x y : K} (h : W.Nonsingular x y) : (W.pointMap L) (Point.some x y h) = Point.some ((algebraMap K L) x) ((algebraMap K L) y) ⋯

The base-change map on an affine point carries its coordinates along algebraMap K L.

noncomputable def WeierstrassCurve.Affine.localCondition {K : Type u_1} [Field K] (W : Affine K) (L : Type u_2) [Field L] [Algebra K L] [WeierstrassCurve.IsElliptic W] [IsCharNeTwoNF W] : Subgroup M

The local 2-descent condition at the extension field L of K (in the applications, L is a completion of K): the subgroup of square classes in the étale algebra of W whose image over L comes from an L-point of the curve.

Equations

• W.localCondition L = Subgroup.comap (W.localRes L) WeierstrassCurve.Affine.μ.range

@[simp]

theorem WeierstrassCurve.Affine.mem_localCondition_iff {K : Type u_1} [Field K] (W : Affine K) (L : Type u_2) [Field L] [Algebra K L] [WeierstrassCurve.IsElliptic W] [IsCharNeTwoNF W] {m : M} : m ∈ W.localCondition L ↔ (W.localRes L) m ∈ μ.range

theorem WeierstrassCurve.Affine.localRes_μX {K : Type u_1} [Field K] (W : Affine K) (L : Type u_2) [Field L] [Algebra K L] [WeierstrassCurve.IsElliptic W] [IsCharNeTwoNF W] (x : K) : (W.localRes L) (μX x) = μX ((algebraMap K L) x)

The local restriction map is compatible with the x - T maps: the square class of x - T restricts to that of σ(x) - T, and likewise for the modified class at a 2-torsion x-coordinate.

theorem WeierstrassCurve.Affine.localRes_comp_μ {K : Type u_1} [Field K] (W : Affine K) (L : Type u_2) [Field L] [Algebra K L] [WeierstrassCurve.IsElliptic W] [IsCharNeTwoNF W] : (W.localRes L).comp μ = μ.comp (AddMonoidHom.toMultiplicative (W.pointMap L))

Naturality of the descent map under base change: restricting square classes after the global μ is applying the local μ after the base change of points.

theorem WeierstrassCurve.Affine.range_μ_le_localCondition {K : Type u_1} [Field K] (W : Affine K) (L : Type u_2) [Field L] [Algebra K L] [WeierstrassCurve.IsElliptic W] [IsCharNeTwoNF W] : μ.range ≤ W.localCondition L

The image of the global descent map μ satisfies the local condition at every extension field: this is formal from the naturality localRes_comp_μ.

Base change along an isomorphism

If L/K is an isomorphism rather than a proper extension, nothing is lost: the étale algebras are isomorphic, so the descent map has the same image over L as over K. This is what lets a count established over a concrete field — ℝ, say — be transported to a completion that is merely isomorphic to it.

theorem WeierstrassCurve.Affine.range_μ_of_surjective_algebraMap {K : Type u_1} [Field K] (W : Affine K) (L : Type u_2) [Field L] [Algebra K L] [WeierstrassCurve.IsElliptic W] [IsCharNeTwoNF W] (h : Function.Surjective ⇑(algebraMap K L)) : μ.range = Subgroup.map (W.localRes L) μ.range

Along an isomorphism, the descent image over L is the image of the descent image over K under the local restriction of square classes. Formal from the naturality localRes_comp_μ, once base change of points is seen to be surjective.

theorem WeierstrassCurve.Affine.card_range_μ_of_surjective_algebraMap {K : Type u_1} [Field K] (W : Affine K) (L : Type u_2) [Field L] [Algebra K L] [WeierstrassCurve.IsElliptic W] [IsCharNeTwoNF W] (h : Function.Surjective ⇑(algebraMap K L)) : Nat.card ↥μ.range = Nat.card ↥μ.range

Base change along an isomorphism preserves the size of the descent image. This is the transport step: a count of #(im μ) established over one field carries to any field isomorphic to it.