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

25 declarations, 0 contain sorry, 0 declared as axioms

Complements on reduction of elliptic curves

Material for Mathlib.AlgebraicGeometry.EllipticCurve.Reduction: the node polynomial and its splitting criteria (answering the discriminant-characterization TODO there), a minimality criterion via c₄, and uniqueness of minimal models (Silverman VII.1.3(b)): split multiplicative reduction is an isomorphism invariant of minimal models.

Imports (5)

Imported by 3 files

def WeierstrassCurve.nodePoly Documented declaration: nodePoly line 39 source
Source documentation
The node polynomial c₄ T² + a₁ c₄ T - (54 b₆ - 3 b₂ b₄ + a₂ c₄), whose roots are the slopes of the two tangent directions at the node of a multiplicative reduction; its splitting over the residue field governs whether the reduction is split (see HasSplitMultiplicativeReduction).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, WeierstrassCurve, Polynomial
Proof uses: HSub.hSub, HAdd.hAdd, HMul.hMul, RingHom, Polynomial.C, WeierstrassCurve.c₄, HPow.hPow, Nat, Polynomial.X, OfNat.ofNat, WeierstrassCurve.a₁, WeierstrassCurve.b₆, WeierstrassCurve.b₂, WeierstrassCurve.b₄, WeierstrassCurve.a₂
32 instances, coercions and auxiliary constants left out.
```
noncomputable def nodePoly {A : Type*} [CommRing A] (W : WeierstrassCurve A) : Polynomial A :=
…
```
lemma WeierstrassCurve.nodePoly_map The node polynomial base-changed along a ring homomorphism line 43 source
Source documentation
The node polynomial base-changed along a ring homomorphism.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, RingHom, WeierstrassCurve, Eq, Polynomial, Polynomial.map, WeierstrassCurve.nodePoly, HSub.hSub, HAdd.hAdd, HMul.hMul, Polynomial.C, WeierstrassCurve.c₄, HPow.hPow, Nat, Polynomial.X, OfNat.ofNat, WeierstrassCurve.a₁, WeierstrassCurve.b₆, WeierstrassCurve.b₂, WeierstrassCurve.b₄ and 1 more
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Polynomial.map_sub, congr, Polynomial.map_add, Polynomial.map_mul, Polynomial.map_C, Polynomial.map_pow, Polynomial.map_X, eq_self
63 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma nodePoly_map {A : Type*} [CommRing A] {B : Type*} [CommRing B] (φ : A →+* B)
    (W : WeierstrassCurve A) :
    W.nodePoly.map φ = .C (φ W.c₄) * .X ^ 2 + .C (φ (W.a₁ * W.c₄)) * .X
      - .C (φ (54 * W.b₆ - 3 * W.b₂ * W.b₄ + W.a₂ * W.c₄)) := by
…
```
lemma WeierstrassCurve.map_nodePoly Documented declaration: map_nodePoly line 53 source
Source documentation
The node polynomial is natural in the coefficient ring: it commutes with base change of the Weierstrass equation along any ring homomorphism, since every coefficient is a polynomial in the aᵢ and Polynomial.map is a ring homomorphism on each.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, RingHom, WeierstrassCurve, Eq, Polynomial, WeierstrassCurve.nodePoly, WeierstrassCurve.map, Polynomial.map
Proof uses: of_eq_true, Eq.trans, HSub.hSub, HAdd.hAdd, HMul.hMul, Polynomial.C, WeierstrassCurve.c₄, HPow.hPow, Nat, Polynomial.X, OfNat.ofNat, WeierstrassCurve.a₁, WeierstrassCurve.b₆, WeierstrassCurve.b₂, WeierstrassCurve.b₄, WeierstrassCurve.a₂, True, congr, congrArg, congrFun' and 18 more
51 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma map_nodePoly {A : Type*} [CommRing A] {B : Type*} [CommRing B] (φ : A →+* B)
    (W : WeierstrassCurve A) :
    (W.map φ).nodePoly = W.nodePoly.map φ := by
…
```
Mentions: WeierstrassCurve.nodePoly
lemma WeierstrassCurve.aeval_root_nodePoly_map The root of the (base-changed) node polynomial satisfies its defining quadratic relation line 62 source
Source documentation
The root of the (base-changed) node polynomial satisfies its defining quadratic relation.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, RingHom, WeierstrassCurve, Eq, AdjoinRoot, Polynomial.map, WeierstrassCurve.nodePoly, HSub.hSub, HAdd.hAdd, HMul.hMul, Algebra.algebraMap, WeierstrassCurve.c₄, HPow.hPow, Nat, AdjoinRoot.root, OfNat.ofNat, WeierstrassCurve.a₁, WeierstrassCurve.b₆, WeierstrassCurve.b₂, WeierstrassCurve.b₄ and 1 more
Proof uses: AlgHom, Polynomial, Polynomial.aeval, Polynomial.C, Polynomial.X, congrArg, WeierstrassCurve.nodePoly_map, Eq.mpr, id, congrFun', congr, Eq.trans, map_mul, map_add, map_sub, Eq.mp, outParam, MonoidHom, MonoidHom.id, RingHom.id and 7 more
112 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma aeval_root_nodePoly_map {A : Type*} [CommRing A] {B : Type*} [CommRing B] (φ : A →+* B)
    (W : WeierstrassCurve A) :
    algebraMap B (AdjoinRoot (W.nodePoly.map φ)) (φ W.c₄) * AdjoinRoot.root (W.nodePoly.map φ) ^ 2
      + algebraMap B (AdjoinRoot (W.nodePoly.map φ)) (φ (W.a₁ * W.c₄))
        * AdjoinRoot.root (W.nodePoly.map φ)
      - algebraMap B (AdjoinRoot (W.nodePoly.map φ))
        (φ (54 * W.b₆ - 3 * W.b₂ * W.b₄ + W.a₂ * W.c₄)) = 0 := by
