NYLL

theorem · Jacobian varieties

Abel–Jacobi and the full Tate module

Under explicit Picard representation and class-compatibility hypotheses, Abel–Jacobi identifies the abelianized fundamental group with the full Tate module.

The compatibility with Abel–Jacobi identifies the geometric morphism that carries abelian covering data into compatible systems of torsion points. It gives a link between covering theory and the Jacobian's torsion beyond an abstract group isomorphism. Milne's Abelian Varieties, Section 15, describes the fundamental-group/Tate-module comparison for abelian varieties, which combines here with the Jacobian's description of abelian covers of a curve.

JacobianVarieties on GitHub ↗

Mathematical statement

Let $C/K$ be a geometrically integral smooth proper curve model over an algebraically closed field of characteristic $0$, with base point $P$. Supply a smooth proper geometrically connected object $J$ representing the designated degree-zero relative Picard functor, and a morphism $a:C\to J$ whose Poincaré pullbacks give the classes $\mathcal O(Q-P)$ after field extensions.

For every geometric point $\xi$ of $C$, the theorem constructs a continuous group isomorphism

$$e:\pi_1^{\mathrm{\acute et}}(C,\xi)^{\mathrm{ab}}\xrightarrow{\sim}T(J),$$

where $T(J)=\varprojlim_n J(K)[n]$ is the full Tate module. It also proves that $e$ agrees with the map induced by $a$ followed by the fundamental-group/Tate comparison for $J$.

Lean code

JacobianVarieties.Kummer.exists_abelJacobi_fullTate_equiv

Published library source ↗Same source in NYLL ↗

