Galois descent for Weierstrass curve data

Let L/K be a separable quadratic extension. Data attached to a Weierstrass curve over L and fixed by the nontrivial σ ∈ Gal(L/K) descends to K, because an element of L fixed by σ is already in K (Algebra.IsQuadraticExtension.mem_range_algebraMap_of_apply_eq). Two descent results are proved here:

• WeierstrassCurve.VariableChange.exists_baseChange_eq_of_map_eq: an admissible change of variables over L fixed by σ is the base change of one over K;
• WeierstrassCurve.Affine.Point.exists_baseChange_eq_of_map_eq: an affine point of W over L fixed by σ is the base change of a point over K.

Both are stated with σ an explicit nontrivial automorphism rather than a quantifier over Gal(L/K): for a quadratic extension the two are equivalent, and the consumers have a distinguished σ in hand.

These are the descent steps of the quadratic-twist layer of TauCetiRoadmap/EllipticCurves/README.md (§Layer 5): the twist point isomorphism and the classification of twists both descend L-data fixed by the Galois action to K-data.

Adapted from the FLT project (ImperialCollegeLondon/FLT, FLT/Mathlib/AlgebraicGeometry/EllipticCurve/GaloisDescent.lean at the roadmap's pin bc2fe8ff7396, FLT PR #1088, Apache 2.0). That file's own header reads Authors: Kevin Buzzard, Michael Stoll, Claude; following this repository's convention for adapted material, the upstream authorship is credited here rather than in the copyright header. Ported against Mathlib's own VariableChange.baseChange and Affine.Point.baseChange rather than the source's complements to them.

theorem WeierstrassCurve.VariableChange.exists_baseChange_eq_of_map_eq {K : Type u_1} [Field K] (L : Type u_2) [Field L] [Algebra K L] [Algebra.IsQuadraticExtension K L] [Algebra.IsSeparable K L] {σ : Gal(L/K)} (hσ : σ ≠ 1) {C : VariableChange L} (hCinv : C.map (↑σ).toRingHom = C) : ∃ (CK : VariableChange K), CK.baseChange L = C

Galois descent for changes of variables. A change of variables over L fixed by the nontrivial σ ∈ Gal(L/K) has all its coefficients in K, so it is the base change of a change of variables over K.

theorem WeierstrassCurve.Affine.Point.exists_baseChange_eq_of_map_eq {K : Type u_1} [Field K] (L : Type u_2) [Field L] [Algebra K L] [Algebra.IsQuadraticExtension K L] [Algebra.IsSeparable K L] [DecidableEq K] [DecidableEq L] {W : WeierstrassCurve K} {σ : Gal(L/K)} (hσ : σ ≠ 1) {R : (Affine.baseChange W L).Point} (hR : (map ↑σ) R = R) : ∃ (Q : (Affine.baseChange W K).Point), (baseChange K L) Q = R

Galois descent for points. A point of W(L) fixed by the nontrivial σ ∈ Gal(L/K) (hence, as [L : K] = 2, by all of Gal(L/K)) is the base change of a point of W(K): its coordinates, being fixed by σ, lie in K.