Galois descent for Weierstrass curve data

Proposed new Mathlib file Mathlib.AlgebraicGeometry.EllipticCurve.GaloisDescent: a change of variables (or a point) over a separable quadratic extension L/K fixed by Gal(L/K) descends to K.

theorem WeierstrassCurve.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.exists_baseChange_point_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 : (Affine.Point.map ↑σ) R = R) : ∃ (Q : (Affine.baseChange W K).Point), (Affine.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.