AnabelianGeometry.not_surjective_open_finiteH1Pullback
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicCurve TopologicalSpace NeronModelInfra
open CategoryTheory.PreGaloisCategory EtaleFundamentalGroups
open EtaleFundamentalGroups.Cohomology
namespace AnabelianGeometry
attribute [local instance] CurveModel.isIntegral CurveModel.isProper CurveModel.smoothLean source · statement
theorem not_surjective_open_finiteH1Pullback
{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)
(W : FiniteEtale X) [IsGalois W] (σ : Aut W) (hσ : σ ≠ 1)
(n : ℕ+) (hn : 1 < (n : ℕ))
{Ω : Type} [Field Ω] [IsSepClosed Ω] (geom : Spec (.of Ω) ⟶ W.left) :
¬ Function.Surjective (constantCohomologyPullback (X := W.left) (Y := X) W.hom
(AddCommGrpCat.of (Additive (rootsOfUnity (n : ℕ) K))) 1)