Module

ProperIntermediateH1.lean

Nyll.AnabelianGeometry.GeometricFundamentalGroup.ProperIntermediateH1

1 declaration indexed from sourceView source ↗

Module documentation

Actual intermediate covers of a proper hyperbolic curve

Both intermediate schemes are realized by curve models, with their actual maps and deck transformations transported through proved isomorphism squares. Riemann--Hurwitz and actual finite H¹ cardinality then obstruct surjective pullback. No Galoisness of a chosen model is assumed.

Imports7

Imported by2

theorem

not_surjective_finiteH1Pullback_intermediate

L34 ↗

AnabelianGeometry.not_surjective_finiteH1Pullback_intermediate

Documentation

A map between actual connected finite étale covers of a proper hyperbolic curve, admitting a nonidentity deck transformation, cannot induce surjective pullback on actual nontrivial roots-of-unity H¹.

Source context 5 commands

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

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

Lean source · statement

theorem not_surjective_finiteH1Pullback_intermediate
    {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 B : FiniteEtale M.C) [IsConnected A] [IsConnected B]
    (f : A ⟶ B) (σ : Aut (FiniteEtale.mk f.left)) (hσ : σ ≠ 1)
    (n : ℕ+) (hn : 1 < (n : ℕ))
    {Ω : Type} [Field Ω] [IsSepClosed Ω]
    (geom : Spec (.of Ω) ⟶ A.left) :
    ¬ Function.Surjective (constantCohomologyPullback f.left
      (AddCommGrpCat.of (Additive (rootsOfUnity (n : ℕ) K))) 1)

Module documentation

Actual intermediate covers of a proper hyperbolic curve

Declarations

not_surjective_finiteH1Pullback_intermediate