EtaleFundamentalGroups.Cohomology.constantFiniteH1Pullback_comp
Actual derived finite-coefficient H¹ pullback is contravariantly compatible with composition of connected scheme morphisms.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory AlgebraicGeometry
namespace EtaleFundamentalGroups.CohomologyLean source · statement
theorem constantFiniteH1Pullback_comp
{X Y Z : Scheme} [ConnectedSpace X] [ConnectedSpace Y] [ConnectedSpace Z]
(f : X ⟶ Y) (g : Y ⟶ Z)
{Ω : Type} [Field Ω] [IsSepClosed Ω]
(geom : Spec (.of Ω) ⟶ X) (A : AddCommGrpCat.{0}) [Finite A]
(c : Sheaf.H.{0} ((constantSheaf Z.smallEtaleTopology AddCommGrpCat.{0}).obj A) 1) :
constantCohomologyPullback (f ≫ g) A 1 c =
constantCohomologyPullback f A 1 (constantCohomologyPullback g A 1 c)