theorem exists_abelJacobi_fullTate_equiv
    {K F₀ : Type} [Field K] [IsAlgClosed K] [CharZero K]
    [Field F₀] [Algebra K F₀] [IsCurveOver K F₀]
    (M₀ : CurveModel K F₀)
    [GeometricallyIntegral M₀.toBase]
    (ε : SchemeHomOver (𝟙 (Spec (.of K))) M₀.toBase)
    (D : RelativePic0Designation K M₀.toBase)
    (hD : RepresentsRelSubPic M₀.toBase ε (algEquivZeroCut M₀.toBase ε) D)
    [Smooth D.toBase] [IsProper D.toBase] [GeometricallyConnected D.toBase]
    (aj : SchemeHomOver M₀.toBase D.toBase)
    (hclass : ∀ (L : Type) [Field L] (t : Spec (.of L) ⟶ Spec (.of K))
      (x : SchemeHomOver t M₀.toBase),
      Nonempty ((hD.poincare.pullbackAlong
        ⟨x.1 ≫ aj.1, (Category.assoc _ _ _).trans
          ((congrArg (x.1 ≫ ·) aj.2).trans x.2)⟩).L ≅
        (RelEffCartierDiv.ofPoint M₀.toBase x.1 x.2).lineBundle ⊗
          (RelEffCartierDiv.ofPoint M₀.toBase (t ≫ ε.1)
            ((Category.assoc _ _ _).trans
              ((congrArg (t ≫ ·) ε.2).trans (Category.comp_id t)))).idealModule))
 :
    let G := RepresentsRelSubPic.relativeGroupLaw
      (P := algEquivZeroGroupCut M₀.toBase ε) hD
    let hc : G.IsCommutative := RepresentsRelSubPic.relativeGroupLaw_isCommutative
      (P := algEquivZeroGroupCut M₀.toBase ε) hD
    ∀ (Ω : Type) [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ M₀.C),
      ∃ e : TopologicalAbelianization (Aut (FiniteEtale.fiber ξ)) ≃ₜ*
          Multiplicative (ProCGroups.FullTateModule (G.AlgPoints hc K)),
        ∀ γ : Aut (FiniteEtale.fiber ξ),
          e (ProCGroups.Abelian.TopologicalAbelianization.mk _ γ) =
            G.fundamentalGroupEquivFullTateAt hc (ξ ≫ aj.1)
              (FiniteEtale.fundamentalGroupHom aj.1 ξ γ) := by
  intro G hc Ω hΩ hsep ξ
  have : ConnectedSpace D.P :=
    GeometricallyConnected.connectedSpace D.toBase D.toBase.isOpenMap
  let eT := G.fundamentalGroupEquivFullTateAt hc (ξ ≫ aj.1)
  have : IsMulCommutative (Aut (FiniteEtale.fiber (ξ ≫ aj.1))) :=
    ⟨⟨fun a b => eT.injective
      ((eT.map_mul a b).trans ((mul_comm (eT a) (eT b)).trans
        (eT.map_mul b a).symm))⟩⟩
  let f := ProCGroups.Abelian.TopologicalAbelianization.lift
    (FiniteEtale.fundamentalGroupHom aj.1 ξ)
  have hf (n : ℕ+) :
      let : TopologicalSpace (rootsOfUnity (n : ℕ) K) := ⊥
      let : DiscreteTopology (rootsOfUnity (n : ℕ) K) := ⟨rfl⟩
      Function.Bijective (f.compLeft (rootsOfUnity (n : ℕ) K)) := by
    intro htop hdiscrete
    have hn : IsUnit ((n : ℕ) : K) := isUnit_iff_ne_zero.mpr
      (Nat.cast_ne_zero.mpr n.ne_zero)
    let A := AddCommGrpCat.of (Additive (rootsOfUnity (n : ℕ) K))
    exact (bijective_constantH1Pullback_iff_abelianCharacterPullback aj.1 A ξ).mp
      (abelJacobi_finiteH1Pullback_bijective M₀ ε D hD aj hclass n hn)
  have : TotallyDisconnectedSpace
      (TopologicalAbelianization (Aut (FiniteEtale.fiber ξ))) :=
    ProCGroups.totallyDisconnectedSpace_quotient_closedNormal
      (Subgroup.closedCommutator (Aut (FiniteEtale.fiber ξ)))
      (Subgroup.isClosed_closedCommutator _)
  let e := ProCGroups.Duality.equivOfBijectiveRootsOfUnityPullback K f hf
  refine ⟨e.trans eT, ?_⟩
  intro γ
  change eT (f (ProCGroups.Abelian.TopologicalAbelianization.mk _ γ)) = _
  rw [ProCGroups.Abelian.TopologicalAbelianization.lift_apply_mk]
In-scope Lean context
noncomputable section

open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory

open AlgebraicGeometry AlgebraicGeometry.RelPicard

open AlgebraicCurve NeronModelInfra GoodReductionJacobian

open scoped IsMulCommutative