…
```
lemma WeierstrassCurve.nodePoly_map_eq_quadratic The reduced node polynomial, presented as a quadratic with an additive constant term — the form consumed by the quadratic separability and splitting criteria line 76 source
Source documentation
The reduced node polynomial, presented as a quadratic with an additive constant term — the form consumed by the quadratic separability and splitting criteria.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, RingHom, WeierstrassCurve, Eq, Polynomial, Polynomial.map, WeierstrassCurve.nodePoly, HAdd.hAdd, HMul.hMul, Polynomial.C, WeierstrassCurve.c₄, HPow.hPow, Nat, Polynomial.X, OfNat.ofNat, WeierstrassCurve.a₁, Neg.neg, HSub.hSub, WeierstrassCurve.b₆, WeierstrassCurve.b₂ and 2 more
Proof uses: Eq.mpr, id, congrArg, WeierstrassCurve.nodePoly_map, map_neg, sub_eq_add_neg, Eq.refl
80 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma nodePoly_map_eq_quadratic {A : Type*} [CommRing A] {B : Type*} [CommRing B] (φ : A →+* B)
    (W : WeierstrassCurve A) :
    W.nodePoly.map φ = .C (φ W.c₄) * .X ^ 2 + .C (φ (W.a₁ * W.c₄)) * .X
      + .C (-φ (54 * W.b₆ - 3 * W.b₂ * W.b₄ + W.a₂ * W.c₄)) := by
…
```
lemma WeierstrassCurve.map_splitPolynomial_discrim The image of the discriminant identity splitPolynomial_discrim under a ring homomorphism, in the shape produced by the quadratic criteria applied to nodePoly_map_eq_quadratic line 84 source
Source documentation
The image of the discriminant identity splitPolynomial_discrim under a ring homomorphism, in the shape produced by the quadratic criteria applied to nodePoly_map_eq_quadratic.

standard axioms: Quot.sound, propext what this means
Statement uses: CommRing, RingHom, WeierstrassCurve, Eq, HSub.hSub, HPow.hPow, Nat, HMul.hMul, WeierstrassCurve.a₁, WeierstrassCurve.c₄, OfNat.ofNat, Neg.neg, HAdd.hAdd, WeierstrassCurve.b₆, WeierstrassCurve.b₂, WeierstrassCurve.b₄, WeierstrassCurve.a₂, WeierstrassCurve.c₆
Proof uses: Eq.mpr, id, congrArg, mul_neg, sub_neg_eq_add, Eq.symm, map_pow, map_ofNat, map_mul, map_add, WeierstrassCurve.splitPolynomial_discrim
89 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma map_splitPolynomial_discrim {A : Type*} [CommRing A] {B : Type*} [CommRing B] (φ : A →+* B)
    (W : WeierstrassCurve A) :
    φ (W.a₁ * W.c₄) ^ 2 - 4 * φ W.c₄ * (-φ (54 * W.b₆ - 3 * W.b₂ * W.b₄ + W.a₂ * W.c₄))
      = φ (-(W.c₄ * W.c₆)) := by
