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

11 declarations, 0 contain sorry, 0 declared as axioms

Multiplicative reduction becomes split after a quadratic twist

Let R be a discrete valuation ring with fraction field K (for example the ring of integers of a nonarchimedean local field), and let E be an elliptic curve over K with multiplicative reduction. This file proves that if the reduction is nonsplit, then the quadratic twist of E (FLT.KnownIn1980s.EllipticCurves.QuadraticTwists.QuadraticTwists) by the unramified quadratic extension of K (FLT.Mathlib.RingTheory.Unramified.LocalRing) has split multiplicative reduction: the reduction of the twist is the same nodal cubic with the Galois action on the two tangent directions at the node twisted into triviality.

Main definitions and statements

WeierstrassCurve.exists_quadraticTwist_hasSplitMultiplicativeReduction : over the fraction field of a discrete valuation ring, an elliptic curve with nonsplit multiplicative reduction has a quadratic twist with split multiplicative reduction.

The generic ingredients — the node polynomial WeierstrassCurve.nodePoly with its splitting criteria, and the invariance of split multiplicative reduction under isomorphism of minimal models (WeierstrassCurve.HasSplitMultiplicativeReduction.of_isMinimal_smul) — are in FLT.Mathlib.AlgebraicGeometry.EllipticCurve.Reduction and FLT.Mathlib.Algebra.QuadraticDiscriminant.

TODO

Behaviour of reduction types under twisting in general: over the fraction field of a DVR, an unramified quadratic twist preserves good and multiplicative reduction (exchanging split and nonsplit), while a ramified quadratic twist of a curve with good or multiplicative reduction has additive reduction (at least in residue characteristic ≠ 2).
Compatibility with the Tate curve (FLT.KnownIn1980s.EllipticCurves.TateCurve): for E with nonsplit multiplicative reduction over a nonarchimedean local field, the Galois representation of E is the unramified quadratic twist of the Tate-curve representation of its split twist. This is the main FLT-facing application of this file together with exists_quadraticTwist_hasSplitMultiplicativeReduction.

References

[J. Silverman, The Arithmetic of Elliptic Curves][silverman2009], VII.§1 and VII.§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 (9)

Imported by 1 file

FLT.lean

lemma WeierstrassCurve.nodePoly_quadraticTwistOf_map_splits_iff Twisting flips the square class (residue characteristic ≠ 2) line 84 source
Source documentation
Twisting flips the square class (residue characteristic ≠ 2). Combining the split criterion nodePoly_map_splits_iff_isSquare with the coefficient scaling of the quadratic twist (c₄_quadraticTwistOf, c₆_quadraticTwistOf), the node polynomial of W.quadraticTwistOf t n splits over a field k of characteristic ≠ 2 exactly when D · (-c₄ c₆) is a square there, where D = t² - 4n. Thus twisting multiplies the square class governing splitting by D: it converts a nonsplit reduction into a split one precisely when D and -c₄ c₆ lie in the same square class.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Field, NeZero, OfNat.ofNat, Nat, RingHom, WeierstrassCurve, Ne, WeierstrassCurve.c₄, HSub.hSub, HPow.hPow, HMul.hMul, Iff, Polynomial.Splits, Polynomial.map, WeierstrassCurve.nodePoly, WeierstrassCurve.quadraticTwistOf, IsSquare, Neg.neg, WeierstrassCurve.c₆
Proof uses: Iff.intro, Eq, Exists.intro, HDiv.hDiv, Eq.mpr, inferInstance, CommGroupWithZero, GroupWithZero, id, Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq, Mathlib.Tactic.FieldSimp.NF.eval, Mathlib.Tactic.FieldSimp.NF.cons, Prod.mk, Int, List.nil, Prod, Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul, rfl, Eq.trans, Eq.refl and 99 more
127 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma nodePoly_quadraticTwistOf_map_splits_iff {A : Type*} [CommRing A] {k : Type*} [Field k]
    [NeZero (2 : k)] (φ : A →+* k) (W : WeierstrassCurve A) (t n : A) (hc₄ : φ W.c₄ ≠ 0)
    (hD : φ (t ^ 2 - 4 * n) ≠ 0) :
    ((W.quadraticTwistOf t n).nodePoly.map φ).Splits
      ↔ IsSquare (φ ((t ^ 2 - 4 * n) * -(W.c₄ * W.c₆))) := by
