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

3 declarations, 3 contain sorry, 0 declared as axioms

Good reduction implies flat torsion

Let E be an elliptic curve over the field of fractions K of a discrete valuation ring R, suppose that E has good reduction over R, and let n ≥ 1 be a natural number. Then the n-torsion of E "is a finite flat group scheme": the Galois module E(Kˢᵉᵖ)[n] is, Galois-equivariantly, the group of Kˢᵉᵖ-points of the generic fibre of a finite flat group scheme over R.

Mathlib has no group schemes, so we speak throughout of the (commutative) Hopf algebra of functions on the group scheme instead: the statement below produces a commutative Hopf algebra H over R, finite and flat as an R-module (R is a DVR, so this says finite free; over a general base the right condition is finite locally free), together with a Galois-equivariant isomorphism of groups from the Kˢᵉᵖ-points K ⊗[R] H →ₐ[K] Kˢᵉᵖ of its generic fibre (a group under convolution, K ⊗[R] H being a Hopf algebra over K) to the n-torsion subgroup of E(Kˢᵉᵖ).

Mathematical discussion: what is the correct generality?

Good reduction means that the minimal Weierstrass equation of E has unit discriminant over R, so it defines an elliptic scheme (an abelian scheme of relative dimension 1) 𝓔 over R with generic fibre E. Multiplication by n on an elliptic scheme is a finite locally free morphism of degree n² for every n ≥ 1 [Katz–Mazur, Arithmetic moduli of elliptic curves, Theorem 2.3.1], so its kernel 𝓔[n] is a finite flat group scheme over R of order n² with generic fibre E[n]. This is the robust form of the statement: it holds for every n over any DVR (indeed over any base scheme), in every characteristic.

The statement formalised below is instead about the Galois module E(Kˢᵉᵖ)[n], because mathlib cannot yet express E[n] as a group scheme. How the two statements compare depends on whether n is invertible in K:

If n is invertible in K then E[n] is a finite étale group scheme over K of order n². It is therefore determined by its Galois module of Kˢᵉᵖ-points, which is free of rank 2 over ℤ/nℤ, and the statement below carries the full content of the group-scheme statement.
If K has characteristic p and p ∣ n then E[n] is not étale, and E(Kˢᵉᵖ)[n] sees only its maximal étale quotient (for n = p: a group of order p if the reduction is ordinary and of order 1 if it is supersingular). The statement below should still be true — for H one can take the Cartier dual of the schematic closure in 𝓔[n] of the Cartier dual of the maximal étale quotient of E[n] — but it is strictly weaker than flatness of E[n] itself. The honest statement in this case is the group-scheme statement of the previous paragraph, which cannot yet be formalised.

Which values of n make flatness interesting? Let p denote the characteristic of the residue field of R.