…
```
lemma WeierstrassCurve.nodePoly_smul Documented declaration: nodePoly_smul line 94 source
Source documentation
Under a change of variables C = (u, r, s, t), the node polynomial transforms by the affine substitution T ↦ u T + s and the unit scalar u⁻⁶ — reflecting that the tangent slopes λ transform as λ ↦ (λ - s)/u. In particular its splitting field is unchanged.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, WeierstrassCurve, WeierstrassCurve.VariableChange, Eq, Polynomial, WeierstrassCurve.nodePoly, HSMul.hSMul, HMul.hMul, RingHom, Polynomial.C, HPow.hPow, Nat, Inv.inv, Units, WeierstrassCurve.VariableChange.u, OfNat.ofNat, Polynomial.comp, HAdd.hAdd, Polynomial.X, WeierstrassCurve.VariableChange.s
Proof uses: congrArg, Eq.mpr, Int, Neg.neg, id, congr, Eq.trans, congrFun', Int.neg_mul, one_mul, of_eq_true, inferInstance, Ring, True, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Mathlib.Tactic.Ring.Common.neg_congr, Mathlib.Tactic.Ring.cast_pos and 85 more
138 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
lemma nodePoly_smul {A : Type*} [CommRing A] (W : WeierstrassCurve A) (C : VariableChange A) :
    (C • W).nodePoly = .C ((↑C.u⁻¹ : A) ^ 6)
      * W.nodePoly.comp (.C (↑C.u : A) * .X + .C C.s) := by
…
```
Mentions: WeierstrassCurve.nodePoly
lemma WeierstrassCurve.nodePoly_map_splits_smul_iff Invariance of the node polynomial's splitting under change of variables line 127 source
Source documentation
Invariance of the node polynomial's splitting under change of variables. Since a change of variables transforms the node polynomial by an affine substitution and a nonzero scalar (nodePoly_smul), whether it splits over a field k is unchanged. This is what makes split multiplicative reduction an isomorphism invariant.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Field, RingHom, WeierstrassCurve, WeierstrassCurve.VariableChange, Iff, Polynomial.Splits, Polynomial.map, WeierstrassCurve.nodePoly, HSMul.hSMul
Proof uses: Ne, WeierstrassCurve.VariableChange.u, OfNat.ofNat, IsUnit.ne_zero, RingHom.isUnit_map, Units.isUnit, HPow.hPow, Nat, Inv.inv, Units, Eq.mpr, id, Eq, congrArg, map_pow, pow_ne_zero, HMul.hMul, Polynomial, Polynomial.C, Polynomial.comp and 17 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma nodePoly_map_splits_smul_iff {A : Type*} [CommRing A] {k : Type*} [Field k] (φ : A →+* k)
    (W : WeierstrassCurve A) (C : VariableChange A) :
    ((C • W).nodePoly.map φ).Splits ↔ (W.nodePoly.map φ).Splits := by
…
```
lemma WeierstrassCurve.nodePoly_map_splits_iff_isSquare Split criterion (residue characteristic ≠ 2) line 145 source
Source documentation
Split criterion (residue characteristic ≠ 2). Over a field k of characteristic ≠ 2, the node polynomial splits — i.e. the two tangent directions at the node are k-rational — exactly when its discriminant -c₄ c₆ (splitPolynomial_discrim) is a square in k. This is the tool that, applied to a quadratic twist via the scaling -c₄' c₆' = (t²-4n)⁵ · (-c₄ c₆), turns a nonsplit reduction into a split one after twisting by the right 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₄, Iff, Polynomial.Splits, Polynomial.map, WeierstrassCurve.nodePoly, IsSquare, Neg.neg, HMul.hMul, WeierstrassCurve.c₆
Proof uses: Eq.mpr, HAdd.hAdd, Polynomial, Polynomial.C, HPow.hPow, Polynomial.X, WeierstrassCurve.a₁, HSub.hSub, WeierstrassCurve.b₆, WeierstrassCurve.b₂, WeierstrassCurve.b₄, WeierstrassCurve.a₂, id, Eq, congrArg, WeierstrassCurve.nodePoly_map_eq_quadratic, discrim, propext, Polynomial.splits_quadratic_iff, discrim.eq_1 and 2 more
74 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma nodePoly_map_splits_iff_isSquare {A : Type*} [CommRing A] {k : Type*} [Field k]
    [NeZero (2 : k)] (φ : A →+* k) (W : WeierstrassCurve A) (hc₄ : φ W.c₄ ≠ 0) :
    (W.nodePoly.map φ).Splits ↔ IsSquare (φ (-(W.c₄ * W.c₆))) := by
…
```
lemma WeierstrassCurve.nodePoly_map_splits_iff_of_two_eq_zero Split criterion (residue characteristic 2) line 157 source
Source documentation
Split criterion (residue characteristic 2). Over a field k of characteristic 2, where the square-class criterion nodePoly_map_splits_iff_isSquare fails, the node polynomial splits exactly when its Artin–Schreier invariant lies in the image of z ↦ z² + z. Here c₄ and c₆ are units, and separability (b² = -c₄ c₆ ≠ 0, since 4 = 0) forces the linear coefficient a₁ c₄ to be nonzero, so splits_quadratic_iff_of_two_eq_zero applies.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Field, Eq, OfNat.ofNat, Nat, RingHom, WeierstrassCurve, Ne, WeierstrassCurve.c₄, WeierstrassCurve.c₆, Iff, Polynomial.Splits, Polynomial.map, WeierstrassCurve.nodePoly, Exists, HMul.hMul, HPow.hPow, WeierstrassCurve.a₁, HAdd.hAdd, Neg.neg and 5 more
Proof uses: Mathlib.Tactic.LinearCombination.eq_of_eq, Mathlib.Tactic.LinearCombination.mul_const_eq, Mathlib.Tactic.LinearCombination.eq_rearrange, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.sub_congr, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_zero, Nat.cast_zero, Mathlib.Tactic.Ring.Common.add_mul, Mathlib.Tactic.Ring.Common.mul_zero, Mathlib.Tactic.Ring.Common.zero_mul, Mathlib.Tactic.Ring.Common.add_pf_zero_add, Mathlib.Tactic.Ring.Common.add_pf_add_zero, Mathlib.Tactic.Ring.Common.mul_add and 56 more
102 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma nodePoly_map_splits_iff_of_two_eq_zero {A : Type*} [CommRing A] {k : Type*} [Field k]
    (h2 : (2 : k) = 0) (φ : A →+* k) (W : WeierstrassCurve A) (hc₄ : φ W.c₄ ≠ 0)
    (hc₆ : φ W.c₆ ≠ 0) :
    (W.nodePoly.map φ).Splits ↔ ∃ z, φ (W.a₁ * W.c₄) ^ 2 * (z ^ 2 + z)
      = φ W.c₄ * (-φ (54 * W.b₆ - 3 * W.b₂ * W.b₄ + W.a₂ * W.c₄)) := by
