AnabelianGeometry.WeightFiltration.finiteH1Pullback_genericPoint
The actual generic-point square induces the corresponding commutative square on derived finite-coefficient H¹.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicGeometry CategoryTheory EtaleFundamentalGroups.Cohomology
namespace AnabelianGeometry.WeightFiltrationLean source · statement
theorem finiteH1Pullback_genericPoint
{X Y : Scheme} [IsIntegral X] [IsIntegral Y]
(f : X ⟶ Y) (hf : DenseRange f)
{Ω : Type} [Field Ω] [IsSepClosed Ω]
(η : Spec (.of Ω) ⟶ Spec (.of X.functionField))
(A : AddCommGrpCat.{0}) [Finite A]
(a : Sheaf.H.{0} ((constantSheaf Y.smallEtaleTopology AddCommGrpCat.{0}).obj A) 1) :
constantCohomologyPullback (X.fromSpecStalk (genericPoint X)) A 1
(constantCohomologyPullback f A 1 a) =
constantCohomologyPullback (Spec.map (CommRingCat.ofHom (f.functionFieldMap hf))) A 1
(constantCohomologyPullback (Y.fromSpecStalk (genericPoint Y)) A 1 a)