AlgebraicCurve.CurveModel.natCard_open_finiteH1_eq_pow_genus_boundary
The actual derived finite-coefficient H¹ of a smooth open curve with nonempty boundary has cardinality n^(2g+r-1). The comparison is supplied by the actual Kummer covers, not by an assumed cohomology model.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory AlgebraicGeometry NeronModelInfra TopologicalSpace
namespace AlgebraicCurve.CurveModelLean source · statement
theorem natCard_open_finiteH1_eq_pow_genus_boundary
{K F : Type} [Field K] [IsAlgClosed K] [CharZero K]
[Field F] [Algebra K F] [IsCurveOver K F]
(M : CurveModel K F)
(ε : SchemeHomOver (𝟙 (Spec (.of K))) M.toBase)
{X : Scheme} [IsIntegral X] [CompactSpace X]
(j : X ⟶ M.C) [IsOpenImmersion j] (hj : DenseRange j)
[Fintype (M.openBoundaryPlaces j)] (v₀ : M.openBoundaryPlaces j)
(n : ℕ+) {Ω : Type} [Field Ω] [IsSepClosed Ω]
(xi : Spec (.of Ω) ⟶ X) :
Nat.card (Sheaf.H.{0}
((constantSheaf X.smallEtaleTopology AddCommGrpCat.{0}).obj
(AddCommGrpCat.of (Additive (rootsOfUnity (n : ℕ) K)))) 1) =
(n : ℕ) ^ (2 * genusFF K F + Fintype.card (M.openBoundaryPlaces j) - 1)