FLT/Mathlib/AlgebraicGeometry/EllipticCurve/GaloisDescent.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned FLT blueprint introduction

2 declarations, 0 contain sorry, 0 declared as axioms

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.

Imports (3)
Imported by 2 files
  1. lemma WeierstrassCurve.exists_baseChange_eq_of_map_eq Galois descent for changes of variables line 34 source

    Source documentation

    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.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Field, Algebra, Algebra.IsQuadraticExtension, Algebra.IsSeparable, AlgEquiv, Ne, OfNat.ofNat, WeierstrassCurve.VariableChange, Eq, WeierstrassCurve.VariableChange.map, AlgHom.toRingHom, Exists, WeierstrassCurve.VariableChange.baseChange

    Proof uses: RingHom, rfl, Membership.mem, Set, Set.range, Algebra.algebraMap, Algebra.IsQuadraticExtension.mem_range_algebraMap_of_apply_eq, WeierstrassCurve.VariableChange.u, congrArg, WeierstrassCurve.VariableChange.r, WeierstrassCurve.VariableChange.s, WeierstrassCurve.VariableChange.t, False, Units.ne_zero, Eq.symm, Eq.mp, map_zero, Exists.intro, WeierstrassCurve.VariableChange.mk, Units.mk0 and 3 more

    52 instances, coercions and auxiliary constants left out.

    Tactic trace: 20 steps

    Open to load the checked before-and-after goal states.

    lemma exists_baseChange_eq_of_map_eq {σ : L ≃ₐ[K] L} (hσ : σ ≠ 1) {C : VariableChange L}
    (hCinv : C.map σ.toAlgHom.toRingHom = C) : ∃ CK : VariableChange K, CK.baseChange L = C := by
…
  2. theorem WeierstrassCurve.exists_baseChange_point_eq_of_map_eq Galois descent for points line 58 source

    Source documentation

    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.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Field, Algebra, Algebra.IsQuadraticExtension, Algebra.IsSeparable, DecidableEq, WeierstrassCurve, AlgEquiv, Ne, OfNat.ofNat, WeierstrassCurve.Affine.Point, WeierstrassCurve.Affine.baseChange, Eq, AddMonoidHom, WeierstrassCurve.Affine.Point.map, Exists, WeierstrassCurve.Affine.Point.baseChange

    Proof uses: WeierstrassCurve.Affine.Point.zero, Exists.intro, rfl, WeierstrassCurve.Affine.Nonsingular, WeierstrassCurve.Affine.Point.some, AlgHom, Iff.mpr, WeierstrassCurve.Affine.baseChange_nonsingular, RingHom.injective, AlgHom.toRingHom, Eq.mp, congrArg, WeierstrassCurve.Affine.Point.map_some, HEq, RingHom, Algebra.algebraMap, Membership.mem, Set, Set.range, Algebra.IsQuadraticExtension.mem_range_algebraMap_of_apply_eq and 4 more

    89 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

    Open to load the checked before-and-after goal states.

    theorem exists_baseChange_point_eq_of_map_eq [DecidableEq K] [DecidableEq L]
    {W : WeierstrassCurve K} {σ : L ≃ₐ[K] L} (hσ : σ ≠ 1) {R : (W⁄L).Point}
    (hR : Affine.Point.map σ.toAlgHom R = R) :
    ∃ Q : (W⁄K).Point, Affine.Point.baseChange K L Q = R := by
…