The quadratic twist of a Weierstrass curve: definition and invariants

The quadratic twist E.quadraticTwistOf t n of a Weierstrass curve by parameters (t, n) — to be thought of as the trace and norm of a generator θ of a separable quadratic extension L/K, with D := t² - 4n the discriminant of its minimal polynomial — together with the behaviour of the standard invariants under twisting, uniformly in the characteristic: over any commutative ring b₂, b₄, b₆ scale by D, D², D³, c₄, c₆ by D², D³, and Δ by D⁶, so the twist of an elliptic curve is elliptic exactly when D is a unit — over a field, when D ≠ 0 — with the same j-invariant. Twisting by a split quadratic, twisting twice by (t, n), or changing (t, n) to the trace and norm of another generator, all move the twist by an explicit change of variables, again over any commutative ring in which the relevant parameter is a unit.

Main definitions

• WeierstrassCurve.quadraticTwistOf: the quadratic twist of a Weierstrass curve by (t, n), an explicit Weierstrass model over any commutative ring.
• WeierstrassCurve.nodePolynomial_coeff_zero_quadraticTwistOf: the constant coefficient of nodePolynomial is the one quantity here that does not simply scale by a power of t² - 4n; it acquires + D² n a₁² c₄. Splitting of the node polynomial is not determined by this coefficient alone, so this is a record of how it transforms, not a reduction statement.
• WeierstrassCurve.nodePolynomial_quadraticTwistOf_neg_a₁: twisting by the trace -a₁ and norm n of a root of the node quadratic T² + a₁ T + n makes the node polynomial split, with roots a₁² - 2n and 2n.
• WeierstrassCurve.Δ_quadraticTwistOf, WeierstrassCurve.c₄_quadraticTwistOf, WeierstrassCurve.c₆_quadraticTwistOf: the invariants of the twist.
• WeierstrassCurve.isElliptic_quadraticTwistOf_iff and its field specialisation WeierstrassCurve.isElliptic_quadraticTwistOf, and WeierstrassCurve.j_quadraticTwistOf: the twist of an elliptic curve is elliptic exactly when t² - 4n is a unit — over a field, when it is nonzero — with equal j.
• WeierstrassCurve.exists_smul_eq_quadraticTwistOf_quadraticTwistOf, WeierstrassCurve.exists_smul_quadraticTwistOf_eq: the double twist is isomorphic to the original curve, and changing the generator moves the twist by a change of variables.
• WeierstrassCurve.isElliptic_quadraticTwistOf_trace_norm, WeierstrassCurve.exists_smul_quadraticTwistOf_trace_norm_eq: the twist by the trace and norm of a generator θ of a separable quadratic extension L/K is elliptic when E is, and changing the generator moves it by a change of variables — which is what makes the twist by the extension well posed.
• WeierstrassCurve.quadraticTwist: the quadratic twist of E by a separable quadratic extension L/K, the twist by the trace and norm of a generator chosen by Algebra.IsQuadraticExtension.exists_discrim_ne_zero. Separability is required: without it the extension could be purely inseparable, where the trace form vanishes and the model is singular for every E.
• WeierstrassCurve.exists_quadraticTwist_eq: elimination — the twist equals the twist by the trace and norm of some generator, so everything above about quadraticTwistOf transfers. WeierstrassCurve.exists_smul_quadraticTwist_eq adds that any other generator gives the same curve up to a change of variables.
• WeierstrassCurve.isElliptic_quadraticTwist (an instance) and WeierstrassCurve.j_quadraticTwist: the twist of an elliptic curve is elliptic, with the same j-invariant.
• WeierstrassCurve.quadraticTwistOfTraceNormVariableChange: the explicit change of variables over L carrying the twist by θ back to E, with WeierstrassCurve.quadraticTwistOfTraceNormVariableChange_smul_baseChange saying that it does so — the twist is an L-form of E — and WeierstrassCurve.map_quadraticTwistOfTraceNormVariableChange giving the Galois cocycle it carries: conjugating it by the nontrivial σ ∈ Gal(L/K) changes it by negVariableChange. The witness is a definition rather than an existential precisely because the cocycle identity is a statement about this change of variables and not about an arbitrary one carrying the twist to E. WeierstrassCurve.exists_smul_quadraticTwist_baseChange_eq is the corresponding statement for quadraticTwist itself, where the generator is the one chosen internally.
• WeierstrassCurve.quadraticTwistVariableChange: the same change of variables in the other direction, carrying E to the twist, at the generator quadraticTwist chooses internally — the inverse of the previous one, with WeierstrassCurve.quadraticTwistVariableChange_smul and the cocycle WeierstrassCurve.map_quadraticTwistVariableChange, where the negVariableChange factor sits on the right because inverting a product reverses it.
• WeierstrassCurve.not_exists_smul_quadraticTwist_eq and WeierstrassCurve.exists_smul_eq_or_exists_smul_eq_quadraticTwist: the classification, for j ∉ {0, 1728}. The twist is not K-isomorphic to E, and any curve becoming isomorphic to E over L is K-isomorphic to one of the two. This is where the cocycle is used: forms are classified by H¹(Gal(L/K), Aut Eᴸ) = Hom(ℤ/2, {±1}), of order two, and the two branches of the proof are its two classes.

These are the quadraticTwistOf seeds of TauCetiRoadmap/EllipticCurves/README.md §Layer 5 (twists), pinned in that roadmap's Suggested.lean, together with the extension twist they make well posed, the classification of the L-forms that the cocycle delivers, and the point isomorphism quadraticTwistPointEquiv that quadraticTwistVariableChange induces; the twist formulas here, in particular nodePolynomial_quadraticTwistOf_neg_a₁, are applied to curves with multiplicative reduction in QuadraticTwist/SplitMultiplicative.lean.

The point isomorphism

