QuadraticTwists.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

39 declarations, 0 contain sorry, 0 declared as axioms

Quadratic twists of elliptic curves

Let E be an elliptic curve over a field K and let L/K be a separable quadratic extension. The quadratic twist Eᴸ of E by L/K is an elliptic curve over K, well-defined up to K-isomorphism, characterised by the following two properties:

Eᴸ becomes isomorphic to E over L (but is not isomorphic to E over K, at least when j(E) ∉ {0, 1728});
the isomorphism φ : Eᴸ ≅ E over L can be chosen so that the Galois action on the points of Eᴸ corresponds, under φ, to the Galois action on the points of E twisted by the quadratic character χ of L/K. More precisely, for every field M in a tower K ⊆ L ⊆ M and every σ ∈ Aut(M/K), we have φ(σ P) = χ(σ) • σ(φ P) on M-points, where χ(σ) = 1 if σ fixes L pointwise and χ(σ) = -1 otherwise.

Taking M to be a separable closure of K, the second property says exactly that the Galois representations attached to Eᴸ (for example on torsion points, via FLT.KnownIn1980s.EllipticCurves.Torsion) are the twists by χ of those attached to E. Taking M = L and σ the nontrivial element of Gal(L/K), it says φ(σ P) = -σ(φ P), which is the classical description of the twist by Galois descent: Eᴸ is the descent to K of E ×_K L along the twisted action σ ↦ (-1) ∘ σ.

Concretely, when char K ≠ 2 we may complete the square and assume E : y² = x³ + a₂x² + a₄x + a₆, and L = K(√d); then Eᴸ : y² = x³ + da₂x² + d²a₄x + d³a₆, with isomorphism φ : (x, y) ↦ (x/d, y/(d√d)) over L.

The generality

Twisting by a separable quadratic extension L/K is the right generality for quadratic twists, uniformly in all characteristics:

Quadratic twists of E/K are classified by the continuous characters χ : Gal(Kˢᵉᵖ/K) → {±1} = μ₂ ⊆ Aut(E), and by Galois theory the nontrivial such characters correspond exactly to separable quadratic extensions L/K (take the fixed field of ker χ). In characteristic 2 the separable quadratic extensions are the Artin–Schreier extensions L = K(℘⁻¹(d)), which are invisible to the familiar "twist by d ∈ K^×/(K^×)²" parametrisation available only when char K ≠ 2.
Every degree 2 field extension is automatically normal; separability is precisely the condition making Aut(L/K) have order 2 rather than 1. An inseparable quadratic extension has trivial automorphism group, hence carries no quadratic character and produces no twist.
A mild generalisation, deliberately not adopted here: one can twist by an arbitrary étale quadratic K-algebra, allowing the split algebra K × K which corresponds to the trivial character and gives back E itself. This makes twisting an action of the group H¹(Gal(Kˢᵉᵖ/K), ℤ/2) on curves at the cost of formalisation noise; all the content is in the field case.
When j(E) ∈ {0, 1728} the curve has automorphisms beyond ±1 and hence also quartic, sextic (and, in characteristics 2 and 3, wilder) twists; but the quadratic twist by L/K, i.e. by the cocycle valued in {±1} ⊆ Aut(E), is defined for every E, and everything below except the two classification statements holds with no hypothesis on j.

Main definitions and statements

The basic algebraic theory of the twist is carried out in full: the explicit Weierstrass model (quadraticTwistOf, quadraticTwistBy), its ellipticity, its independence of the choice of generator of L/K (exists_smul_quadraticTwistBy_eq), the invariance of the j-invariant (j_quadraticTwist), and the fact that twisting is an involution up to K-isomorphism (exists_smul_quadraticTwist_quadraticTwist_eq), together with the Galois-theoretic statements: the isomorphism on points over L and its χ-twisted equivariance, and the classification of forms of E. The reduction-theoretic statements are in FLT.KnownIn1980s.EllipticCurves.QuadraticTwists.SplitMultiplicativeReduction.

WeierstrassCurve.quadraticTwistOf, WeierstrassCurve.quadraticTwistBy and WeierstrassCurve.quadraticTwist E L : an explicit Weierstrass model of the quadratic twist, uniform in the characteristic — parametrised respectively by a pair (t, n), by a generator θ of L/K (with t, n its trace and norm), and by the extension L/K itself.
WeierstrassCurve.quadraticTwistPointEquiv E L M : the isomorphism Eᴸ(M) ≅ E(M) of groups of M-points, for every field M in a tower K ⊆ L ⊆ M, natural in M (quadraticTwistPointEquiv_map).
WeierstrassCurve.quadraticTwistPointEquiv_galois : the key statement φ(σ P) = χ(σ) • σ(φ P) above.
WeierstrassCurve.exists_smul_eq_or_exists_smul_eq_quadraticTwist : for j(E) ∉ {0, 1728}, a curve over K becoming isomorphic to E over L is isomorphic over K to E or to its quadratic twist.

Design notes

"Separable quadratic extension" is spelled as the pair of mathlib typeclasses [Algebra.IsQuadraticExtension K L] [Algebra.IsSeparable K L] (the former is free of rank 2, which over a field just means [L:K] = 2).
A Weierstrass model of the twist is well defined only up to K-isomorphism, i.e. up to the action of WeierstrassCurve.VariableChange K (over a field, isomorphisms of Weierstrass curves are exactly the admissible changes of variables), and the isomorphism φ over L is well defined only up to composition with an L-automorphism of E. Here quadraticTwist is an explicit model, depending on a choice of generator of L/K which is harmless by exists_smul_quadraticTwistBy_eq, while quadraticTwistPointEquiv is a choice, pinned down up to exactly this ambiguity by the theorems about it. Note that quadraticTwistPointEquiv_galois is insensitive to replacing φ by -φ, so the sign ambiguity in φ (which is the whole ambiguity, generically) is harmless.
The isomorphism over L is recorded twice: once at the level of Weierstrass equations, as a change of variables over L (exists_smul_quadraticTwist_baseChange_eq), and once at the level of points, as an AddEquiv on M-points for every M in a tower K ⊆ L ⊆ M, natural for L-algebra maps (quadraticTwistPointEquiv_map). The point-level form is the one consumed by Galois representations.

TODO

Explicit Artin–Schreier formulas for the twist in characteristic 2 (twisting y² + a₁xy + a₃y = x³ + ⋯ by L = K(℘⁻¹(d)) modifies a₂ by d·a₁², etc.), analogous to quadraticTwist_of_two_ne_zero below.
Galois descent for points, E(K) ≃ E(L)^{Gal(L/K)}, and the resulting statement that E(K) × Eᴸ(K) → E(L) has kernel and cokernel killed by 2; over a number field this gives rank E(L) = rank E(K) + rank Eᴸ(K).

References

