AnabelianGeometry.not_surjective_open_finiteH1Pullback_intermediate
The intermediate curve inherits its geometry from the original open curve. A nonidentity deck transformation over it forces strict H¹ growth.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicCurve TopologicalSpace
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_intermediate
{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 B : FiniteEtale X) [IsConnected A] [IsConnected B] [ConnectedSpace B.left]
(f : A ⟶ B) [CategoryTheory.PreGaloisCategory.IsGalois (FiniteEtale.mk f.left)]
(σ : 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)