VariableChange.lean`

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

Annotation provenance. This overlay contains 8 curated AI-written annotations and 1204 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

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

12 declarations, 0 contain sorry, 0 declared as axioms

Complements on admissible changes of variables

Material for Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange: decidable equality, the negation automorphism [-1], compatibility of changes of variables with base change, and Galois descent for changes of variables.

Imports (3)

Imported by 3 files

instance WeierstrassCurve.VariableChange.instDecidableEq Two admissible changes of variables agree iff their four coefficients do; this makes equality of changes of variables decidable over a commutative ring with decidable equality line 28 source
Source documentation
Two admissible changes of variables agree iff their four coefficients do; this makes equality of changes of variables decidable over a commutative ring with decidable equality.

no axioms what this means
Statement uses: CommRing, DecidableEq, WeierstrassCurve.VariableChange
Proof uses: decidable_of_iff, Eq, And, Units, WeierstrassCurve.VariableChange.u, WeierstrassCurve.VariableChange.r, WeierstrassCurve.VariableChange.s, WeierstrassCurve.VariableChange.t
6 instances, coercions and auxiliary constants left out.
```
instance VariableChange.instDecidableEq {R : Type*} [CommRing R] [DecidableEq R] :
    DecidableEq (VariableChange R) :=
…
```
def WeierstrassCurve.negVariableChange The automorphism [-1] : (x, y) ↦ (x, -y - a₁x - a₃) of a Weierstrass curve, as an admissible change of variables ⟨-1, 0, -a₁, -a₃⟩ line 37 source
Source documentation
The automorphism [-1] : (x, y) ↦ (x, -y - a₁x - a₃) of a Weierstrass curve, as an admissible change of variables ⟨-1, 0, -a₁, -a₃⟩. It fixes E (negVariableChange_smul_self) and is an involution (negVariableChange_mul_self).

standard axioms: Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, WeierstrassCurve.VariableChange
Proof uses: WeierstrassCurve.VariableChange.mk, Neg.neg, Units, OfNat.ofNat, WeierstrassCurve.a₁, WeierstrassCurve.a₃
25 instances, coercions and auxiliary constants left out.
```
def negVariableChange : VariableChange K :=
…
```
lemma WeierstrassCurve.negVariableChange_u line 40 source
standard axioms: Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, Eq, Units, WeierstrassCurve.VariableChange.u, WeierstrassCurve.negVariableChange, Neg.neg, OfNat.ofNat
Proof uses: rfl
15 instances, coercions and auxiliary constants left out.
lemma WeierstrassCurve.negVariableChange_smul_self line 42 source
standard axioms: Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, Eq, HSMul.hSMul, WeierstrassCurve.VariableChange, WeierstrassCurve.negVariableChange
Proof uses: Eq.mpr, WeierstrassCurve.mk, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Nat, WeierstrassCurve.a₁, Neg.neg, HSub.hSub, WeierstrassCurve.a₂, HPow.hPow, WeierstrassCurve.a₃, WeierstrassCurve.a₄, WeierstrassCurve.a₆, id, congrFun', congrArg, congr, Inv.inv, Units and 93 more
97 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma WeierstrassCurve.negVariableChange_mul_self line 46 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, Eq, WeierstrassCurve.VariableChange, HMul.hMul, WeierstrassCurve.negVariableChange, OfNat.ofNat
Proof uses: of_eq_true, WeierstrassCurve.VariableChange.mk, Units, Eq.trans, True, congrFun', congrArg, congr, WeierstrassCurve.VariableChange.u, Neg.neg, WeierstrassCurve.a₁, WeierstrassCurve.a₃, HAdd.hAdd, WeierstrassCurve.VariableChange.r, HPow.hPow, Nat, WeierstrassCurve.VariableChange.s, WeierstrassCurve.VariableChange.t, mul_neg, mul_one and 21 more
75 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma WeierstrassCurve.negVariableChange_inv line 50 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, Eq, WeierstrassCurve.VariableChange, Inv.inv, WeierstrassCurve.negVariableChange
Proof uses: inv_eq_of_mul_eq_one_right, WeierstrassCurve.negVariableChange_mul_self
5 instances, coercions and auxiliary constants left out.
lemma WeierstrassCurve.negVariableChange_map Base change commutes with the negation automorphism: mapping [-1] on W through a ring homomorphism φ gives [-1] on W.map φ line 55 source
Source documentation
Base change commutes with the negation automorphism: mapping [-1] on W through a ring homomorphism φ gives [-1] on W.map φ.

standard axioms: Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, RingHom, Eq, WeierstrassCurve.VariableChange, WeierstrassCurve.VariableChange.map, WeierstrassCurve.negVariableChange, WeierstrassCurve.map
Proof uses: WeierstrassCurve.VariableChange.ext, Units.ext, WeierstrassCurve.VariableChange.u, of_eq_true, Eq.trans, Neg.neg, OfNat.ofNat, True, congr, congrArg, Units, WeierstrassCurve.VariableChange.mk, WeierstrassCurve.a₁, WeierstrassCurve.a₃, MonoidHom, Units.map, WeierstrassCurve.VariableChange.map_u, Units.map_neg, map_one, WeierstrassCurve.map_a₁ and 10 more
60 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma negVariableChange_map {A B : Type*} [Field A] [Field B] (W : WeierstrassCurve A)
    (φ : A →+* B) : W.negVariableChange.map φ = (W.map φ).negVariableChange := by
…
```
Mentions: WeierstrassCurve.negVariableChange
lemma WeierstrassCurve.negVariableChange_ne_one Documented declaration: negVariableChange_ne_one line 62 source
Source documentation
The negation automorphism is nontrivial for an elliptic curve: in characteristic ≠ 2 it has u = -1 ≠ 1, and in characteristic 2 it has (s, t) = (-a₁, -a₃) ≠ (0, 0), since an elliptic curve in characteristic 2 cannot have a₁ = a₃ = 0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, WeierstrassCurve.IsElliptic, Ne, WeierstrassCurve.VariableChange, WeierstrassCurve.negVariableChange, OfNat.ofNat
Proof uses: Eq, Nat, Or, False, eq_or_ne, WeierstrassCurve.VariableChange.s, congrArg, WeierstrassCurve.VariableChange.t, Eq.mp, WeierstrassCurve.a₁, WeierstrassCurve.a₃, Mathlib.Tactic.Contrapose.contrapose₂, Not, Neg.neg, WeierstrassCurve.VariableChange.u, Mathlib.Tactic.LinearCombination.eq_of_eq, Eq.symm, Mathlib.Tactic.LinearCombination.eq_rearrange, HAdd.hAdd, Mathlib.Tactic.Ring.of_eq and 33 more
51 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma negVariableChange_ne_one [E.IsElliptic] : E.negVariableChange ≠ 1 := by
…
```
lemma WeierstrassCurve.negVariableChange_baseChange_map The automorphism [-1] of E over L is defined over K, hence fixed by the Galois action: its components -1, 0, -a₁, -a₃ all lie in K line 80 source
Source documentation
The automorphism [-1] of E over L is defined over K, hence fixed by the Galois action: its components -1, 0, -a₁, -a₃ all lie in K.

standard axioms: Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, Algebra, AlgEquiv, Eq, WeierstrassCurve.VariableChange, WeierstrassCurve.VariableChange.map, WeierstrassCurve.negVariableChange, WeierstrassCurve.baseChange, AlgHom.toRingHom
Proof uses: WeierstrassCurve.VariableChange.ext, Units.ext, WeierstrassCurve.VariableChange.u, of_eq_true, Eq.trans, Neg.neg, OfNat.ofNat, True, congr, congrArg, Units, WeierstrassCurve.VariableChange.mk, RingHom, Algebra.algebraMap, WeierstrassCurve.a₁, WeierstrassCurve.a₃, MonoidHom, Units.map, WeierstrassCurve.VariableChange.r, WeierstrassCurve.VariableChange.s and 9 more
67 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma negVariableChange_baseChange_map (σ : L ≃ₐ[K] L) :
    (E.baseChange L).negVariableChange.map σ.toAlgHom.toRingHom
      = (E.baseChange L).negVariableChange := by
…
```
Mentions: WeierstrassCurve.negVariableChange
lemma WeierstrassCurve.baseChange_smul_baseChange Base change commutes with the action of changes of variables line 87 source
Source documentation
Base change commutes with the action of changes of variables.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, WeierstrassCurve.VariableChange, WeierstrassCurve, Eq, HSMul.hSMul, WeierstrassCurve.VariableChange.baseChange, WeierstrassCurve.baseChange
Proof uses: WeierstrassCurve.map_variableChange, Algebra.algebraMap
10 instances, coercions and auxiliary constants left out.
```
lemma baseChange_smul_baseChange (C : VariableChange K) (V : WeierstrassCurve K) :
    (C.baseChange L) • V.baseChange L = (C • V).baseChange L :=
…
```
lemma WeierstrassCurve.smul_eq_of_baseChange_smul_eq A relation Cᴸ • Vᴸ = Wᴸ between base changes, with C defined over K, descends to C • V = W over K line 93 source
Source documentation
A relation Cᴸ • Vᴸ = Wᴸ between base changes, with C defined over K, descends to C • V = W over K.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, WeierstrassCurve.VariableChange, WeierstrassCurve, Eq, HSMul.hSMul, WeierstrassCurve.VariableChange.baseChange, WeierstrassCurve.baseChange
Proof uses: WeierstrassCurve.map_injective, Algebra.algebraMap, FaithfulSMul.algebraMap_injective, Eq.trans, WeierstrassCurve.map, Eq.symm, WeierstrassCurve.baseChange_smul_baseChange
17 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma smul_eq_of_baseChange_smul_eq (C : VariableChange K) {V W : WeierstrassCurve K}
    (h : (C.baseChange L) • V.baseChange L = W.baseChange L) : C • V = W := by
…
```
lemma WeierstrassCurve.map_smul_baseChange_eq The Galois conjugate of an L-isomorphism between base-changed curves is again one line 99 source
Source documentation
The Galois conjugate of an L-isomorphism between base-changed curves is again one.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, AlgEquiv, WeierstrassCurve, WeierstrassCurve.VariableChange, Eq, HSMul.hSMul, WeierstrassCurve.baseChange, WeierstrassCurve.VariableChange.map, AlgHom.toRingHom
Proof uses: WeierstrassCurve.map, WeierstrassCurve.map_baseChange, WeierstrassCurve.map_variableChange, Eq.mp, congrArg
23 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma map_smul_baseChange_eq (σ : L ≃ₐ[K] L) {V W : WeierstrassCurve K} {ρ : VariableChange L}
    (hρ : ρ • V.baseChange L = W.baseChange L) :
    (ρ.map σ.toAlgHom.toRingHom) • V.baseChange L = W.baseChange L := by
…
```