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

14 declarations, 6 contain sorry, 0 declared as axioms

See https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/n-torsion.20or.20multiplication.20by.20n.20as.20an.20additive.20group.20hom/near/429096078

The main theorems in this file are part of the PhD thesis work of David Angdinata, one of KB's PhD students. It would be great if anyone who is interested in working on these results could talk to David first. Note that he has already made substantial progress.

Imports (3)

Imported by 4 files

abbrev WeierstrassCurve.nTorsion The n-torsion subgroup of an elliptic curve E over k: the kernel of multiplication by n on the group of k-points of E line 33 source
Source documentation
The n-torsion subgroup of an elliptic curve E over k: the kernel of multiplication by n on the group of k-points of E.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, DecidableEq, Nat
Proof uses: Subtype, WeierstrassCurve.Affine.Point, WeierstrassCurve.Affine.baseChange, Membership.mem, Submodule, Int, Submodule.torsionBy
12 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
abbrev WeierstrassCurve.nTorsion (n : ℕ) : Type u := Submodule.torsionBy ℤ (E⁄k).Point n
```
instance (instance at line 39) line 39 source
Source comment
not sure if this instance will cause more trouble than it's worth
```
noncomputable instance (n : ℕ) : Module (ZMod n) (E.nTorsion n) :=
…
```
theorem WeierstrassCurve.n_torsion_finite This theorem needs e.g. a theory of division polynomials sorry line 46 source
Source comment
This theorem needs e.g. a theory of division polynomials. It's ongoing work of David Angdinata. Please do not work on it without talking to KB and David first.

depends on sorry what this means
Statement uses: Field, WeierstrassCurve, WeierstrassCurve.IsElliptic, DecidableEq, Nat, LT.lt, OfNat.ofNat, Finite, WeierstrassCurve.nTorsion
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
6 instances, coercions and auxiliary constants left out.
```
theorem WeierstrassCurve.n_torsion_finite {n : ℕ} (hn : 0 < n) : Finite (E.nTorsion n) := sorry
```
theorem WeierstrassCurve.n_torsion_card This theorem needs e.g. a theory of division polynomials sorry line 51 source
Source comment
This theorem needs e.g. a theory of division polynomials. It's ongoing work of David Angdinata. Please do not work on it without talking to KB and David first. This theorem was well-known in the early part of the 20th century.

depends on sorry what this means
Statement uses: Field, WeierstrassCurve, WeierstrassCurve.IsElliptic, DecidableEq, IsSepClosed, Nat, Ne, OfNat.ofNat, Eq, Nat.card, WeierstrassCurve.nTorsion, HPow.hPow
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
36 instances, coercions and auxiliary constants left out.
```
theorem WeierstrassCurve.n_torsion_card [IsSepClosed k] {n : ℕ} (hn : (n : k) ≠ 0) :
    Nat.card (E.nTorsion n) = n^2 := sorry
```
theorem group_theory_lemma This theorem was well-known in the early part of the 20th century sorry line 55 source
Source comment
This theorem was well-known in the early part of the 20th century.

depends on sorry what this means
Statement uses: AddCommGroup, Nat, LT.lt, OfNat.ofNat, Dvd.dvd, Eq, Nat.card, Subtype, Membership.mem, Submodule, Int, Submodule.torsionBy, HPow.hPow, Nonempty, AddEquiv, Fin, ZMod
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
42 instances, coercions and auxiliary constants left out.
```
theorem group_theory_lemma {A : Type*} [AddCommGroup A] {n : ℕ} (hn : 0 < n) (r : ℕ)
    (h : ∀ d : ℕ, d ∣ n → Nat.card (Submodule.torsionBy ℤ A d) = d ^ r) :
    Nonempty ((Submodule.torsionBy ℤ A n) ≃+ (Fin r → (ZMod n))) := sorry
