Galois conjugation of changes of variables

An admissible change of variables with algebraic coefficients has a locally constant orbit under the Krull topology. This gives continuity for the cocycles attached to pointed twists of Weierstrass curves. Descent is developed in TauCeti/AlgebraicGeometry/EllipticCurve/GaloisDescent.lean.

theorem WeierstrassCurve.VariableChange.isLocallyConstant_map {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (C : VariableChange L) (hu : IsIntegral K ↑C.u) (hr : IsIntegral K C.r) (hs : IsIntegral K C.s) (ht : IsIntegral K C.t) : IsLocallyConstant fun (σ : Gal(L/K)) => C.map ↑σ

Conjugation of a change of variables with integral coefficients is locally constant for the Krull topology. No algebraicity assumption on the whole extension is needed.

theorem WeierstrassCurve.VariableChange.isLocallyConstant_map_of_isAlgebraic {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] (C : VariableChange L) : IsLocallyConstant fun (σ : Gal(L/K)) => C.map ↑σ

Over an algebraic extension, every change of variables has a locally constant Galois orbit.