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

38 declarations, 11 contain sorry, 0 declared as axioms

The Tate curve

Let k be a nonarchimedean local field and let E/k be an elliptic curve, given by a minimal Weierstrass equation, with split multiplicative reduction. Tate's theory attaches to E a canonical Tate parameter, an element q = q(E) of k with 0 < |q| < 1, and an isomorphism of groups E(k) ≅ kˣ/qᶻ (Tate's uniformisation). The construction is functorial: if k → l is a valuation-compatible morphism of nonarchimedean local fields then the base change of E to l again has split multiplicative reduction, the Tate parameter of the base change is the image of q, and the uniformisations over k and l fit into a commutative diagram — in general only up to an unremovable sign, but on the nose when the morphism is k-linear (see tateEquiv_baseChange and tateEquiv_galois). The k-linear case gives the Galois-equivariance needed to compute the Galois representations attached to E.

These results are due to Tate, in a manuscript which circulated from the early 1960s and was eventually published in 1995 as A review of non-Archimedean elliptic curves. See also Roquette, Analytic theory of elliptic functions over local fields (1970), and Silverman, Advanced topics in the arithmetic of elliptic curves, V.3 and V.5, for textbook accounts.

TODO

Rank 1 generality. Tate's theory works over any field complete with respect to a nontrivial rank 1 (i.e. real-valued) nonarchimedean valuation, for example ℂ_p or the completion of the maximal unramified extension of ℚ_p: completeness and |q| < 1 are all that is needed for the relevant power series to converge. But right now we can't talk about an elliptic curve over ℂ_p having split multiplicative reduction, so we stick to nonarchimedean local fields: mathlib's WeierstrassCurve.HasSplitMultiplicativeReduction is defined via minimal Weierstrass equations, and mathlib's WeierstrassCurve.IsMinimal requires IsDiscreteValuationRing (its existence theorem exists_isMinimal is proved by well-foundedness of the value group, which fails for dense value groups).
Mathematics question: is there a theory of minimal models for elliptic curves with multiplicative reduction over fields complete wrt an arbitrary rank 1 valuation? For additive reduction you have no chance (consider y² = x³ + p over ℂₚ).
Topology. tateEquiv below should be an isomorphism of topological groups, where kˣ/qᶻ carries the quotient topology and E(k) the topology coming from k. This cannot currently be stated: mathlib has no topology on WeierstrassCurve.Affine.Point (nor on Projectivization, from which it could be induced).
Signs. There is a choice of sign for the Tate uniformisation. I propose that we simply use the definition in e.g. Silverman. One could say explicitly what the sign is by asking what the pullback of the invariant differential dx/(2y + a₁x + a₃) to kˣ is; it will be some constant times du/u (for the Tate curve E_q itself, with Silverman's series, it is exactly du/u).

Imports (6)

Imported by 1 file

FLT.lean

def WeierstrassCurve.tateA₄ The coefficient a₄(q) = -5s₃(q) of the Tate curve, where sₖ(q) = ∑_{n≥1} nᵏqⁿ/(1-qⁿ) (Silverman, ATAEC V.3) line 95 source
Source documentation
The coefficient a₄(q) = -5s₃(q) of the Tate curve, where sₖ(q) = ∑_{n≥1} nᵏqⁿ/(1-qⁿ) (Silverman, ATAEC V.3).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, TopologicalSpace
Proof uses: HMul.hMul, Neg.neg, OfNat.ofNat, tsum, Nat, HDiv.hDiv, HPow.hPow, HAdd.hAdd, HSub.hSub, SummationFilter.unconditional
37 instances, coercions and auxiliary constants left out.
```
noncomputable def WeierstrassCurve.tateA₄ (q : k) : k :=
…
```
Mentions: WeierstrassCurve.q
def WeierstrassCurve.tateA₆ Documented declaration: tateA₆ line 101 source
Source documentation
The coefficient a₆(q) = -(5s₃(q) + 7s₅(q))/12 of the Tate curve, where sₖ(q) = ∑_{n≥1} nᵏqⁿ/(1-qⁿ); the integrality 12 ∣ 5n³ + 7n⁵ makes sense of the division by 12 in every characteristic (Silverman, ATAEC V.3).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, TopologicalSpace
Proof uses: tsum, Nat, HDiv.hDiv, HMul.hMul, Neg.neg, Int, HAdd.hAdd, OfNat.ofNat, HPow.hPow, HSub.hSub, SummationFilter.unconditional
42 instances, coercions and auxiliary constants left out.
```
noncomputable def WeierstrassCurve.tateA₆ (q : k) : k :=
…
```
Mentions: WeierstrassCurve.q
def WeierstrassCurve.tateCurve The Tate curve E_q : y² + xy = x³ + a₄(q)x + a₆(q) (Silverman, ATAEC V.3) line 106 source
Source documentation
The Tate curve E_q : y² + xy = x³ + a₄(q)x + a₆(q) (Silverman, ATAEC V.3).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, TopologicalSpace, WeierstrassCurve
Proof uses: WeierstrassCurve.mk, OfNat.ofNat, WeierstrassCurve.tateA₄, WeierstrassCurve.tateA₆
12 instances, coercions and auxiliary constants left out.
```
noncomputable def WeierstrassCurve.tateCurve (q : k) : WeierstrassCurve k :=
…
```
Mentions: WeierstrassCurve.q
def WeierstrassCurve.tateCurveEquiv Tate's uniformisation of the Tate curve E_q, given by the explicit power series x = X(u, q), y = Y(u, q) of Silverman, ATAEC V.3 sorry line 121 source
Source documentation
Tate's uniformisation of the Tate curve E_q, given by the explicit power series x = X(u, q), y = Y(u, q) of Silverman, ATAEC V.3. Unlike tateEquiv below, this involves no choices at all: it commutes on the nose with every valuative field morphism (see tateCurve_baseChange for the equation-level statement).

depends on sorry what this means
Statement uses: Field, ValuativeRel, TopologicalSpace, DecidableEq, Units, LT.lt, ValuativeRel.ValueGroupWithZero, Valuation, ValuativeRel.valuation, OfNat.ofNat, AddEquiv, Additive, HasQuotient.Quotient, Subgroup, Subgroup.zpowers, WeierstrassCurve.Affine.Point, WeierstrassCurve.Affine.baseChange, WeierstrassCurve.tateCurve
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat
77 instances, coercions and auxiliary constants left out.
```
noncomputable def WeierstrassCurve.tateCurveEquiv (q : kˣ) (hq : valuation k (q : k) < 1) :
    Additive (kˣ ⧸ Subgroup.zpowers q) ≃+ ((tateCurve (q : k))⁄k).Point :=
…
```
Mentions: WeierstrassCurve.q, WeierstrassCurve.tateCurve
lemma WeierstrassCurve.tateParameter_eq line 132 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, TopologicalSpace, Eq, WeierstrassCurve.tateParameter, TateCurve.evalInt, Inv.inv, TateCurve.jInvReverse
Proof uses: Eq.refl
7 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem WeierstrassCurve.valuation_tateParameter_eq The Tate parameter of j has valuation exactly |j|⁻¹: the leading term j⁻¹ of the inverse series q = j⁻¹ + 744j⁻² + ⋯ dominates ultrametrically line 138 source
Source documentation
The Tate parameter of j has valuation exactly |j|⁻¹: the leading term j⁻¹ of the inverse series q = j⁻¹ + 744j⁻² + ⋯ dominates ultrametrically.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, ValuativeRel, TopologicalSpace, IsNonarchimedeanLocalField, LT.lt, ValuativeRel.ValueGroupWithZero, OfNat.ofNat, Valuation, ValuativeRel.valuation, Eq, WeierstrassCurve.tateParameter, Inv.inv
Proof uses: Ne, False, False.elim, Eq.mp, Eq.trans, congrArg, map_zero, Eq.symm, TateCurve.evalInt, TateCurve.jInvReverse, TateCurve.valuation_evalInt_eq, inv_ne_zero, Eq.mpr, id, congrFun', map_inv₀, inv_lt_one_of_one_lt₀, TateCurve.constantCoeff_jInvReverse, TateCurve.coeff_one_jInvReverse, WeierstrassCurve.tateParameter_eq and 1 more
74 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
theorem WeierstrassCurve.valuation_tateParameter_eq {j : k} (hj : 1 < valuation k j) :
    valuation k (tateParameter j) = (valuation k j)⁻¹ := by
…
```
Mentions: WeierstrassCurve.tateParameter
theorem WeierstrassCurve.tateParameter_ne_zero line 148 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, ValuativeRel, TopologicalSpace, IsNonarchimedeanLocalField, LT.lt, ValuativeRel.ValueGroupWithZero, OfNat.ofNat, Valuation, ValuativeRel.valuation, Ne, WeierstrassCurve.tateParameter
Proof uses: Eq, Inv.inv, WeierstrassCurve.valuation_tateParameter_eq, inv_ne_zero, ne_of_gt, lt_trans, zero_lt_one, Eq.symm, Eq.mp, congrArg, map_zero
62 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem WeierstrassCurve.valuation_tateParameter_lt_one line 155 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, ValuativeRel, TopologicalSpace, IsNonarchimedeanLocalField, LT.lt, ValuativeRel.ValueGroupWithZero, OfNat.ofNat, Valuation, ValuativeRel.valuation, WeierstrassCurve.tateParameter
Proof uses: Eq.mpr, Inv.inv, id, Eq, congrFun', congrArg, WeierstrassCurve.valuation_tateParameter_eq, inv_lt_one_of_one_lt₀
56 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem WeierstrassCurve.valuation_Δ_lt_one An elliptic curve over k with bad (here multiplicative) reduction has discriminant of valuation less than 1: the discriminant of the integral model lies in the maximal ideal line 165 source
Source documentation
An elliptic curve over k with bad (here multiplicative) reduction has discriminant of valuation less than 1: the discriminant of the integral model lies in the maximal ideal.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, ValuativeRel, TopologicalSpace, IsNonarchimedeanLocalField, WeierstrassCurve, WeierstrassCurve.HasMultiplicativeReduction, Subtype, Membership.mem, Subring, Valuation.integer, ValuativeRel.ValueGroupWithZero, ValuativeRel.valuation, LT.lt, Valuation, WeierstrassCurve.Δ, OfNat.ofNat
Proof uses: WithZero, Multiplicative, Int, IsDedekindDomain.HeightOneSpectrum.valuation, IsDiscreteValuationRing.maximalIdeal, WeierstrassCurve.HasMultiplicativeReduction.badReduction, Eq.mpr, RingHom, Algebra.algebraMap, WeierstrassCurve.integralModel, id, Eq, congrArg, Eq.symm, WeierstrassCurve.integralModel_Δ_eq, Iff.mp, ValuativeRel.adicValuation_lt_one_iff, Eq.mp
88 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem WeierstrassCurve.valuation_Δ_lt_one (E : WeierstrassCurve k)
    [E.HasMultiplicativeReduction 𝒪[k]] :
    valuation k E.Δ < 1 := by
…
```
theorem WeierstrassCurve.valuation_c₄_eq_one An elliptic curve over k with multiplicative reduction has c₄ of valuation exactly 1: c₄ of the integral model is a unit of 𝒪[k] line 174 source
Source documentation
An elliptic curve over k with multiplicative reduction has c₄ of valuation exactly 1: c₄ of the integral model is a unit of 𝒪[k].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, ValuativeRel, TopologicalSpace, IsNonarchimedeanLocalField, WeierstrassCurve, WeierstrassCurve.HasMultiplicativeReduction, Subtype, Membership.mem, Subring, Valuation.integer, ValuativeRel.ValueGroupWithZero, ValuativeRel.valuation, Eq, Valuation, WeierstrassCurve.c₄, OfNat.ofNat
Proof uses: WithZero, Multiplicative, Int, IsDedekindDomain.HeightOneSpectrum.valuation, IsDiscreteValuationRing.maximalIdeal, WeierstrassCurve.HasMultiplicativeReduction.multiplicativeReduction, Eq.mpr, RingHom, Algebra.algebraMap, WeierstrassCurve.integralModel, id, congrArg, Eq.symm, WeierstrassCurve.integralModel_c₄_eq, Iff.mp, ValuativeRel.adicValuation_eq_one_iff, Eq.mp
76 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem WeierstrassCurve.valuation_c₄_eq_one (E : WeierstrassCurve k)
    [E.HasMultiplicativeReduction 𝒪[k]] :
    valuation k E.c₄ = 1 := by
…
```
theorem WeierstrassCurve.valuation_Δ_ne_zero The discriminant of an elliptic curve has nonzero valuation line 183 source
Source documentation
The discriminant of an elliptic curve has nonzero valuation.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, ValuativeRel, WeierstrassCurve, WeierstrassCurve.IsElliptic, Ne, ValuativeRel.ValueGroupWithZero, Valuation, ValuativeRel.valuation, WeierstrassCurve.Δ, OfNat.ofNat
Proof uses: Eq.mpr, id, Eq, congrArg, propext, Valuation.ne_zero_iff, WeierstrassCurve.Δ', Eq.symm, WeierstrassCurve.coe_Δ', Units.ne_zero
41 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem WeierstrassCurve.valuation_Δ_ne_zero (E : WeierstrassCurve k) [E.IsElliptic] :
    valuation k E.Δ ≠ 0 := by
…
```
theorem WeierstrassCurve.valuation_j_eq An elliptic curve over k with multiplicative reduction has |j| = |c₄|³/|Δ| = |Δ|⁻¹ line 189 source
Source documentation
An elliptic curve over k with multiplicative reduction has |j| = |c₄|³/|Δ| = |Δ|⁻¹.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, ValuativeRel, TopologicalSpace, IsNonarchimedeanLocalField, WeierstrassCurve, WeierstrassCurve.IsElliptic, WeierstrassCurve.HasMultiplicativeReduction, Subtype, Membership.mem, Subring, Valuation.integer, ValuativeRel.ValueGroupWithZero, ValuativeRel.valuation, Eq, Valuation, WeierstrassCurve.j, Inv.inv, WeierstrassCurve.Δ
Proof uses: Eq.mpr, HMul.hMul, Units, WeierstrassCurve.Δ', HPow.hPow, Nat, WeierstrassCurve.c₄, OfNat.ofNat, id, congrArg, rfl, map_mul, map_pow, WeierstrassCurve.valuation_c₄_eq_one, one_pow, mul_one, Units.val_inv_eq_inv_val, map_inv₀, WeierstrassCurve.coe_Δ', Eq.refl
85 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem WeierstrassCurve.valuation_j_eq (E : WeierstrassCurve k) [E.IsElliptic]
    [E.HasMultiplicativeReduction 𝒪[k]] :
    valuation k E.j = (valuation k E.Δ)⁻¹ := by
…
```
theorem WeierstrassCurve.one_lt_valuation_j Documented declaration: one_lt_valuation_j line 198 source
Source documentation
An elliptic curve over k with split multiplicative reduction has non-integral j-invariant, |j(E)| > 1: indeed v(j) = -v(Δ_min) < 0, since c₄ is a unit when the reduction is multiplicative.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, ValuativeRel, TopologicalSpace, IsNonarchimedeanLocalField, WeierstrassCurve, WeierstrassCurve.IsElliptic, WeierstrassCurve.HasSplitMultiplicativeReduction, Subtype, Membership.mem, Subring, Valuation.integer, ValuativeRel.ValueGroupWithZero, ValuativeRel.valuation, LT.lt, OfNat.ofNat, Valuation, WeierstrassCurve.j
Proof uses: Eq.mpr, Inv.inv, WeierstrassCurve.Δ, id, Eq, congrArg, WeierstrassCurve.valuation_j_eq, Iff.mpr, one_lt_inv₀, Ne, zero_lt_iff, WeierstrassCurve.valuation_Δ_ne_zero, WeierstrassCurve.valuation_Δ_lt_one
77 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem WeierstrassCurve.one_lt_valuation_j (E : WeierstrassCurve k) [E.IsElliptic]
    [E.HasSplitMultiplicativeReduction 𝒪[k]] :
    1 < valuation k E.j := by
…
```
def WeierstrassCurve.q Documented declaration: q line 212 source
Source documentation
The Tate parameter of an elliptic curve E, given by a minimal Weierstrass equation with split multiplicative reduction over a nonarchimedean local field k: the unique element q of k with 0 < |q| < 1 such that j(E) = j(q) = q⁻¹ + 744 + 196884q + ⋯, defined directly (with no appeal to choice) as tateParameter E.j, the inverse j-series evaluated at j(E). Equivalently, the unique q such that E(k̄) is Galois-equivariantly isomorphic to k̄ˣ/q^ℤ. (The bare existence of an abstract isomorphism E(k) ≅ kˣ/q^ℤ would not pin down q: already over ℚ_p the groups ℚ_pˣ/p^ℤ and ℚ_pˣ/(p(1+p))^ℤ are isomorphic, even topologically.)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, TopologicalSpace, WeierstrassCurve, WeierstrassCurve.IsElliptic
Proof uses: WeierstrassCurve.tateParameter, WeierstrassCurve.j
2 instances, coercions and auxiliary constants left out.
```
noncomputable def WeierstrassCurve.q (E : WeierstrassCurve k) [E.IsElliptic] : k :=
…
```
theorem WeierstrassCurve.q_ne_zero line 221 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, ValuativeRel, TopologicalSpace, IsNonarchimedeanLocalField, WeierstrassCurve, WeierstrassCurve.IsElliptic, WeierstrassCurve.HasSplitMultiplicativeReduction, Subtype, Membership.mem, Subring, Valuation.integer, ValuativeRel.ValueGroupWithZero, ValuativeRel.valuation, Ne, WeierstrassCurve.q, OfNat.ofNat
Proof uses: WeierstrassCurve.tateParameter_ne_zero, WeierstrassCurve.j, WeierstrassCurve.one_lt_valuation_j
37 instances, coercions and auxiliary constants left out.
theorem WeierstrassCurve.valuation_q_lt_one The Tate parameter has norm less than 1 line 226 source
Source documentation
The Tate parameter has norm less than 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, ValuativeRel, TopologicalSpace, IsNonarchimedeanLocalField, WeierstrassCurve, WeierstrassCurve.IsElliptic, WeierstrassCurve.HasSplitMultiplicativeReduction, Subtype, Membership.mem, Subring, Valuation.integer, ValuativeRel.ValueGroupWithZero, ValuativeRel.valuation, LT.lt, Valuation, WeierstrassCurve.q, OfNat.ofNat
Proof uses: WeierstrassCurve.valuation_tateParameter_lt_one, WeierstrassCurve.j, WeierstrassCurve.one_lt_valuation_j
46 instances, coercions and auxiliary constants left out.
```
theorem WeierstrassCurve.valuation_q_lt_one : valuation k E.q < 1 :=
…
```
def WeierstrassCurve.qUnit The Tate parameter as an element of kˣ line 230 source
Source documentation
The Tate parameter as an element of kˣ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, ValuativeRel, TopologicalSpace, IsNonarchimedeanLocalField, WeierstrassCurve, WeierstrassCurve.IsElliptic, WeierstrassCurve.HasSplitMultiplicativeReduction, Subtype, Membership.mem, Subring, Valuation.integer, ValuativeRel.ValueGroupWithZero, ValuativeRel.valuation, Units
Proof uses: Units.mk0, WeierstrassCurve.q, WeierstrassCurve.q_ne_zero
36 instances, coercions and auxiliary constants left out.
```
noncomputable def WeierstrassCurve.qUnit : kˣ :=
…
```
def WeierstrassCurve.tateEquiv Tate's uniformization theorem: if E/k is an elliptic curve with split multiplicative reduction then E(k) is isomorphic to kˣ/⟨q⟩ sorry line 238 source
Source documentation
Tate's uniformization theorem: if E/k is an elliptic curve with split multiplicative reduction then E(k) is isomorphic to kˣ/⟨q⟩.

depends on sorry what this means
Statement uses: Field, ValuativeRel, TopologicalSpace, IsNonarchimedeanLocalField, WeierstrassCurve, WeierstrassCurve.IsElliptic, WeierstrassCurve.HasSplitMultiplicativeReduction, Subtype, Membership.mem, Subring, Valuation.integer, ValuativeRel.ValueGroupWithZero, ValuativeRel.valuation, DecidableEq, AddEquiv, Additive, HasQuotient.Quotient, Units, Subgroup, Subgroup.zpowers and 3 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
68 instances, coercions and auxiliary constants left out.
```
noncomputable def WeierstrassCurve.tateEquiv :
    Additive (kˣ ⧸ Subgroup.zpowers E.qUnit) ≃+ (E⁄k).Point :=
…
```
theorem WeierstrassCurve.exists_variableChange_tateCurve Documented declaration: exists_variableChange_tateCurve sorry line 248 source
Source comment
Tate's theorem (Silverman, ATAEC V.5.3): an elliptic curve with split multiplicative reduction is isomorphic, by a change of Weierstrass coordinates, to the Tate curve of its Tate parameter. Since `j(E)` is non-integral, `Aut` of the curve is `{±1}` and there are exactly *two* such `C`, differing by negation. `tateEquiv` is `tateCurveEquiv` transported along a choice of one of them; this binary choice, for each `E`, is the only choice in the whole theory, and it cannot be made functorially in `E` — see `tateEquiv_baseChange`.

depends on sorry what this means
Statement uses: Field, ValuativeRel, TopologicalSpace, IsNonarchimedeanLocalField, WeierstrassCurve, WeierstrassCurve.IsElliptic, WeierstrassCurve.HasSplitMultiplicativeReduction, Subtype, Membership.mem, Subring, Valuation.integer, ValuativeRel.ValueGroupWithZero, ValuativeRel.valuation, WeierstrassCurve.IsMinimal, Exists, WeierstrassCurve.VariableChange, Eq, HSMul.hSMul, WeierstrassCurve.tateCurve, WeierstrassCurve.q
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
39 instances, coercions and auxiliary constants left out.
```
theorem WeierstrassCurve.exists_variableChange_tateCurve :
    ∃ C : VariableChange k, C • tateCurve E.q = E :=
…
```
Mentions: WeierstrassCurve.tateCurve
theorem WeierstrassCurve.tateA₄_eq_evalInt Documented declaration: tateA₄_eq_evalInt line 256 source
Source documentation
The Lambert series rearrangement ∑_{n≥1} n³qⁿ/(1-qⁿ) = ∑_{n≥1} σ₃(n)qⁿ for |q| < 1: the defining series of tateA₄ is the evaluation of the formal series a₄(q) = -5s₃(q) ∈ ℤ⟦q⟧.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, ValuativeRel, TopologicalSpace, IsNonarchimedeanLocalField, LT.lt, ValuativeRel.ValueGroupWithZero, Valuation, ValuativeRel.valuation, OfNat.ofNat, Eq, WeierstrassCurve.tateA₄, TateCurve.evalInt, TateCurve.a₄Formal
Proof uses: Nat, Int, LinearMap, RingHom.id, PowerSeries, Unit, PowerSeries.coeff, Finset.sum, Nat.divisors, HMul.hMul, Neg.neg, HPow.hPow, Eq.mpr, ArithmeticFunction, ArithmeticFunction.sigma, id, congrArg, TateCurve.coeff_a₄Formal, ArithmeticFunction.sigma_apply, congrFun' and 85 more
134 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
theorem WeierstrassCurve.tateA₄_eq_evalInt (q : k) (hq : valuation k q < 1) :
    tateA₄ q = TateCurve.evalInt q TateCurve.a₄Formal := by
…
```
Mentions: WeierstrassCurve.q, WeierstrassCurve.tateA₄, TateCurve.evalInt, TateCurve.a₄Formal
theorem WeierstrassCurve.tateA₆_eq_evalInt The Lambert series rearrangement for tateA₆, as for tateA₄_eq_evalInt; the bookkeeping of the exact division by 12 uses 12 ∣ 5d³ + 7d⁵ termwise line 272 source
Source documentation
The Lambert series rearrangement for tateA₆, as for tateA₄_eq_evalInt; the bookkeeping of the exact division by 12 uses 12 ∣ 5d³ + 7d⁵ termwise.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, ValuativeRel, TopologicalSpace, IsNonarchimedeanLocalField, LT.lt, ValuativeRel.ValueGroupWithZero, Valuation, ValuativeRel.valuation, OfNat.ofNat, Eq, WeierstrassCurve.tateA₆, TateCurve.evalInt, TateCurve.a₆Formal
Proof uses: Int, Dvd.dvd, HAdd.hAdd, HMul.hMul, HPow.hPow, Nat, ZMod, Eq.mpr, id, congrFun', congrArg, Eq.trans, Int.cast_add, congr, Int.cast_mul, Int.cast_ofNat, Int.cast_pow, of_decide_eq_true, Bool, Decidable.decide and 91 more
148 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
```
theorem WeierstrassCurve.tateA₆_eq_evalInt (q : k) (hq : valuation k q < 1) :
    tateA₆ q = TateCurve.evalInt q TateCurve.a₆Formal := by
…
```
Mentions: WeierstrassCurve.q, WeierstrassCurve.tateA₆, TateCurve.evalInt, TateCurve.a₆Formal
instance (instance at line 328) line 328 source
Source comment
The base change of E is elliptic. (Mathlib has this instance for `E.map f`, but `WeierstrassCurve.baseChange` is a non-reducible `def`, so instance search cannot see through it.)
```
instance : (E.baseChange l).IsElliptic :=
…
```
theorem WeierstrassCurve.tateCurve_baseChange Documented declaration: tateCurve_baseChange line 351 source
Source documentation
The construction of the Tate curve commutes on the nose with any valuative morphism: its coefficients are power series in q with integer coefficients, and the partial sums converge at matching rates on both sides (TateCurve.evalInt_map). The same is true of the uniformisation tateCurveEquiv (a statement we defer, as it needs transport along this equality).
On the hypothesis |q| < 1: the coefficient series tateA₄, tateA₆ are tsums, which take junk values outside the open unit disc (the tsum of a non-summable family is 0, and terms with vanishing denominators 1 - qⁿ = 0 are the junk x/0 = 0). Without the hypothesis this lemma would be a statement about the alignment of junk values across two different fields: for |q| > 1 it would hold by accident — each term of tateA₄ has size |(n+1)³|, which does not tend to 0, so both sides are non-summable and both junk to 0 — but for |q| = 1 summability hinges on how well qⁿ approximates 1, a Diophantine condition on q, and transferring (non-)summability along k → l would further require the image of ValuativeExtension.mapValueGroupWithZero to be cofinal in the value group of l (true for local fields, by finiteness of ramification, but yet another argument). None of this buys anything: every consumer feeds this lemma a Tate parameter, which lies strictly inside the disc (valuation_q_lt_one). So the hypothesis is free in practice, and keeps the statement the honest identity of convergent series that it is in Silverman.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, ValuativeRel, TopologicalSpace, IsNonarchimedeanLocalField, Algebra, ValuativeExtension, LT.lt, ValuativeRel.ValueGroupWithZero, Valuation, ValuativeRel.valuation, OfNat.ofNat, Eq, WeierstrassCurve.Affine, WeierstrassCurve.Affine.baseChange, WeierstrassCurve.tateCurve, RingHom, Algebra.algebraMap
Proof uses: TateCurve.valuation_algebraMap_lt_one, WeierstrassCurve.tateA₄, Eq.mpr, TateCurve.evalInt, TateCurve.a₄Formal, id, congrArg, WeierstrassCurve.tateA₄_eq_evalInt, TateCurve.evalInt_map, Eq.refl, WeierstrassCurve.tateA₆, TateCurve.a₆Formal, WeierstrassCurve.tateA₆_eq_evalInt, WeierstrassCurve.ext, of_eq_true, WeierstrassCurve.a₁, Eq.trans, True, congrFun', WeierstrassCurve.mk and 14 more
59 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
theorem WeierstrassCurve.tateCurve_baseChange (q : k) (hq : valuation k q < 1) :
    (tateCurve q)⁄l = tateCurve (algebraMap k l q) := by
…
```
Mentions: WeierstrassCurve.q, WeierstrassCurve.tateCurve
instance (instance at line 364) line 364 source
Source comment
The base change of `E` to `l` is still given by a minimal Weierstrass equation. This uses the multiplicative reduction hypothesis (which makes `c₄` a unit): minimality by itself is not preserved by ramified base change — `y² = x³ + p` is minimal over `ℚ_p` but not over `ℚ_p(p^{1/6})`. See `WeierstrassCurve.isMinimal_baseChange` in `ReductionBaseChange`.
```
instance : (E.baseChange l).IsMinimal 𝒪[l] :=
…
```
instance (instance at line 370) line 370 source
Source comment
and it still has split multiplicative reduction, via `WeierstrassCurve.hasSplitMultiplicativeReduction_baseChange` in `ReductionBaseChange` (from which the preceding `IsMinimal` also follows by class-parent projection).
```
instance : (E.baseChange l).HasSplitMultiplicativeReduction 𝒪[l] :=
…
```
theorem WeierstrassCurve.tateParameter_map The Tate parameter series commutes with valuative extensions: it is the evaluation of an integral power series at j⁻¹, so this is a direct instance of evalInt_map line 375 source
Source documentation
The Tate parameter series commutes with valuative extensions: it is the evaluation of an integral power series at j⁻¹, so this is a direct instance of evalInt_map.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, ValuativeRel, TopologicalSpace, IsNonarchimedeanLocalField, Algebra, ValuativeExtension, LT.lt, ValuativeRel.ValueGroupWithZero, OfNat.ofNat, Valuation, ValuativeRel.valuation, Eq, WeierstrassCurve.tateParameter, RingHom, Algebra.algebraMap
Proof uses: Inv.inv, Eq.mpr, id, congrFun', congrArg, map_inv₀, inv_lt_one_of_one_lt₀, TateCurve.evalInt, TateCurve.jInvReverse, congr, WeierstrassCurve.tateParameter_eq, PowerSeries, Int, TateCurve.evalInt_map, of_eq_true, Eq.trans, True, eq_self
69 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem WeierstrassCurve.tateParameter_map {j : k} (hj : 1 < valuation k j) :
    tateParameter (algebraMap k l j) = algebraMap k l (tateParameter j) := by
…
```
Mentions: WeierstrassCurve.tateParameter
theorem WeierstrassCurve.q_baseChange line 382 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, ValuativeRel, TopologicalSpace, IsNonarchimedeanLocalField, WeierstrassCurve, WeierstrassCurve.IsElliptic, WeierstrassCurve.HasSplitMultiplicativeReduction, Subtype, Membership.mem, Subring, Valuation.integer, ValuativeRel.ValueGroupWithZero, ValuativeRel.valuation, Algebra, ValuativeExtension, Eq, WeierstrassCurve.q, WeierstrassCurve.baseChange, RingHom, Algebra.algebraMap
Proof uses: Eq.mpr, WeierstrassCurve.tateParameter, WeierstrassCurve.j, id, congrArg, rfl, WeierstrassCurve.map_j, WeierstrassCurve.tateParameter_map, WeierstrassCurve.one_lt_valuation_j, Eq.refl
42 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem WeierstrassCurve.tateEquiv_baseChange sorry line 404 source
depends on sorry what this means
Statement uses: Field, ValuativeRel, TopologicalSpace, IsNonarchimedeanLocalField, WeierstrassCurve, WeierstrassCurve.IsElliptic, WeierstrassCurve.HasSplitMultiplicativeReduction, Subtype, Membership.mem, Subring, Valuation.integer, ValuativeRel.ValueGroupWithZero, ValuativeRel.valuation, WeierstrassCurve.IsMinimal, Algebra, ValuativeExtension, DecidableEq, Exists, Units, Int and 19 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
131 instances, coercions and auxiliary constants left out.
theorem WeierstrassCurve.tateEquiv_galois sorry line 419 source
depends on sorry what this means
Statement uses: Field, ValuativeRel, TopologicalSpace, IsNonarchimedeanLocalField, WeierstrassCurve, WeierstrassCurve.IsElliptic, WeierstrassCurve.HasSplitMultiplicativeReduction, Subtype, Membership.mem, Subring, Valuation.integer, ValuativeRel.ValueGroupWithZero, ValuativeRel.valuation, WeierstrassCurve.IsMinimal, Algebra, ValuativeExtension, DecidableEq, AlgEquiv, Continuous, Units and 18 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
119 instances, coercions and auxiliary constants left out.
instance (instance at line 448) line 448 source
Source comment
the base change of E to Ω is elliptic (same remark as for `l` above)
```
instance : (E.baseChange Ω).IsElliptic :=
…
```
def WeierstrassCurve.qUnitSepClosure The image of the Tate parameter in a separable closure Ω of k, as a unit line 453 source
Source documentation
The image of the Tate parameter in a separable closure Ω of k, as a unit. (Ω is not a nonarchimedean local field, so this is not literally (E.baseChange Ω).qUnit.)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, ValuativeRel, TopologicalSpace, IsNonarchimedeanLocalField, WeierstrassCurve, WeierstrassCurve.IsElliptic, WeierstrassCurve.HasSplitMultiplicativeReduction, Subtype, Membership.mem, Subring, Valuation.integer, ValuativeRel.ValueGroupWithZero, ValuativeRel.valuation, Algebra, Units
Proof uses: MonoidHom, Units.map, Algebra.algebraMap, WeierstrassCurve.qUnit
41 instances, coercions and auxiliary constants left out.
```
noncomputable def WeierstrassCurve.qUnitSepClosure : Ωˣ :=
…
```
def WeierstrassCurve.tateEquivSepClosure Tate's uniformisation over a separable closure Ω of k: the union of the uniformisations of the E(l) over the finite subextensions l/k of Ω sorry line 462 source
Source documentation
Tate's uniformisation over a separable closure Ω of k: the union of the uniformisations of the E(l) over the finite subextensions l/k of Ω. Its sign is pinned to that of tateEquiv by tatePoint_baseChange.

depends on sorry what this means
Statement uses: Field, ValuativeRel, TopologicalSpace, IsNonarchimedeanLocalField, WeierstrassCurve, WeierstrassCurve.IsElliptic, WeierstrassCurve.HasSplitMultiplicativeReduction, Subtype, Membership.mem, Subring, Valuation.integer, ValuativeRel.ValueGroupWithZero, ValuativeRel.valuation, Algebra, DecidableEq, AddEquiv, Additive, HasQuotient.Quotient, Units, Subgroup and 4 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
64 instances, coercions and auxiliary constants left out.
```
noncomputable def WeierstrassCurve.tateEquivSepClosure :
    Additive (Ωˣ ⧸ Subgroup.zpowers (E.qUnitSepClosure Ω)) ≃+ (E⁄Ω).Point :=
…
```
def WeierstrassCurve.tatePoint The point of E(Ω) corresponding to a unit x ∈ Ωˣ under Tate's uniformisation line 467 source
Source documentation
The point of E(Ω) corresponding to a unit x ∈ Ωˣ under Tate's uniformisation.

depends on sorry what this means
Statement uses: Field, ValuativeRel, TopologicalSpace, IsNonarchimedeanLocalField, WeierstrassCurve, WeierstrassCurve.IsElliptic, WeierstrassCurve.HasSplitMultiplicativeReduction, Subtype, Membership.mem, Subring, Valuation.integer, ValuativeRel.ValueGroupWithZero, ValuativeRel.valuation, Algebra, DecidableEq, Units, WeierstrassCurve.Affine.Point, WeierstrassCurve.Affine.baseChange
Proof uses: AddEquiv, Additive, HasQuotient.Quotient, Subgroup, Subgroup.zpowers, WeierstrassCurve.qUnitSepClosure, WeierstrassCurve.tateEquivSepClosure, Equiv, Additive.ofMul
51 instances, coercions and auxiliary constants left out.
```
noncomputable def WeierstrassCurve.tatePoint (x : Ωˣ) : (E⁄Ω).Point :=
…
```
theorem WeierstrassCurve.tatePoint_baseChange sorry line 475 source
depends on sorry what this means
Statement uses: Field, ValuativeRel, TopologicalSpace, IsNonarchimedeanLocalField, WeierstrassCurve, WeierstrassCurve.IsElliptic, WeierstrassCurve.HasSplitMultiplicativeReduction, Subtype, Membership.mem, Subring, Valuation.integer, ValuativeRel.ValueGroupWithZero, ValuativeRel.valuation, WeierstrassCurve.IsMinimal, Algebra, IsSepClosed, Algebra.IsSeparable, DecidableEq, Units, Eq and 17 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
111 instances, coercions and auxiliary constants left out.
theorem WeierstrassCurve.tatePoint_galois Galois equivariance of the uniformisation over Ω: no continuity hypothesis is needed this time, since Ω/k is algebraic sorry line 482 source
Source comment
Galois equivariance of the uniformisation over `Ω`: no continuity hypothesis is needed this time, since `Ω/k` is algebraic.

depends on sorry what this means
Statement uses: Field, ValuativeRel, TopologicalSpace, IsNonarchimedeanLocalField, WeierstrassCurve, WeierstrassCurve.IsElliptic, WeierstrassCurve.HasSplitMultiplicativeReduction, Subtype, Membership.mem, Subring, Valuation.integer, ValuativeRel.ValueGroupWithZero, ValuativeRel.valuation, WeierstrassCurve.IsMinimal, Algebra, IsSepClosed, Algebra.IsSeparable, DecidableEq, AlgEquiv, Units and 9 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
73 instances, coercions and auxiliary constants left out.
```
theorem WeierstrassCurve.tatePoint_galois (σ : Ω ≃ₐ[k] Ω) (u : Ωˣ) :
    Affine.Point.map (W' := E) σ.toAlgHom (E.tatePoint Ω u) =
…
```
theorem WeierstrassCurve.tatePoint_mem_torsionBy_of_mem_rootsOfUnity N-th roots of unity give N-torsion points of E under Tate's uniformisation sorry line 488 source
Source documentation
N-th roots of unity give N-torsion points of E under Tate's uniformisation.

depends on sorry what this means
Statement uses: Field, ValuativeRel, TopologicalSpace, IsNonarchimedeanLocalField, WeierstrassCurve, WeierstrassCurve.IsElliptic, WeierstrassCurve.HasSplitMultiplicativeReduction, Subtype, Membership.mem, Subring, Valuation.integer, ValuativeRel.ValueGroupWithZero, ValuativeRel.valuation, WeierstrassCurve.IsMinimal, Algebra, IsSepClosed, Algebra.IsSeparable, DecidableEq, Nat, Units and 8 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
55 instances, coercions and auxiliary constants left out.
```
theorem WeierstrassCurve.tatePoint_mem_torsionBy_of_mem_rootsOfUnity {N : ℕ} {ζ : Ωˣ}
    (hζ : ζ ∈ rootsOfUnity N Ω) :
    E.tatePoint Ω ζ ∈ AddSubgroup.torsionBy (E⁄Ω).Point (N : ℤ) :=
…
```
theorem WeierstrassCurve.tatePoint_mem_torsionBy_of_pow_eq N-th roots of the Tate parameter give N-torsion points of E under Tate's uniformisation sorry line 495 source
Source documentation
N-th roots of the Tate parameter give N-torsion points of E under Tate's uniformisation.

depends on sorry what this means
Statement uses: Field, ValuativeRel, TopologicalSpace, IsNonarchimedeanLocalField, WeierstrassCurve, WeierstrassCurve.IsElliptic, WeierstrassCurve.HasSplitMultiplicativeReduction, Subtype, Membership.mem, Subring, Valuation.integer, ValuativeRel.ValueGroupWithZero, ValuativeRel.valuation, WeierstrassCurve.IsMinimal, Algebra, IsSepClosed, Algebra.IsSeparable, DecidableEq, Nat, Units and 9 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
55 instances, coercions and auxiliary constants left out.
```
theorem WeierstrassCurve.tatePoint_mem_torsionBy_of_pow_eq {N : ℕ} {r : Ωˣ}
    (hr : r ^ N = E.qUnitSepClosure Ω) :
    E.tatePoint Ω r ∈ AddSubgroup.torsionBy (E⁄Ω).Point (N : ℤ) :=
…
```
theorem WeierstrassCurve.weilPairing_tatePoint weilPairing and tateEquiv/tateEquivSepClosure are all currently sorryed data, each pinned down mathematically only up to a sign sorry line 506 source
Source comment
`weilPairing` and `tateEquiv`/`tateEquivSepClosure` are all currently `sorry`ed data, each pinned down mathematically only up to a sign. The following compatibility, due to Tate, is the demand that these signs be chosen coherently. Note that it constrains the sign convention in the *Weil pairing* (about which the literature does not agree) in terms of the uniformisation, and not vice versa: by bilinearity `e_N(-P, -Q) = e_N(P, Q)`, so the demand is insensitive to negating `tateEquivSepClosure`.

depends on sorry what this means
Statement uses: Field, ValuativeRel, TopologicalSpace, IsNonarchimedeanLocalField, WeierstrassCurve, WeierstrassCurve.IsElliptic, WeierstrassCurve.HasSplitMultiplicativeReduction, Subtype, Membership.mem, Subring, Valuation.integer, ValuativeRel.ValueGroupWithZero, ValuativeRel.valuation, WeierstrassCurve.IsMinimal, Algebra, IsSepClosed, Algebra.IsSeparable, DecidableEq, Nat, NeZero and 20 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
121 instances, coercions and auxiliary constants left out.
```
theorem WeierstrassCurve.weilPairing_tatePoint (N : ℕ) [NeZero (N : Ω)] {ζ r : Ωˣ}
    (hζ : ζ ∈ rootsOfUnity N Ω) (hr : r ^ N = E.qUnitSepClosure Ω) :
    (E⁄Ω).weilPairing Ω N
      ⟨E.tatePoint Ω ζ, E.tatePoint_mem_torsionBy_of_mem_rootsOfUnity Ω hζ⟩
      ⟨E.tatePoint Ω r, E.tatePoint_mem_torsionBy_of_pow_eq Ω hr⟩ =
    Additive.ofMul (⟨ζ, hζ⟩ : rootsOfUnity N Ω) :=
…
```
Mentions: WeierstrassCurve.weilPairing