…
```
theorem WeierstrassCurve.baseChange_integralModel_quadraticTwistOf Documented declaration: baseChange_integralModel_quadraticTwistOf line 105 source
Source documentation
The R-model twist base-changes to the twist over K: for E integral over R, twisting its integral model by t, n : R and base-changing to K equals twisting E by the images (algebraMap R K t, algebraMap R K n). Together with the coefficient laws this is the bridge from the K-twist E.quadraticTwist L to a genuine R-model whose reduction can be computed.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, CommRing, Algebra, WeierstrassCurve.IsIntegral, Eq, WeierstrassCurve.baseChange, WeierstrassCurve.quadraticTwistOf, WeierstrassCurve.integralModel, RingHom, Algebra.algebraMap
Proof uses: id, Eq.mpr, WeierstrassCurve.map, congrArg, WeierstrassCurve.quadraticTwistOf_map, WeierstrassCurve.baseChange_integralModel_eq, Eq.refl
16 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem baseChange_integralModel_quadraticTwistOf [IsIntegral R E] (t n : R) :
    ((E.integralModel R).quadraticTwistOf t n)⁄K
      = E.quadraticTwistOf (algebraMap R K t) (algebraMap R K n) := by
…
```
Mentions: WeierstrassCurve.quadraticTwistOf
theorem WeierstrassCurve.Δ_baseChange_quadraticTwistOf_ne_zero The base change of the twisted integral model has nonzero discriminant: its Δ is (t'² - 4n')⁶ · Δ (Δ_quadraticTwistOf), and both factors are nonzero line 118 source
Source documentation
The base change of the twisted integral model has nonzero discriminant: its Δ is (t'² - 4n')⁶ · Δ (Δ_quadraticTwistOf), and both factors are nonzero.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, CommRing, Algebra, IsFractionRing, IsDomain, WeierstrassCurve.IsElliptic, WeierstrassCurve.IsIntegral, Ne, HSub.hSub, HPow.hPow, Nat, OfNat.ofNat, HMul.hMul, WeierstrassCurve.Δ, WeierstrassCurve.baseChange, WeierstrassCurve.quadraticTwistOf, WeierstrassCurve.integralModel
Proof uses: Eq, IsUnit.ne_zero, WeierstrassCurve.isUnit_Δ, Eq.mpr, RingHom, Algebra.algebraMap, id, congrArg, Eq.symm, WeierstrassCurve.integralModel_Δ_eq, map_zero, Eq.refl, WeierstrassCurve.map_Δ, WeierstrassCurve.Δ_quadraticTwistOf, Not, Ne.eq_1, propext, map_eq_zero_iff, IsFractionRing.injective, Or and 6 more
69 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem Δ_baseChange_quadraticTwistOf_ne_zero [E.IsElliptic] [IsIntegral R E] (t' n' : R)
    (hD : t' ^ 2 - 4 * n' ≠ 0) :
    ((((E.integralModel R).quadraticTwistOf t' n'))⁄K).Δ ≠ 0 := by