Over any field M in a tower K ⊆ L ⊆ M, the base change of quadraticTwistVariableChange carries E to its twist (quadraticTwistVariableChange_smul_baseChange) and satisfies the cocycle identity (map_quadraticTwistVariableChange_baseChange). Transporting along it gives quadraticTwistPointEquiv : ((E.quadraticTwist L)⁄M).Point ≃+ (E⁄M).Point, with quadraticTwistPointEquiv_some the coordinate equation a consumer needs. It is natural in M (quadraticTwistPointEquiv_map) and anti-equivariant for the Galois elements that move L (quadraticTwistPointEquiv_map_eq_neg_map_of_not_fixed): that sign is what makes the twist a twist. quadraticTwistPointEquiv_map_eq_quadraticCharacter_smul_map packages the two cases as φ(σP) = χ(σ|_L) • σ(φP), uniformly in σ, where χ is Algebra.IsQuadraticExtension.quadraticCharacter — the Gal(L/K) →* ℤˣ sending the nontrivial automorphism to -1. That is the canonical form of the statement: the isomorphism is defined over L rather than over K, and χ measures precisely that failure.

The twist by a generator is deliberately not given its own constructor here. Such a definition would accept any field extension, and outside the finite-dimensional case Mathlib's Algebra.trace and Algebra.norm are 0 and 1, so every θ would yield the same unrelated (0, 1) twist. The results below instead name Algebra.trace K L θ and Algebra.norm K θ directly and carry [Algebra.IsQuadraticExtension K L], where the construction has its intended meaning.

Adapted from the FLT project's quadratic-twist development (ImperialCollegeLondon/FLT, FLT/KnownIn1980s/EllipticCurves/QuadraticTwists/QuadraticTwists.lean at the roadmap's pin bc2fe8ff7396, FLT PR #1088, Apache 2.0). That file's own header reads Authors: Kevin Buzzard, Claude, and it has not been touched in FLT since bc2fe8ff7396, so the pin and the working clone (d18b563029f3, a later Mathlib bump) agree on it verbatim. Following this repository's convention for adapted material, the upstream authorship is credited here rather than in the copyright header.

References

• J. Silverman, The Arithmetic of Elliptic Curves, III.§10, X.§2 and X.§5

def WeierstrassCurve.quadraticTwistOf {A : Type u_1} [CommRing A] (E : WeierstrassCurve A) (t n : A) : WeierstrassCurve A

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 (so that θ² = tθ - n, and D := t² - 4n is the discriminant of the minimal polynomial of θ). The parameters are arbitrary elements of any commutative ring A; the reading of (t, n) as the trace and norm of a generator of a separable quadratic extension, with D ≠ 0 the separability criterion, is the field case. Over a general commutative ring the condition that makes the twist behave — and the hypothesis the results below take — is that D be a unit.

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 exactly when D is a unit (isElliptic_quadraticTwistOf_iff) — over a field, 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₃²).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem WeierstrassCurve.a₁_quadraticTwistOf {A : Type u_1} [CommRing A] (E : WeierstrassCurve A) (t n : A) : (E.quadraticTwistOf t n).a₁ = t * E.a₁

The coefficient a₁ of the quadratic twist.

@[simp]

theorem WeierstrassCurve.a₂_quadraticTwistOf {A : Type u_1} [CommRing A] (E : WeierstrassCurve A) (t n : A) : (E.quadraticTwistOf t n).a₂ = (t ^ 2 - 4 * n) * E.a₂ - n * E.a₁ ^ 2

The coefficient a₂ of the quadratic twist.

@[simp]

theorem WeierstrassCurve.a₃_quadraticTwistOf {A : Type u_1} [CommRing A] (E : WeierstrassCurve A) (t n : A) : (E.quadraticTwistOf t n).a₃ = (t ^ 2 - 4 * n) * t * E.a₃

The coefficient a₃ of the quadratic twist.

@[simp]

theorem WeierstrassCurve.a₄_quadraticTwistOf {A : Type u_1} [CommRing A] (E : WeierstrassCurve A) (t n : A) : (E.quadraticTwistOf t n).a₄ = (t ^ 2 - 4 * n) ^ 2 * E.a₄ - 2 * (t ^ 2 - 4 * n) * n * E.a₁ * E.a₃

The coefficient a₄ of the quadratic twist.

@[simp]

theorem WeierstrassCurve.a₆_quadraticTwistOf {A : Type u_1} [CommRing A] (E : WeierstrassCurve A) (t n : A) : (E.quadraticTwistOf t n).a₆ = (t ^ 2 - 4 * n) ^ 3 * E.a₆ - (t ^ 2 - 4 * n) ^ 2 * n * E.a₃ ^ 2

The coefficient a₆ of the quadratic twist.

@[simp]

theorem WeierstrassCurve.quadraticTwistOf_one_zero {A : Type u_1} [CommRing A] (E : WeierstrassCurve A) : E.quadraticTwistOf 1 0 = E

Twisting by (t, n) = (1, 0) — the split quadratic x² - x, with D = 1 — returns the curve itself.

@[simp]

theorem WeierstrassCurve.b₂_quadraticTwistOf {A : Type u_1} [CommRing A] (E : WeierstrassCurve A) (t n : A) : (E.quadraticTwistOf t n).b₂ = (t ^ 2 - 4 * n) * E.b₂

The invariant b₂ of the quadratic twist: b₂ ↦ Db₂ with D = t² - 4n.

@[simp]

theorem WeierstrassCurve.b₄_quadraticTwistOf {A : Type u_1} [CommRing A] (E : WeierstrassCurve A) (t n : A) : (E.quadraticTwistOf t n).b₄ = (t ^ 2 - 4 * n) ^ 2 * E.b₄

The invariant b₄ of the quadratic twist: b₄ ↦ D²b₄ with D = t² - 4n.

@[simp]