…
```
lemma WeierstrassCurve.integralModel_baseChange The integral model of the base change to K of an integral Weierstrass curve W over R is W itself (integral models are unique, as R → K is injective) line 176 source
Source documentation
The integral model of the base change to K of an integral Weierstrass curve W over R is W itself (integral models are unique, as R → K is injective).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsFractionRing, WeierstrassCurve, WeierstrassCurve.IsIntegral, WeierstrassCurve.baseChange, Eq, WeierstrassCurve.integralModel
Proof uses: WeierstrassCurve.ext, IsFractionRing.injective, WeierstrassCurve.a₁, of_eq_true, RingHom, Algebra.algebraMap, Eq.trans, True, congrFun', congrArg, WeierstrassCurve.map, id, Eq.refl, WeierstrassCurve.integralModel_a₁_eq, WeierstrassCurve.map_a₁, eq_self, WeierstrassCurve.a₂, WeierstrassCurve.integralModel_a₂_eq, WeierstrassCurve.map_a₂, WeierstrassCurve.a₃ and 8 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma integralModel_baseChange (W : WeierstrassCurve R) [IsIntegral R (W⁄K)] :
    integralModel R (W⁄K) = W := by
…
```
theorem WeierstrassCurve.HasSplitMultiplicativeReduction.baseChange_smul Split multiplicative reduction is a change-of-variables invariant line 190 source
Source documentation
Split multiplicative reduction is a change-of-variables invariant. If W (over R) gives a curve with split multiplicative reduction over K, then so does any R-change of variables C • W that still has multiplicative reduction — because the split condition is the splitting of the node polynomial of the integral model, which is invariant by nodePoly_map_splits_smul_iff.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsFractionRing, IsDomain, IsDiscreteValuationRing, WeierstrassCurve, WeierstrassCurve.VariableChange, WeierstrassCurve.IsMinimal, WeierstrassCurve.baseChange, WeierstrassCurve.HasSplitMultiplicativeReduction, WeierstrassCurve.HasMultiplicativeReduction, HSMul.hSMul
Proof uses: Polynomial.Splits, IsLocalRing.ResidueField, Polynomial.map, Algebra.algebraMap, HSub.hSub, Polynomial, HAdd.hAdd, HMul.hMul, RingHom, Polynomial.C, WeierstrassCurve.c₄, WeierstrassCurve.integralModel, HPow.hPow, Nat, Polynomial.X, OfNat.ofNat, WeierstrassCurve.a₁, WeierstrassCurve.b₆, WeierstrassCurve.b₂, WeierstrassCurve.b₄ and 12 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem HasSplitMultiplicativeReduction.baseChange_smul {W : WeierstrassCurve R}
    (C : VariableChange R) [IsMinimal R (W⁄K)]
    (hW : (W⁄K).HasSplitMultiplicativeReduction R)
    [((C • W)⁄K).HasMultiplicativeReduction R] :
    ((C • W)⁄K).HasSplitMultiplicativeReduction R := by