[J. Silverman, The Arithmetic of Elliptic Curves][silverman2009], III.§10, X.§2 and X.§5
[J.-P. Serre, Propriétés galoisiennes des points d'ordre fini des courbes elliptiques], §5.3 (for the interaction of twists with reduction types)

Imports (6)

Imported by 2 files

def WeierstrassCurve.quadraticTwistOf Documented declaration: quadraticTwistOf line 185 source
Source documentation
The quadratic twist of a Weierstrass curve E over K by parameters t, n, to be thought of as the trace and norm of a generator θ of a separable quadratic extension L/K (see WeierstrassCurve.quadraticTwistBy), so that θ² = tθ - n and D := t² - 4n is the discriminant of the minimal polynomial of θ, nonzero exactly when θ is separable.
The construction: writing the equation of E as y² + A(x)y = f(x) with A(x) = a₁x + a₃, the functions x and Y := (t - 2θ)y - θ·A(x) on E are invariant under the Galois action twisted by the quadratic character of L/K, and satisfy Y² + t·A(x)·Y = D·(y² + A(x)y) - n·A(x)²; clearing denominators via (x, Y) ↦ (Dx, DY) turns this relation into the Weierstrass model below of the twist:
y² + ta₁·xy + Dta₃·y = x³ + (Da₂ - na₁²)·x² + (D²a₄ - 2Dna₁a₃)·x + (D³a₆ - D²na₃²).
Its discriminant is D⁶·Δ(E) (Δ_quadraticTwistOf), so the twist of an elliptic curve is elliptic when D ≠ 0 (isElliptic_quadraticTwistOf), with the same j-invariant (j_quadraticTwistOf).
Sanity checks. If char K ≠ 2 we may take θ = √d, so t = 0, n = -d, D = 4d; for E : y² = x³ + a₂x² + a₄x + a₆ the model is y² = x³ + 4da₂x² + 16d²a₄x + 64d³a₆, the classical twist by 4d ≡ d mod (K^×)². If char K = 2 we may take θ with θ² + θ = d (Artin–Schreier), so t = 1, n = -d, D = 1; for ordinary E : y² + xy = x³ + a₂x² + a₆ the model is the classical twist y² + xy = x³ + (a₂ + d)x² + a₆, and for supersingular E : y² + a₃y = x³ + a₄x + a₆ it is y² + a₃y = x³ + a₄x + (a₆ + da₃²).

standard axioms: propext what this means
Statement uses: CommRing, WeierstrassCurve
Proof uses: WeierstrassCurve.mk, HMul.hMul, WeierstrassCurve.a₁, HSub.hSub, HPow.hPow, Nat, OfNat.ofNat, WeierstrassCurve.a₂, WeierstrassCurve.a₃, WeierstrassCurve.a₄, WeierstrassCurve.a₆
21 instances, coercions and auxiliary constants left out.
```
def quadraticTwistOf (t n : A) : WeierstrassCurve A where
…
```
theorem WeierstrassCurve.c₄_quadraticTwistOf line 194 source
standard axioms: Quot.sound, propext what this means
Statement uses: CommRing, WeierstrassCurve, Eq, WeierstrassCurve.c₄, WeierstrassCurve.quadraticTwistOf, HMul.hMul, HPow.hPow, Nat, HSub.hSub, OfNat.ofNat
Proof uses: id, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, WeierstrassCurve.a₁, WeierstrassCurve.a₂, WeierstrassCurve.a₄, WeierstrassCurve.a₃, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, inferInstance, Ring, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr and 48 more
64 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem WeierstrassCurve.Δ_quadraticTwistOf line 198 source
standard axioms: Quot.sound, propext what this means
Statement uses: CommRing, WeierstrassCurve, Eq, WeierstrassCurve.Δ, WeierstrassCurve.quadraticTwistOf, HMul.hMul, HPow.hPow, Nat, HSub.hSub, OfNat.ofNat
Proof uses: id, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, Neg.neg, WeierstrassCurve.a₁, WeierstrassCurve.a₂, WeierstrassCurve.a₆, WeierstrassCurve.a₃, WeierstrassCurve.a₄, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.neg_congr, Mathlib.Tactic.Ring.Common.pow_congr and 53 more
66 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem WeierstrassCurve.c₆_quadraticTwistOf line 202 source
standard axioms: Quot.sound, propext what this means
Statement uses: CommRing, WeierstrassCurve, Eq, WeierstrassCurve.c₆, WeierstrassCurve.quadraticTwistOf, HMul.hMul, HPow.hPow, Nat, HSub.hSub, OfNat.ofNat
Proof uses: id, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, Neg.neg, WeierstrassCurve.a₁, WeierstrassCurve.a₂, WeierstrassCurve.a₄, WeierstrassCurve.a₃, WeierstrassCurve.a₆, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, inferInstance, Ring, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.neg_congr, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.mul_congr and 51 more
65 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem WeierstrassCurve.b₂_quadraticTwistOf line 206 source
standard axioms: Quot.sound, propext what this means
Statement uses: CommRing, WeierstrassCurve, Eq, WeierstrassCurve.b₂, WeierstrassCurve.quadraticTwistOf, HMul.hMul, HSub.hSub, HPow.hPow, Nat, OfNat.ofNat
Proof uses: id, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, WeierstrassCurve.a₁, WeierstrassCurve.a₂, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, congrArg, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.Common.add_mul and 34 more
61 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem WeierstrassCurve.b₄_quadraticTwistOf line 209 source
standard axioms: Quot.sound, propext what this means
Statement uses: CommRing, WeierstrassCurve, Eq, WeierstrassCurve.b₄, WeierstrassCurve.quadraticTwistOf, HMul.hMul, HPow.hPow, Nat, HSub.hSub, OfNat.ofNat
Proof uses: id, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, WeierstrassCurve.a₄, WeierstrassCurve.a₁, WeierstrassCurve.a₃, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.pow_congr and 47 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem WeierstrassCurve.b₆_quadraticTwistOf line 212 source
standard axioms: Quot.sound, propext what this means
Statement uses: CommRing, WeierstrassCurve, Eq, WeierstrassCurve.b₆, WeierstrassCurve.quadraticTwistOf, HMul.hMul, HPow.hPow, Nat, HSub.hSub, OfNat.ofNat
Proof uses: id, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, WeierstrassCurve.a₃, WeierstrassCurve.a₆, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, inferInstance, Ring, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, congrArg, Eq.symm and 47 more
61 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem WeierstrassCurve.quadraticTwistOf_map The quadratic twist commutes with a ring homomorphism f (in particular with base change): (E.quadraticTwistOf t n).map f = (E.map f).quadraticTwistOf (f t) (f n) line 217 source
Source documentation
The quadratic twist commutes with a ring homomorphism f (in particular with base change): (E.quadraticTwistOf t n).map f = (E.map f).quadraticTwistOf (f t) (f n).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, WeierstrassCurve, RingHom, Eq, WeierstrassCurve.map, WeierstrassCurve.quadraticTwistOf
Proof uses: WeierstrassCurve.ext, of_eq_true, WeierstrassCurve.a₁, Eq.trans, HMul.hMul, True, congr, congrArg, WeierstrassCurve.mk, HSub.hSub, HPow.hPow, Nat, OfNat.ofNat, WeierstrassCurve.a₂, WeierstrassCurve.a₃, WeierstrassCurve.a₄, WeierstrassCurve.a₆, WeierstrassCurve.map_a₁, map_mul, WeierstrassCurve.map_a₂ and 8 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem quadraticTwistOf_map {B : Type*} [CommRing B] (f : A →+* B) :
    (E.quadraticTwistOf t n).map f = (E.map f).quadraticTwistOf (f t) (f n) := by
…
```
Mentions: WeierstrassCurve.quadraticTwistOf
theorem WeierstrassCurve.kappa_quadraticTwistOf The node-polynomial constant κ = 54 b₆ - 3 b₂ b₄ + a₂ c₄ of the quadratic twist by (t, n) in terms of that of E: κ_W = D³ κ - D² n a₁² c₄ where D = t² - 4n line 226 source
Source documentation
The node-polynomial constant κ = 54 b₆ - 3 b₂ b₄ + a₂ c₄ of the quadratic twist by (t, n) in terms of that of E: κ_W = D³ κ - D² n a₁² c₄ where D = t² - 4n.

standard axioms: Quot.sound, propext what this means
Statement uses: CommRing, WeierstrassCurve, Eq, HAdd.hAdd, HSub.hSub, HMul.hMul, OfNat.ofNat, Nat, WeierstrassCurve.b₆, WeierstrassCurve.quadraticTwistOf, WeierstrassCurve.b₂, WeierstrassCurve.b₄, WeierstrassCurve.a₂, WeierstrassCurve.c₄, HPow.hPow, WeierstrassCurve.a₁
Proof uses: Eq.mpr, id, congrArg, WeierstrassCurve.b₆_quadraticTwistOf, WeierstrassCurve.b₂_quadraticTwistOf, WeierstrassCurve.b₄_quadraticTwistOf, WeierstrassCurve.c₄_quadraticTwistOf, rfl, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat and 48 more
61 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem kappa_quadraticTwistOf :
    54 * (E.quadraticTwistOf t n).b₆
      - 3 * (E.quadraticTwistOf t n).b₂ * (E.quadraticTwistOf t n).b₄
      + (E.quadraticTwistOf t n).a₂ * (E.quadraticTwistOf t n).c₄
      = (t ^ 2 - 4 * n) ^ 3 * (54 * E.b₆ - 3 * E.b₂ * E.b₄ + E.a₂ * E.c₄)
        - (t ^ 2 - 4 * n) ^ 2 * n * E.a₁ ^ 2 * E.c₄ := by
…
```
theorem WeierstrassCurve.isElliptic_quadraticTwistOf line 246 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, WeierstrassCurve.IsElliptic, Ne, HSub.hSub, HPow.hPow, Nat, OfNat.ofNat, HMul.hMul, WeierstrassCurve.quadraticTwistOf
Proof uses: Eq.mpr, IsUnit, WeierstrassCurve.Δ, id, Eq, congrArg, propext, WeierstrassCurve.isElliptic_iff, WeierstrassCurve.Δ_quadraticTwistOf, IsUnit.mul, Iff.mpr, isUnit_iff_ne_zero, pow_ne_zero, WeierstrassCurve.isUnit_Δ
66 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem WeierstrassCurve.j_quadraticTwistOf line 251 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, WeierstrassCurve.IsElliptic, WeierstrassCurve.quadraticTwistOf, Eq, WeierstrassCurve.j
Proof uses: Ne, HSub.hSub, HPow.hPow, Nat, OfNat.ofNat, HMul.hMul, IsUnit.ne_zero, WeierstrassCurve.Δ, WeierstrassCurve.isUnit_Δ, Eq.mpr, id, congrArg, WeierstrassCurve.Δ_quadraticTwistOf, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.mul_congr, HAdd.hAdd, Nat.rawCast, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.cast_zero, Mathlib.Meta.NormNum.isNat_ofNat and 68 more
72 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
theorem WeierstrassCurve.exists_smul_eq_quadraticTwistOf_quadraticTwistOf Documented declaration: exists_smul_eq_quadraticTwistOf_quadraticTwistOf line 262 source
Source documentation
Twisting twice by the same parameters (t, n) gives a curve isomorphic to E over K: explicitly, the double twist is obtained from E by the change of variables (x, y) ↦ (D²x, D³y + 2nD²(a₁x + a₃)), where D = t² - 4n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, Ne, HSub.hSub, HPow.hPow, Nat, OfNat.ofNat, HMul.hMul, Exists, WeierstrassCurve.VariableChange, Eq, HSMul.hSMul, WeierstrassCurve.quadraticTwistOf
Proof uses: Exists.intro, WeierstrassCurve.VariableChange.mk, Inv.inv, Units, Units.mk0, HDiv.hDiv, WeierstrassCurve.a₁, WeierstrassCurve.a₃, Eq.mpr, WeierstrassCurve.mk, WeierstrassCurve.VariableChange.u, HAdd.hAdd, WeierstrassCurve.VariableChange.s, WeierstrassCurve.a₂, WeierstrassCurve.VariableChange.r, WeierstrassCurve.VariableChange.t, WeierstrassCurve.a₄, WeierstrassCurve.a₆, id, congrArg and 117 more
111 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem exists_smul_eq_quadraticTwistOf_quadraticTwistOf (hD : t ^ 2 - 4 * n ≠ 0) :
    ∃ C : VariableChange K, C • E = (E.quadraticTwistOf t n).quadraticTwistOf t n := by
…
```
Mentions: WeierstrassCurve.quadraticTwistOf
theorem WeierstrassCurve.exists_smul_quadraticTwistOf_eq Documented declaration: exists_smul_quadraticTwistOf_eq line 272 source
Source documentation
Changing the parameters (t, n) — the trace and norm of a generator θ of a quadratic extension — into the trace and norm (at + 2b, b² + abt + a²n) of another generator aθ + b changes the quadratic twist by an explicit change of variables over K.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, Ne, OfNat.ofNat, Exists, WeierstrassCurve.VariableChange, Eq, HSMul.hSMul, WeierstrassCurve.quadraticTwistOf, HAdd.hAdd, HMul.hMul, Nat, HPow.hPow
Proof uses: Exists.intro, WeierstrassCurve.VariableChange.mk, Inv.inv, Units, Units.mk0, WeierstrassCurve.a₁, HSub.hSub, WeierstrassCurve.a₃, Eq.mpr, WeierstrassCurve.mk, WeierstrassCurve.VariableChange.u, WeierstrassCurve.VariableChange.s, WeierstrassCurve.a₂, WeierstrassCurve.VariableChange.r, WeierstrassCurve.VariableChange.t, WeierstrassCurve.a₄, WeierstrassCurve.a₆, id, congrArg, WeierstrassCurve.variableChange_def and 113 more
109 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem exists_smul_quadraticTwistOf_eq {a : K} (b : K) (ha : a ≠ 0) :
    ∃ C : VariableChange K, C • E.quadraticTwistOf t n
      = E.quadraticTwistOf (a * t + 2 * b) (b ^ 2 + a * b * t + a ^ 2 * n) := by
…
```
def WeierstrassCurve.quadraticTwistBy The quadratic twist of a Weierstrass curve E over K by an element θ of an extension L/K: the twist WeierstrassCurve.quadraticTwistOf by the trace and norm of θ line 290 source
Source documentation
The quadratic twist of a Weierstrass curve E over K by an element θ of an extension L/K: the twist WeierstrassCurve.quadraticTwistOf by the trace and norm of θ. This is "the" quadratic twist of E by the extension L/K whenever L/K is separable quadratic and θ generates it, i.e. θ ∉ K; the choice of generator does not matter, up to isomorphism over K (exists_smul_quadraticTwistBy_eq).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, WeierstrassCurve
Proof uses: WeierstrassCurve.quadraticTwistOf, LinearMap, RingHom.id, Algebra.trace, MonoidHom, Algebra.norm
21 instances, coercions and auxiliary constants left out.
```
noncomputable def quadraticTwistBy (θ : L) : WeierstrassCurve K :=
…
```
theorem WeierstrassCurve.isElliptic_quadraticTwistBy line 295 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, WeierstrassCurve, Algebra.IsQuadraticExtension, Algebra.IsSeparable, WeierstrassCurve.IsElliptic, Not, Membership.mem, Set, Set.range, RingHom, Algebra.algebraMap, WeierstrassCurve.quadraticTwistBy
Proof uses: WeierstrassCurve.isElliptic_quadraticTwistOf, LinearMap, RingHom.id, Algebra.trace, MonoidHom, Algebra.norm, Algebra.IsQuadraticExtension.discrim_ne_zero
36 instances, coercions and auxiliary constants left out.
theorem WeierstrassCurve.exists_smul_quadraticTwistBy_eq The quadratic twist by a generator θ of a separable quadratic extension L/K depends on the choice of θ only up to isomorphism over K: all generators give isomorphic twists line 301 source
Source documentation
The quadratic twist by a generator θ of a separable quadratic extension L/K depends on the choice of θ only up to isomorphism over K: all generators give isomorphic twists.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, WeierstrassCurve, Algebra.IsQuadraticExtension, Algebra.IsSeparable, Not, Membership.mem, Set, Set.range, RingHom, Algebra.algebraMap, Exists, WeierstrassCurve.VariableChange, Eq, HSMul.hSMul, WeierstrassCurve.quadraticTwistBy
Proof uses: And, Ne, OfNat.ofNat, HAdd.hAdd, HMul.hMul, Algebra.IsQuadraticExtension.exists_eq_algebraMap_add_algebraMap_mul, Eq.mpr, WeierstrassCurve.quadraticTwistOf, LinearMap, RingHom.id, Algebra.trace, MonoidHom, Algebra.norm, Nat, HPow.hPow, id, congrArg, funext, congr, Algebra.IsQuadraticExtension.trace_algebraMap_add_algebraMap_mul and 3 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem exists_smul_quadraticTwistBy_eq {θ θ' : L} (hθ : θ ∉ Set.range (algebraMap K L))
    (hθ' : θ' ∉ Set.range (algebraMap K L)) :
    ∃ C : VariableChange K, C • E.quadraticTwistBy θ = E.quadraticTwistBy θ' := by
…
```
def WeierstrassCurve.quadraticTwist Documented declaration: quadraticTwist line 319 source
Source documentation
The quadratic twist of an elliptic curve E over K by a separable quadratic extension L/K: the twist WeierstrassCurve.quadraticTwistBy by an arbitrarily chosen generator θ ∈ L ∖ K. The twist is independent of this choice up to isomorphism over K (exists_smul_quadraticTwist_eq_quadraticTwistBy), that is, up to the action of WeierstrassCurve.VariableChange K; see WeierstrassCurve.quadraticTwistOf for the explicit Weierstrass model. (The separability hypothesis is not used to write down the model, but the twist is only meaningful for separable extensions — see the module docstring.)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, Algebra, Algebra.IsQuadraticExtension, Algebra.IsSeparable
Proof uses: WeierstrassCurve.quadraticTwistBy, Exists.choose, Not, Membership.mem, Set, Set.range, RingHom, Algebra.algebraMap, Algebra.IsQuadraticExtension.exists_notMem_range_algebraMap
20 instances, coercions and auxiliary constants left out.
```
noncomputable def quadraticTwist (E : WeierstrassCurve K) (L : Type*) [Field L] [Algebra K L]
    [Algebra.IsQuadraticExtension K L] [Algebra.IsSeparable K L] : WeierstrassCurve K :=
…
```
lemma WeierstrassCurve.baseChange_c₄_ne_zero If j(E) ≠ 0 then c₄ ≠ 0, also after base change to a field extension line 339 source
Source documentation
If j(E) ≠ 0 then c₄ ≠ 0, also after base change to a field extension.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, Algebra, WeierstrassCurve.IsElliptic, Ne, WeierstrassCurve.j, OfNat.ofNat, WeierstrassCurve.c₄, WeierstrassCurve.baseChange
Proof uses: Eq.mpr, RingHom, Algebra.algebraMap, id, Eq, congrFun', congrArg, WeierstrassCurve.map_c₄, Iff.mpr, map_ne_zero_iff, FaithfulSMul.algebraMap_injective, Iff.mp, Not, Iff.not, WeierstrassCurve.j_eq_zero_iff
35 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma baseChange_c₄_ne_zero (hj₀ : E.j ≠ 0) : (E.baseChange L).c₄ ≠ 0 := by
…
```
lemma WeierstrassCurve.baseChange_c₆_ne_zero If j(E) ≠ 1728 then c₆ ≠ 0, also after base change to a field extension line 345 source
Source documentation
If j(E) ≠ 1728 then c₆ ≠ 0, also after base change to a field extension.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, Algebra, WeierstrassCurve.IsElliptic, Ne, WeierstrassCurve.j, OfNat.ofNat, Nat, WeierstrassCurve.c₆, WeierstrassCurve.baseChange
Proof uses: Eq.mpr, RingHom, Algebra.algebraMap, id, Eq, congrFun', congrArg, WeierstrassCurve.map_c₆, Iff.mpr, map_ne_zero_iff, FaithfulSMul.algebraMap_injective, Not, Iff.not, WeierstrassCurve.c₆_eq_zero_iff_j_eq_1728
47 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma baseChange_c₆_ne_zero (hj₁₇₂₈ : E.j ≠ 1728) : (E.baseChange L).c₆ ≠ 0 := by
…
```
theorem WeierstrassCurve.exists_smul_quadraticTwist_eq_quadraticTwistBy The quadratic twist of E by L/K is isomorphic over K to the twist by any given generator θ ∈ L ∖ K: the arbitrary choice made in its definition is harmless line 356 source
Source documentation
The quadratic twist of E by L/K is isomorphic over K to the twist by any given generator θ ∈ L ∖ K: the arbitrary choice made in its definition is harmless.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, Algebra, Algebra.IsQuadraticExtension, Algebra.IsSeparable, Not, Membership.mem, Set, Set.range, RingHom, Algebra.algebraMap, Exists, WeierstrassCurve.VariableChange, Eq, HSMul.hSMul, WeierstrassCurve.quadraticTwist, WeierstrassCurve.quadraticTwistBy
Proof uses: WeierstrassCurve.exists_smul_quadraticTwistBy_eq, Exists.choose, Algebra.IsQuadraticExtension.exists_notMem_range_algebraMap, Exists.choose_spec
28 instances, coercions and auxiliary constants left out.
```
theorem exists_smul_quadraticTwist_eq_quadraticTwistBy {θ : L}
    (hθ : θ ∉ Set.range (algebraMap K L)) :
    ∃ C : VariableChange K, C • E.quadraticTwist L = E.quadraticTwistBy θ :=
…
```
theorem WeierstrassCurve.exists_smul_baseChange_and_map_eq Documented declaration: exists_smul_baseChange_and_map_eq line 365 source
Source documentation
An explicit L-isomorphism (Eᶿ)ᴸ ≅ Eᴸ (the change of variables of the module docstring) which moreover is anti-equivariant for the Galois action: its conjugate by the nontrivial σ ∈ Gal(L/K) differs from it by the automorphism [-1] of E. This nontrivial cocycle is the origin of the twist being a nontrivial form of E.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, Algebra, Algebra.IsQuadraticExtension, Algebra.IsSeparable, Not, Membership.mem, Set, Set.range, RingHom, Algebra.algebraMap, AlgEquiv, Ne, OfNat.ofNat, Exists, WeierstrassCurve.VariableChange, And, Eq, HSMul.hSMul, WeierstrassCurve.baseChange and 5 more
Proof uses: Algebra.IsQuadraticExtension.algEquiv_apply_ne, HSub.hSub, Iff.mpr, sub_ne_zero, LinearMap, RingHom.id, Algebra.trace, HAdd.hAdd, Algebra.IsQuadraticExtension.algebraMap_trace_eq_add, MonoidHom, Algebra.norm, Algebra.IsQuadraticExtension.algebraMap_norm_eq_mul, Eq.mpr, id, congrArg, Eq.symm, AlgEquiv.mul_apply, Algebra.IsQuadraticExtension.algEquiv_mul_self, AlgEquiv.one_apply, Eq.refl and 155 more
153 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
theorem exists_smul_baseChange_and_map_eq {θ : L} (hθ : θ ∉ Set.range (algebraMap K L))
    {σ : L ≃ₐ[K] L} (hσ : σ ≠ 1) :
    ∃ C : VariableChange L, C • (E.quadraticTwistBy θ).baseChange L = E.baseChange L ∧
      C.map σ.toAlgHom.toRingHom = (E.baseChange L).negVariableChange * C := by
…
```
Mentions: WeierstrassCurve.negVariableChange
theorem WeierstrassCurve.exists_smul_quadraticTwist_baseChange_eq The quadratic twist becomes isomorphic to E after base change to L line 399 source
Source documentation
The quadratic twist becomes isomorphic to E after base change to L. (Over a field, isomorphisms of Weierstrass curves are exactly the admissible changes of variables WeierstrassCurve.VariableChange, acting via •.) The point-level consequences of this isomorphism, which is what most applications need, are recorded separately in quadraticTwistPointEquiv below.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, Algebra, Algebra.IsQuadraticExtension, Algebra.IsSeparable, Exists, WeierstrassCurve.VariableChange, Eq, HSMul.hSMul, WeierstrassCurve.baseChange, WeierstrassCurve.quadraticTwist
Proof uses: AlgEquiv, Ne, OfNat.ofNat, Algebra.IsQuadraticExtension.exists_algEquiv_ne_one, Not, Membership.mem, Set, Set.range, RingHom, Algebra.algebraMap, Algebra.IsQuadraticExtension.exists_notMem_range_algebraMap, And, WeierstrassCurve.quadraticTwistBy, WeierstrassCurve.VariableChange.map, AlgHom.toRingHom, HMul.hMul, WeierstrassCurve.negVariableChange, WeierstrassCurve.exists_smul_baseChange_and_map_eq, WeierstrassCurve.exists_smul_quadraticTwist_eq_quadraticTwistBy, Exists.intro and 7 more
45 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
theorem exists_smul_quadraticTwist_baseChange_eq :
    ∃ C : VariableChange L, C • (E.quadraticTwist L).baseChange L = E.baseChange L := by
…
```
theorem WeierstrassCurve.exists_smul_quadraticTwist_quadraticTwist_eq Twisting twice by the same quadratic extension gives back E, up to K-isomorphism line 411 source
Source documentation
Twisting twice by the same quadratic extension gives back E, up to K-isomorphism. (Both twists are taken with respect to the same chosen generator of L/K, which is harmless by exists_smul_quadraticTwist_eq_quadraticTwistBy.)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, Algebra, Algebra.IsQuadraticExtension, Algebra.IsSeparable, Exists, WeierstrassCurve.VariableChange, Eq, HSMul.hSMul, WeierstrassCurve.quadraticTwist
Proof uses: WeierstrassCurve.quadraticTwistOf, LinearMap, RingHom.id, Algebra.trace, Exists.choose, Not, Membership.mem, Set, Set.range, RingHom, Algebra.algebraMap, Algebra.IsQuadraticExtension.exists_notMem_range_algebraMap, MonoidHom, Algebra.norm, WeierstrassCurve.exists_smul_eq_quadraticTwistOf_quadraticTwistOf, Algebra.IsQuadraticExtension.discrim_ne_zero, Exists.choose_spec, Exists.intro, Inv.inv, Iff.mpr and 2 more
46 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem exists_smul_quadraticTwist_quadraticTwist_eq :
    ∃ C : VariableChange K, C • (E.quadraticTwist L).quadraticTwist L = E := by
…
```
Mentions: WeierstrassCurve.quadraticTwist
theorem WeierstrassCurve.quadraticTwist_of_two_ne_zero The classical formula for the quadratic twist away from characteristic 2 line 422 source
Source documentation
The classical formula for the quadratic twist away from characteristic 2. Suppose char K ≠ 2, so that after completing the square we may assume E has the form y² = x³ + a₂x² + a₄x + a₆, and suppose L = K(α) where α² = d is a nonsquare in K (every separable quadratic extension arises this way when char K ≠ 2). Then the quadratic twist of E by L is y² = x³ + da₂x² + d²a₄x + d³a₆, up to K-isomorphism.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, Algebra, Algebra.IsQuadraticExtension, Algebra.IsSeparable, Ne, OfNat.ofNat, Nat, Eq, WeierstrassCurve.a₁, WeierstrassCurve.a₃, Not, IsSquare, HPow.hPow, RingHom, Algebra.algebraMap, Exists, WeierstrassCurve.VariableChange, HSMul.hSMul, WeierstrassCurve.quadraticTwist and 5 more
Proof uses: Membership.mem, Set, Set.range, notMem_range_algebraMap_of_not_isSquare, LinearMap, RingHom.id, Algebra.trace, Algebra.IsQuadraticExtension.trace_eq_zero_of_sq_eq, MonoidHom, Algebra.norm, Neg.neg, Algebra.IsQuadraticExtension.norm_eq_neg_of_sq_eq, WeierstrassCurve.quadraticTwistBy, WeierstrassCurve.exists_smul_quadraticTwist_eq_quadraticTwistBy, Exists.intro, WeierstrassCurve.VariableChange.mk, Units.mk0, Eq.mpr, id, congrArg and 123 more
137 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
theorem quadraticTwist_of_two_ne_zero (h2 : (2 : K) ≠ 0) (ha₁ : E.a₁ = 0) (ha₃ : E.a₃ = 0)
    {d : K} (hd : ¬IsSquare d) {α : L} (hα : α ^ 2 = algebraMap K L d) :
    ∃ C : VariableChange K, C • E.quadraticTwist L =
      { a₁ := 0, a₂ := d * E.a₂, a₃ := 0, a₄ := d ^ 2 * E.a₄, a₆ := d ^ 3 * E.a₆ } := by
…
```
def WeierstrassCurve.quadraticTwistVarChange A choice of change of variables over L carrying E to its quadratic twist Eᴸ line 444 source
Source documentation
A choice of change of variables over L carrying E to its quadratic twist Eᴸ. Using the explicit isomorphism of exists_smul_baseChange_and_map_eq (rather than an arbitrary one) ensures its Galois cocycle is exactly [-1] (quadraticTwistVarChange_map), unconditionally in j.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, Algebra, Algebra.IsQuadraticExtension, Algebra.IsSeparable, WeierstrassCurve.VariableChange
Proof uses: Inv.inv, Exists.choose, And, Eq, HSMul.hSMul, WeierstrassCurve.baseChange, WeierstrassCurve.quadraticTwistBy, Not, Membership.mem, Set, Set.range, RingHom, Algebra.algebraMap, Algebra.IsQuadraticExtension.exists_notMem_range_algebraMap, WeierstrassCurve.VariableChange.map, AlgHom.toRingHom, AlgEquiv, Ne, OfNat.ofNat, Algebra.IsQuadraticExtension.exists_algEquiv_ne_one and 2 more
33 instances, coercions and auxiliary constants left out.
```
noncomputable def quadraticTwistVarChange : VariableChange L :=
…
```
lemma WeierstrassCurve.quadraticTwistVarChange_smul line 449 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, Algebra, Algebra.IsQuadraticExtension, Algebra.IsSeparable, Eq, HSMul.hSMul, WeierstrassCurve.VariableChange, WeierstrassCurve.quadraticTwistVarChange, WeierstrassCurve.baseChange, WeierstrassCurve.quadraticTwist
Proof uses: id, Eq.mpr, Inv.inv, Exists.choose, And, WeierstrassCurve.quadraticTwistBy, Not, Membership.mem, Set, Set.range, RingHom, Algebra.algebraMap, Algebra.IsQuadraticExtension.exists_notMem_range_algebraMap, WeierstrassCurve.VariableChange.map, AlgHom.toRingHom, AlgEquiv, Ne, OfNat.ofNat, Algebra.IsQuadraticExtension.exists_algEquiv_ne_one, HMul.hMul and 8 more
45 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma WeierstrassCurve.quadraticTwistVarChange_map The defining cocycle of the quadratic twist line 461 source
Source documentation
The defining cocycle of the quadratic twist. The nontrivial σ ∈ Gal(L/K) conjugates the change of variables quadraticTwistVarChange (carrying E to Eᴸ) by the automorphism [-1] of E. This is the datum expressing that Eᴸ is the descent of E along the twisted Galois action σ ↦ (-1) ∘ σ, and it holds for every j.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, Algebra, Algebra.IsQuadraticExtension, Algebra.IsSeparable, AlgEquiv, Ne, OfNat.ofNat, Eq, WeierstrassCurve.VariableChange, WeierstrassCurve.VariableChange.map, WeierstrassCurve.quadraticTwistVarChange, AlgHom.toRingHom, HMul.hMul, WeierstrassCurve.negVariableChange, WeierstrassCurve.baseChange
Proof uses: Exists.choose, Algebra.IsQuadraticExtension.exists_algEquiv_ne_one, Exists.choose_spec, And, HSMul.hSMul, WeierstrassCurve.quadraticTwistBy, Not, Membership.mem, Set, Set.range, RingHom, Algebra.algebraMap, Algebra.IsQuadraticExtension.exists_notMem_range_algebraMap, WeierstrassCurve.exists_smul_baseChange_and_map_eq, And.right, Inv.inv, map_inv, MonoidHom, WeierstrassCurve.VariableChange.mapHom, id and 8 more
55 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma quadraticTwistVarChange_map {σ : L ≃ₐ[K] L} (hσ : σ ≠ 1) :
    (E.quadraticTwistVarChange L).map σ.toAlgHom.toRingHom
      = (E.quadraticTwistVarChange L) * (E.baseChange L).negVariableChange := by
…
```
Mentions: WeierstrassCurve.negVariableChange
instance WeierstrassCurve.(instance at line 483) line 483 source
Source documentation
The quadratic twist of an elliptic curve is an elliptic curve: the twisted model has discriminant D⁶·Δ(E), and D ≠ 0 by separability (Algebra.IsQuadraticExtension.discrim_ne_zero).
```
instance : (E.quadraticTwist L).IsElliptic :=
…
```
theorem WeierstrassCurve.j_quadraticTwist Twisting does not change the j-invariant, since the curves become isomorphic over L line 487 source
Source documentation
Twisting does not change the j-invariant, since the curves become isomorphic over L.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, Algebra, Algebra.IsQuadraticExtension, Algebra.IsSeparable, WeierstrassCurve.IsElliptic, Eq, WeierstrassCurve.j, WeierstrassCurve.quadraticTwist
Proof uses: WeierstrassCurve.j_quadraticTwistOf, LinearMap, RingHom.id, Algebra.trace, Exists.choose, Not, Membership.mem, Set, Set.range, RingHom, Algebra.algebraMap, Algebra.IsQuadraticExtension.exists_notMem_range_algebraMap, MonoidHom, Algebra.norm, WeierstrassCurve.isElliptic_quadraticTwistOf, Algebra.IsQuadraticExtension.discrim_ne_zero, Exists.choose_spec
33 instances, coercions and auxiliary constants left out.
```
theorem j_quadraticTwist : (E.quadraticTwist L).j = E.j :=
…
```
theorem WeierstrassCurve.not_exists_smul_quadraticTwist_eq If j(E) ∉ {0, 1728} (so that the only automorphisms of E are ±1) then the quadratic twist is not isomorphic to E over K: twisting by L/K is a nontrivial operation line 496 source
Source documentation
If j(E) ∉ {0, 1728} (so that the only automorphisms of E are ±1) then the quadratic twist is not isomorphic to E over K: twisting by L/K is a nontrivial operation. This can fail for j ∈ {0, 1728}: e.g. for E : y² = x³ + x of j-invariant 1728 over K = ℚ(i), the quadratic twist by any L = K(d^{1/2}) with d ∈ (K^×)⁴ ∖ (K^×)² is isomorphic to E over K, because E admits the automorphism (x, y) ↦ (-x, iy) of order 4.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, Algebra, Algebra.IsQuadraticExtension, Algebra.IsSeparable, WeierstrassCurve.IsElliptic, Ne, WeierstrassCurve.j, OfNat.ofNat, Nat, Not, Exists, WeierstrassCurve.VariableChange, Eq, HSMul.hSMul, WeierstrassCurve.quadraticTwist
Proof uses: False, AlgEquiv, Algebra.IsQuadraticExtension.exists_algEquiv_ne_one, Membership.mem, Set, Set.range, RingHom, Algebra.algebraMap, Algebra.IsQuadraticExtension.exists_notMem_range_algebraMap, And, WeierstrassCurve.baseChange, WeierstrassCurve.quadraticTwistBy, WeierstrassCurve.VariableChange.map, AlgHom.toRingHom, HMul.hMul, WeierstrassCurve.negVariableChange, WeierstrassCurve.exists_smul_baseChange_and_map_eq, WeierstrassCurve.exists_smul_quadraticTwist_eq_quadraticTwistBy, Inv.inv, Eq.mpr and 30 more
95 instances, coercions and auxiliary constants left out.

Tactic trace: 36 steps
Open to load the checked before-and-after goal states.
```
theorem not_exists_smul_quadraticTwist_eq (hj₀ : E.j ≠ 0) (hj₁₇₂₈ : E.j ≠ 1728) :
    ¬∃ C : VariableChange K, C • E.quadraticTwist L = E := by
…
```
theorem WeierstrassCurve.exists_smul_eq_or_exists_smul_eq_quadraticTwist Documented declaration: exists_smul_eq_or_exists_smul_eq_quadraticTwist line 547 source
Source documentation
Classification of the forms of E split by L/K, for j(E) ∉ {0, 1728}: an elliptic curve over K which becomes isomorphic to E over L is isomorphic over K either to E or to its quadratic twist by L. (Such forms are classified by H¹(Gal(L/K), Aut(E_L)) = Hom(ℤ/2, {±1}), which has order 2. For j ∈ {0, 1728} the automorphism group is larger and there can be more forms; the statement including these j is left as a further target.) Together with not_exists_smul_quadraticTwist_eq this pins down E.quadraticTwist L up to K-isomorphism.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, Algebra, Algebra.IsQuadraticExtension, Algebra.IsSeparable, WeierstrassCurve.IsElliptic, Ne, WeierstrassCurve.j, OfNat.ofNat, Nat, Exists, WeierstrassCurve.VariableChange, Eq, HSMul.hSMul, WeierstrassCurve.baseChange, Or, WeierstrassCurve.quadraticTwist
Proof uses: AlgEquiv, Algebra.IsQuadraticExtension.exists_algEquiv_ne_one, Not, Membership.mem, Set, Set.range, RingHom, Algebra.algebraMap, Algebra.IsQuadraticExtension.exists_notMem_range_algebraMap, And, WeierstrassCurve.quadraticTwistBy, WeierstrassCurve.VariableChange.map, AlgHom.toRingHom, HMul.hMul, WeierstrassCurve.negVariableChange, WeierstrassCurve.exists_smul_baseChange_and_map_eq, WeierstrassCurve.c₄, WeierstrassCurve.baseChange_c₄_ne_zero, WeierstrassCurve.c₆, WeierstrassCurve.baseChange_c₆_ne_zero and 29 more
78 instances, coercions and auxiliary constants left out.

Tactic trace: 40 steps
Open to load the checked before-and-after goal states.
```
theorem exists_smul_eq_or_exists_smul_eq_quadraticTwist (hj₀ : E.j ≠ 0) (hj₁₇₂₈ : E.j ≠ 1728)
    (E' : WeierstrassCurve K)
    (h : ∃ C : VariableChange L, C • E'.baseChange L = E.baseChange L) :
    (∃ C : VariableChange K, C • E' = E) ∨ ∃ C : VariableChange K, C • E' = E.quadraticTwist L := by
…
```
lemma WeierstrassCurve.quadraticTwistVarChange_smul_baseChange line 609 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, Algebra, Algebra.IsQuadraticExtension, Algebra.IsSeparable, IsScalarTower, Eq, HSMul.hSMul, WeierstrassCurve.VariableChange, WeierstrassCurve.VariableChange.baseChange, WeierstrassCurve.quadraticTwistVarChange, WeierstrassCurve.baseChange, WeierstrassCurve.quadraticTwist
Proof uses: WeierstrassCurve.VariableChange.map, Algebra.algebraMap, WeierstrassCurve.map, WeierstrassCurve.map_variableChange, Eq.mp, congrArg, WeierstrassCurve.baseChange_map_algebraMap, WeierstrassCurve.quadraticTwistVarChange_smul
24 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma WeierstrassCurve.quadraticTwistVarChange_baseChange_map Documented declaration: quadraticTwistVarChange_baseChange_map line 620 source
Source documentation
The M-level form of the twist's defining cocycle: any σ ∈ Aut(M/K) not fixing L pointwise (i.e. with χ(σ) = -1) conjugates the base change to M of quadraticTwistVarChange by the automorphism [-1] of E. This is the base change of quadraticTwistVarChange_map.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, Algebra, Algebra.IsQuadraticExtension, Algebra.IsSeparable, IsScalarTower, AlgEquiv, Not, Eq, RingHom, Algebra.algebraMap, WeierstrassCurve.VariableChange, WeierstrassCurve.VariableChange.map, WeierstrassCurve.VariableChange.baseChange, WeierstrassCurve.quadraticTwistVarChange, AlgHom.toRingHom, HMul.hMul, WeierstrassCurve.negVariableChange, WeierstrassCurve.baseChange
Proof uses: Ne, OfNat.ofNat, Exists, Algebra.IsQuadraticExtension.exists_algEquiv_ne_one, AlgEquiv.restrictNormal, Or.resolve_left, Algebra.IsQuadraticExtension.algEquiv_eq_one_or_eq, Iff.mpr, forall_apply_algebraMap_iff_restrictNormal_eq_one, RingHom.comp, RingHom.ext, Eq.symm, AlgEquiv.restrictNormal_commutes, id, Eq.mp, congrArg, WeierstrassCurve.VariableChange.map_map, map_mul, MonoidHom, WeierstrassCurve.VariableChange.mapHom and 6 more
52 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma quadraticTwistVarChange_baseChange_map {σ : M ≃ₐ[K] M}
    (hσ : ¬ ∀ x : L, σ (algebraMap L M x) = algebraMap L M x) :
    ((E.quadraticTwistVarChange L).baseChange M).map σ.toAlgHom.toRingHom
      = (E.quadraticTwistVarChange L).baseChange M * (E.baseChange M).negVariableChange := by
…
```
Mentions: WeierstrassCurve.negVariableChange
def WeierstrassCurve.quadraticTwistPointEquiv The isomorphism Eᴸ(M) ≅ E(M) on M-points, for any field M in a tower K ⊆ L ⊆ M: the base change to M of a choice of isomorphism between Eᴸ and E over L line 656 source
Source documentation
The isomorphism Eᴸ(M) ≅ E(M) on M-points, for any field M in a tower K ⊆ L ⊆ M: the base change to M of a choice of isomorphism between Eᴸ and E over L. It is natural in M (quadraticTwistPointEquiv_map) and transforms the Galois action into the Galois action twisted by the quadratic character of L/K (quadraticTwistPointEquiv_galois).
Like the twist itself, this isomorphism is well defined only up to composition with an L-automorphism of E — generically, up to sign — and this definition makes an arbitrary but single choice, consistent across all M.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, Algebra, Algebra.IsQuadraticExtension, Algebra.IsSeparable, IsScalarTower, WeierstrassCurve.IsElliptic, DecidableEq, AddEquiv, WeierstrassCurve.Affine.Point, WeierstrassCurve.Affine.baseChange, WeierstrassCurve.quadraticTwist
Proof uses: WeierstrassCurve.baseChange, AddEquiv.trans, WeierstrassCurve.toAffine, HSMul.hSMul, WeierstrassCurve.VariableChange, WeierstrassCurve.VariableChange.baseChange, WeierstrassCurve.quadraticTwistVarChange, WeierstrassCurve.Affine.Point.equivOfEq, WeierstrassCurve.Affine.Point.equivVariableChange
24 instances, coercions and auxiliary constants left out.
```
noncomputable def quadraticTwistPointEquiv :
    ((E.quadraticTwist L)⁄M).Point ≃+ (E⁄M).Point :=
…
```
theorem WeierstrassCurve.quadraticTwistPointEquiv_map Documented declaration: quadraticTwistPointEquiv_map line 665 source
Source documentation
Naturality of quadraticTwistPointEquiv in M: the isomorphisms on M-points over varying M ⊇ L are all induced by a single isomorphism of curves over L, so they commute with the maps on points induced by any L-algebra homomorphism.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, Algebra, Algebra.IsQuadraticExtension, Algebra.IsSeparable, IsScalarTower, WeierstrassCurve.IsElliptic, DecidableEq, AlgHom, WeierstrassCurve.Affine.Point, WeierstrassCurve.Affine.baseChange, WeierstrassCurve.quadraticTwist, Eq, AddEquiv, WeierstrassCurve.quadraticTwistPointEquiv, AddMonoidHom, WeierstrassCurve.Affine.Point.map
Proof uses: WeierstrassCurve.VariableChange.u, WeierstrassCurve.VariableChange.baseChange, WeierstrassCurve.quadraticTwistVarChange, id, Eq.symm, RingHom, Algebra.algebraMap, AlgHom.commutes, WeierstrassCurve.VariableChange.r, WeierstrassCurve.VariableChange.s, WeierstrassCurve.VariableChange.t, of_eq_true, WeierstrassCurve.Affine.Point.zero, Eq.trans, OfNat.ofNat, True, congr, congrArg, map_zero, eq_self and 30 more
84 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
theorem quadraticTwistPointEquiv_map {N : Type*} [Field N] [Algebra K N] [Algebra L N]
    [IsScalarTower K L N] [DecidableEq N] (f : M →ₐ[L] N)
    (P : ((E.quadraticTwist L)⁄M).Point) :
    E.quadraticTwistPointEquiv L N (Affine.Point.map f P) =
      Affine.Point.map f (E.quadraticTwistPointEquiv L M P) := by
…
```
theorem WeierstrassCurve.quadraticTwistPointEquiv_map_of_not_fixed Documented declaration: quadraticTwistPointEquiv_map_of_not_fixed line 692 source
Source documentation
The anti-equivariance underlying quadraticTwistPointEquiv_galois: if σ ∈ Aut(M/K) does not fix L pointwise (χ(σ) = -1), then transporting its action through Eᴸ(M) ≅ E(M) gives minus its action. This is the point-level shadow of quadraticTwistVarChange_baseChange_map.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, Algebra, Algebra.IsQuadraticExtension, Algebra.IsSeparable, IsScalarTower, WeierstrassCurve.IsElliptic, DecidableEq, AlgEquiv, Not, Eq, RingHom, Algebra.algebraMap, WeierstrassCurve.Affine.Point, WeierstrassCurve.Affine.baseChange, WeierstrassCurve.quadraticTwist, AddEquiv, WeierstrassCurve.quadraticTwistPointEquiv, AddMonoidHom, WeierstrassCurve.Affine.Point.map and 1 more
Proof uses: WeierstrassCurve.VariableChange, WeierstrassCurve.VariableChange.map, WeierstrassCurve.VariableChange.baseChange, WeierstrassCurve.quadraticTwistVarChange, AlgHom.toRingHom, HMul.hMul, WeierstrassCurve.negVariableChange, WeierstrassCurve.baseChange, WeierstrassCurve.quadraticTwistVarChange_baseChange_map, AlgHom, WeierstrassCurve.VariableChange.u, id, Eq.mp, congr, congrArg, Units, MonoidHom, Units.map, WeierstrassCurve.VariableChange.map_u, WeierstrassCurve.VariableChange.mk and 114 more
162 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
```
theorem quadraticTwistPointEquiv_map_of_not_fixed {σ : M ≃ₐ[K] M}
    (hσ : ¬ ∀ x : L, σ (algebraMap L M x) = algebraMap L M x)
    (P : ((E.quadraticTwist L)⁄M).Point) :
    E.quadraticTwistPointEquiv L M (Affine.Point.map σ.toAlgHom P) =
      -Affine.Point.map σ.toAlgHom (E.quadraticTwistPointEquiv L M P) := by
…
```
theorem WeierstrassCurve.quadraticTwistPointEquiv_galois Twisting the Galois action line 737 source
Source documentation
Twisting the Galois action. The Galois action on the points of the quadratic twist is the Galois action on the points of E, twisted by the quadratic character of L/K: for σ ∈ Aut(M/K), transporting the action of σ on Eᴸ(M) through Eᴸ(M) ≅ E(M) gives χ(σ) times the action of σ on E(M).
Taking M to be a separable closure of K, this says that the Galois representations attached to Eᴸ (e.g. on torsion points) are those attached to E, twisted by χ. Taking M = L and σ ≠ 1 recovers the classical anti-equivariance of the isomorphism φ : Eᴸ ≅ E over L (see quadraticTwistPointEquiv_conj). Note the statement is unchanged under replacing φ by -φ, so it does not depend on the sign choice hidden in quadraticTwistPointEquiv. Note also that for σ fixing L pointwise (i.e. σ ∈ Aut(M/L), χ(σ) = 1) it is a special case of naturality, via the L-algebra map underlying σ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, Algebra, Algebra.IsQuadraticExtension, Algebra.IsSeparable, IsScalarTower, WeierstrassCurve.IsElliptic, DecidableEq, AlgEquiv, WeierstrassCurve.Affine.Point, WeierstrassCurve.Affine.baseChange, WeierstrassCurve.quadraticTwist, Eq, AddEquiv, WeierstrassCurve.quadraticTwistPointEquiv, AddMonoidHom, WeierstrassCurve.Affine.Point.map, HSMul.hSMul, Int, MonoidHom and 2 more
Proof uses: dite, RingHom, Algebra.algebraMap, Classical.propDecidable, Eq.mpr, OfNat.ofNat, id, congrArg, Iff.mpr, quadraticCharacter_eq_one_iff, Units.val_one, one_zsmul, WeierstrassCurve.quadraticTwistPointEquiv_map, AlgHom, AlgHom.mk, AlgHom.toRingHom, Not, Neg.neg, Or.resolve_left, Int.units_eq_one_or and 4 more
102 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
theorem quadraticTwistPointEquiv_galois (σ : M ≃ₐ[K] M) (P : ((E.quadraticTwist L)⁄M).Point) :
    E.quadraticTwistPointEquiv L M (Affine.Point.map σ.toAlgHom P) =
      (quadraticCharacter K L M σ : ℤ) •
        Affine.Point.map σ.toAlgHom (E.quadraticTwistPointEquiv L M P) := by
…
```
Mentions: quadraticCharacter
theorem WeierstrassCurve.quadraticTwistPointEquiv_conj Special case of quadraticTwistPointEquiv_galois over M = L itself: the isomorphism φ : Eᴸ(L) ≅ E(L) intertwines the action of the nontrivial element σ ∈ Gal(L/K) with -σ line 755 source
Source documentation
Special case of quadraticTwistPointEquiv_galois over M = L itself: the isomorphism φ : Eᴸ(L) ≅ E(L) intertwines the action of the nontrivial element σ ∈ Gal(L/K) with -σ. This is the datum classically used to define the twist by Galois descent.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, Algebra, Algebra.IsQuadraticExtension, Algebra.IsSeparable, WeierstrassCurve.IsElliptic, DecidableEq, AlgEquiv, Ne, OfNat.ofNat, WeierstrassCurve.Affine.Point, WeierstrassCurve.Affine.baseChange, WeierstrassCurve.quadraticTwist, Eq, AddEquiv, WeierstrassCurve.quadraticTwistPointEquiv, AddMonoidHom, WeierstrassCurve.Affine.Point.map, Neg.neg
Proof uses: WeierstrassCurve.quadraticTwistPointEquiv_map_of_not_fixed, RingHom, Algebra.algebraMap, AlgEquiv.ext, id
55 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem quadraticTwistPointEquiv_conj [DecidableEq L] {σ : L ≃ₐ[K] L} (hσ : σ ≠ 1)
    (P : ((E.quadraticTwist L)⁄L).Point) :
    E.quadraticTwistPointEquiv L L (Affine.Point.map σ.toAlgHom P) =
      -Affine.Point.map σ.toAlgHom (E.quadraticTwistPointEquiv L L P) := by
…
```
theorem WeierstrassCurve.exists_quadraticTwistPointEquiv_baseChange_eq_iff Documented declaration: exists_quadraticTwistPointEquiv_baseChange_eq_iff line 770 source
Source documentation
The rational points of the quadratic twist, viewed inside E(L) via the isomorphism over L, are exactly the points of E(L) on which the nontrivial element of Gal(L/K) acts as -1 (just as E(K) consists of the points on which it acts as +1). One inclusion is Affine.Point.map_baseChange (the base change of a K-point is σ-fixed) together with quadraticTwistPointEquiv_conj; the other is Galois descent for points (exists_baseChange_point_eq_of_map_eq). Combined with Galois descent this yields, over a number field, rank E(L) = rank E(K) + rank Eᴸ(K).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, Algebra, Algebra.IsQuadraticExtension, Algebra.IsSeparable, WeierstrassCurve.IsElliptic, DecidableEq, AlgEquiv, Ne, OfNat.ofNat, WeierstrassCurve.Affine.Point, WeierstrassCurve.Affine.baseChange, Iff, Exists, WeierstrassCurve.quadraticTwist, Eq, AddEquiv, WeierstrassCurve.quadraticTwistPointEquiv, AddMonoidHom, WeierstrassCurve.Affine.Point.baseChange and 2 more
Proof uses: Iff.intro, WeierstrassCurve.Affine.Point.map_baseChange, WeierstrassCurve.quadraticTwistPointEquiv_conj, Iff.mp, neg_eq_iff_eq_neg, Eq.symm, Eq.mp, congrArg, AddEquiv.symm, AddEquiv.injective, Eq.mpr, id, AddEquiv.apply_symm_apply, neg_neg, Eq.refl, WeierstrassCurve.exists_baseChange_point_eq_of_map_eq, Exists.intro
72 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
theorem exists_quadraticTwistPointEquiv_baseChange_eq_iff [DecidableEq K] [DecidableEq L]
    {σ : L ≃ₐ[K] L} (hσ : σ ≠ 1) (P : (E⁄L).Point) :
    (∃ Q : ((E.quadraticTwist L)⁄K).Point,
        E.quadraticTwistPointEquiv L L (Affine.Point.baseChange K L Q) = P) ↔
      Affine.Point.map σ.toAlgHom P = -P := by
…
```