Finite étale H¹ of a proper curve

Mathematical statement

Let $K$ be algebraically closed of characteristic $0$, and let $C$ be a geometrically integral smooth proper curve model of $F/K$, equipped with a $K$-point and a geometric point. For $n\ge1$,

$$\#H^1_{\mathrm{\acute et}}(C,\underline{\mu_n(K)})=n^{2g(F/K)}.$$

The coefficient object is the constant étale sheaf on the finite abelian group $\mu_n(K)$.

Lean code

`AlgebraicCurve.CurveModel.natCard_finiteH1_eq_pow_genus`

Published library source ↗Same source in NYLL ↗

theorem natCard_finiteH1_eq_pow_genus
    {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)
    (n : ℕ+) {Ω : Type} [Field Ω] [IsSepClosed Ω]
    (ξ : Spec (.of Ω) ⟶ M.C) :
    Nat.card (Sheaf.H.{0}
      ((constantSheaf M.C.smallEtaleTopology AddCommGrpCat.{0}).obj
        (AddCommGrpCat.of (Additive (rootsOfUnity (n : ℕ) K)))) 1) =
      (n : ℕ) ^ (2 * genusFF K F)

In-scope Lean context

noncomputable section

open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory

open AlgebraicGeometry AlgebraicGeometry.RelPicard AlgebraicCurve

open NeronModelInfra GoodReductionJacobian

open JacobianVarieties.Picard.Proofs.Pic0PointsAbelJacobi.AlgebraicGeometry.RelPicard

namespace AlgebraicCurve.CurveModel

Full declaration and proof

/-- The genus cardinality formula without a chosen Picard representation or
Abel--Jacobi morphism: these are constructed from the curve and its point. -/
theorem natCard_finiteH1_eq_pow_genus
    {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)
    (n : ℕ+) {Ω : Type} [Field Ω] [IsSepClosed Ω]
    (ξ : Spec (.of Ω) ⟶ M.C) :
    Nat.card (Sheaf.H.{0}
      ((constantSheaf M.C.smallEtaleTopology AddCommGrpCat.{0}).obj
        (AddCommGrpCat.of (Additive (rootsOfUnity (n : ℕ) K)))) 1) =
      (n : ℕ) ^ (2 * genusFF K F) := by
  obtain ⟨D, hD, aj, hs, hp, hg, _, hclass, _⟩ :=
    M.exists_representsRelSubPic_abelJacobi_of_isAlgClosed K F ε
  have : Smooth D.toBase := hs
  have : IsProper D.toBase := hp
  have : GeometricallyConnected D.toBase := hg
  exact JacobianVarieties.Kummer.natCard_finiteH1_eq_pow_genus
    M ε D hD aj hclass n ξ

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

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.
Alexander Grothendieck et al.. Revêtements étales et groupe fondamental (SGA 1). Springer, Lecture Notes in Mathematics 224, 1971. Link to the updated edition with remarks by Michel Raynaud.