…
```
lemma WeierstrassCurve.residue_integralModel_c₄_ne_zero Multiplicative reduction forces c₄ of the integral model to be a unit: its residue is nonzero (valuation c₄ = 1 means c₄ ∉ maximalIdeal) line 204 source
Source documentation
Multiplicative reduction forces c₄ of the integral model to be a unit: its residue is nonzero (valuation c₄ = 1 means c₄ ∉ maximalIdeal).

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, WeierstrassCurve.c₄, WeierstrassCurve.integralModel, OfNat.ofNat
Proof uses: Eq.mpr, Not, Eq, id, congrArg, Ne.eq_1, Membership.mem, Ideal, IsLocalRing.maximalIdeal, propext, IsLocalRing.residue_eq_zero_iff, WithZero, Multiplicative, Int, Valuation, IsDedekindDomain.HeightOneSpectrum.valuation, IsDiscreteValuationRing.maximalIdeal, WeierstrassCurve.HasMultiplicativeReduction.multiplicativeReduction, Eq.mp, Algebra.algebraMap and 4 more
56 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma residue_integralModel_c₄_ne_zero [E.HasMultiplicativeReduction R] :
    residue R ((E.integralModel R).c₄) ≠ 0 := by
…
```
lemma WeierstrassCurve.residue_integralModel_Δ_eq_zero Multiplicative reduction (bad reduction) means the discriminant of the integral model has zero residue line 214 source
Source documentation
Multiplicative reduction (bad reduction) means the discriminant of the integral model has zero residue.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, CommRing, Algebra, IsFractionRing, IsDomain, IsDiscreteValuationRing, WeierstrassCurve.HasMultiplicativeReduction, Eq, IsLocalRing.ResidueField, RingHom, IsLocalRing.residue, WeierstrassCurve.Δ, WeierstrassCurve.integralModel, OfNat.ofNat
Proof uses: Eq.mpr, Membership.mem, Ideal, IsLocalRing.maximalIdeal, id, congrArg, propext, IsLocalRing.residue_eq_zero_iff, LT.lt, WithZero, Multiplicative, Int, Valuation, IsDedekindDomain.HeightOneSpectrum.valuation, IsDiscreteValuationRing.maximalIdeal, WeierstrassCurve.HasMultiplicativeReduction.badReduction, Eq.mp, IsDedekindDomain.HeightOneSpectrum.asIdeal, IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_mem, Algebra.algebraMap and 2 more
61 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma residue_integralModel_Δ_eq_zero [E.HasMultiplicativeReduction R] :
    residue R ((E.integralModel R).Δ) = 0 := by
…
```
lemma WeierstrassCurve.residue_integralModel_c₆_ne_zero Multiplicative reduction forces c₆ of the integral model to be a unit too: from 1728 Δ = c₄³ - c₆² and Δ ≡ 0, c₆² ≡ c₄³ ≢ 0 line 224 source
Source documentation
Multiplicative reduction forces c₆ of the integral model to be a unit too: from 1728 Δ = c₄³ - c₆² and Δ ≡ 0, c₆² ≡ c₄³ ≢ 0.

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, WeierstrassCurve.c₆, WeierstrassCurve.integralModel, OfNat.ofNat
Proof uses: Eq, WeierstrassCurve.residue_integralModel_c₄_ne_zero, HPow.hPow, Nat, HSub.hSub, WeierstrassCurve.c₄, HMul.hMul, WeierstrassCurve.Δ, congrArg, WeierstrassCurve.c_relation, Mathlib.Tactic.LinearCombination.eq_of_eq, Eq.mp, congr, Eq.trans, map_mul, congrFun', map_ofNat, map_sub, map_pow, Mathlib.Tactic.LinearCombination.eq_rearrange and 65 more
87 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma residue_integralModel_c₆_ne_zero [E.HasMultiplicativeReduction R] :
    residue R ((E.integralModel R).c₆) ≠ 0 := by
…
```
lemma WeierstrassCurve.not_splits_nodePoly_of_not_hasSplit Nonsplit multiplicative reduction means precisely that the node polynomial of the integral model does not split over the residue field line 239 source
Source documentation
Nonsplit multiplicative reduction means precisely that the node polynomial of the integral model does not split over the residue field.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, CommRing, Algebra, IsFractionRing, IsDomain, IsDiscreteValuationRing, WeierstrassCurve.HasMultiplicativeReduction, Not, WeierstrassCurve.HasSplitMultiplicativeReduction, Polynomial.Splits, IsLocalRing.ResidueField, Polynomial.map, Algebra.algebraMap, WeierstrassCurve.nodePoly, WeierstrassCurve.integralModel
Proof uses: WeierstrassCurve.HasSplitMultiplicativeReduction.mk
20 instances, coercions and auxiliary constants left out.
```
lemma not_splits_nodePoly_of_not_hasSplit [E.HasMultiplicativeReduction R]
    (h : ¬ E.HasSplitMultiplicativeReduction R) :
    ¬ ((E.integralModel R).nodePoly.map (algebraMap R (ResidueField R))).Splits :=
…
```
lemma WeierstrassCurve.natDegree_nodePoly_map The node polynomial over the residue field is a genuine quadratic (leading coefficient c₄ is a unit) line 247 source
Source documentation
The node polynomial over the residue field is a genuine quadratic (leading coefficient c₄ is a unit).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, CommRing, Algebra, IsFractionRing, IsDomain, IsDiscreteValuationRing, WeierstrassCurve.HasMultiplicativeReduction, Eq, Nat, Polynomial.natDegree, IsLocalRing.ResidueField, Polynomial.map, Algebra.algebraMap, WeierstrassCurve.nodePoly, WeierstrassCurve.integralModel, OfNat.ofNat
Proof uses: Ne, RingHom, WeierstrassCurve.c₄, Eq.mpr, IsLocalRing.residue, id, congrArg, IsLocalRing.ResidueField.algebraMap_eq, WeierstrassCurve.residue_integralModel_c₄_ne_zero, HAdd.hAdd, Polynomial, HMul.hMul, Polynomial.C, HPow.hPow, Polynomial.X, WeierstrassCurve.a₁, Neg.neg, HSub.hSub, WeierstrassCurve.b₆, WeierstrassCurve.b₂ and 4 more
58 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma natDegree_nodePoly_map [E.HasMultiplicativeReduction R] :
    ((E.integralModel R).nodePoly.map (algebraMap R (ResidueField R))).natDegree = 2 := by
