Nyll.AnabelianGeometry.GeometricFundamentalGroup.OpenDeckFaithfulness

Module documentation

Faithfulness of actual finite H¹ on open 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

open_deck_eq_one_of_all_finiteH1_trivial

L28 ↗

AnabelianGeometry.open_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 open 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 open_deck_eq_one_of_all_finiteH1_trivial
    {K F : Type} [Field K] [IsAlgClosed K] [CharZero K]
    [Field F] [Algebra K F]
    (M : CurveModel K F) {X : Scheme}
    [IsIntegral X] [IsNormalIntegral X] [IsLocallyNoetherian X] [CompactSpace X]
    (j : X ⟶ M.C) [IsOpenImmersion j] [QuasiCompact j] [QuasiSeparated j]
    (hboundary : (M.openBoundaryPlaces j).Nonempty)
    (hhyperbolic : 0 <
      2 * (genusFF K F : ℤ) + (M.openBoundaryPlaces_finite j).toFinset.card - 2)
    (A : FiniteEtale X) [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 open hyperbolic deck groups

Declarations

open_deck_eq_one_of_all_finiteH1_trivial