namespace JacobianVarieties.Kummer
Full declaration and proof
/-- Actual Abel--Jacobi induces the full Tate isomorphism on the
topological abelianization, with its original quotient map. -/
theorem exists_abelJacobi_fullTate_equiv
    {K F₀ : Type} [Field K] [IsAlgClosed K] [CharZero K]
    [Field F₀] [Algebra K F₀] [IsCurveOver K F₀]
    (M₀ : CurveModel K F₀)
    [GeometricallyIntegral M₀.toBase]
    (ε : SchemeHomOver (𝟙 (Spec (.of K))) M₀.toBase)
    (D : RelativePic0Designation K M₀.toBase)
    (hD : RepresentsRelSubPic M₀.toBase ε (algEquivZeroCut M₀.toBase ε) D)
    [Smooth D.toBase] [IsProper D.toBase] [GeometricallyConnected D.toBase]
    (aj : SchemeHomOver M₀.toBase D.toBase)
    (hclass : ∀ (L : Type) [Field L] (t : Spec (.of L) ⟶ Spec (.of K))
      (x : SchemeHomOver t M₀.toBase),
      Nonempty ((hD.poincare.pullbackAlong
        ⟨x.1 ≫ aj.1, (Category.assoc _ _ _).trans
          ((congrArg (x.1 ≫ ·) aj.2).trans x.2)⟩).L ≅
        (RelEffCartierDiv.ofPoint M₀.toBase x.1 x.2).lineBundle ⊗
          (RelEffCartierDiv.ofPoint M₀.toBase (t ≫ ε.1)
            ((Category.assoc _ _ _).trans
              ((congrArg (t ≫ ·) ε.2).trans (Category.comp_id t)))).idealModule))
 :
    let G := RepresentsRelSubPic.relativeGroupLaw
      (P := algEquivZeroGroupCut M₀.toBase ε) hD
    let hc : G.IsCommutative := RepresentsRelSubPic.relativeGroupLaw_isCommutative
      (P := algEquivZeroGroupCut M₀.toBase ε) hD
    ∀ (Ω : Type) [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ M₀.C),
      ∃ e : TopologicalAbelianization (Aut (FiniteEtale.fiber ξ)) ≃ₜ*
          Multiplicative (ProCGroups.FullTateModule (G.AlgPoints hc K)),
        ∀ γ : Aut (FiniteEtale.fiber ξ),
          e (ProCGroups.Abelian.TopologicalAbelianization.mk _ γ) =
            G.fundamentalGroupEquivFullTateAt hc (ξ ≫ aj.1)
              (FiniteEtale.fundamentalGroupHom aj.1 ξ γ) := by
  intro G hc Ω hΩ hsep ξ
  have : ConnectedSpace D.P :=
    GeometricallyConnected.connectedSpace D.toBase D.toBase.isOpenMap
  let eT := G.fundamentalGroupEquivFullTateAt hc (ξ ≫ aj.1)
  have : IsMulCommutative (Aut (FiniteEtale.fiber (ξ ≫ aj.1))) :=
    ⟨⟨fun a b => eT.injective
      ((eT.map_mul a b).trans ((mul_comm (eT a) (eT b)).trans
        (eT.map_mul b a).symm))⟩⟩
  let f := ProCGroups.Abelian.TopologicalAbelianization.lift
    (FiniteEtale.fundamentalGroupHom aj.1 ξ)
  have hf (n : ℕ+) :
      let : TopologicalSpace (rootsOfUnity (n : ℕ) K) := ⊥
      let : DiscreteTopology (rootsOfUnity (n : ℕ) K) := ⟨rfl⟩
      Function.Bijective (f.compLeft (rootsOfUnity (n : ℕ) K)) := by
    intro htop hdiscrete
    have hn : IsUnit ((n : ℕ) : K) := isUnit_iff_ne_zero.mpr
      (Nat.cast_ne_zero.mpr n.ne_zero)
    let A := AddCommGrpCat.of (Additive (rootsOfUnity (n : ℕ) K))
    exact (bijective_constantH1Pullback_iff_abelianCharacterPullback aj.1 A ξ).mp
      (abelJacobi_finiteH1Pullback_bijective M₀ ε D hD aj hclass n hn)
  have : TotallyDisconnectedSpace
      (TopologicalAbelianization (Aut (FiniteEtale.fiber ξ))) :=
    ProCGroups.totallyDisconnectedSpace_quotient_closedNormal
      (Subgroup.closedCommutator (Aut (FiniteEtale.fiber ξ)))
      (Subgroup.isClosed_closedCommutator _)
  let e := ProCGroups.Duality.equivOfBijectiveRootsOfUnityPullback K f hf
  refine ⟨e.trans eT, ?_⟩
  intro γ
  change eT (f (ProCGroups.Abelian.TopologicalAbelianization.mk _ γ)) = _
  rw [ProCGroups.Abelian.TopologicalAbelianization.lift_apply_mk]
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. Jacobian Varieties. Springer, New York, in Arithmetic Geometry (Storrs, Conn., 1984), Chapter VII, 167–212, 1986. Author's revised version dated June 12, 2021; original numbering retained.
  2. 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