…
```
lemma WeierstrassCurve.irreducible_nodePoly_map For nonsplit multiplicative reduction, the node polynomial is irreducible over the residue field: it is a quadratic that does not split, so (over a field) it has no linear factors line 257 source
Source documentation
For nonsplit multiplicative reduction, the node polynomial is irreducible over the residue field: it is a quadratic that does not split, so (over a field) it has no linear factors.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, CommRing, Algebra, IsFractionRing, IsDomain, IsDiscreteValuationRing, WeierstrassCurve.HasMultiplicativeReduction, Not, WeierstrassCurve.HasSplitMultiplicativeReduction, Irreducible, Polynomial, IsLocalRing.ResidueField, Polynomial.map, Algebra.algebraMap, WeierstrassCurve.nodePoly, WeierstrassCurve.integralModel
Proof uses: Eq.mpr, id, Eq, congrArg, rfl, Polynomial.Splits, WeierstrassCurve.not_splits_nodePoly_of_not_hasSplit, Nat, Polynomial.natDegree, OfNat.ofNat, WeierstrassCurve.natDegree_nodePoly_map, Ne, False.elim, False, Eq.mp, Eq.trans, congrFun', Eq.symm, Irreducible.mk, Polynomial.not_isUnit_of_natDegree_pos and 25 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
```
lemma irreducible_nodePoly_map [E.HasMultiplicativeReduction R]
    (h : ¬ E.HasSplitMultiplicativeReduction R) :
    Irreducible ((E.integralModel R).nodePoly.map (algebraMap R (ResidueField R))) := by
…
```
lemma WeierstrassCurve.separable_nodePoly_map Documented declaration: separable_nodePoly_map line 283 source
Source documentation
For multiplicative reduction the node polynomial is separable over the residue field: its discriminant is -c₄ c₆ (splitPolynomial_discrim), a unit, so the quadratic-separability criterion Polynomial.separable_quadratic_iff applies.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, CommRing, Algebra, IsFractionRing, IsDomain, IsDiscreteValuationRing, WeierstrassCurve.HasMultiplicativeReduction, Polynomial.Separable, IsLocalRing.ResidueField, Polynomial.map, Algebra.algebraMap, WeierstrassCurve.nodePoly, WeierstrassCurve.integralModel
Proof uses: Ne, RingHom, WeierstrassCurve.c₄, OfNat.ofNat, Eq.mpr, IsLocalRing.residue, id, Eq, congrArg, IsLocalRing.ResidueField.algebraMap_eq, WeierstrassCurve.residue_integralModel_c₄_ne_zero, HAdd.hAdd, Polynomial, HMul.hMul, Polynomial.C, HPow.hPow, Nat, Polynomial.X, WeierstrassCurve.a₁, Neg.neg and 17 more
70 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma separable_nodePoly_map [E.HasMultiplicativeReduction R] :
    ((E.integralModel R).nodePoly.map (algebraMap R (ResidueField R))).Separable := by
…
```
theorem WeierstrassCurve.isMinimal_of_valuation_c₄_eq_one Minimality criterion line 305 source
Source documentation
Minimality criterion. An integral Weierstrass equation over K whose c₄ is a unit of R (equivalently, valuation c₄ = 1) is already minimal: any change of variables C keeping the equation integral must have valuation C.u ≥ 1 (else valuation (C • W).c₄ = valuation C.u⁻⁴ > 1, contradicting integrality), so valuation (C • W).Δ = valuation C.u⁻¹² · valuation W.Δ ≤ valuation W.Δ. This is the tool that shows the twist W we build is minimal without minimising by hand.
This is the unit-c₄ case of the Kraus–Laska criterion: the special case "v(c₄) < 4 or v(Δ) < 12 implies minimal" of Silverman, The Arithmetic of Elliptic Curves, Remark VII.1.1, restricted to v(c₄) = 0. The hypothesis is stated at the field level — via the adic valuation of W.c₄ : K — to match mathlib's phrasing of WeierstrassCurve.HasMultiplicativeReduction, whose multiplicativeReduction field is exactly (maximalIdeal R).valuation K W.c₄ = 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsFractionRing, IsDomain, IsDiscreteValuationRing, WeierstrassCurve, WeierstrassCurve.IsIntegral, Eq, WithZero, Multiplicative, Int, Valuation, IsDedekindDomain.HeightOneSpectrum.valuation, IsDiscreteValuationRing.maximalIdeal, WeierstrassCurve.c₄, OfNat.ofNat, WeierstrassCurve.IsMinimal
Proof uses: WeierstrassCurve.IsMinimal.mk, And.intro, WeierstrassCurve.VariableChange, HSMul.hSMul, LE.le, Subtype, WeierstrassCurve.valuation_Δ_aux, Eq.mpr, id, congrArg, one_smul, WeierstrassCurve.Δ, Eq.trans, WeierstrassCurve.valuation_Δ_aux.congr_simp, congr, WeierstrassCurve.valuation_Δ_aux_eq_of_isIntegral, RingHom, Algebra.algebraMap, WeierstrassCurve.integralModel, congrFun' and 27 more
141 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
theorem isMinimal_of_valuation_c₄_eq_one (W : WeierstrassCurve K) [IsIntegral R W]
    (hc₄ : valuation K (maximalIdeal R) W.c₄ = 1) : IsMinimal R W := by