…
```
Mentions: WeierstrassCurve.quadraticTwistOf
theorem WeierstrassCurve.hasMultiplicativeReduction_baseChange_quadraticTwistOf The twist by a unit discriminant keeps multiplicative reduction line 137 source
Source documentation
The twist by a unit discriminant keeps multiplicative reduction. If E has multiplicative reduction and D = t² - 4n is a unit of R (residue ≠ 0), then the base change of the R-model twist (E.integralModel R).quadraticTwistOf t n again has multiplicative reduction: its c₄ = D² · c₄ is a unit (so the model is minimal and the reduction multiplicative) and its Δ = D⁶ · Δ still has positive valuation.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, CommRing, Algebra, IsFractionRing, IsDomain, IsDiscreteValuationRing, WeierstrassCurve.HasMultiplicativeReduction, Ne, IsLocalRing.ResidueField, RingHom, IsLocalRing.residue, HSub.hSub, HPow.hPow, Nat, OfNat.ofNat, HMul.hMul, WeierstrassCurve.baseChange, WeierstrassCurve.quadraticTwistOf, WeierstrassCurve.integralModel
Proof uses: Eq.mpr, id, Eq, congrArg, rfl, WeierstrassCurve.IsIntegral, WeierstrassCurve.IsIntegral.mk, Exists.intro, WeierstrassCurve.c₄, WeierstrassCurve.c₄_quadraticTwistOf, map_mul, map_pow, mul_ne_zero, pow_ne_zero, WeierstrassCurve.residue_integralModel_c₄_ne_zero, WeierstrassCurve.Δ, WeierstrassCurve.Δ_quadraticTwistOf, WeierstrassCurve.residue_integralModel_Δ_eq_zero, MulZeroClass.mul_zero, Eq.refl and 23 more
112 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
theorem hasMultiplicativeReduction_baseChange_quadraticTwistOf [E.HasMultiplicativeReduction R]
    (t n : R) (hD : residue R (t ^ 2 - 4 * n) ≠ 0) :
    (((E.integralModel R).quadraticTwistOf t n)⁄K).HasMultiplicativeReduction R := by
…
```
Mentions: WeierstrassCurve.quadraticTwistOf
theorem WeierstrassCurve.notMem_range_algebraMap_of_residue_notMem Documented declaration: notMem_range_algebraMap_of_residue_notMem line 164 source
Source documentation
If the residue of an integral element θ of S does not come from the residue field of R, then θ does not come from K either: an element of K integral over the integrally closed R lies in R, and residues are compatible.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsFractionRing, IsDomain, IsDiscreteValuationRing, IsLocalRing, Algebra.IsIntegral, IsLocalHom, RingHom, Algebra.algebraMap, IsScalarTower, Not, Membership.mem, IsLocalRing.ResidueField, Set, Set.range, IsLocalRing.residue
Proof uses: Eq, False, IsIntegral, IsIntegral.map, AlgHom, IsScalarTower.toAlgHom, Algebra.IsIntegral.isIntegral, Iff.mp, isIntegral_algHom_iff, FaithfulSMul.algebraMap_injective, Eq.mp, congrArg, Eq.symm, Exists, IsIntegrallyClosed.isIntegral_iff, Exists.intro, Eq.mpr, id, of_eq_true, eq_self and 8 more
52 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
theorem notMem_range_algebraMap_of_residue_notMem {S : Type u} [CommRing S] [IsLocalRing S]
    [Algebra R S] [Algebra.IsIntegral R S] [IsLocalHom (algebraMap R S)] {L : Type u} [Field L]
    [Algebra K L] [Algebra R L] [Algebra S L] [IsScalarTower R S L] [IsScalarTower R K L]
    [IsFractionRing S L] {θ : S}
    (hθ : residue S θ ∉ Set.range (algebraMap (ResidueField R) (ResidueField S))) :
    algebraMap S L θ ∉ Set.range (algebraMap K L) := by