theorem WeierstrassCurve.b₆_quadraticTwistOf {A : Type u_1} [CommRing A] (E : WeierstrassCurve A) (t n : A) : (E.quadraticTwistOf t n).b₆ = (t ^ 2 - 4 * n) ^ 3 * E.b₆

The invariant b₆ of the quadratic twist: b₆ ↦ D³b₆ with D = t² - 4n.

@[simp]

theorem WeierstrassCurve.b₈_quadraticTwistOf {A : Type u_1} [CommRing A] (E : WeierstrassCurve A) (t n : A) : (E.quadraticTwistOf t n).b₈ = (t ^ 2 - 4 * n) ^ 4 * E.b₈

The invariant b₈ of the quadratic twist: b₈ ↦ D⁴b₈ with D = t² - 4n.

@[simp]

theorem WeierstrassCurve.c₄_quadraticTwistOf {A : Type u_1} [CommRing A] (E : WeierstrassCurve A) (t n : A) : (E.quadraticTwistOf t n).c₄ = (t ^ 2 - 4 * n) ^ 2 * E.c₄

The invariant c₄ of the quadratic twist: c₄ ↦ D²c₄ with D = t² - 4n.

@[simp]

theorem WeierstrassCurve.c₆_quadraticTwistOf {A : Type u_1} [CommRing A] (E : WeierstrassCurve A) (t n : A) : (E.quadraticTwistOf t n).c₆ = (t ^ 2 - 4 * n) ^ 3 * E.c₆

The invariant c₆ of the quadratic twist: c₆ ↦ D³c₆ with D = t² - 4n.

@[simp]

theorem WeierstrassCurve.Δ_quadraticTwistOf {A : Type u_1} [CommRing A] (E : WeierstrassCurve A) (t n : A) : (E.quadraticTwistOf t n).Δ = (t ^ 2 - 4 * n) ^ 6 * E.Δ

The discriminant of the quadratic twist: Δ ↦ D⁶Δ with D = t² - 4n.

@[simp]

theorem WeierstrassCurve.nodePolynomial_coeff_zero_quadraticTwistOf {A : Type u_1} [CommRing A] (E : WeierstrassCurve A) (t n : A) : (E.quadraticTwistOf t n).nodePolynomial.coeff 0 = (t ^ 2 - 4 * n) ^ 3 * E.nodePolynomial.coeff 0 + (t ^ 2 - 4 * n) ^ 2 * n * E.a₁ ^ 2 * E.c₄

The constant coefficient of the node polynomial, under twisting. Unlike b₂, b₄, b₆, c₄, c₆ and Δ, which all simply scale by a power of D = t² - 4n, this coefficient picks up an extra + D² n a₁² c₄. That term vanishes when any of a₁, n, c₄ or D does — and, over a general commutative ring, it can vanish from zero divisors without any factor being zero.

Whether the node polynomial splits over the residue field is what distinguishes split from non-split multiplicative reduction, so a twist can change that behaviour — but splitting is not determined by this coefficient alone, and this lemma establishes no reduction statement by itself. It records the coefficient's transformation, which such an argument would use (for instance in the characteristic-two Artin–Schreier calculation), and nothing more.

theorem WeierstrassCurve.nodePolynomial_quadraticTwistOf_neg_a₁ {A : Type u_1} [CommRing A] (E : WeierstrassCurve A) (n : A) (hn : E.c₄ * n = E.nodePolynomial.coeff 0) : (E.quadraticTwistOf (-E.a₁) n).nodePolynomial = Polynomial.C ((E.a₁ ^ 2 - 4 * n) ^ 2 * E.c₄) * (Polynomial.X - Polynomial.C (E.a₁ ^ 2 - 2 * n)) * (Polynomial.X - Polynomial.C (2 * n))

Twisting by the node quadratic splits the node polynomial. Let n be such that c₄ n is the constant coefficient of the node polynomial, so that the node polynomial is c₄ · (T² + a₁ T + n) (nodePolynomial_eq_C_mul). Twisting by the trace -a₁ and norm n of a root of T² + a₁ T + n gives a curve whose node polynomial is D² c₄ · (T - (a₁² - 2n)) · (T - 2n), with D = a₁² - 4n: its roots lie in the base ring. This holds over any commutative ring, with no hypothesis on c₄ or D.

@[simp]

theorem WeierstrassCurve.map_quadraticTwistOf {A : Type u_1} [CommRing A] (E : WeierstrassCurve A) (t n : A) {B : Type u_2} [CommRing B] (f : A →+* B) : (E.quadraticTwistOf t n).map f = (E.map f).quadraticTwistOf (f t) (f n)

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

@[simp]

theorem WeierstrassCurve.baseChange_quadraticTwistOf {A : Type u_1} [CommRing A] (E : WeierstrassCurve A) (t n : A) {B : Type u_2} [CommRing B] [Algebra A B] : (E.quadraticTwistOf t n).baseChange B = (E.baseChange B).quadraticTwistOf ((algebraMap A B) t) ((algebraMap A B) n)

Quadratic twisting commutes with extension of scalars: the twist of the base change is the base change of the twist, by the images of the parameters.

theorem WeierstrassCurve.isElliptic_quadraticTwistOf_iff {A : Type u_1} [CommRing A] (E : WeierstrassCurve A) (t n : A) : (E.quadraticTwistOf t n).IsElliptic ↔ IsUnit (t ^ 2 - 4 * n) ∧ E.IsElliptic

The quadratic twist of an elliptic curve is elliptic exactly when the discriminant D = t² - 4n of the twisting parameters is a unit. Over a general commutative ring D ≠ 0 is not the right criterion (take A = ℤ, D = 2); over a field the two coincide, which is isElliptic_quadraticTwistOf.

theorem WeierstrassCurve.j_quadraticTwistOf {A : Type u_1} [CommRing A] (E : WeierstrassCurve A) (t n : A) [E.IsElliptic] (h : (E.quadraticTwistOf t n).IsElliptic) : (E.quadraticTwistOf t n).j = E.j