…
```
theorem WeierstrassCurve.valuation_Δ_aux_smul_le For a minimal Weierstrass model W, no integral change of variables increases the valuation of the discriminant line 319 source
Source documentation
For a minimal Weierstrass model W, no integral change of variables increases the valuation of the discriminant.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsFractionRing, IsDomain, IsDiscreteValuationRing, WeierstrassCurve, WeierstrassCurve.IsMinimal, WeierstrassCurve.VariableChange, WeierstrassCurve.IsIntegral, HSMul.hSMul, LE.le, Subtype, WithZero, Multiplicative, Int, OfNat.ofNat, WeierstrassCurve.valuation_Δ_aux
Proof uses: Or.elim, le_total, And.right, WeierstrassCurve.IsMinimal.val_Δ_maximal, id
44 instances, coercions and auxiliary constants left out.
```
theorem valuation_Δ_aux_smul_le {W : WeierstrassCurve K} [hm : IsMinimal R W]
    (D : VariableChange K) (hint : IsIntegral R (D • W)) :
    valuation_Δ_aux R (D • W) ≤ valuation_Δ_aux R ((1 : VariableChange K) • W) :=
…
```
theorem WeierstrassCurve.valuation_Δ_eq_of_isMinimal_smul Two minimal Weierstrass models related by a change of variables have the same valuation of the discriminant line 328 source
Source documentation
Two minimal Weierstrass models related by a change of variables have the same valuation of the discriminant.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsFractionRing, IsDomain, IsDiscreteValuationRing, WeierstrassCurve, WeierstrassCurve.IsMinimal, WeierstrassCurve.VariableChange, Eq, HSMul.hSMul, WithZero, Multiplicative, Int, Valuation, IsDedekindDomain.HeightOneSpectrum.valuation, IsDiscreteValuationRing.maximalIdeal, WeierstrassCurve.Δ
Proof uses: Eq.mpr, LE.le, OfNat.ofNat, WeierstrassCurve.valuation_Δ_aux, id, congrArg, Eq.symm, WeierstrassCurve.valuation_Δ_aux_eq_of_isIntegral, le_antisymm, Iff.mpr, Subtype, Subtype.coe_le_coe, WeierstrassCurve.valuation_Δ_aux_smul_le, WeierstrassCurve.IsIntegral, inferInstance, Eq.mp, one_smul, Inv.inv, inv_smul_smul, Eq.refl
83 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
theorem valuation_Δ_eq_of_isMinimal_smul {W₁ W₂ : WeierstrassCurve K} [IsMinimal R W₁]
    [IsMinimal R W₂] (D : VariableChange K) (hD : D • W₁ = W₂) :
    valuation K (maximalIdeal R) W₂.Δ = valuation K (maximalIdeal R) W₁.Δ := by
…
```
theorem WeierstrassCurve.valuation_u_eq_one_of_isMinimal_smul Documented declaration: valuation_u_eq_one_of_isMinimal_smul line 344 source
Source documentation
The scaling factor of a change of variables between two minimal models of an elliptic curve has valuation 1: the valuations of the discriminants agree and differ by a factor v(u)⁻¹².

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsFractionRing, IsDomain, IsDiscreteValuationRing, WeierstrassCurve, WeierstrassCurve.IsMinimal, WeierstrassCurve.IsElliptic, WeierstrassCurve.VariableChange, Eq, HSMul.hSMul, WithZero, Multiplicative, Int, Valuation, IsDedekindDomain.HeightOneSpectrum.valuation, IsDiscreteValuationRing.maximalIdeal, WeierstrassCurve.VariableChange.u, OfNat.ofNat
Proof uses: Ne, WeierstrassCurve.Δ, Iff.mpr, Valuation.ne_zero_iff, IsUnit.ne_zero, WeierstrassCurve.isUnit_Δ, HPow.hPow, Nat, HMul.hMul, Inv.inv, Eq.mpr, Units, id, Eq.rec, Eq.refl, Eq.trans, congrArg, Eq.symm, WeierstrassCurve.valuation_Δ_eq_of_isMinimal_smul, WeierstrassCurve.variableChange_Δ and 16 more
170 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
theorem valuation_u_eq_one_of_isMinimal_smul {W₁ W₂ : WeierstrassCurve K} [IsMinimal R W₁]
    [IsMinimal R W₂] [W₁.IsElliptic] (D : VariableChange K) (hD : D • W₁ = W₂) :
    valuation K (maximalIdeal R) ↑D.u = 1 := by