…
```
theorem WeierstrassCurve.nodePoly_map_root_relations Documented declaration: nodePoly_map_root_relations line 191 source
Source documentation
If the root of the reduced node polynomial P̄ (assumed irreducible) satisfies a monic quadratic relation X² - t·X + n over the residue field, then comparing with the defining relation of P̄ (aeval_root_nodePoly_map) and using the linear independence of 1 and the root (AdjoinRoot.eq_zero_of_mul_root_add_eq_zero) yields the relations φc₄·t + φ(a₁c₄) = 0 and φc₄·n + φκ = 0 (φ = residue, κ = 54b₆ - 3b₂b₄ + a₂c₄).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, CommRing, Algebra, IsFractionRing, IsDomain, IsDiscreteValuationRing, WeierstrassCurve.HasMultiplicativeReduction, Irreducible, Polynomial, IsLocalRing.ResidueField, Polynomial.map, Algebra.algebraMap, WeierstrassCurve.nodePoly, WeierstrassCurve.integralModel, Eq, AdjoinRoot, HAdd.hAdd, HSub.hSub, HPow.hPow and 13 more
Proof uses: rfl, Fact, Fact.mk, Eq.mp, congrArg, Polynomial.natDegree, WeierstrassCurve.natDegree_nodePoly_map, WeierstrassCurve.aeval_root_nodePoly_map, Neg.neg, AdjoinRoot.eq_zero_of_mul_root_add_eq_zero, Eq.ge, Eq.mpr, id, congrFun', congr, Eq.trans, map_mul, map_add, map_neg, Mathlib.Tactic.LinearCombination.eq_of_eq and 59 more
116 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
theorem nodePoly_map_root_relations [E.HasMultiplicativeReduction R]
    (hirr : Irreducible ((E.integralModel R).nodePoly.map (algebraMap R (ResidueField R))))
    {t n : ResidueField R}
    (hρ : AdjoinRoot.root ((E.integralModel R).nodePoly.map (algebraMap R (ResidueField R))) ^ 2
        - algebraMap (ResidueField R)
            (AdjoinRoot ((E.integralModel R).nodePoly.map (algebraMap R (ResidueField R)))) t
          * AdjoinRoot.root ((E.integralModel R).nodePoly.map (algebraMap R (ResidueField R)))
        + algebraMap (ResidueField R)
            (AdjoinRoot ((E.integralModel R).nodePoly.map (algebraMap R (ResidueField R)))) n
        = 0) :
    residue R (E.integralModel R).c₄ * t
        + residue R ((E.integralModel R).a₁ * (E.integralModel R).c₄) = 0
…
```
theorem WeierstrassCurve.residue_c₄_mul_residue_eq_neg_c₆ Documented declaration: residue_c₄_mul_residue_eq_neg_c₆ line 237 source
Source documentation
The key identity φc₄ · φ(t'² - 4n') = -φc₆ of the twisting datum (t', n'): if its residues satisfy the trace and norm relations cut out by the node polynomial (κ = 54 b₆ - 3 b₂ b₄ + a₂ c₄), then the discriminant identity splitPolynomial_discrim turns them into this identity.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, CommRing, Algebra, IsFractionRing, IsDomain, IsDiscreteValuationRing, WeierstrassCurve.HasMultiplicativeReduction, Eq, IsLocalRing.ResidueField, HAdd.hAdd, HMul.hMul, RingHom, IsLocalRing.residue, WeierstrassCurve.c₄, WeierstrassCurve.integralModel, WeierstrassCurve.a₁, OfNat.ofNat, HSub.hSub, Nat and 7 more
Proof uses: Eq.mpr, id, congrArg, rfl, WeierstrassCurve.splitPolynomial_discrim, mul_left_cancel₀, WeierstrassCurve.residue_integralModel_c₄_ne_zero, congrFun', Eq.trans, map_sub, congr, map_pow, map_mul, map_ofNat, Mathlib.Tactic.LinearCombination.eq_of_eq, Mathlib.Tactic.LinearCombination.add_eq_eq, Eq.mp, map_add, map_neg, Mathlib.Tactic.LinearCombination.mul_const_eq and 57 more
115 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
theorem residue_c₄_mul_residue_eq_neg_c₆ [E.HasMultiplicativeReduction R] (t' n' : R)
    (hA : residue R (E.integralModel R).c₄ * residue R t'
      + residue R ((E.integralModel R).a₁ * (E.integralModel R).c₄) = 0)
    (hB : residue R (E.integralModel R).c₄ * residue R n'
      + residue R (54 * (E.integralModel R).b₆
        - 3 * (E.integralModel R).b₂ * (E.integralModel R).b₄
        + (E.integralModel R).a₂ * (E.integralModel R).c₄) = 0) :
    residue R (E.integralModel R).c₄ * residue R (t' ^ 2 - 4 * n')
      = -residue R (E.integralModel R).c₆ := by
…
```
theorem WeierstrassCurve.nodePoly_quadraticTwistOf_map_splits_of_residue_of_two_eq_zero Documented declaration: nodePoly_quadraticTwistOf_map_splits_of_residue_of_two_eq_zero line 268 source
Source documentation
The residue characteristic 2 case of nodePoly_quadraticTwistOf_map_splits_of_residue: the Artin–Schreier split condition (nodePoly_map_splits_iff_of_two_eq_zero) holds with z = 0, because φ κ_W = 0. Indeed κ_W = D³κ - D²·n·a₁²·c₄ (kappa_quadraticTwistOf), and φκ = -φc₄·φn (hB), φa₁ = -φt' (hA), φD = φt'² (as 4 = 0), so φκ_W = -φD²·φc₄·φn·(φD + φa₁²) = -φD²·φc₄·φn·(2·φt'²) = 0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, CommRing, Algebra, IsFractionRing, IsDomain, IsDiscreteValuationRing, WeierstrassCurve.HasMultiplicativeReduction, Eq, IsLocalRing.ResidueField, OfNat.ofNat, Nat, HAdd.hAdd, HMul.hMul, RingHom, IsLocalRing.residue, WeierstrassCurve.c₄, WeierstrassCurve.integralModel, WeierstrassCurve.a₁, HSub.hSub and 9 more
Proof uses: HPow.hPow, Neg.neg, WeierstrassCurve.c₆, WeierstrassCurve.residue_c₄_mul_residue_eq_neg_c₆, Ne, WeierstrassCurve.residue_integralModel_c₆_ne_zero, Iff.mp, neg_eq_zero, Eq.mpr, id, congrArg, Eq.symm, MulZeroClass.mul_zero, Eq.refl, rfl, WeierstrassCurve.residue_integralModel_c₄_ne_zero, IsLocalRing.ResidueField.algebraMap_eq, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.instAtLeastTwo and 88 more
107 instances, coercions and auxiliary constants left out.

Tactic trace: 46 steps
Open to load the checked before-and-after goal states.
```
theorem nodePoly_quadraticTwistOf_map_splits_of_residue_of_two_eq_zero
    [E.HasMultiplicativeReduction R] (t' n' : R) (h2 : (2 : ResidueField R) = 0)
    (hA : residue R (E.integralModel R).c₄ * residue R t'
      + residue R ((E.integralModel R).a₁ * (E.integralModel R).c₄) = 0)
    (hB : residue R (E.integralModel R).c₄ * residue R n'
      + residue R (54 * (E.integralModel R).b₆
        - 3 * (E.integralModel R).b₂ * (E.integralModel R).b₄
        + (E.integralModel R).a₂ * (E.integralModel R).c₄) = 0) :
    Polynomial.Splits (((E.integralModel R).quadraticTwistOf t' n').nodePoly.map
      (algebraMap R (ResidueField R))) := by
