AnabelianGeometry.WeightFiltration.finiteH1Pullback_genericPoint_injective
On a normal integral scheme, the actual generic-point pullback on finite constant-coefficient H¹ is injective.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.PreGaloisCategory
open EtaleFundamentalGroups.Cohomology JacobianVarieties.Kummer
namespace AnabelianGeometry.WeightFiltrationLean source · statement
theorem finiteH1Pullback_genericPoint_injective
(X : Scheme) [IsIntegral X] [IsNormalIntegral X]
(Ω : Type) [Field Ω] [Algebra X.functionField Ω]
[IsSepClosed Ω] [IsSepClosure X.functionField Ω]
(A : AddCommGrpCat.{0}) [Finite A] :
Function.Injective (constantCohomologyPullback
(X.fromSpecStalk (genericPoint X)) A 1)