…
```
theorem WeierstrassCurve.exists_variableChange_baseChange_eq_of_smul_eq Documented declaration: exists_variableChange_baseChange_eq_of_smul_eq line 364 source
Source documentation
A change of variables D relating two integral Weierstrass models whose scaling factor D.u is the image of a unit of R is itself defined over R: r, s, t are integral over R — roots of monic polynomials obtained from the change-of-variables formulas for the b₆/b₈/a₂/a₆-invariants — hence lie in R since R is integrally closed.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsFractionRing, IsDomain, IsDiscreteValuationRing, WeierstrassCurve, WeierstrassCurve.IsIntegral, WeierstrassCurve.VariableChange, Eq, HSMul.hSMul, Units, RingHom, Algebra.algebraMap, WeierstrassCurve.VariableChange.u, Exists, WeierstrassCurve.VariableChange.baseChange
Proof uses: Ne, OfNat.ofNat, Units.ne_zero, HMul.hMul, HPow.hPow, Nat, WeierstrassCurve.b₆, HAdd.hAdd, WeierstrassCurve.VariableChange.r, WeierstrassCurve.b₄, WeierstrassCurve.b₂, Eq.mpr, id, congrArg, Eq.symm, Inv.inv, WeierstrassCurve.variableChange_b₆, congrFun', Units.val_inv_eq_inv_val, inferInstance and 175 more
198 instances, coercions and auxiliary constants left out.

Tactic trace: 36 steps
Open to load the checked before-and-after goal states.
```
theorem exists_variableChange_baseChange_eq_of_smul_eq {W₁ W₂ : WeierstrassCurve K}
    [IsIntegral R W₁] [IsIntegral R W₂] (D : VariableChange K) (hD : D • W₁ = W₂) (u₀ : Rˣ)
    (hau : algebraMap R K ↑u₀ = ↑D.u) : ∃ C₀ : VariableChange R, C₀.baseChange K = D := by
…
```
theorem WeierstrassCurve.HasSplitMultiplicativeReduction.of_isMinimal_smul Split multiplicative reduction is an isomorphism invariant of minimal models line 434 source
Source documentation
Split multiplicative reduction is an isomorphism invariant of minimal models. If two minimal Weierstrass models W₁, W₂ of an elliptic curve over K are related by a change of variables (D • W₁ = W₂), and W₁ has split multiplicative reduction, then so does W₂.
This is a form of Silverman VII.1.3(b) (uniqueness of minimal models over a discrete valuation ring): the change D has u ∈ Rˣ (valuation_u_eq_one_of_isMinimal_smul), so it is defined over R (exists_variableChange_baseChange_eq_of_smul_eq); then the node polynomial's splitting transfers by nodePoly_map_splits_smul_iff.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, CommRing, Algebra, IsFractionRing, IsDomain, IsDiscreteValuationRing, WeierstrassCurve, WeierstrassCurve.IsMinimal, WeierstrassCurve.IsElliptic, WeierstrassCurve.VariableChange, Eq, HSMul.hSMul, WeierstrassCurve.HasSplitMultiplicativeReduction
Proof uses: WithZero, Multiplicative, Int, Valuation, IsDedekindDomain.HeightOneSpectrum.valuation, IsDiscreteValuationRing.maximalIdeal, WeierstrassCurve.VariableChange.u, OfNat.ofNat, WeierstrassCurve.valuation_u_eq_one_of_isMinimal_smul, Units, RingHom, Algebra.algebraMap, Exists, exists_algebraMap_unit_eq_of_valuation_eq_one, WeierstrassCurve.VariableChange.baseChange, WeierstrassCurve.exists_variableChange_baseChange_eq_of_smul_eq, WeierstrassCurve.baseChange, WeierstrassCurve.integralModel, Eq.mpr, WeierstrassCurve.map and 53 more
126 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
```
theorem HasSplitMultiplicativeReduction.of_isMinimal_smul {W₁ W₂ : WeierstrassCurve K}
    [IsMinimal R W₁] [IsMinimal R W₂] [W₁.IsElliptic] (D : VariableChange K) (hD : D • W₁ = W₂)
    (h₁ : W₁.HasSplitMultiplicativeReduction R) :
    W₂.HasSplitMultiplicativeReduction R := by
…
```