Module

FiniteH1Cardinality.lean

Nyll.JacobianVarieties.Kummer.FiniteH1Cardinality

2 declarations indexed from sourceView source ↗

Module documentation

Genus and the cardinality of actual étale H¹

Actual Kummer cohomology identifies finite-coefficient derived H¹ with divisor torsion. The actual Picard representation, the geometric dimension formula, and multiplication degree compute its cardinality.

Imports5

Imported by3

theorem

natCard_finiteH1_eq_pow_genus

L32 ↗

JacobianVarieties.Kummer.natCard_finiteH1_eq_pow_genus

Documentation

The actual finite-coefficient étale H¹ of a smooth proper curve over an algebraically closed field of characteristic zero has cardinality n^(2g).

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory
open AlgebraicGeometry AlgebraicGeometry.RelPicard AlgebraicCurve
open NeronModelInfra GoodReductionJacobian
open JacobianVarieties.Picard.Proofs.Pic0PointsAbelJacobi.AlgebraicGeometry.RelPicard
namespace JacobianVarieties.Kummer

Lean source · statement

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)
    (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))
    (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₀)

theorem

natCard_finiteH1_eq_pow_genus

L95 ↗

AlgebraicCurve.CurveModel.natCard_finiteH1_eq_pow_genus

Documentation

The genus cardinality formula without a chosen Picard representation or Abel--Jacobi morphism: these are constructed from the curve and its point.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

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

Lean source · statement

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)

Module documentation

Genus and the cardinality of actual étale H¹

Declarations

natCard_finiteH1_eq_pow_genus

natCard_finiteH1_eq_pow_genus