```
theorem WeierstrassCurve.n_torsion_dimension I only need this if n is prime but there's no harm thinking about it in general I guess line 62 source
Source comment
I only need this if n is prime but there's no harm thinking about it in general I guess. It follows from the previous theorem using pure group theory (possibly including the structure theorem for finite abelian groups)

depends on sorry what this means
Statement uses: Field, WeierstrassCurve, WeierstrassCurve.IsElliptic, DecidableEq, IsSepClosed, Nat, Ne, OfNat.ofNat, Nonempty, AddEquiv, WeierstrassCurve.nTorsion, Prod, ZMod, Int, WeierstrassCurve.Affine.Point, WeierstrassCurve.Affine.baseChange, Submodule.torsionBy
Proof uses: Fin, group_theory_lemma, Nat.pos_of_ne_zero, Eq, False.elim, False, Eq.mp, Eq.trans, congrFun', congrArg, Nat.cast_zero, Not, True, eq_self, not_true_eq_false, Dvd.dvd, WeierstrassCurve.n_torsion_card, Mathlib.Tactic.Contrapose.contrapose₄, HMul.hMul, of_eq_true and 7 more
70 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
theorem WeierstrassCurve.n_torsion_dimension [IsSepClosed k] {n : ℕ} (hn : (n : k) ≠ 0) :
    Nonempty (E.nTorsion n ≃+ (ZMod n) × (ZMod n)) := by
…
```
instance (instance at line 74) sorry line 74 source
Source comment
follows easily from the above
```
noncomputable instance (n : ℕ) : Module.Finite (ZMod n) (E.nTorsion n) := by
…
```
def WeierstrassCurve.Points.map The map on points for an elliptic curve over k induced by a morphism of k-algebras is a group homomorphism line 80 source
Source documentation
The map on points for an elliptic curve over k induced by a morphism of k-algebras is a group homomorphism.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, Algebra, DecidableEq, AlgHom, AddMonoidHom, WeierstrassCurve.Affine.Point, WeierstrassCurve.Affine.baseChange
Proof uses: WeierstrassCurve.Affine.Point.map
13 instances, coercions and auxiliary constants left out.
```
noncomputable def WeierstrassCurve.Points.map {K L : Type u} [Field K] [Field L] [Algebra k K]
    [Algebra k L] [DecidableEq K] [DecidableEq L]
    (f : K →ₐ[k] L) : (E⁄K).Point →+ (E⁄L).Point := WeierstrassCurve.Affine.Point.map f
…
```
lemma WeierstrassCurve.Points.map_id line 85 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, DecidableEq, Algebra, Eq, AddMonoidHom, WeierstrassCurve.Affine.Point, WeierstrassCurve.Affine.baseChange, WeierstrassCurve.Points.map, AlgHom.id, AddMonoidHom.id
Proof uses: AddMonoidHom.ext, WeierstrassCurve.Affine.Point.map_id
12 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma WeierstrassCurve.Points.map_comp line 91 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, DecidableEq, Algebra, AlgHom, Eq, AddMonoidHom, WeierstrassCurve.Affine.Point, WeierstrassCurve.Affine.baseChange, AddMonoidHom.comp, WeierstrassCurve.Affine.Point.map, AlgHom.comp
Proof uses: AddMonoidHom.ext, WeierstrassCurve.Affine.Point.map_map
30 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
instance WeierstrassCurve.galoisRepresentationSmul The Galois action on the points of an elliptic curve line 100 source
Source documentation
The Galois action on the points of an elliptic curve.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, WeierstrassCurve, DecidableEq, Algebra, SMul, AlgEquiv, WeierstrassCurve.Affine.Point, WeierstrassCurve.Affine.baseChange
Proof uses: SMul.mk, AddMonoidHom, WeierstrassCurve.Affine.Point.map
16 instances, coercions and auxiliary constants left out.
```
noncomputable instance WeierstrassCurve.galoisRepresentationSmul
    (K : Type u) [Field K] [DecidableEq K] [Algebra k K] :
    SMul (K ≃ₐ[k] K) (E⁄K).Point := ⟨
…
```
instance WeierstrassCurve.galoisRepresentation The Galois action on the points of an elliptic curve sorry line 106 source
Source documentation
The Galois action on the points of an elliptic curve.

depends on sorry what this means
Statement uses: Field, WeierstrassCurve, DecidableEq, Algebra, DistribMulAction, AlgEquiv, WeierstrassCurve.Affine.Point, WeierstrassCurve.Affine.baseChange
Proof uses: DistribMulAction.mk, MulAction.mk, SemigroupAction.mk, sorryAx, Lean.Name, Eq, HSMul.hSMul, HMul.hMul, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat, HAdd.hAdd
39 instances, coercions and auxiliary constants left out.
```
noncomputable instance WeierstrassCurve.galoisRepresentation
    (K : Type u) [Field K] [DecidableEq K] [Algebra k K] :
    DistribMulAction (K ≃ₐ[k] K) (E⁄K).Point where
…
```
instance (instance at line 119) line 119 source
Source documentation
A classical decidable instance on AlgebraicClosure ℚ, given that there is no hope of a constructive one with the current definition of algebraic closure.
```
noncomputable instance : DecidableEq (AlgebraicClosure ℚ) := Classical.typeDecidableEq _
```
def WeierstrassCurve.galoisRep The continuous Galois representation associated to an elliptic curve over a field sorry line 122 source
Source documentation
The continuous Galois representation associated to an elliptic curve over a field.

depends on sorry what this means
Statement uses: Field, WeierstrassCurve, WeierstrassCurve.IsElliptic, DecidableEq, AlgebraicClosure, Nat, LT.lt, OfNat.ofNat, GaloisRep, ZMod, WeierstrassCurve.nTorsion, WeierstrassCurve.map, Algebra.algebraMap, Int, WeierstrassCurve.Affine.Point, WeierstrassCurve.Affine.baseChange, Submodule.torsionBy
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
44 instances, coercions and auxiliary constants left out.
```
def WeierstrassCurve.galoisRep {K : Type u} [Field K] (E : WeierstrassCurve K) [E.IsElliptic]
    [DecidableEq K] [DecidableEq (AlgebraicClosure K)] (n : ℕ) (hn : 0 < n) :
  GaloisRep K (ZMod n) ((E.map (algebraMap K (AlgebraicClosure K))).nTorsion n) := sorry
```
Mentions: GaloisRep, WeierstrassCurve.nTorsion