The j-invariant is a twist invariant: j(E_{t,n}) = j(E).

theorem WeierstrassCurve.quadraticTwistOf_quadraticTwistOf {A : Type u_1} [CommRing A] (E : WeierstrassCurve A) (t n : A) : (E.quadraticTwistOf t n).quadraticTwistOf t n = E.quadraticTwistOf (t ^ 2) (2 * t ^ 2 * n - 4 * n ^ 2)

Twisting twice by the same parameters is twisting once by their composite: the quadratic x² - t²x + (2t²n - 4n²) is split, with roots t² - 2n and 2n — it represents the trivial twist, which is why the double twist is isomorphic to E whenever t² - 4n is a unit. No hypothesis.

def WeierstrassCurve.quadraticTwistOfVariableChange {A : Type u_1} [CommRing A] (E : WeierstrassCurve A) (t n : A) (u : Aˣ) (b : A) : VariableChange A

The change of variables carrying the twist by the trace and norm of aθ + b back to the twist by those of θ. It is the single witness behind every isomorphism in this file: exists_smul_quadraticTwistOf_eq supplies its inverse, and quadraticTwistOfTraceNormVariableChange is its base change at (t, n) = (1, 0).

Stated over any commutative ring, since the identity it satisfies is polynomial; only invertibility of a is needed.

Its four projections are quadraticTwistOfVariableChange_u/_r/_s/_t, as negVariableChange has negVariableChange_u/_r/_s/_t: the body does not unfold outside this module, and the action identity below does not pin the value down on its own, since composing with an automorphism of the twisted curve gives another change of variables satisfying it.

Equations

• E.quadraticTwistOfVariableChange t n u b = { u := u, r := 0, s := -(b * E.a₁), t := -(↑u ^ 2 * b * (t ^ 2 - 4 * n) * E.a₃) }

@[simp]

theorem WeierstrassCurve.quadraticTwistOfVariableChange_u {A : Type u_1} [CommRing A] (E : WeierstrassCurve A) (t n : A) (u : Aˣ) (b : A) : (E.quadraticTwistOfVariableChange t n u b).u = u

@[simp]

theorem WeierstrassCurve.quadraticTwistOfVariableChange_r {A : Type u_1} [CommRing A] (E : WeierstrassCurve A) (t n : A) (u : Aˣ) (b : A) : (E.quadraticTwistOfVariableChange t n u b).r = 0

@[simp]

theorem WeierstrassCurve.quadraticTwistOfVariableChange_s {A : Type u_1} [CommRing A] (E : WeierstrassCurve A) (t n : A) (u : Aˣ) (b : A) : (E.quadraticTwistOfVariableChange t n u b).s = -(b * E.a₁)

@[simp]

theorem WeierstrassCurve.quadraticTwistOfVariableChange_t {A : Type u_1} [CommRing A] (E : WeierstrassCurve A) (t n : A) (u : Aˣ) (b : A) : (E.quadraticTwistOfVariableChange t n u b).t = -(↑u ^ 2 * b * (t ^ 2 - 4 * n) * E.a₃)

@[simp]

theorem WeierstrassCurve.quadraticTwistOfVariableChange_smul {A : Type u_1} [CommRing A] (E : WeierstrassCurve A) (t n : A) (u : Aˣ) (b : A) : E.quadraticTwistOfVariableChange t n u b • E.quadraticTwistOf (↑u * t + 2 * b) (b ^ 2 + ↑u * b * t + ↑u ^ 2 * n) = E.quadraticTwistOf t n

The defining identity of quadraticTwistOfVariableChange: it carries the twist by the transformed parameters (ut + 2b, b² + ubt + u²n) — those of the generator uθ + b — back to the twist by (t, n) themselves. Every isomorphism in this file is an instance of this one.

theorem WeierstrassCurve.exists_smul_quadraticTwistOf_eq {A : Type u_1} [CommRing A] (E : WeierstrassCurve A) (t n : A) {a : A} (b : A) (ha : IsUnit a) : ∃ (C : VariableChange A), C • E.quadraticTwistOf t n = E.quadraticTwistOf (a * t + 2 * b) (b ^ 2 + a * b * t + a ^ 2 * n)

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 a field the hypothesis is a ≠ 0 (isUnit_iff_ne_zero).

theorem WeierstrassCurve.exists_smul_eq_quadraticTwistOf_add_mul {A : Type u_1} [CommRing A] (E : WeierstrassCurve A) (r s : A) (h : IsUnit (s - r)) : ∃ (C : VariableChange A), C • E = E.quadraticTwistOf (r + s) (r * s)

Twisting by a split quadratic (x - r)(x - s) is trivial up to isomorphism: the twist by its trace and norm (r + s, rs) is a change of variables away from E, provided the difference of the roots is a unit (that difference squared is the discriminant).

theorem WeierstrassCurve.exists_smul_eq_quadraticTwistOf_quadraticTwistOf {A : Type u_1} [CommRing A] (E : WeierstrassCurve A) (t n : A) (hD : IsUnit (t ^ 2 - 4 * n)) : ∃ (C : VariableChange A), C • E = (E.quadraticTwistOf t n).quadraticTwistOf t n

Twisting twice by the same parameters (t, n) gives an isomorphic curve, provided the discriminant D = t² - 4n is a unit.

theorem WeierstrassCurve.isElliptic_quadraticTwistOf {K : Type u_1} [Field K] (E : WeierstrassCurve K) (t n : K) [E.IsElliptic] (hD : t ^ 2 - 4 * n ≠ 0) : (E.quadraticTwistOf t n).IsElliptic

Over a field, the quadratic twist of an elliptic curve is elliptic when the discriminant D = t² - 4n of the twisting parameters is nonzero. This is the form the roadmap and the source state; isElliptic_quadraticTwistOf_iff is the ring-level equivalence it specialises.

