Nyll.AnabelianGeometry.GeometricFundamentalGroup.ProperDeckFaithfulness

Module documentation

Faithfulness of actual finite H¹ on proper hyperbolic deck groups

A nonidentity element would yield its actual cyclic intermediate cover. Choosing coefficients after constructing that cover avoids any coprimality assumption. Transfer would make all H¹ descend, contradicting the geometric genus and cohomology cardinality calculation.

theorem

deck_eq_one_of_all_finiteH1_trivial

L28 ↗

AnabelianGeometry.deck_eq_one_of_all_finiteH1_trivial

Documentation

The joint action of the actual deck group on actual finite-coefficient derived H¹ has trivial kernel for a proper hyperbolic curve.

Source context 4 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicCurve
open CategoryTheory.PreGaloisCategory EtaleFundamentalGroups.Cohomology
namespace AnabelianGeometry

Lean source · statement

theorem deck_eq_one_of_all_finiteH1_trivial
    {K F : Type} [Field K] [IsAlgClosed K] [CharZero K]
    [Field F] [Algebra K F] [IsCurveOver K F]
    (M : CurveModel K F) (hg : 2 ≤ genusFF K F)
    (A : FiniteEtale M.C) [CategoryTheory.PreGaloisCategory.IsGalois A]
    {Ω : Type} [Field Ω] [IsSepClosed Ω]
    (geom : Spec (.of Ω) ⟶ A.left) (σ : Aut A)
    (hσ : ∀ (C : AddCommGrpCat.{0}) [Finite C] c,
      constantCohomologyPullback σ.hom.left C 1 c = c) :
    σ = 1

Module documentation

Faithfulness of actual finite H¹ on proper hyperbolic deck groups

Declarations

deck_eq_one_of_all_finiteH1_trivial