If n is invertible in the residue field then the conclusion is equivalent to the Galois module E(Kˢᵉᵖ)[n] being unramified, which is the statement of FLT.KnownIn1980s.EllipticCurves.GoodReduction. Indeed, the order of a finite flat group scheme kills its module of invariant differentials [Tate, Finite flat group schemes, in Modular forms and Fermat's Last Theorem], so a finite flat group scheme over R whose order is invertible in R is unramified over R, hence finite étale; and finite étale group schemes over R are the same thing as unramified Galois modules, via normalization. In particular "unramified implies flat" holds for any finite abelian Galois module of order invertible in the residue field, for reasons having nothing to do with elliptic curves.
The interesting case is therefore p > 0 and p ∣ n, where flatness is genuinely stronger than anything expressible via ramification: for K of characteristic zero (e.g. a finite extension of ℚ_p) and n = p, this is the sense in which "ρ is flat at p" is used for mod p representations in [Serre, Sur les représentations modulaires de degré 2 de Gal(ℚ̄/ℚ), Duke Math. J. 54 (1987), §2.8] and in the modularity lifting literature, and it matches the definition GaloisRep.IsFlatAt in FLT.Deformations.RepresentationTheory.GaloisRep (stated there for number fields; the theorem below is the local statement feeding into it). Note that flat does not imply unramified here: the p-torsion of a curve with good reduction is flat but in general highly ramified at p.

The Algebra.Etale K (K ⊗[R] H) condition below pins down the generic fibre as the finite étale group scheme attached to the Galois module E(Kˢᵉᵖ)[n] (in particular it forces the R-rank of H to equal the number of n-torsion points). It is automatic when K has characteristic zero, by Cartier's theorem that finite group schemes in characteristic zero are étale, and it is what makes the equivalence "flat ⟺ unramified" above honest; compare the corresponding condition in GaloisRep.HasFlatProlongationAt.

TODO

FLT.GroupScheme.FiniteFlat plans a definition of what it means for an action of Gal(Kˢᵉᵖ/K) on a finite abelian group to be flat, for K the field of fractions of a DVR. Once that definition exists, the conclusion below should be refactored to "the Galois module E(Kˢᵉᵖ)[n] is flat".
Once E[n] can be expressed as a group scheme (equivalently, once its Hopf algebra of functions is available), state the stronger result that E[n] itself, not just its Galois module of points, prolongs to a finite flat group scheme over R; as explained above, this is insensitive to the characteristic of K.
Prove the division polynomial lemmas at the bottom of this file (WeierstrassCurve.resultant_Φ_ΨSq and WeierstrassCurve.isCoprime_Φ_ΨSq), which isolate the arithmetic input to the theorem as a purely polynomial statement.

Imports (7)

Imported by 1 file

FLT.lean

theorem WeierstrassCurve.torsion_flat_of_good_reduction Documented declaration: torsion_flat_of_good_reduction sorry line 144 source
Source documentation
If E is an elliptic curve over the field of fractions K of a discrete valuation ring R with good reduction over R, then the n-torsion of E is a finite flat group scheme: there is a commutative Hopf algebra H over R, finite and flat as an R-module, whose generic fibre K ⊗[R] H is étale over K and whose group of Kˢᵉᵖ-points (a group under convolution) is isomorphic, compatibly with the actions of Gal(Kˢᵉᵖ/K) on the two sides, to the n-torsion subgroup of E(Kˢᵉᵖ).

depends on sorry what this means
Statement uses: CommRing, IsDomain, IsDiscreteValuationRing, Field, Algebra, IsFractionRing, WeierstrassCurve, WeierstrassCurve.IsElliptic, WeierstrassCurve.HasGoodReduction, Nat, NeZero, IsSepClosure, DecidableEq, Exists, HopfAlgebra, Module.Finite, Module.Flat, Algebra.Etale, TensorProduct, AddEquiv and 18 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
87 instances, coercions and auxiliary constants left out.
```
theorem WeierstrassCurve.torsion_flat_of_good_reduction :
    -- There is a commutative Hopf algebra H over R (the functions on a group scheme over R),
    ∃ (H : Type u) (_ : CommRing H) (_ : HopfAlgebra R H)
      -- finite and flat as an R-module (so the group scheme is finite flat),
      (_ : Module.Finite R H) (_ : Module.Flat R H)
      -- whose generic fibre K ⊗[R] H is étale over K,
      (_ : Algebra.Etale K (K ⊗[R] H))
      -- together with an isomorphism of groups from the Kˢᵉᵖ-points of the generic fibre
      -- (a group under convolution, because K ⊗[R] H is a Hopf algebra over K)
      -- to the n-torsion subgroup of E(Kˢᵉᵖ),
      (f : Additive (WithConv (K ⊗[R] H →ₐ[K] Ksep)) ≃+
        AddSubgroup.torsionBy (E⁄Ksep).Point (n : ℤ)),
…
```
theorem WeierstrassCurve.resultant_Φ_ΨSq The resultant of the division polynomials Φ n (taken with degree n²) and ΨSq n (taken with degree n² - 1) is ±Δ ^ ((n⁴ - n²)/6) sorry line 223 source
Source documentation
The resultant of the division polynomials Φ n (taken with degree n²) and ΨSq n (taken with degree n² - 1) is ±Δ ^ ((n⁴ - n²)/6). The sign presumably depends on n and on the conventions in Polynomial.resultant; whoever proves this should pin it down and upgrade the statement.

depends on sorry what this means
Statement uses: CommRing, WeierstrassCurve, Int, Ne, OfNat.ofNat, Or, Eq, Polynomial.resultant, WeierstrassCurve.Φ, WeierstrassCurve.ΨSq, HPow.hPow, Nat, Int.natAbs, HSub.hSub, WeierstrassCurve.Δ, HDiv.hDiv, Neg.neg
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
40 instances, coercions and auxiliary constants left out.
```
theorem WeierstrassCurve.resultant_Φ_ΨSq {R₀ : Type*} [CommRing R₀] (W : WeierstrassCurve R₀)
    {n : ℤ} (hn : n ≠ 0) :
    (W.Φ n).resultant (W.ΨSq n) (n.natAbs ^ 2) (n.natAbs ^ 2 - 1) =
        W.Δ ^ ((n.natAbs ^ 4 - n.natAbs ^ 2) / 6) ∨
      (W.Φ n).resultant (W.ΨSq n) (n.natAbs ^ 2) (n.natAbs ^ 2 - 1) =
        -W.Δ ^ ((n.natAbs ^ 4 - n.natAbs ^ 2) / 6) :=
…
```
theorem WeierstrassCurve.isCoprime_Φ_ΨSq Documented declaration: isCoprime_Φ_ΨSq sorry line 238 source
Source documentation
If the discriminant of a Weierstrass curve over a commutative ring is a unit then the division polynomials Φ n and ΨSq n are coprime, i.e. there is a Bézout identity F * Φ n + G * ΨSq n = 1. This is the form of the resultant identity that the applications consume. It follows from resultant_Φ_ΨSq, because the resultant lies in the ideal generated by the two polynomials and is a unit here; note also that it is stable under base change, so it suffices to prove it for the universal Weierstrass curve over ℤ[a₁, …, a₆][Δ⁻¹].

depends on sorry what this means
Statement uses: CommRing, WeierstrassCurve, Int, Ne, OfNat.ofNat, IsUnit, WeierstrassCurve.Δ, IsCoprime, Polynomial, WeierstrassCurve.Φ, WeierstrassCurve.ΨSq
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat
11 instances, coercions and auxiliary constants left out.
```
theorem WeierstrassCurve.isCoprime_Φ_ΨSq {R₀ : Type*} [CommRing R₀] (W : WeierstrassCurve R₀)
    {n : ℤ} (hn : n ≠ 0) (hΔ : IsUnit W.Δ) :
    IsCoprime (W.Φ n) (W.ΨSq n) :=
…
```