theorem WeierstrassCurve.exists_smul_quadraticTwistOf_trace_norm_eq {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (E : WeierstrassCurve K) [Algebra.IsQuadraticExtension K L] {θ θ' : L} (hθ : θ ∉ Set.range ⇑(algebraMap K L)) (hθ' : θ' ∉ Set.range ⇑(algebraMap K L)) : ∃ (C : VariableChange K), C • E.quadraticTwistOf ((Algebra.trace K L) θ) ((Algebra.norm K) θ) = E.quadraticTwistOf ((Algebra.trace K L) θ') ((Algebra.norm K) θ')

The quadratic twist by a generator θ of a quadratic extension L/K depends on the choice of θ only up to isomorphism over K: all generators give isomorphic twists. This is what makes the twist by the extension itself well posed. Separability is not needed — only the trace and norm of b + aθ, which any quadratic extension supplies.

theorem WeierstrassCurve.isElliptic_quadraticTwistOf_trace_norm {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (E : WeierstrassCurve K) [Algebra.IsQuadraticExtension K L] [Algebra.IsSeparable K L] [E.IsElliptic] {θ : L} (hθ : θ ∉ Set.range ⇑(algebraMap K L)) : (E.quadraticTwistOf ((Algebra.trace K L) θ) ((Algebra.norm K) θ)).IsElliptic

The twist of an elliptic curve by a generator of a separable quadratic extension is elliptic: the discriminant t² - 4n of the generator's minimal polynomial is nonzero.

noncomputable def WeierstrassCurve.quadraticTwist {K : Type u_1} [Field K] (E : WeierstrassCurve K) (L : Type u_3) [Field L] [Algebra K L] [Algebra.IsQuadraticExtension K L] [Algebra.IsSeparable K L] : WeierstrassCurve K

The quadratic twist of E by the separable quadratic extension L/K: the twist by the trace and norm of a generator of L/K. The choice of generator is harmless — exists_quadraticTwist_eq names one, and exists_smul_quadraticTwist_eq says every other gives the same curve up to a change of variables over K.

Separability is not decoration. On a purely inseparable quadratic extension the trace form vanishes, so t = 0 and — in characteristic 2, the only characteristic where such an extension exists — the discriminant D = t² - 4n is 0, and the model is singular for every E and barely depends on E. This is a different failure from the one the module docstring gives for refusing a twist-by-a-generator constructor, which is (t, n) = (0, 1) and so D = -4: there the parameters cease to reflect the extension but the twist stays generically nonsingular. The two coincide only in characteristic 2. Choosing the generator by Algebra.IsQuadraticExtension.exists_discrim_ne_zero rules this case out, so the twist parameters never degenerate. That is all it can rule out: E is arbitrary here, so a singular E still gives a singular twist. Nonsingularity of the result needs E elliptic too, which is isElliptic_quadraticTwist.

Equations

• E.quadraticTwist L = E.quadraticTwistOf ((Algebra.trace K L) ⋯.choose) ((Algebra.norm K) ⋯.choose)

theorem WeierstrassCurve.exists_quadraticTwist_eq {K : Type u_1} [Field K] (L : Type u_2) [Field L] [Algebra K L] (E : WeierstrassCurve K) [Algebra.IsQuadraticExtension K L] [Algebra.IsSeparable K L] : ∃ θ ∉ Set.range ⇑(algebraMap K L), E.quadraticTwist L = E.quadraticTwistOf ((Algebra.trace K L) θ) ((Algebra.norm K) θ)

Elimination for quadraticTwist. The twist is the twist by the trace and norm of some generator of L/K — an equation, not merely an isomorphism, so everything proved about quadraticTwistOf (the coefficients, Δ, c₄, c₆) transfers to quadraticTwist. Use it to discharge a quadraticTwist goal. L is explicit because it occurs only inside the existential.

instance WeierstrassCurve.isElliptic_quadraticTwist {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (E : WeierstrassCurve K) [Algebra.IsQuadraticExtension K L] [Algebra.IsSeparable K L] [E.IsElliptic] : (E.quadraticTwist L).IsElliptic

The twist of an elliptic curve by a separable quadratic extension is elliptic. Registered as an instance so that downstream statements needing [(E.quadraticTwist L).IsElliptic] discharge it by typeclass inference.

@[simp]

theorem WeierstrassCurve.j_quadraticTwist {K : Type u_1} [Field K] (L : Type u_2) [Field L] [Algebra K L] (E : WeierstrassCurve K) [Algebra.IsQuadraticExtension K L] [Algebra.IsSeparable K L] [E.IsElliptic] : (E.quadraticTwist L).j = E.j

Twisting does not change the j-invariant.

theorem WeierstrassCurve.exists_smul_quadraticTwist_eq {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (E : WeierstrassCurve K) [Algebra.IsQuadraticExtension K L] [Algebra.IsSeparable K L] {θ : L} (hθ : θ ∉ Set.range ⇑(algebraMap K L)) : ∃ (C : VariableChange K), C • E.quadraticTwist L = E.quadraticTwistOf ((Algebra.trace K L) θ) ((Algebra.norm K) θ)

The twist by the extension agrees, up to a change of variables over K, with the twist by any generator θ: the arbitrary choice in quadraticTwist is harmless.

def WeierstrassCurve.quadraticTwistOfTraceNormVariableChange {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (E : WeierstrassCurve K) [Algebra.IsQuadraticExtension K L] [Algebra.IsSeparable K L] {θ : L} (hθ : θ ∉ Set.range ⇑(algebraMap K L)) {σ : Gal(L/K)} (hσ : σ ≠ 1) : VariableChange L

The change of variables over L that carries the twist by θ back to E. It rescales by σ θ - θ, a square root of the discriminant of θ's minimal polynomial, and shears and translates by the amounts that clear the twisted model's a₁ and a₃ terms.

This is the witness of quadraticTwistOfTraceNormVariableChange_smul_baseChange; it is a definition rather than an existential because map_quadraticTwistOfTraceNormVariableChange is a statement about this change of variables, and does not hold of an arbitrary one carrying the twist to E — two such differ by an automorphism of E, which the cocycle identity does not tolerate.

Equations

• E.quadraticTwistOfTraceNormVariableChange hθ hσ = (E.baseChange L).quadraticTwistOfVariableChange 1 0 (Units.mk0 (σ θ - θ) ⋯) θ

@[simp]

theorem WeierstrassCurve.quadraticTwistOfTraceNormVariableChange_u {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (E : WeierstrassCurve K) [Algebra.IsQuadraticExtension K L] [Algebra.IsSeparable K L] {θ : L} (hθ : θ ∉ Set.range ⇑(algebraMap K L)) {σ : Gal(L/K)} (hσ : σ ≠ 1) : (E.quadraticTwistOfTraceNormVariableChange hθ hσ).u = Units.mk0 (σ θ - θ) ⋯

@[simp]

theorem WeierstrassCurve.quadraticTwistOfTraceNormVariableChange_r {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (E : WeierstrassCurve K) [Algebra.IsQuadraticExtension K L] [Algebra.IsSeparable K L] {θ : L} (hθ : θ ∉ Set.range ⇑(algebraMap K L)) {σ : Gal(L/K)} (hσ : σ ≠ 1) : (E.quadraticTwistOfTraceNormVariableChange hθ hσ).r = 0

@[simp]

theorem WeierstrassCurve.quadraticTwistOfTraceNormVariableChange_s {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (E : WeierstrassCurve K) [Algebra.IsQuadraticExtension K L] [Algebra.IsSeparable K L] {θ : L} (hθ : θ ∉ Set.range ⇑(algebraMap K L)) {σ : Gal(L/K)} (hσ : σ ≠ 1) : (E.quadraticTwistOfTraceNormVariableChange hθ hσ).s = -(θ * (E.baseChange L).a₁)

@[simp]

theorem WeierstrassCurve.quadraticTwistOfTraceNormVariableChange_t {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (E : WeierstrassCurve K) [Algebra.IsQuadraticExtension K L] [Algebra.IsSeparable K L] {θ : L} (hθ : θ ∉ Set.range ⇑(algebraMap K L)) {σ : Gal(L/K)} (hσ : σ ≠ 1) : (E.quadraticTwistOfTraceNormVariableChange hθ hσ).t = -((σ θ - θ) ^ 2 * θ * (E.baseChange L).a₃)

theorem WeierstrassCurve.quadraticTwistOfTraceNormVariableChange_smul_baseChange {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (E : WeierstrassCurve K) [Algebra.IsQuadraticExtension K L] [Algebra.IsSeparable K L] {θ : L} (hθ : θ ∉ Set.range ⇑(algebraMap K L)) {σ : Gal(L/K)} (hσ : σ ≠ 1) : E.quadraticTwistOfTraceNormVariableChange hθ hσ • (E.quadraticTwistOf ((Algebra.trace K L) θ) ((Algebra.norm K) θ)).baseChange L = E.baseChange L

The twist becomes isomorphic to E over L, by the explicit change of variables quadraticTwistOfTraceNormVariableChange. Over a field, isomorphisms of Weierstrass curves are exactly the admissible changes of variables, acting via •.

@[simp]

theorem WeierstrassCurve.map_quadraticTwistOfTraceNormVariableChange {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (E : WeierstrassCurve K) [Algebra.IsQuadraticExtension K L] [Algebra.IsSeparable K L] {θ : L} (hθ : θ ∉ Set.range ⇑(algebraMap K L)) {σ : Gal(L/K)} (hσ : σ ≠ 1) : (E.quadraticTwistOfTraceNormVariableChange hθ hσ).map ↑σ = (E.baseChange L).negVariableChange * E.quadraticTwistOfTraceNormVariableChange hθ hσ

The Galois cocycle carried by that isomorphism. Conjugating quadraticTwistOfTraceNormVariableChange by the nontrivial σ ∈ Gal(L/K) changes it by negVariableChange, the change of variables [-1]: this is the cocycle identity for H¹(Gal(L/K), Aut E).

It does not say the class is nontrivial. E here is an arbitrary Weierstrass curve, and when negVariableChange = 1 — a singular curve in characteristic 2 with a₁ = a₃ = 0, say — the identity below is plain equivariance. Nontriviality needs hypotheses this statement does not carry.

theorem WeierstrassCurve.exists_smul_quadraticTwist_baseChange_eq {K : Type u_1} [Field K] (L : Type u_2) [Field L] [Algebra K L] (E : WeierstrassCurve K) [Algebra.IsQuadraticExtension K L] [Algebra.IsSeparable K L] : ∃ (C : VariableChange L), C • (E.quadraticTwist L).baseChange L = E.baseChange L

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

noncomputable def WeierstrassCurve.quadraticTwistVariableChange {K : Type u_1} [Field K] (L : Type u_2) [Field L] [Algebra K L] (E : WeierstrassCurve K) [Algebra.IsQuadraticExtension K L] [Algebra.IsSeparable K L] : VariableChange L

The change of variables over L carrying E to its quadratic twist. It is the inverse of quadraticTwistOfTraceNormVariableChange, taken at the generator quadraticTwist chooses internally, so no bridging change of variables is needed: at that generator the twist is quadraticTwistOf of its trace and norm, by definition.

Naming an explicit witness rather than an existential is what makes the cocycle identity map_quadraticTwistVariableChange statable: that identity is false of an arbitrary change of variables carrying E to the twist, since two such differ by an automorphism of the twist.

Equations

• WeierstrassCurve.quadraticTwistVariableChange L E = (E.quadraticTwistOfTraceNormVariableChange ⋯ ⋯)⁻¹

@[simp]

theorem WeierstrassCurve.quadraticTwistVariableChange_smul {K : Type u_1} [Field K] (L : Type u_2) [Field L] [Algebra K L] (E : WeierstrassCurve K) [Algebra.IsQuadraticExtension K L] [Algebra.IsSeparable K L] : quadraticTwistVariableChange L E • E.baseChange L = (E.quadraticTwist L).baseChange L

quadraticTwistVariableChange does carry E to the twist, after base change to L.

@[simp]

theorem WeierstrassCurve.map_quadraticTwistVariableChange {K : Type u_1} [Field K] (L : Type u_2) [Field L] [Algebra K L] (E : WeierstrassCurve K) [Algebra.IsQuadraticExtension K L] [Algebra.IsSeparable K L] {σ : Gal(L/K)} (hσ : σ ≠ 1) : (quadraticTwistVariableChange L E).map ↑σ = quadraticTwistVariableChange L E * (E.baseChange L).negVariableChange

The defining cocycle of the quadratic twist. The nontrivial σ ∈ Gal(L/K) conjugates quadraticTwistVariableChange by the automorphism [-1] of E. This is the mirror of map_quadraticTwistOfTraceNormVariableChange, and the factor lands on the right here because inverting a product reverses it and [-1] is its own inverse (negVariableChange_inv).

As there, this is the cocycle identity and not a nontriviality claim.

theorem WeierstrassCurve.not_exists_smul_quadraticTwist_eq {K : Type u_1} [Field K] (L : Type u_2) [Field L] [Algebra K L] (E : WeierstrassCurve K) [Algebra.IsQuadraticExtension K L] [Algebra.IsSeparable K L] [E.IsElliptic] (hj₀ : E.j ≠ 0) (hj₁₇₂₈ : E.j ≠ 1728) : ¬∃ (C : VariableChange K), C • E.quadraticTwist L = E

The quadratic twist is not isomorphic to E over K, when j(E) ∉ {0, 1728}. Twisting is a genuinely nontrivial operation: this is what map_quadraticTwistOfTraceNormVariableChange deliberately stopped short of claiming, and the j-hypotheses are exactly what it lacked.

What the j-hypotheses buy is Aut(Eᴸ) = {±1} (eq_one_or_eq_negVariableChange_map). At j ∈ {0, 1728} the automorphism group can be strictly larger, and the statement is not claimed there; nor is a counterexample asserted.

theorem WeierstrassCurve.exists_smul_eq_or_exists_smul_eq_quadraticTwist {K : Type u_1} [Field K] (L : Type u_2) [Field L] [Algebra K L] (E : WeierstrassCurve K) [Algebra.IsQuadraticExtension K L] [Algebra.IsSeparable K L] [E.IsElliptic] (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

Classification of the forms of E split by L/K, for j(E) ∉ {0, 1728}. A curve over K that becomes isomorphic to E over L is isomorphic over K either to E or to its quadratic twist by L — and, by not_exists_smul_quadraticTwist_eq, those two alternatives are distinct.

There are exactly two alternatives because such forms are classified by H¹(Gal(L/K), Aut Eᴸ) = Hom(ℤ/2, {±1}), a group of order two. The j-hypotheses are what give Aut Eᴸ = {±1} (eq_one_or_eq_negVariableChange_map); for the excluded j the automorphism group can be larger and there can be more forms.

The isomorphism on points and its Galois anti-equivariance

The curve-level identity below is about base change alone, so it asks only for a commutative L-algebra. Everything after it — the Galois cocycle, the isomorphism on points, and the equivariance statements — genuinely needs M to be a field, and lives in the section after.

theorem WeierstrassCurve.quadraticTwistVariableChange_smul_baseChange {K : Type u_1} [Field K] (L : Type u_2) [Field L] [Algebra K L] (E : WeierstrassCurve K) [Algebra.IsQuadraticExtension K L] [Algebra.IsSeparable K L] (M : Type u_3) [CommRing M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] : (quadraticTwistVariableChange L E).baseChange M • E.baseChange M = (E.quadraticTwist L).baseChange M

The change of variables carries E to its twist over every commutative L-algebra M, not just over L: quadraticTwistVariableChange_smul base changed along L → M.

theorem WeierstrassCurve.map_quadraticTwistVariableChange_baseChange {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (E : WeierstrassCurve K) [Algebra.IsQuadraticExtension K L] [Algebra.IsSeparable K L] (M : Type u_3) [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] {σ : Gal(M/K)} (hσ : ¬∀ (x : L), σ ((algebraMap L M) x) = (algebraMap L M) x) : ((quadraticTwistVariableChange L E).baseChange M).map ↑σ = (quadraticTwistVariableChange L E).baseChange M * (E.baseChange M).negVariableChange

The twist's defining cocycle over M. Applying any σ ∈ Aut(M/K) that does not fix L pointwise multiplies the base change of quadraticTwistVariableChange on the right by the automorphism [-1] of E. This is map_quadraticTwistVariableChange base changed to M: σ restricts to the nontrivial element of Gal(L/K) precisely because it moves L, which is what AlgEquiv.restrictNormal_eq_one_iff_algebraMap records.

noncomputable def WeierstrassCurve.quadraticTwistPointEquiv {K : Type u_1} [Field K] (L : Type u_2) [Field L] [Algebra K L] (E : WeierstrassCurve K) [Algebra.IsQuadraticExtension K L] [Algebra.IsSeparable K L] (M : Type u_3) [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] [DecidableEq M] : ((E.quadraticTwist L).baseChange M).toAffine.Point ≃+ (E.baseChange M).toAffine.Point

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 the change of variables carrying E to its twist over L. It is natural in M (quadraticTwistPointEquiv_map) and anti-equivariant for the Galois elements that move L (quadraticTwistPointEquiv_map_eq_neg_map_of_not_fixed); quadraticTwistPointEquiv_map_eq_quadraticCharacter_smul_map bundles those two branches into a single statement, uniform in σ, twisted by the quadratic character of L/K.

Like the twist itself this is well defined only up to an L-automorphism of E — generically up to sign — and this definition makes one arbitrary choice, consistently across all M.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem WeierstrassCurve.quadraticTwistPointEquiv_some {K : Type u_1} [Field K] (L : Type u_2) [Field L] [Algebra K L] (E : WeierstrassCurve K) [Algebra.IsQuadraticExtension K L] [Algebra.IsSeparable K L] (M : Type u_3) [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] [DecidableEq M] {x y : M} (h : ((E.quadraticTwist L).baseChange M).toAffine.Nonsingular x y) : (quadraticTwistPointEquiv L E M) (Affine.Point.some x y h) = Affine.Point.some (↑((quadraticTwistVariableChange L E).baseChange M).u ^ 2 * x + ((quadraticTwistVariableChange L E).baseChange M).r) (↑((quadraticTwistVariableChange L E).baseChange M).u ^ 3 * y + ↑((quadraticTwistVariableChange L E).baseChange M).u ^ 2 * ((quadraticTwistVariableChange L E).baseChange M).s * x + ((quadraticTwistVariableChange L E).baseChange M).t) ⋯

What the isomorphism does to a point given by coordinates. The change of variables acting is quadraticTwistVariableChange base changed to M.

@[simp]

theorem WeierstrassCurve.quadraticTwistPointEquiv_symm_some {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (E : WeierstrassCurve K) [Algebra.IsQuadraticExtension K L] [Algebra.IsSeparable K L] (M : Type u_3) [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] [DecidableEq M] {x y : M} (h : (E.baseChange M).toAffine.Nonsingular x y) : (quadraticTwistPointEquiv L E M).symm (Affine.Point.some x y h) = Affine.Point.some (↑((quadraticTwistVariableChange L E).baseChange M)⁻¹.u ^ 2 * x + ((quadraticTwistVariableChange L E).baseChange M)⁻¹.r) (↑((quadraticTwistVariableChange L E).baseChange M)⁻¹.u ^ 3 * y + ↑((quadraticTwistVariableChange L E).baseChange M)⁻¹.u ^ 2 * ((quadraticTwistVariableChange L E).baseChange M)⁻¹.s * x + ((quadraticTwistVariableChange L E).baseChange M)⁻¹.t) ⋯

What the inverse isomorphism does to a point given by coordinates. It is the map induced by the inverse of the base-changed change of variables.

@[simp]

theorem WeierstrassCurve.quadraticTwistPointEquiv_map {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] (E : WeierstrassCurve K) [Algebra.IsQuadraticExtension K L] [Algebra.IsSeparable K L] (M : Type u_3) [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] [DecidableEq M] {N : Type u_4} [Field N] [Algebra K N] [Algebra L N] [IsScalarTower K L N] [DecidableEq N] (f : M →ₐ[L] N) (P : ((E.quadraticTwist L).baseChange M).toAffine.Point) : (quadraticTwistPointEquiv L E N) ((Affine.Point.map f) P) = (Affine.Point.map f) ((quadraticTwistPointEquiv L E M) P)

Naturality of quadraticTwistPointEquiv in M. The isomorphisms on M-points over varying M ⊇ L all come from one isomorphism of curves over L, so they commute with the maps on points induced by any L-algebra homomorphism.

@[simp]

theorem WeierstrassCurve.quadraticTwistPointEquiv_map_eq_neg_map_of_not_fixed {K : Type u_1} [Field K] (L : Type u_2) [Field L] [Algebra K L] (E : WeierstrassCurve K) [Algebra.IsQuadraticExtension K L] [Algebra.IsSeparable K L] (M : Type u_3) [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] [DecidableEq M] {σ : Gal(M/K)} (hσ : ¬∀ (x : L), σ ((algebraMap L M) x) = (algebraMap L M) x) (P : ((E.quadraticTwist L).baseChange M).toAffine.Point) : (quadraticTwistPointEquiv L E M) ((Affine.Point.map ↑σ) P) = -(Affine.Point.map ↑σ) ((quadraticTwistPointEquiv L E M) P)

Anti-equivariance: if σ ∈ Aut(M/K) does not fix L pointwise, transporting its action through Eᴸ(M) ≅ E(M) gives minus its action.

theorem WeierstrassCurve.quadraticTwistPointEquiv_map_eq_quadraticCharacter_smul_map {K : Type u_1} [Field K] (L : Type u_2) [Field L] [Algebra K L] (E : WeierstrassCurve K) [Algebra.IsQuadraticExtension K L] [Algebra.IsSeparable K L] (M : Type u_3) [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] [DecidableEq M] (σ : Gal(M/K)) (P : ((E.quadraticTwist L).baseChange M).toAffine.Point) : (quadraticTwistPointEquiv L E M) ((Affine.Point.map ↑σ) P) = ↑((Algebra.IsQuadraticExtension.quadraticCharacter K L) (σ.restrictNormal L)) • (Affine.Point.map ↑σ) ((quadraticTwistPointEquiv L E M) P)

Galois equivariance of the point isomorphism, twisted by the quadratic character. For every σ ∈ Aut(M/K), transporting the action of σ through Eᴸ(M) ≅ E(M) multiplies it by χ(σ|_L) = ±1, the quadratic character of L/K. This is the uniform statement that quadraticTwistPointEquiv_map (the σ|_L = 1 branch, where the isomorphism is L-linear) and quadraticTwistPointEquiv_map_eq_neg_map_of_not_fixed (the moved branch, where it is anti-equivariant) together assert: the isomorphism is defined over L, not over K, and the character measures exactly that failure.