…
```
Mentions: WeierstrassCurve.quadraticTwistOf
theorem WeierstrassCurve.nodePoly_quadraticTwistOf_map_splits_of_residue Documented declaration: nodePoly_quadraticTwistOf_map_splits_of_residue line 339 source
Source documentation
If the residues of (t', n') satisfy the trace and norm relations cut out by the node polynomial, then the node polynomial of the quadratic twist of the integral model by (t', n') splits over the residue field: the key identity φc₄ · φ(t'² - 4n') = -φc₆ (residue_c₄_mul_residue_eq_neg_c₆) reduces this to a square-class computation for residue characteristic ≠ 2, and to an Artin–Schreier computation for residue characteristic 2 (nodePoly_quadraticTwistOf_map_splits_of_residue_of_two_eq_zero).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, CommRing, Algebra, IsFractionRing, IsDomain, IsDiscreteValuationRing, WeierstrassCurve.HasMultiplicativeReduction, Eq, IsLocalRing.ResidueField, HAdd.hAdd, HMul.hMul, RingHom, IsLocalRing.residue, WeierstrassCurve.c₄, WeierstrassCurve.integralModel, WeierstrassCurve.a₁, OfNat.ofNat, HSub.hSub, Nat and 9 more
Proof uses: Ne, Or, ne_or_eq, HPow.hPow, Neg.neg, WeierstrassCurve.c₆, WeierstrassCurve.residue_c₄_mul_residue_eq_neg_c₆, WeierstrassCurve.residue_integralModel_c₆_ne_zero, Iff.mp, neg_eq_zero, Eq.mpr, id, congrArg, Eq.symm, MulZeroClass.mul_zero, Eq.refl, WeierstrassCurve.residue_integralModel_c₄_ne_zero, NeZero, NeZero.mk, IsSquare and 59 more
101 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
theorem nodePoly_quadraticTwistOf_map_splits_of_residue
    [E.HasMultiplicativeReduction R] (t' n' : R)
    (hA : residue R (E.integralModel R).c₄ * residue R t'
      + residue R ((E.integralModel R).a₁ * (E.integralModel R).c₄) = 0)
    (hB : residue R (E.integralModel R).c₄ * residue R n'
      + residue R (54 * (E.integralModel R).b₆
        - 3 * (E.integralModel R).b₂ * (E.integralModel R).b₄
        + (E.integralModel R).a₂ * (E.integralModel R).c₄) = 0) :
    Polynomial.Splits (((E.integralModel R).quadraticTwistOf t' n').nodePoly.map
      (algebraMap R (ResidueField R))) := by
…
```
Mentions: WeierstrassCurve.quadraticTwistOf
theorem WeierstrassCurve.hasSplitMultiplicativeReduction_quadraticTwistOf_of_residue Documented declaration: hasSplitMultiplicativeReduction_quadraticTwistOf_of_residue line 372 source
Source documentation
Packaging nodePoly_quadraticTwistOf_map_splits_of_residue: if the base change of the twisted integral model has multiplicative reduction and the residues of (t', n') satisfy the trace and norm relations, then the reduction is split multiplicative.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, CommRing, Algebra, IsFractionRing, IsDomain, IsDiscreteValuationRing, WeierstrassCurve.HasMultiplicativeReduction, WeierstrassCurve.baseChange, WeierstrassCurve.quadraticTwistOf, WeierstrassCurve.integralModel, Eq, IsLocalRing.ResidueField, HAdd.hAdd, HMul.hMul, RingHom, IsLocalRing.residue, WeierstrassCurve.c₄, WeierstrassCurve.a₁, OfNat.ofNat and 7 more
Proof uses: WeierstrassCurve.HasSplitMultiplicativeReduction.mk, Eq.mpr, Polynomial.Splits, Polynomial.map, Algebra.algebraMap, Polynomial, Polynomial.C, HPow.hPow, Polynomial.X, id, congrArg, WeierstrassCurve.integralModel_baseChange, WeierstrassCurve.nodePoly_quadraticTwistOf_map_splits_of_residue
74 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem hasSplitMultiplicativeReduction_quadraticTwistOf_of_residue
    [E.HasMultiplicativeReduction R] (t' n' : R)
    [hW : (((E.integralModel R).quadraticTwistOf t' n')⁄K).HasMultiplicativeReduction R]
    (hA : residue R (E.integralModel R).c₄ * residue R t'
      + residue R ((E.integralModel R).a₁ * (E.integralModel R).c₄) = 0)
    (hB : residue R (E.integralModel R).c₄ * residue R n'
      + residue R (54 * (E.integralModel R).b₆
        - 3 * (E.integralModel R).b₂ * (E.integralModel R).b₄
        + (E.integralModel R).a₂ * (E.integralModel R).c₄) = 0) :
    (((E.integralModel R).quadraticTwistOf t' n')⁄K).HasSplitMultiplicativeReduction R := by
