NYLL

theorem · Jacobian varieties

Counting torsion points

An abelian variety of dimension d over an algebraically closed field of characteristic zero has n^(2d) points killed by n.

For a Jacobian, the torsion count is $n^{2g}$, directly linking the genus to the finite groups from which Tate modules are assembled. Their size is a basic input to the study of Galois representations and étale cohomology. Milne's Abelian Varieties derives the count from the degree of multiplication by an integer in Section 8 and explains the passage to prime-power Tate modules.

JacobianVarieties on GitHub ↗

Mathematical statement

Let $K$ be algebraically closed of characteristic $0$. Let $A/K$ carry a commutative relative group law and the source's abelian-scheme properties, with smooth relative dimension $d$. For every integer $n\ge1$,

$$\#A(K)[n]=n^{2d},\qquad A(K)[n]=\{x\in A(K):nx=0\}.$$

Lean code

GoodReductionJacobian.RelativeGroupLaw.natCard_torsionLevel_eq_pow

Published library source ↗Same source in NYLL ↗

theorem natCard_torsionLevel_eq_pow
    {K : Type} [Field K] [IsAlgClosed K] [CharZero K]
    {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of K)}
    (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
    (hA : AbelianSchemePropertyBundle K f)
    (d : ℕ) [SmoothOfRelativeDimension d f] (n : ℕ+) :
    Nat.card (ProCGroups.torsionLevel (G.AlgPoints hc K) n) =
      (n : ℕ) ^ (2 * d)
In-scope Lean context
noncomputable section

open CategoryTheory AlgebraicGeometry NeronModelInfra

open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs

open RelativeGroupLaw_isFinite_endKerStr_and_natCard_eq_endDegree_of_etale.P2mSepKer

namespace GoodReductionJacobian.RelativeGroupLaw
Full declaration and proof
/-- A positive multiplication kernel of a proper smooth commutative group
scheme of dimension `d` has exactly `n ^ (2 * d)` algebraic points in
characteristic zero. -/
theorem natCard_torsionLevel_eq_pow
    {K : Type} [Field K] [IsAlgClosed K] [CharZero K]
    {A : Scheme.{0}} {f : A ⟶ Spec (CommRingCat.of K)}
    (G : RelativeGroupLaw K f) (hc : G.IsCommutative)
    (hA : AbelianSchemePropertyBundle K f)
    (d : ℕ) [SmoothOfRelativeDimension d f] (n : ℕ+) :
    Nat.card (ProCGroups.torsionLevel (G.AlgPoints hc K) n) =
      (n : ℕ) ^ (2 * d) := by
  have : IsProper f := hA.proper
  have hn : ((n : ℕ) : K) ≠ 0 :=
    Nat.cast_ne_zero.mpr (Nat.ne_of_gt n.property)
  have : Etale (G.schemeNsmul (n : ℕ)) :=
    G.etale_schemeNsmul_of_isUnit_of_smoothOfRelativeDimension hc d
      (n : ℕ) (isUnit_iff_ne_zero.mpr hn)
  have : Etale (G.endKerStr (G.nsmul f (n : ℕ) idPoint)) :=
    inferInstanceAs (Etale (G.schemeKerStr (n : ℕ)))
  let e := (G.torsionLevelEquivSchemeKerPoints hc n).trans
    (kerPtsEquiv G (G.nsmul f (n : ℕ) idPoint))
  calc
    Nat.card (ProCGroups.torsionLevel (G.AlgPoints hc K) n) =
        Nat.card (KerPts G (G.nsmul f (n : ℕ) idPoint)) :=
      Nat.card_congr e
    _ = G.endDegree (G.nsmul f (n : ℕ) idPoint) :=
      (G.isFinite_endKerStr_and_natCard_eq_endDegree_of_etale K f
        (G.nsmul f (n : ℕ) idPoint)).2.2
    _ = (n : ℕ) ^ (2 * d) :=
      G.endDegree_nsmul_idPoint_eq_pow_of_natCast_ne_zero K f hc hA d
        (n : ℕ) hn
Source credits and license
Copyright (c) 2026 Naganori Yamaguchi (https://github.com/n-yamaguchi-0729).
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Naganori Yamaguchi (assisted by OpenAI Codex)

References

  1. J. S. Milne. Abelian Varieties. Springer, New York, in Arithmetic Geometry (Storrs, Conn., 1984), Chapter V, 103–150, 1986. Author's revised version dated January 2, 2022; original numbering retained.

Published source: fec50451.

← All selected results in Jacobian varieties