Module

ProperCurveH1Deck.lean

Nyll.AnabelianGeometry.GeometricFundamentalGroup.ProperCurveH1Deck

2 declarations indexed from sourceView source ↗

Module documentation

Nontrivial deck action from proper hyperbolic geometry

Riemann--Hurwitz makes the genus strictly increase in a nontrivial finite étale cover of a proper hyperbolic curve. Actual finite-coefficient H¹ therefore cannot all descend. For a Galois cover, the proved transfer and deck comparison then exhibit a class moved by an actual deck transformation.

This is a nontriviality theorem for the whole deck action. Faithfulness of each nonidentity deck transformation additionally requires applying this argument to the quotient by its cyclic subgroup.

Imports4

Imported by2

theorem

not_surjective_finiteH1Pullback_of_hyperbolic

L52 ↗

AnabelianGeometry.not_surjective_finiteH1Pullback_of_hyperbolic

Documentation

Pullback is not surjective on actual finite-coefficient H¹ for a nontrivial finite étale cover of a proper curve of genus at least two.

Source context 8 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicCurve NeronModelInfra
open CategoryTheory.PreGaloisCategory
open EtaleFundamentalGroups.Cohomology
open JacobianVarieties.Picard.Proofs.Pic0PointsAbelJacobi.AlgebraicGeometry.RelPicard
namespace AnabelianGeometry
variable {K F E : Type} [Field K] [IsAlgClosed K] [CharZero K]
  [Field F] [Field E] [Algebra K F] [Algebra K E]
  [IsCurveOver K F] [IsCurveOver K E]
  (M : CurveModel K F) (N : CurveModel K E)
  [GeometricallyIntegral M.toBase] [GeometricallyIntegral N.toBase]
  (εM : SchemeHomOver (𝟙 (Spec (.of K))) M.toBase)
  (εN : SchemeHomOver (𝟙 (Spec (.of K))) N.toBase)
  (d : N.C ⟶ M.C) (hd : d ≫ M.toBase = N.toBase)
  [IsFiniteEtale d]
  (hg : 2 ≤ genusFF K F)
  (hdeg : 1 < finrankAlong K (M.finiteEtaleFieldMap N d hd))
  (n : ℕ+) (hn : 1 < (n : ℕ))
  {Ω : Type} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ N.C)
include εM εN hd hg hdeg hn ξ

Lean source · statement

theorem not_surjective_finiteH1Pullback_of_hyperbolic :
    ¬ Function.Surjective (constantCohomologyPullback d
      (AddCommGrpCat.of (Additive (rootsOfUnity (n : ℕ) K))) 1)

theorem

exists_deck_moves_finiteH1

L80 ↗

AnabelianGeometry.exists_deck_moves_finiteH1