…
```
Mentions: WeierstrassCurve.quadraticTwistOf
theorem WeierstrassCurve.exists_quadraticTwist_hasSplitMultiplicativeReduction Documented declaration: exists_quadraticTwist_hasSplitMultiplicativeReduction line 404 source
Source documentation
If E has multiplicative reduction which is not split, then E has a quadratic twist with split multiplicative reduction — namely the twist by the unramified quadratic extension of K: the reduction of the twist is the same nodal cubic with the Galois action on the two tangent directions at the node twisted into triviality.
Mathlib's reduction-type predicates apply to a specific Weierstrass equation and require it to be minimal, while our chosen model E.quadraticTwist L of the twist need not be; so the conclusion is phrased via the minimal model (E.quadraticTwist L).minimal R. (Being split multiplicative is intrinsic, so any other minimal model would do.)
The nonsplitness hypothesis h cannot be dropped: if E already has split multiplicative reduction then no quadratic twist of E has split multiplicative reduction, since the unramified quadratic twist has nonsplit multiplicative reduction and ramified quadratic twists have additive reduction.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, CommRing, Algebra, IsFractionRing, IsDomain, IsDiscreteValuationRing, WeierstrassCurve.IsElliptic, WeierstrassCurve.HasMultiplicativeReduction, Not, WeierstrassCurve.HasSplitMultiplicativeReduction, Exists, Algebra.IsQuadraticExtension, Algebra.IsSeparable, WeierstrassCurve.minimal, WeierstrassCurve.quadraticTwist
Proof uses: Polynomial, IsLocalRing.ResidueField, Polynomial.map, Algebra.algebraMap, WeierstrassCurve.nodePoly, WeierstrassCurve.integralModel, Eq, rfl, Irreducible, WeierstrassCurve.irreducible_nodePoly_map, Fact, Fact.mk, Nat, Polynomial.natDegree, OfNat.ofNat, WeierstrassCurve.natDegree_nodePoly_map, Module.finrank, AdjoinRoot, Eq.trans, AdjoinRoot.finrank_eq_natDegree and 93 more
123 instances, coercions and auxiliary constants left out.

Tactic trace: 41 steps
Open to load the checked before-and-after goal states.
```
theorem exists_quadraticTwist_hasSplitMultiplicativeReduction [E.HasMultiplicativeReduction R]
    (h : ¬E.HasSplitMultiplicativeReduction R) :
    ∃ (L : Type u) (_ : Field L) (_ : Algebra K L) (_ : Algebra.IsQuadraticExtension K L)
      (_ : Algebra.IsSeparable K L),
      ((E.quadraticTwist L).minimal R).HasSplitMultiplicativeReduction R := by
…
```