59.46 Closed immersions and… to 59.55 Vanishing of finite…
Section59.46 Closed immersions and pushforward#
Section 59.46 of the Stacks Project, Tag 04E1. 4 tags here are carried by 14 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 04FV, a lemma
Tag 04FV in the Stacks Project.
AlgebraicGeometry.exists_span_baseChange_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ClosedImmersionsPushforward/LiftingMorphisms.lean, line 83.
Stacks Project, Tag 04FV. A morphism over a closed subscheme between the base changes of two étale schemes is induced by a span over the original scheme, and the left leg of that span becomes an isomorphism after base change.
theorem exists_span_baseChange_iso
{X Z U U' : Scheme.{u}} (i : Z ⟶ X) [IsClosedImmersion i]
(f : U ⟶ X) (g : U' ⟶ X) [Etale f] [Etale g]
(h : pullback f i ⟶ pullback g i)
(h_over : h ≫ pullback.snd g i = pullback.snd f i) :
∃ (W : Scheme.{u}) (a : W ⟶ U) (b : W ⟶ U')
(hab : a ≫ f = b ≫ g) (_hW : Etale (a ≫ f)),
let aZ : pullback (a ≫ f) i ⟶ pullback f i :=
pullback.lift (pullback.fst (a ≫ f) i ≫ a) (pullback.snd (a ≫ f) i) (by
rw [Category.assoc]
exact pullback.condition)
let bZ : pullback (a ≫ f) i ⟶ pullback g i :=
pullback.lift (pullback.fst (a ≫ f) i ≫ b) (pullback.snd (a ≫ f) i) (by
rw [Category.assoc, ← hab]
exact pullback.condition)
∃ e : pullback (a ≫ f) i ≅ pullback f i,
e.hom = aZ ∧ h = e.inv ≫ bZ
AlgebraicGeometry.Space.exists_isIso_smallBaseChange_map_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ClosedImmersionChartLocalFullness.lean, line 345. The attribute's comment: “for algebraic spaces”.
Stacks 04FV for algebraic spaces. Let
i : Z ⟶ Xbe a closed immersion of algebraic spaces over a schemeS, letUandU'be étale scheme charts ofX, and letφbe a morphism overZbetween their base changes alongi. Then there is an étale scheme chartWofXand a morphism of chartsa : W ⟶ Uwhose base change alongiis an isomorphism and which lies in the image sieve ofφ: the base change ofafollowed byφis the base change of a morphism of chartsW ⟶ U'.The chart
Wis an open subscheme ofU ×_X U'containing the image of the graph ofφ.
theorem exists_isIso_smallBaseChange_map_of_isClosedImmersion
{Z X : AlgebraicSpaces B S hS} (i : Z ⟶ X) (hi : IsClosedImmersion B S hS i.hom)
(U U' : SmallEtale B S hS X.1)
(φ : (smallBaseChange B S hS i hi.rep).obj U ⟶ (smallBaseChange B S hS i hi.rep).obj U') :
∃ (W : SmallEtale B S hS X.1) (a : W ⟶ U),
IsIso ((smallBaseChange B S hS i hi.rep).map a) ∧
((smallBaseChange B S hS i hi.rep).imageSieve φ).arrows a
Tag 04FW, a lemma
Tag 04FW in the Stacks Project.
Stacks.Etale.exists_etale_openCover_isomorphic_pullback_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/LiftAcrossClosedImmersion.lean, line 219.
Stacks Project, Tag 04FW. If
i : Z ⟶ Xis a closed immersion andp : V ⟶ Zis étale, thenVhas a Zariski open cover whose members are, overZ, base changes alongiof étale schemes overX.
theorem exists_etale_openCover_isomorphic_pullback_of_isClosedImmersion
{X Z V : AlgebraicGeometry.Scheme.{u}} (i : Z ⟶ X) [IsClosedImmersion i]
(p : V ⟶ Z) [Etale p] :
∃ (W : Scheme.OpenCover.{max u v, u} V)
(U : W.I₀ → AlgebraicGeometry.Scheme.{u}) (f : ∀ j, U j ⟶ X),
(∀ j, Etale (f j)) ∧
∀ j, ∃ e : W.X j ≅ pullback (f j) i,
e.hom ≫ pullback.snd (f j) i = W.f j ≫ p
Tag 04FX, a lemma
Tag 04FX in the Stacks Project.
AlgebraicGeometry.stalkPushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ClosedImmersionsPushforward/StalkInside.lean, line 504. The attribute's comment: “stalk_pushforward_inside”.
At a geometric point of the closed subscheme, direct image on the small étale site does not change the stalk. This is natural in the sheaf.
public noncomputable def stalkPushforwardIso (B : BigEtaleSite.{u})
{S T : B.Scheme} (i : T ⟶ S) [IsClosedImmersion (B.inclusion.map i)]
(s : GeometricPoint T.1) :
(smallEtaleBaseChange B i).sheafPushforwardContinuous (Type (u + 1))
(SmallEtale.topology B S.1 S.property) (SmallEtale.topology B T.1 T.property) ⋙
sheafToPresheaf (SmallEtale.topology B S.1 S.property) (Type (u + 1)) ⋙
etaleStalkPresheafFunctor B S.1 S.property
(s.map (B.inclusion.map i)) (Type (u + 1)) ≅
sheafToPresheaf (SmallEtale.topology B T.1 T.property) (Type (u + 1)) ⋙
etaleStalkPresheafFunctor B T.1 T.property s (Type (u + 1))
AlgebraicGeometry.stalkPushforwardIso_germ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ClosedImmersionsPushforward/StalkInside.lean, line 563. The attribute's comment: “stalk_pushforward_inside”.
The canonical comparison takes the germ of a section over an étale neighborhood of the image point to the germ of the same section over its base change. The compatibility of the two chosen lifts is expressed by the first pullback projection.
public theorem stalkPushforwardIso_germ (B : BigEtaleSite.{u})
{S T : B.Scheme} (i : T ⟶ S) [IsClosedImmersion (B.inclusion.map i)]
(s : GeometricPoint T.1)
(F : Sheaf (SmallEtale.topology B T.1 T.property) (Type (u + 1)))
(N : (geometricPointFiber B S.1 S.property
(s.map (B.inclusion.map i))).Elements)
(q : (geometricPointFiber B T.1 T.property s).obj
((smallEtaleBaseChange B i).obj N.1))
(hq : q.1 ≫ B.inclusion.map (pullback.fst N.1.obj.hom i) = N.2.1)
(σ : (((smallEtaleBaseChange B i).sheafPushforwardContinuous
(Type (u + 1)) (SmallEtale.topology B S.1 S.property)
(SmallEtale.topology B T.1 T.property)).obj F).obj.obj (Opposite.op N.1)) :
((stalkPushforwardIso B i s).hom.app F).hom
((colimit.ι
((Functor.Elements.π (geometricPointFiber B S.1 S.property
(s.map (B.inclusion.map i)))).op ⋙
(((smallEtaleBaseChange B i).sheafPushforwardContinuous
(Type (u + 1)) (SmallEtale.topology B S.1 S.property)
(SmallEtale.topology B T.1 T.property)).obj F).obj)
(Opposite.op N)).hom σ) =
(colimit.ι
((Functor.Elements.π (geometricPointFiber B T.1 T.property s)).op ⋙
F.obj)
(Opposite.op (Functor.elementsMk _ ((smallEtaleBaseChange B i).obj N.1) q))).hom σ
AlgebraicGeometry.smallEtalePushforward_stalk_unique_of_not_mem_range, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ClosedImmersionsPushforward/StalkOutside.lean, line 142. The attribute's comment: “stalk_pushforward_outside”.
The stalk of the direct image from a closed subscheme is a singleton outside that subscheme.
public theorem smallEtalePushforward_stalk_unique_of_not_mem_range
(B : BigEtaleSite.{u}) {Z X : B.Scheme}
(i : Z ⟶ X) [IsClosedImmersion (B.inclusion.map i)]
(G : Sheaf (SmallEtale.topology B Z.1 Z.property)
(Type (max (u + 1) v)))
(s : GeometricPoint X.1)
(hs : s.hom default ∉ Set.range (B.inclusion.map i).base) :
∃! _ : (etaleStalk B X.1 X.property s
(((smallEtaleBaseChange B i).sheafPushforwardContinuous
(Type (max (u + 1) v))
(SmallEtale.topology B X.1 X.property)
(SmallEtale.topology B Z.1 Z.property)).obj G).obj), True
AlgebraicGeometry.smallEtalePushforwardStalkIsoAb, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SupportedDerivedEquivalence.lean, line 202. The attribute's comment: “stalk of a direct image inside the closed subscheme, abelian sheaves”.
Stacks 04FX for abelian sheaves. At a geometric point of the closed subscheme, direct image of abelian sheaves along a closed immersion does not change the stalk, naturally in the sheaf: base change of pointed étale neighbourhoods is initial, so the two colimits agree.
public def smallEtalePushforwardStalkIsoAb (s : GeometricPoint Z.1) :
(smallEtaleBaseChange B i).sheafPushforwardContinuous AddCommGrpCat.{u + 1}
(SmallEtale.topology B X.1 X.property)
(SmallEtale.topology B Z.1 Z.property) ⋙
sheafToPresheaf (SmallEtale.topology B X.1 X.property) AddCommGrpCat.{u + 1} ⋙
etaleStalkPresheafFunctor B X.1 X.property
(s.map (B.inclusion.map i)) AddCommGrpCat.{u + 1} ≅
sheafToPresheaf (SmallEtale.topology B Z.1 Z.property) AddCommGrpCat.{u + 1} ⋙
etaleStalkPresheafFunctor B Z.1 Z.property s AddCommGrpCat.{u + 1}
Tag 04CA, a proposition
Tag 04CA in the Stacks Project.
AlgebraicGeometry.smallEtaleAdjunction_counit_isIso_abelian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ClosedImmersionsPushforward/AbelianSheafEssentialImage.lean, line 255. The attribute's comment: “left inverse, abelian sheaves”.
Stacks 04CA. The counit of the inverse image/direct image adjunction along a closed immersion is an isomorphism on every abelian sheaf.
public theorem smallEtaleAdjunction_counit_isIso_abelian
(F : Sheaf (SmallEtale.topology B Z.1 Z.property) AddCommGrpCat.{u + 1}) :
IsIso (((smallEtaleBaseChange B i).sheafAdjunctionContinuous AddCommGrpCat.{u + 1}
(SmallEtale.topology B X.1 X.property)
(SmallEtale.topology B Z.1 Z.property)).counit.app F)
AlgebraicGeometry.smallEtalePushforwardCompPullbackIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ClosedImmersionsPushforward/AbelianSheafEssentialImage.lean, line 265. The attribute's comment: “left inverse, abelian sheaves”.
Stacks 04CA. Inverse image along a closed immersion is a left inverse to direct image on abelian sheaves: the counit of the adjunction is a natural isomorphism.
public def smallEtalePushforwardCompPullbackIso :
(smallEtaleBaseChange B i).sheafPushforwardContinuous AddCommGrpCat.{u + 1}
(SmallEtale.topology B X.1 X.property)
(SmallEtale.topology B Z.1 Z.property) ⋙
(smallEtaleBaseChange B i).sheafPullback AddCommGrpCat.{u + 1}
(SmallEtale.topology B X.1 X.property)
(SmallEtale.topology B Z.1 Z.property) ≅
𝟭 (Sheaf (SmallEtale.topology B Z.1 Z.property) AddCommGrpCat.{u + 1})
AlgebraicGeometry.smallEtalePushforward_essImage_iff_abelian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ClosedImmersionsPushforward/AbelianSheafEssentialImage.lean, line 422. The attribute's comment: “part (2): essential image”.
Stacks 04CA, part (2). An abelian sheaf on the small étale site of
Xlies in the essential image of direct image along a closed immersioni : Z ⟶ Xexactly when its support is contained inZ, that is, exactly when its stalk vanishes at every geometric point ofXwhose image missesZ.
public theorem smallEtalePushforward_essImage_iff_abelian
(F : Sheaf (SmallEtale.topology B X.1 X.property) AddCommGrpCat.{u + 1}) :
((smallEtaleBaseChange B i).sheafPushforwardContinuous AddCommGrpCat.{u + 1}
(SmallEtale.topology B X.1 X.property)
(SmallEtale.topology B Z.1 Z.property)).essImage F ↔
SmallEtale.supportSheaf B X.1 X.property F ⊆
Set.range (B.inclusion.map i).base
Stacks.EtaleCohomology.smallEtalePushforwardFullyFaithful, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ClosedImmersionsPushforward/SetSheafEssentialImage.lean, line 148. The attribute's comment: “part (1): fully faithful”.
Direct image of sheaves of sets along a closed immersion is fully faithful.
public def smallEtalePushforwardFullyFaithful {Z X : Scheme.{u}} (i : Z ⟶ X)
[IsClosedImmersion i] :
((smallEtaleBaseChange i).sheafPushforwardContinuous (Type (max (u + 1) v))
(Scheme.smallEtaleTopology X) (Scheme.smallEtaleTopology Z)).FullyFaithful
Stacks.EtaleCohomology.smallEtalePushforwardCompInverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ClosedImmersionsPushforward/SetSheafEssentialImage.lean, line 156. The attribute's comment: “left inverse, sheaves of sets”.
The counit
i^{-1} i_* ⟶ 𝟭of the adjunction is an isomorphism.
public def smallEtalePushforwardCompInverseImageIso {Z X : Scheme.{u}} (i : Z ⟶ X)
[IsClosedImmersion i] :
(smallEtaleBaseChange i).sheafPushforwardContinuous (Type (max (u + 1) v))
(Scheme.smallEtaleTopology X) (Scheme.smallEtaleTopology Z) ⋙
smallEtaleInverseImage.{u, v} i ≅
𝟭 (Sheaf (Scheme.smallEtaleTopology Z) (Type (max (u + 1) v)))
Stacks.EtaleCohomology.smallEtalePushforward_essImage_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ClosedImmersionsPushforward/SetSheafEssentialImage.lean, line 318. The attribute's comment: “part (1): essential image”.
A sheaf of sets on
X_étalelies in the essential image of direct image along a closed immersioni : Z ⟶ Xexactly when its restriction to the open complement ofZis the singleton sheaf.
public theorem smallEtalePushforward_essImage_iff {Z X : Scheme.{u}} (i : Z ⟶ X)
[IsClosedImmersion i] (F : Sheaf (Scheme.smallEtaleTopology X) (Type (max (u + 1) v))) :
((smallEtaleBaseChange i).sheafPushforwardContinuous (Type (max (u + 1) v))
(Scheme.smallEtaleTopology X) (Scheme.smallEtaleTopology Z)).essImage F ↔
Nonempty (IsTerminal ((smallEtaleInverseImage.{u, v} (openComplement i).ι).obj F))
Stacks.EtaleCohomology.smallEtalePushforwardAb_essImage_iff_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/IntegralUniversallyInjectivePushforwardEssImage.lean, line 59. The attribute's comment: “part (2): essential image”.
An abelian sheaf on
W_étaleis a direct image along a closed immersionj : Z ⟶ Wexactly when its restriction to an open subschemeUcomplementary to the image ofjvanishes, that is, exactly when its support is contained inj(Z).
public theorem smallEtalePushforwardAb_essImage_iff_of_isClosedImmersion {Z W : Scheme.{u}}
(j : Z ⟶ W) [IsClosedImmersion j] (U : W.Opens) (hU : (U : Set W) = (Set.range j.base)ᶜ)
(G : Sheaf (smallEtaleTopology W) Ab.{u + 1}) :
(smallEtalePushforwardAb j).essImage G ↔
IsZero (((smallEtaleBaseChange U.ι).sheafPullback Ab.{u + 1}
(smallEtaleTopology W) (smallEtaleTopology U.toScheme)).obj G)
Declarations registered for the tag:
CategoryTheory.Functor.IsCoverDense.full_sheafPushforwardContinuousregistered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/EtaleCohomology/ClosedImmersionsPushforward/AbelianSheafEssentialImage.lean, line 245 (StacksFrontier): “part (2): fully faithful”. References: SGA 4 III (4.1), “i) ⇒ ii)”.CategoryTheory.Functor.IsCoverDense.faithful_sheafPushforwardContinuousregistered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/EtaleCohomology/ClosedImmersionsPushforward/AbelianSheafEssentialImage.lean, line 249 (StacksFrontier): “part (2): fully faithful”.
Sources
Section59.47 Integral universally injective morphisms#
Section 59.47 of the Stacks Project, Tag 04FY. 1 tag here is carried by 8 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 04FZ, a proposition
Tag 04FZ in the Stacks Project.
Stacks.EtaleCohomology.smallEtalePushforwardFullyFaithful_of_integral_universallyInjective, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/IntegralUniversallyInjectivePushforward.lean, line 179. The attribute's comment: “part (1): fully faithful”.
Stacks 04FZ, part (1). Direct image of sheaves of sets along an integral universally injective morphism is fully faithful.
public def smallEtalePushforwardFullyFaithful_of_integral_universallyInjective :
((smallEtaleBaseChange f).sheafPushforwardContinuous (Type (max (u + 1) v))
(smallEtaleTopology Y) (smallEtaleTopology X)).FullyFaithful
Stacks.EtaleCohomology.smallEtalePushforward_essImage_iff_of_integral_universallyInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/IntegralUniversallyInjectivePushforward.lean, line 194. The attribute's comment: “part (1): essential image”.
Stacks 04FZ, part (1). A sheaf of sets on
Y_étalelies in the essential image of direct image along an integral universally injective morphism exactly when its restriction to the open complement off(X)is the singleton sheaf.
public theorem smallEtalePushforward_essImage_iff_of_integral_universallyInjective
(F : Sheaf (smallEtaleTopology Y) (Type (max (u + 1) v))) :
((smallEtaleBaseChange f).sheafPushforwardContinuous (Type (max (u + 1) v))
(smallEtaleTopology Y) (smallEtaleTopology X)).essImage F ↔
Nonempty (IsTerminal
((smallEtaleInverseImage.{u, v} (openComplementRange f).ι).obj F))
Stacks.EtaleCohomology.smallEtalePushforwardCompInverseImageIso_of_integral_universallyInjective, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/IntegralUniversallyInjectivePushforward.lean, line 208. The attribute's comment: “trailing clause for sheaves of sets: left inverse”.
Stacks 04FZ, trailing clause. Inverse image along an integral universally injective morphism is a left inverse to direct image on sheaves of sets.
public def smallEtalePushforwardCompInverseImageIso_of_integral_universallyInjective :
(smallEtaleBaseChange f).sheafPushforwardContinuous (Type (max (u + 1) v))
(smallEtaleTopology Y) (smallEtaleTopology X) ⋙
smallEtaleInverseImage.{u, v} f ≅
𝟭 (Sheaf (smallEtaleTopology X) (Type (max (u + 1) v)))
Stacks.EtaleCohomology.smallEtalePushforwardAbFullyFaithful_of_integral_universallyInjective, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/IntegralUniversallyInjectivePushforward.lean, line 246. The attribute's comment: “part (2): fully faithful”.
Stacks 04FZ, part (2). Direct image of abelian sheaves along an integral universally injective morphism is fully faithful.
public def smallEtalePushforwardAbFullyFaithful_of_integral_universallyInjective :
(smallEtalePushforwardAb f).FullyFaithful
Stacks.EtaleCohomology.smallEtalePushforwardAb_essImage_iff_of_integral_universallyInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/IntegralUniversallyInjectivePushforward.lean, line 268. The attribute's comment: “part (2): essential image”.
Stacks 04FZ, part (2). An abelian sheaf on
Y_étalelies in the essential image of direct image along an integral universally injective morphism exactly when its support is contained inf(X), that is, exactly when its restriction to the open complement off(X)vanishes.
public theorem smallEtalePushforwardAb_essImage_iff_of_integral_universallyInjective
(h04CA : AbelianEssImageClosedImmersion.{u})
(F : Sheaf (smallEtaleTopology Y) Ab.{u + 1}) :
(smallEtalePushforwardAb f).essImage F ↔
IsZero (((smallEtaleBaseChange (openComplementRange f).ι).sheafPullback Ab.{u + 1}
(smallEtaleTopology Y)
(smallEtaleTopology (openComplementRange f).toScheme)).obj F)
Stacks.EtaleCohomology.smallEtalePushforwardAbCompPullbackIso_of_integral_universallyInjective, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/IntegralUniversallyInjectivePushforward.lean, line 288. The attribute's comment: “trailing clause for abelian sheaves: left inverse”.
Stacks 04FZ, trailing clause. Inverse image along an integral universally injective morphism is a left inverse to direct image on abelian sheaves.
public def smallEtalePushforwardAbCompPullbackIso_of_integral_universallyInjective :
smallEtalePushforwardAb f ⋙ (smallEtaleBaseChange f).sheafPullback Ab.{u + 1}
(smallEtaleTopology Y) (smallEtaleTopology X) ≅
𝟭 (Sheaf (smallEtaleTopology X) Ab.{u + 1})
Stacks.EtaleCohomology.smallEtalePushforwardAb_essImage_iff_of_integral_universallyInjective', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/IntegralUniversallyInjectivePushforwardEssImage.lean, line 144. The attribute's comment: “part (2): essential image, with the closed-immersion case supplied by Tag 04CA”.
An abelian sheaf on
Y_étalelies in the essential image of direct image along an integral universally injective morphism exactly when its restriction to the open complement off(X)vanishes.
public theorem smallEtalePushforwardAb_essImage_iff_of_integral_universallyInjective'
(F : Sheaf (smallEtaleTopology Y) Ab.{u + 1}) :
(smallEtalePushforwardAb f).essImage F ↔
IsZero (((smallEtaleBaseChange (openComplementRange f).ι).sheafPullback Ab.{u + 1}
(smallEtaleTopology Y)
(smallEtaleTopology (openComplementRange f).toScheme)).obj F)
Stacks.EtaleCohomology.smallEtalePushforward_fullyFaithful_essImage_leftInverse_of_integral_universallyInjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/IntegralUniversallyInjectivePushforwardEssImage.lean, line 178.
Let
f : X ⟶ Ybe a morphism of schemes which is integral and universally injective. Then (1)f_{small, *} : Sh(X_étale) ⟶ Sh(Y_étale)is fully faithful and its essential image is those sheaves of sets onY_étalewhose restriction toY \ f(X)is isomorphic to*, and (2)f_{small, *} : Ab(X_étale) ⟶ Ab(Y_étale)is fully faithful and its essential image is those abelian sheaves onY_étalewhose support is contained inf(X); and in both casesf_{small}^{-1}is a left inverse tof_{small, *}.The four conjuncts are, in order: part (1), part (2), and the trailing clause for each of the two sheaf categories. The complement
Y \ f(X)is the open subschemeopenComplementRange f, open because an integral morphism is universally closed; being isomorphic to*is being a terminal object of the category of sheaves of sets on that complement; and the support of an abelian sheaf issmallEtaleSupportAb, the set of points ofYat which some geometric stalk of the sheaf is nonzero.
public theorem
smallEtalePushforward_fullyFaithful_essImage_leftInverse_of_integral_universallyInjective :
(((smallEtaleBaseChange f).sheafPushforwardContinuous (Type (max (u + 1) v))
(smallEtaleTopology Y) (smallEtaleTopology X)).Full ∧
((smallEtaleBaseChange f).sheafPushforwardContinuous (Type (max (u + 1) v))
(smallEtaleTopology Y) (smallEtaleTopology X)).Faithful ∧
∀ F : Sheaf (smallEtaleTopology Y) (Type (max (u + 1) v)),
((smallEtaleBaseChange f).sheafPushforwardContinuous (Type (max (u + 1) v))
(smallEtaleTopology Y) (smallEtaleTopology X)).essImage F ↔
Nonempty (IsTerminal
((smallEtaleInverseImage.{u, v} (openComplementRange f).ι).obj F))) ∧
((smallEtalePushforwardAb f).Full ∧ (smallEtalePushforwardAb f).Faithful ∧
∀ F : Sheaf (smallEtaleTopology Y) Ab.{u + 1},
(smallEtalePushforwardAb f).essImage F ↔
smallEtaleSupportAb F ⊆ Set.range f.base) ∧
Nonempty ((smallEtaleBaseChange f).sheafPushforwardContinuous (Type (max (u + 1) v))
(smallEtaleTopology Y) (smallEtaleTopology X) ⋙
smallEtaleInverseImage.{u, v} f ≅
𝟭 (Sheaf (smallEtaleTopology X) (Type (max (u + 1) v)))) ∧
Nonempty (smallEtalePushforwardAb f ⋙ (smallEtaleBaseChange f).sheafPullback Ab.{u + 1}
(smallEtaleTopology Y) (smallEtaleTopology X) ≅
𝟭 (Sheaf (smallEtaleTopology X) Ab.{u + 1}))
Sources
Section59.48 Big sites and pushforward#
Section 59.48 of the Stacks Project, Tag 04E2. 6 tags here are carried by 36 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 04C7, a lemma
Tag 04C7 in the Stacks Project.
AlgebraicGeometry.bigZariskiMorphism_counit_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/MonomorphismCounit.lean, line 90. The attribute's comment: “Zariski case”.
Stacks 04C7, the Zariski case. The inverse-image/direct-image counit is invertible for a monomorphism on the big Zariski site.
public theorem bigZariskiMorphism_counit_isIso
(B : BigZariskiSite.{u}) {X Y : B.Schemes} (f : X ⟶ Y) [Mono f]
(F : Sheaf (BigZariskiOver.topology B X.1 X.2) (Type (u + 1))) :
IsIso ((bigZariskiMorphism B X Y f).adj.counit.app F)
AlgebraicGeometry.bigEtaleMorphism_counit_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/MonomorphismCounit.lean, line 99. The attribute's comment: “étale case”.
Stacks 04C7, the étale case. The inverse-image/direct-image counit is invertible for a monomorphism on the big étale site.
public theorem bigEtaleMorphism_counit_isIso
(B : BigEtaleSite.{u}) {X Y : B.Scheme} (f : X ⟶ Y) [Mono f]
(F : Sheaf (BigEtaleOver.topology B X.1 X.2) (Type (u + 1))) :
IsIso ((bigEtaleMorphism B X Y f).adj.counit.app F)
AlgebraicGeometry.bigSmoothMorphism_counit_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/MonomorphismCounit.lean, line 108. The attribute's comment: “smooth case”.
Stacks 04C7, the smooth case. The inverse-image/direct-image counit is invertible for a monomorphism on the big smooth site.
public theorem bigSmoothMorphism_counit_isIso
(B : BigSmoothSite.{u}) {X Y : B.category} (f : X ⟶ Y) [Mono f]
(F : Sheaf (BigSmoothOver.topology B X.1 X.2) (Type (u + 1))) :
IsIso ((bigSmoothMorphismOfTopoi B f).adj.counit.app F)
AlgebraicGeometry.bigSyntomicMorphism_counit_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/MonomorphismCounit.lean, line 117. The attribute's comment: “syntomic case”.
Stacks 04C7, the syntomic case. The inverse-image/direct-image counit is invertible for a monomorphism on the big syntomic site.
public theorem bigSyntomicMorphism_counit_isIso
(B : BigSyntomicSite.{u}) {X Y : B.category} (f : X ⟶ Y) [Mono f]
(F : Sheaf (BigSyntomicOver.topology B X.1 X.2) (Type (u + 1))) :
IsIso ((bigSyntomicMorphismOfTopoi B f).adj.counit.app F)
AlgebraicGeometry.bigFppfMorphism_counit_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/MonomorphismCounit.lean, line 126. The attribute's comment: “fppf case”.
Stacks 04C7, the fppf case. The inverse-image/direct-image counit is invertible for a monomorphism on the big fppf site.
public theorem bigFppfMorphism_counit_isIso
(B : BigFppfSite.{u}) {X Y : B.Schemes} (f : X ⟶ Y) [Mono f]
(F : Sheaf (B.topology.over X) (Type (u + 1))) :
IsIso ((bigFppfMorphism B X Y f).adj.counit.app F)
Tag 04C8, a remark
Tag 04C8 in the Stacks Project.
AlgebraicGeometry.bigZariskiLowerShriek_unit_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/MonomorphismLowerShriekUnit.lean, line 119. The attribute's comment: “sheaves of sets, Zariski case: the canonical map F → f_big⁻¹ f_big! F is an isomorphism, for the set-level f_big!”.
Stacks 04C8, the Zariski case for sheaves of sets. The lower-shriek/inverse-image unit
F ⟶ f_big⁻¹ f_big! Fis invertible for a monomorphism on the big Zariski site.
public theorem bigZariskiLowerShriek_unit_isIso
(B : BigZariskiSite.{u}) {X Y : B.Schemes} (f : X ⟶ Y) [Mono f]
(F : Sheaf (BigZariskiOver.topology B X.1 X.2) (Type (u + 1))) :
IsIso ((bigZariskiLowerShriekAdjunction B X Y f).unit.app F)
AlgebraicGeometry.bigEtaleLowerShriek_unit_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/MonomorphismLowerShriekUnit.lean, line 131. The attribute's comment: “sheaves of sets, étale case: the canonical map F → f_big⁻¹ f_big! F is an isomorphism, for the set-level f_big!”.
Stacks 04C8, the étale case for sheaves of sets. The lower-shriek/inverse-image unit
F ⟶ f_big⁻¹ f_big! Fis invertible for a monomorphism on the big étale site.
public theorem bigEtaleLowerShriek_unit_isIso
(B : BigEtaleSite.{u}) {X Y : B.Scheme} (f : X ⟶ Y) [Mono f]
(F : Sheaf (BigEtaleOver.topology B X.1 X.2) (Type (u + 1))) :
IsIso ((bigEtaleLowerShriekAdjunction B X Y f).unit.app F)
AlgebraicGeometry.bigSmoothLowerShriek_unit_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/MonomorphismLowerShriekUnit.lean, line 143. The attribute's comment: “sheaves of sets, smooth case: the canonical map F → f_big⁻¹ f_big! F is an isomorphism, for the set-level f_big!”.
Stacks 04C8, the smooth case for sheaves of sets. The lower-shriek/inverse-image unit
F ⟶ f_big⁻¹ f_big! Fis invertible for a monomorphism on the big smooth site.
public theorem bigSmoothLowerShriek_unit_isIso
(B : BigSmoothSite.{u}) {X Y : B.category} (f : X ⟶ Y) [Mono f]
(F : Sheaf (BigSmoothOver.topology B X.1 X.2) (Type (u + 1))) :
IsIso ((Adjunction.ofIsRightAdjoint
(bigSmoothMorphismOfTopoi B f).inverseImage).unit.app F)
AlgebraicGeometry.bigSyntomicLowerShriek_unit_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/MonomorphismLowerShriekUnit.lean, line 169. The attribute's comment: “sheaves of sets, syntomic case: the canonical map F → f_big⁻¹ f_big! F is an isomorphism, for the set-level f_big!”.
Stacks 04C8, the syntomic case for sheaves of sets. The lower-shriek/inverse-image unit
F ⟶ f_big⁻¹ f_big! Fis invertible for a monomorphism on the big syntomic site.
public theorem bigSyntomicLowerShriek_unit_isIso
(B : BigSyntomicSite.{u}) {X Y : B.category} (f : X ⟶ Y) [Mono f]
(F : Sheaf (BigSyntomicOver.topology B X.1 X.2) (Type (u + 1))) :
IsIso ((bigSyntomicLowerShriekAdjunction B f).unit.app F)
AlgebraicGeometry.bigFppfLowerShriek_unit_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/MonomorphismLowerShriekUnit.lean, line 181. The attribute's comment: “sheaves of sets, fppf case: the canonical map F → f_big⁻¹ f_big! F is an isomorphism, for the set-level f_big!”.
Stacks 04C8, the fppf case for sheaves of sets. The lower-shriek/inverse-image unit
F ⟶ f_big⁻¹ f_big! Fis invertible for a monomorphism on the big fppf site.
public theorem bigFppfLowerShriek_unit_isIso
(B : BigFppfSite.{u}) {X Y : B.Schemes} (f : X ⟶ Y) [Mono f]
(F : Sheaf (B.topology.over X) (Type (u + 1))) :
IsIso ((bigFppfLowerShriekAdjunction B X Y f).unit.app F)
AlgebraicGeometry.bigZariskiAbelianLowerShriek_unit_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/MonomorphismLowerShriekUnit.lean, line 200. The attribute's comment: “sheaves of abelian groups, Zariski case: the canonical map F → f_big⁻¹ f_big! F is an isomorphism, where f_big! is the abelian lower shriek of Modules on Sites 04BE, i.e. the left adjoint of f_big⁻¹ on abelian sheaves, not the set-level f_big!”.
Stacks 04C8, the Zariski case for sheaves of abelian groups. The unit
F ⟶ f_big⁻¹ f_big! Fof the abelian lower-shriek adjunction of Modules on Sites 04BE is invertible for a monomorphism on the big Zariski site.
public theorem bigZariskiAbelianLowerShriek_unit_isIso
(B : BigZariskiSite.{u}) {X Y : B.Schemes} (f : X ⟶ Y) [Mono f]
(F : Sheaf (BigZariskiOver.topology B X.1 X.2) AbCat.{u, u + 1}) :
IsIso (((Over.map f).sheafAdjunctionContinuous AbCat.{u, u + 1}
(BigZariskiOver.topology B X.1 X.2)
(BigZariskiOver.topology B Y.1 Y.2)).unit.app F)
AlgebraicGeometry.bigEtaleAbelianLowerShriek_unit_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/MonomorphismLowerShriekUnit.lean, line 214. The attribute's comment: “sheaves of abelian groups, étale case: the canonical map F → f_big⁻¹ f_big! F is an isomorphism, where f_big! is the abelian lower shriek of Modules on Sites 04BE, i.e. the left adjoint of f_big⁻¹ on abelian sheaves, not the set-level f_big!”.
Stacks 04C8, the étale case for sheaves of abelian groups. The unit
F ⟶ f_big⁻¹ f_big! Fof the abelian lower-shriek adjunction of Modules on Sites 04BE is invertible for a monomorphism on the big étale site.
public theorem bigEtaleAbelianLowerShriek_unit_isIso
(B : BigEtaleSite.{u}) {X Y : B.Scheme} (f : X ⟶ Y) [Mono f]
(F : Sheaf (BigEtaleOver.topology B X.1 X.2) AbCat.{u, u + 1}) :
IsIso (((Over.map f).sheafAdjunctionContinuous AbCat.{u, u + 1}
(BigEtaleOver.topology B X.1 X.2)
(BigEtaleOver.topology B Y.1 Y.2)).unit.app F)
AlgebraicGeometry.bigSmoothAbelianLowerShriek_unit_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/MonomorphismLowerShriekUnit.lean, line 228. The attribute's comment: “sheaves of abelian groups, smooth case: the canonical map F → f_big⁻¹ f_big! F is an isomorphism, where f_big! is the abelian lower shriek of Modules on Sites 04BE, i.e. the left adjoint of f_big⁻¹ on abelian sheaves, not the set-level f_big!”.
Stacks 04C8, the smooth case for sheaves of abelian groups. The unit
F ⟶ f_big⁻¹ f_big! Fof the abelian lower-shriek adjunction of Modules on Sites 04BE is invertible for a monomorphism on the big smooth site.
public theorem bigSmoothAbelianLowerShriek_unit_isIso
(B : BigSmoothSite.{u}) {X Y : B.category} (f : X ⟶ Y) [Mono f]
(F : Sheaf (BigSmoothOver.topology B X.1 X.2) AbCat.{u, u + 1}) :
IsIso (((Over.map f).sheafAdjunctionContinuous AbCat.{u, u + 1}
(BigSmoothOver.topology B X.1 X.2)
(BigSmoothOver.topology B Y.1 Y.2)).unit.app F)
AlgebraicGeometry.bigSyntomicAbelianLowerShriek_unit_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/MonomorphismLowerShriekUnit.lean, line 243. The attribute's comment: “sheaves of abelian groups, syntomic case: the canonical map F → f_big⁻¹ f_big! F is an isomorphism, where f_big! is the abelian lower shriek of Modules on Sites 04BE, i.e. the left adjoint of f_big⁻¹ on abelian sheaves, not the set-level f_big!”.
Stacks 04C8, the syntomic case for sheaves of abelian groups. The unit
F ⟶ f_big⁻¹ f_big! Fof the abelian lower-shriek adjunction of Modules on Sites 04BE is invertible for a monomorphism on the big syntomic site.
public theorem bigSyntomicAbelianLowerShriek_unit_isIso
(B : BigSyntomicSite.{u}) {X Y : B.category} (f : X ⟶ Y) [Mono f]
(F : Sheaf (BigSyntomicOver.topology B X.1 X.2) AbCat.{u, u + 1}) :
IsIso (((Over.map f).sheafAdjunctionContinuous AbCat.{u, u + 1}
(BigSyntomicOver.topology B X.1 X.2)
(BigSyntomicOver.topology B Y.1 Y.2)).unit.app F)
AlgebraicGeometry.bigFppfAbelianLowerShriek_unit_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChangeOfSites/MonomorphismLowerShriekUnit.lean, line 257. The attribute's comment: “sheaves of abelian groups, fppf case: the canonical map F → f_big⁻¹ f_big! F is an isomorphism, where f_big! is the abelian lower shriek of Modules on Sites 04BE, i.e. the left adjoint of f_big⁻¹ on abelian sheaves, not the set-level f_big!”.
Stacks 04C8, the fppf case for sheaves of abelian groups. The unit
F ⟶ f_big⁻¹ f_big! Fof the abelian lower-shriek adjunction of Modules on Sites 04BE is invertible for a monomorphism on the big fppf site.
public theorem bigFppfAbelianLowerShriek_unit_isIso
(B : BigFppfSite.{u}) {X Y : B.Schemes} (f : X ⟶ Y) [Mono f]
(F : Sheaf (B.topology.over X) AbCat.{u, u + 1}) :
IsIso (((Over.map f).sheafAdjunctionContinuous AbCat.{u, u + 1}
(B.topology.over X) (B.topology.over Y)).unit.app F)
Tag 04E3, a lemma
Tag 04E3 in the Stacks Project.
AlgebraicGeometry.exists_etale_zariskiCover_baseChange_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesPushforward/ClosedImmersionCoverings.lean, line 109. The attribute's comment: “etale_cover”. References: EGA IV (18.1.1), “étale case”.
An étale scheme over a closed subscheme has a Zariski covering by base changes of étale schemes over the ambient scheme.
public theorem exists_etale_zariskiCover_baseChange_of_isClosedImmersion
{X Y U : Scheme.{u}} (i : X ⟶ Y) [IsClosedImmersion i]
(p : U ⟶ X) [Etale p] :
∃ (I : Type u) (V : I → Scheme.{u}) (q : ∀ j, V j ⟶ Y)
(g : ∀ j, pullback (q j) i ⟶ U),
(∀ j, Etale (q j)) ∧
(∀ j, g j ≫ p = pullback.snd (q j) i) ∧
Presieve.ofArrows (fun j ↦ pullback (q j) i) g ∈ Scheme.zariskiPrecoverage U
AlgebraicGeometry.exists_smooth_zariskiCover_baseChange_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesPushforward/ClosedImmersionCoverings.lean, line 178. The attribute's comment: “smooth_cover”. References: EGA IV (18.1.1), “smooth case”.
If
X ⟶ Yis a closed immersion andU ⟶ Xis smooth, thenUhas a Zariski covering by schemes obtained by base change from smooth schemes overY.
public theorem exists_smooth_zariskiCover_baseChange_of_isClosedImmersion
{X Y U : Scheme.{u}} (i : X ⟶ Y) [IsClosedImmersion i]
(p : U ⟶ X) [Smooth p] :
∃ (I : Type u) (V : I → Scheme.{u}) (q : ∀ j, V j ⟶ Y)
(g : ∀ j, pullback (q j) i ⟶ U),
(∀ j, Smooth (q j)) ∧
(∀ j, g j ≫ p = pullback.snd (q j) i) ∧
Presieve.ofArrows (fun j ↦ pullback (q j) i) g ∈ Scheme.zariskiPrecoverage U
AlgebraicGeometry.exists_syntomic_zariskiCover_baseChange_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesPushforward/ClosedImmersionCoverings.lean, line 193. The attribute's comment: “syntomic_cover”.
If
X ⟶ Yis a closed immersion andU ⟶ Xis syntomic, thenUhas a Zariski covering by schemes obtained by base change from syntomic schemes overY.
public theorem exists_syntomic_zariskiCover_baseChange_of_isClosedImmersion
{X Y U : Scheme.{u}} (i : X ⟶ Y) [IsClosedImmersion i]
(p : U ⟶ X) (hp : AlgebraicGeometry.Syntomic p) :
∃ (I : Type u) (V : I → Scheme.{u}) (q : ∀ j, V j ⟶ Y)
(g : ∀ j, pullback (q j) i ⟶ U),
(∀ j, AlgebraicGeometry.Syntomic (q j)) ∧
(∀ j, g j ≫ p = pullback.snd (q j) i) ∧
Presieve.ofArrows (fun j ↦ pullback (q j) i) g ∈ Scheme.zariskiPrecoverage U
Tag 04E4, a lemma
Tag 04E4 in the Stacks Project.
AlgebraicGeometry.exists_syntomicCovering_subordinate_to_closedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesPushforward/SubordinateCoverings.lean, line 127. The attribute's comment: “syntomic case”.
A syntomic covering of a closed subscheme can be prepared by a syntomic covering of the ambient scheme, with each base-changed member empty or subordinate to the original covering.
public theorem exists_syntomicCovering_subordinate_to_closedImmersion
{X Y : Scheme.{u}} (f : X ⟶ Y) [IsClosedImmersion f]
{I : Type v} (U : I → Scheme.{u}) (p : ∀ i, U i ⟶ X)
(hp : AlgebraicGeometry.IsSyntomicCovering U p) :
∃ (J : Type (max u v)) (V : J → Scheme.{u}) (q : ∀ j, V j ⟶ Y),
AlgebraicGeometry.IsSyntomicCovering V q ∧
∀ j, (IsEmpty (pullback (q j) f : Scheme.{u}) ∨
∃ i, ∃ h : pullback (q j) f ⟶ U i,
h ≫ p i = pullback.snd (q j) f)
AlgebraicGeometry.exists_smoothCovering_subordinate_to_closedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesPushforward/SubordinateCoverings.lean, line 155. The attribute's comment: “smooth case”.
A smooth covering of a closed subscheme can be prepared by a smooth covering of the ambient scheme, with each base-changed member empty or subordinate to the original covering.
public theorem exists_smoothCovering_subordinate_to_closedImmersion
{X Y : Scheme.{u}} (f : X ⟶ Y) [IsClosedImmersion f]
{I : Type v} (U : I → Scheme.{u}) (p : ∀ i, U i ⟶ X)
(hp : Presieve.ofArrows U p ∈ Scheme.precoverage (@Smooth.{u}) X) :
∃ (J : Type (max u v)) (V : J → Scheme.{u}) (q : ∀ j, V j ⟶ Y),
Presieve.ofArrows V q ∈ Scheme.precoverage (@Smooth.{u}) Y ∧
∀ j, (IsEmpty (pullback (q j) f : Scheme.{u}) ∨
∃ i, ∃ h : pullback (q j) f ⟶ U i,
h ≫ p i = pullback.snd (q j) f)
AlgebraicGeometry.exists_etaleCovering_subordinate_to_closedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesPushforward/SubordinateCoverings.lean, line 177. The attribute's comment: “étale case”.
An étale covering of a closed subscheme can be prepared by an étale covering of the ambient scheme, with each base-changed member empty or subordinate to the original covering.
public theorem exists_etaleCovering_subordinate_to_closedImmersion
{X Y : Scheme.{u}} (f : X ⟶ Y) [IsClosedImmersion f]
{I : Type v} (U : I → Scheme.{u}) (p : ∀ i, U i ⟶ X)
(hp : Presieve.ofArrows U p ∈ Scheme.etalePrecoverage X) :
∃ (J : Type (max u v)) (V : J → Scheme.{u}) (q : ∀ j, V j ⟶ Y),
Presieve.ofArrows V q ∈ Scheme.etalePrecoverage Y ∧
∀ j, (IsEmpty (pullback (q j) f : Scheme.{u}) ∨
∃ i, ∃ h : pullback (q j) f ⟶ U i,
h ≫ p i = pullback.snd (q j) f)
Tag 04C3, a lemma
Tag 04C3 in the Stacks Project.
AlgebraicGeometry.bigSyntomicPullback_isAlmostCocontinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesPushforward/AlmostCocontinuousPullback.lean, line 251. The attribute's comment: “syntomic case”.
Base change by a closed immersion is almost cocontinuous on big syntomic sites.
public theorem bigSyntomicPullback_isAlmostCocontinuous
(B : AlgebraicGeometry.BigSyntomicSite.{u}) {X Y : B.category} (f : X ⟶ Y)
[IsClosedImmersion (B.inclusion.map f)] :
IsAlmostCocontinuous (Over.pullback f)
(AlgebraicGeometry.BigSyntomicOver.topology B Y.1 Y.2)
(AlgebraicGeometry.BigSyntomicOver.topology B X.1 X.2)
AlgebraicGeometry.bigSmoothPullback_isAlmostCocontinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesPushforward/AlmostCocontinuousPullback.lean, line 284. The attribute's comment: “smooth case”.
Base change by a closed immersion is almost cocontinuous on big smooth sites.
public theorem bigSmoothPullback_isAlmostCocontinuous
(B : AlgebraicGeometry.BigSmoothSite.{u}) {X Y : B.category} (f : X ⟶ Y)
[IsClosedImmersion ((ObjectProperty.ι _).map f)] :
IsAlmostCocontinuous (Over.pullback f)
(AlgebraicGeometry.BigSmoothOver.topology B Y.1 Y.2)
(AlgebraicGeometry.BigSmoothOver.topology B X.1 X.2)
AlgebraicGeometry.bigEtalePullback_isAlmostCocontinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesPushforward/AlmostCocontinuousPullback.lean, line 327. The attribute's comment: “étale case”.
Base change by a closed immersion is almost cocontinuous on big étale sites.
public theorem bigEtalePullback_isAlmostCocontinuous
(B : AlgebraicGeometry.BigEtaleSite.{u}) {X Y : B.Scheme} (f : X ⟶ Y)
[IsClosedImmersion (B.inclusion.map f)] :
IsAlmostCocontinuous (Over.pullback f)
(AlgebraicGeometry.BigEtaleOver.topology B Y.1 Y.2)
(AlgebraicGeometry.BigEtaleOver.topology B X.1 X.2)
Tag 04C4, a lemma
Tag 04C4 in the Stacks Project.
AlgebraicGeometry.bigSyntomicPushforward_preservesConnectedColimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesPushforward/PushforwardExact.lean, line 171. The attribute's comment: “pushforward_coequalizers_pushouts”.
Stacks Project, Tag 04C4, part (1). Direct image of sheaves of sets by a closed immersion of big syntomic sites preserves colimits of every connected shape whose colimits of sets exist.
This is Stacks Project, Tag 04B9 — the general form of the Tag 04BA that the source cites — fed the almost cocontinuity of base change supplied by Stacks Project, Tag 04C3. No passage to an equivalent small site is needed, Tag 04B9 being stated for an arbitrary pair of sites.
public theorem bigSyntomicPushforward_preservesConnectedColimits
(B : AlgebraicGeometry.BigSyntomicSite.{u}) {X Y : B.category} (f : X ⟶ Y)
[IsClosedImmersion (B.inclusion.map f)]
(I : Type t) [Category.{t'} I] [IsConnected I] [HasColimitsOfShape I (Type (u + 1))] :
PreservesColimitsOfShape I
((Over.pullback f).sheafPushforwardContinuous (Type (u + 1))
(AlgebraicGeometry.BigSyntomicOver.topology B Y.1 Y.2)
(AlgebraicGeometry.BigSyntomicOver.topology B X.1 X.2))
AlgebraicGeometry.bigSyntomicPushforward_preservesPushouts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesPushforward/PushforwardExact.lean, line 191. The attribute's comment: “pushforward_coequalizers_pushouts”.
Stacks Project, Tag 04C4, part (1): pushouts. Direct image of sheaves of sets by a closed immersion of big syntomic sites commutes with pushouts,
WalkingSpanbeing a connected shape.
public theorem bigSyntomicPushforward_preservesPushouts
(B : AlgebraicGeometry.BigSyntomicSite.{u}) {X Y : B.category} (f : X ⟶ Y)
[IsClosedImmersion (B.inclusion.map f)] :
PreservesColimitsOfShape WalkingSpan
((Over.pullback f).sheafPushforwardContinuous (Type (u + 1))
(AlgebraicGeometry.BigSyntomicOver.topology B Y.1 Y.2)
(AlgebraicGeometry.BigSyntomicOver.topology B X.1 X.2))
AlgebraicGeometry.bigSyntomicPushforward_preservesCoequalizers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesPushforward/PushforwardExact.lean, line 204. The attribute's comment: “pushforward_coequalizers_pushouts”.
Stacks Project, Tag 04C4, part (1): coequalizers. Direct image of sheaves of sets by a closed immersion of big syntomic sites commutes with coequalizers,
WalkingParallelPairbeing a connected shape.
public theorem bigSyntomicPushforward_preservesCoequalizers
(B : AlgebraicGeometry.BigSyntomicSite.{u}) {X Y : B.category} (f : X ⟶ Y)
[IsClosedImmersion (B.inclusion.map f)] :
PreservesColimitsOfShape WalkingParallelPair
((Over.pullback f).sheafPushforwardContinuous (Type (u + 1))
(AlgebraicGeometry.BigSyntomicOver.topology B Y.1 Y.2)
(AlgebraicGeometry.BigSyntomicOver.topology B X.1 X.2))
AlgebraicGeometry.bigSmoothPushforward_preservesConnectedColimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesPushforward/PushforwardExact.lean, line 216. The attribute's comment: “pushforward_coequalizers_pushouts”.
Stacks Project, Tag 04C4, part (1). Direct image of sheaves of sets by a closed immersion of big smooth sites preserves colimits of every connected shape whose colimits of sets exist.
public theorem bigSmoothPushforward_preservesConnectedColimits
(B : AlgebraicGeometry.BigSmoothSite.{u}) {X Y : B.category} (f : X ⟶ Y)
[IsClosedImmersion ((ObjectProperty.ι _).map f)]
(I : Type t) [Category.{t'} I] [IsConnected I] [HasColimitsOfShape I (Type (u + 1))] :
PreservesColimitsOfShape I
((Over.pullback f).sheafPushforwardContinuous (Type (u + 1))
(AlgebraicGeometry.BigSmoothOver.topology B Y.1 Y.2)
(AlgebraicGeometry.BigSmoothOver.topology B X.1 X.2))
AlgebraicGeometry.bigSmoothPushforward_preservesPushouts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesPushforward/PushforwardExact.lean, line 236. The attribute's comment: “pushforward_coequalizers_pushouts”.
Stacks Project, Tag 04C4, part (1): pushouts. Direct image of sheaves of sets by a closed immersion of big smooth sites commutes with pushouts.
public theorem bigSmoothPushforward_preservesPushouts
(B : AlgebraicGeometry.BigSmoothSite.{u}) {X Y : B.category} (f : X ⟶ Y)
[IsClosedImmersion ((ObjectProperty.ι _).map f)] :
PreservesColimitsOfShape WalkingSpan
((Over.pullback f).sheafPushforwardContinuous (Type (u + 1))
(AlgebraicGeometry.BigSmoothOver.topology B Y.1 Y.2)
(AlgebraicGeometry.BigSmoothOver.topology B X.1 X.2))
AlgebraicGeometry.bigSmoothPushforward_preservesCoequalizers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesPushforward/PushforwardExact.lean, line 248. The attribute's comment: “pushforward_coequalizers_pushouts”.
Stacks Project, Tag 04C4, part (1): coequalizers. Direct image of sheaves of sets by a closed immersion of big smooth sites commutes with coequalizers.
public theorem bigSmoothPushforward_preservesCoequalizers
(B : AlgebraicGeometry.BigSmoothSite.{u}) {X Y : B.category} (f : X ⟶ Y)
[IsClosedImmersion ((ObjectProperty.ι _).map f)] :
PreservesColimitsOfShape WalkingParallelPair
((Over.pullback f).sheafPushforwardContinuous (Type (u + 1))
(AlgebraicGeometry.BigSmoothOver.topology B Y.1 Y.2)
(AlgebraicGeometry.BigSmoothOver.topology B X.1 X.2))
AlgebraicGeometry.bigEtalePushforward_preservesConnectedColimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesPushforward/PushforwardExact.lean, line 260. The attribute's comment: “pushforward_coequalizers_pushouts”.
Stacks Project, Tag 04C4, part (1). Direct image of sheaves of sets by a closed immersion of big étale sites preserves colimits of every connected shape whose colimits of sets exist.
public theorem bigEtalePushforward_preservesConnectedColimits
(B : AlgebraicGeometry.BigEtaleSite.{u}) {X Y : B.Scheme} (f : X ⟶ Y)
[IsClosedImmersion (B.inclusion.map f)]
(I : Type t) [Category.{t'} I] [IsConnected I] [HasColimitsOfShape I (Type (u + 1))] :
PreservesColimitsOfShape I
((Over.pullback f).sheafPushforwardContinuous (Type (u + 1))
(AlgebraicGeometry.BigEtaleOver.topology B Y.1 Y.2)
(AlgebraicGeometry.BigEtaleOver.topology B X.1 X.2))
AlgebraicGeometry.bigEtalePushforward_preservesPushouts, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesPushforward/PushforwardExact.lean, line 280. The attribute's comment: “pushforward_coequalizers_pushouts”.
Stacks Project, Tag 04C4, part (1): pushouts. Direct image of sheaves of sets by a closed immersion of big étale sites commutes with pushouts.
public theorem bigEtalePushforward_preservesPushouts
(B : AlgebraicGeometry.BigEtaleSite.{u}) {X Y : B.Scheme} (f : X ⟶ Y)
[IsClosedImmersion (B.inclusion.map f)] :
PreservesColimitsOfShape WalkingSpan
((Over.pullback f).sheafPushforwardContinuous (Type (u + 1))
(AlgebraicGeometry.BigEtaleOver.topology B Y.1 Y.2)
(AlgebraicGeometry.BigEtaleOver.topology B X.1 X.2))
AlgebraicGeometry.bigEtalePushforward_preservesCoequalizers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesPushforward/PushforwardExact.lean, line 292. The attribute's comment: “pushforward_coequalizers_pushouts”.
Stacks Project, Tag 04C4, part (1): coequalizers. Direct image of sheaves of sets by a closed immersion of big étale sites commutes with coequalizers.
public theorem bigEtalePushforward_preservesCoequalizers
(B : AlgebraicGeometry.BigEtaleSite.{u}) {X Y : B.Scheme} (f : X ⟶ Y)
[IsClosedImmersion (B.inclusion.map f)] :
PreservesColimitsOfShape WalkingParallelPair
((Over.pullback f).sheafPushforwardContinuous (Type (u + 1))
(AlgebraicGeometry.BigEtaleOver.topology B Y.1 Y.2)
(AlgebraicGeometry.BigEtaleOver.topology B X.1 X.2))
AlgebraicGeometry.bigSyntomicPushforward_isExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesPushforward/PushforwardExact.lean, line 305. The attribute's comment: “abelian_pushforward_exact”.
Direct image of abelian sheaves by a closed immersion of big syntomic sites is exact.
public theorem bigSyntomicPushforward_isExact
(B : AlgebraicGeometry.BigSyntomicSite.{u}) {X Y : B.category} (f : X ⟶ Y)
[IsClosedImmersion (B.inclusion.map f)] :
QuasiMorphismOfSites.IsExact
((Over.pullback f).sheafPushforwardContinuous Ab.{u + 1}
(AlgebraicGeometry.BigSyntomicOver.topology B Y.1 Y.2)
(AlgebraicGeometry.BigSyntomicOver.topology B X.1 X.2))
AlgebraicGeometry.bigSmoothPushforward_isExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesPushforward/PushforwardExact.lean, line 317. The attribute's comment: “abelian_pushforward_exact”.
Direct image of abelian sheaves by a closed immersion of big smooth sites is exact.
public theorem bigSmoothPushforward_isExact
(B : AlgebraicGeometry.BigSmoothSite.{u}) {X Y : B.category} (f : X ⟶ Y)
[IsClosedImmersion ((ObjectProperty.ι _).map f)] :
QuasiMorphismOfSites.IsExact
((Over.pullback f).sheafPushforwardContinuous Ab.{u + 1}
(AlgebraicGeometry.BigSmoothOver.topology B Y.1 Y.2)
(AlgebraicGeometry.BigSmoothOver.topology B X.1 X.2))
AlgebraicGeometry.bigEtalePushforward_isExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesPushforward/PushforwardExact.lean, line 329. The attribute's comment: “abelian_pushforward_exact”.
Direct image of abelian sheaves by a closed immersion of big étale sites is exact.
public theorem bigEtalePushforward_isExact
(B : AlgebraicGeometry.BigEtaleSite.{u}) {X Y : B.Scheme} (f : X ⟶ Y)
[IsClosedImmersion (B.inclusion.map f)] :
QuasiMorphismOfSites.IsExact
((Over.pullback f).sheafPushforwardContinuous Ab.{u + 1}
(AlgebraicGeometry.BigEtaleOver.topology B Y.1 Y.2)
(AlgebraicGeometry.BigEtaleOver.topology B X.1 X.2))
Sources
Section59.49 Exactness of big lower shriek#
Section 59.49 of the Stacks Project, Tag 04CB. 2 tags here are carried by 38 declarations of the repository (all in StacksFrontier) and 4 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 04CC, a lemma
Tag 04CC in the Stacks Project.
AlgebraicGeometry.bigZariskiLowerShriek_preservesFiniteLimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesLowerShriek/AbelianExact.lean, line 99. The attribute's comment: “abelian_lower_shriek_exact”.
Stacks 04CC(1), Zariski case. Lower shriek on big Zariski abelian sheaves preserves finite limits.
public theorem bigZariskiLowerShriek_preservesFiniteLimits
(B : BigZariskiSite.{u}) (T S : B.Schemes) (f : T ⟶ S) :
PreservesFiniteLimits ((Over.map f).sheafPullback Ab.{u + 1}
(BigZariskiOver.topology B T.1 T.property)
(BigZariskiOver.topology B S.1 S.property))
AlgebraicGeometry.bigZariskiLowerShriek_preservesFiniteColimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesLowerShriek/AbelianExact.lean, line 109. The attribute's comment: “abelian_lower_shriek_exact”.
Stacks 04CC(1), Zariski case. Lower shriek on big Zariski abelian sheaves preserves finite colimits.
public theorem bigZariskiLowerShriek_preservesFiniteColimits
(B : BigZariskiSite.{u}) (T S : B.Schemes) (f : T ⟶ S) :
PreservesFiniteColimits ((Over.map f).sheafPullback Ab.{u + 1}
(BigZariskiOver.topology B T.1 T.property)
(BigZariskiOver.topology B S.1 S.property))
AlgebraicGeometry.bigEtaleLowerShriek_preservesFiniteLimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesLowerShriek/AbelianExact.lean, line 119. The attribute's comment: “abelian_lower_shriek_exact”.
Stacks 04CC(1), étale case. Lower shriek on big étale abelian sheaves preserves finite limits.
public theorem bigEtaleLowerShriek_preservesFiniteLimits
(B : BigEtaleSite.{u}) (T S : B.Scheme) (f : T ⟶ S) :
PreservesFiniteLimits ((Over.map f).sheafPullback Ab.{u + 1}
(BigEtaleOver.topology B T.obj T.property)
(BigEtaleOver.topology B S.obj S.property))
AlgebraicGeometry.bigEtaleLowerShriek_preservesFiniteColimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesLowerShriek/AbelianExact.lean, line 129. The attribute's comment: “abelian_lower_shriek_exact”.
Stacks 04CC(1), étale case. Lower shriek on big étale abelian sheaves preserves finite colimits.
public theorem bigEtaleLowerShriek_preservesFiniteColimits
(B : BigEtaleSite.{u}) (T S : B.Scheme) (f : T ⟶ S) :
PreservesFiniteColimits ((Over.map f).sheafPullback Ab.{u + 1}
(BigEtaleOver.topology B T.obj T.property)
(BigEtaleOver.topology B S.obj S.property))
AlgebraicGeometry.bigFppfLowerShriek_preservesFiniteLimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesLowerShriek/AbelianExact.lean, line 139. The attribute's comment: “abelian_lower_shriek_exact”.
Stacks 04CC(1), fppf case. Lower shriek on big fppf abelian sheaves preserves finite limits.
public theorem bigFppfLowerShriek_preservesFiniteLimits
(B : BigFppfSite.{u}) (T S : B.Schemes) (f : T ⟶ S) :
PreservesFiniteLimits ((Over.map f).sheafPullback Ab.{u + 1}
(B.topology.over T) (B.topology.over S))
AlgebraicGeometry.bigFppfLowerShriek_preservesFiniteColimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesLowerShriek/AbelianExact.lean, line 148. The attribute's comment: “abelian_lower_shriek_exact”.
Stacks 04CC(1), fppf case. Lower shriek on big fppf abelian sheaves preserves finite colimits.
public theorem bigFppfLowerShriek_preservesFiniteColimits
(B : BigFppfSite.{u}) (T S : B.Schemes) (f : T ⟶ S) :
PreservesFiniteColimits ((Over.map f).sheafPullback Ab.{u + 1}
(B.topology.over T) (B.topology.over S))
AlgebraicGeometry.bigSmoothLowerShriek_preservesFiniteLimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesLowerShriek/AbelianExact.lean, line 157. The attribute's comment: “abelian_lower_shriek_exact”.
Stacks 04CC(1), smooth case. Lower shriek on big smooth abelian sheaves preserves finite limits.
public theorem bigSmoothLowerShriek_preservesFiniteLimits
(B : BigSmoothSite.{u}) {T S : B.category} (f : T ⟶ S) :
PreservesFiniteLimits ((Over.map f).sheafPullback Ab.{u + 1}
(BigSmoothOver.topology B T.1 T.2)
(BigSmoothOver.topology B S.1 S.2))
AlgebraicGeometry.bigSmoothLowerShriek_preservesFiniteColimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesLowerShriek/AbelianExact.lean, line 167. The attribute's comment: “abelian_lower_shriek_exact”.
Stacks 04CC(1), smooth case. Lower shriek on big smooth abelian sheaves preserves finite colimits.
public theorem bigSmoothLowerShriek_preservesFiniteColimits
(B : BigSmoothSite.{u}) {T S : B.category} (f : T ⟶ S) :
PreservesFiniteColimits ((Over.map f).sheafPullback Ab.{u + 1}
(BigSmoothOver.topology B T.1 T.2)
(BigSmoothOver.topology B S.1 S.2))
AlgebraicGeometry.bigSyntomicLowerShriek_preservesFiniteLimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesLowerShriek/AbelianExact.lean, line 177. The attribute's comment: “abelian_lower_shriek_exact”.
Stacks 04CC(1), syntomic case. Lower shriek on big syntomic abelian sheaves preserves finite limits.
public theorem bigSyntomicLowerShriek_preservesFiniteLimits
(B : BigSyntomicSite.{u}) {T S : B.category} (f : T ⟶ S) :
PreservesFiniteLimits ((Over.map f).sheafPullback Ab.{u + 1}
(BigSyntomicOver.topology B T.1 T.2)
(BigSyntomicOver.topology B S.1 S.2))
AlgebraicGeometry.bigSyntomicLowerShriek_preservesFiniteColimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesLowerShriek/AbelianExact.lean, line 187. The attribute's comment: “abelian_lower_shriek_exact”.
Stacks 04CC(1), syntomic case. Lower shriek on big syntomic abelian sheaves preserves finite colimits.
public theorem bigSyntomicLowerShriek_preservesFiniteColimits
(B : BigSyntomicSite.{u}) {T S : B.category} (f : T ⟶ S) :
PreservesFiniteColimits ((Over.map f).sheafPullback Ab.{u + 1}
(BigSyntomicOver.topology B T.1 T.2)
(BigSyntomicOver.topology B S.1 S.2))
AlgebraicGeometry.bigZariskiInverseImageRing_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesLowerShriek/ModuleLowerShriek.lean, line 103. The attribute's comment: “module_lower_shriek_inverse_image_structure_sheaf”.
Stacks 04CC(2), Zariski case. The inverse image of the structure sheaf of the big Zariski site over
Sis the structure sheaf of the big Zariski site overT.
public theorem bigZariskiInverseImageRing_eq :
Stacks.SheafOfModules.inverseImageRing
(BigZariskiOver.topology B T.1 T.property)
(BigZariskiOver.topology B S.1 S.property) (Over.map f)
(BigZariskiOver.structureSheaf B S.1 S.property) =
BigZariskiOver.structureSheaf B T.1 T.property
AlgebraicGeometry.bigZariskiLowerShriekModulesAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesLowerShriek/ModuleLowerShriek.lean, line 134. The attribute's comment: “module_lower_shriek_adjunction”.
Stacks 04CC(2), Zariski case.
f_big^*on sheaves of modules of the big Zariski sites hasf_big!as a left adjoint.
public def bigZariskiLowerShriekModulesAdjunction :
bigZariskiLowerShriekModules B T S f ⊣ bigZariskiInverseImageModules B T S f
AlgebraicGeometry.bigZariskiLowerShriekModulesToSheafIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesLowerShriek/ModuleLowerShriek.lean, line 145. The attribute's comment: “module_lower_shriek_agrees_on_abelian_sheaves”.
Stacks 04CC(2), Zariski case. The two
f_big!agree on underlying sheaves of abelian groups: the underlying abelian sheaf off_big! Misf_big!of the underlying abelian sheaf ofM.
public def bigZariskiLowerShriekModulesToSheafIso :
SheafOfModules.toSheaf.{u + 1} (BigZariskiOver.structureSheaf B T.1 T.property) ⋙
(Over.map f).sheafPullback AddCommGrpCat.{u + 1}
(BigZariskiOver.topology B T.1 T.property)
(BigZariskiOver.topology B S.1 S.property) ≅
bigZariskiLowerShriekModules B T S f ⋙
SheafOfModules.toSheaf.{u + 1} (BigZariskiOver.structureSheaf B S.1 S.property)
AlgebraicGeometry.bigZariskiLowerShriekModules_preservesFiniteLimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesLowerShriek/ModuleLowerShriek.lean, line 161. The attribute's comment: “module_lower_shriek_exact”.
Stacks 04CC(2), Zariski case.
f_big!on sheaves of modules of the big Zariski sites preserves finite limits. Lower shriek on abelian sheaves does, and forgetting the module structure both preserves and reflects finite limits.
public theorem bigZariskiLowerShriekModules_preservesFiniteLimits :
PreservesFiniteLimits (bigZariskiLowerShriekModules B T S f)
AlgebraicGeometry.bigZariskiLowerShriekModules_preservesFiniteColimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesLowerShriek/ModuleLowerShriek.lean, line 171. The attribute's comment: “module_lower_shriek_exact”.
Stacks 04CC(2), Zariski case.
f_big!on sheaves of modules of the big Zariski sites preserves finite colimits: it is a left adjoint.
public theorem bigZariskiLowerShriekModules_preservesFiniteColimits :
PreservesFiniteColimits (bigZariskiLowerShriekModules B T S f)
AlgebraicGeometry.bigEtaleInverseImageRing_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesLowerShriek/ModuleLowerShriek.lean, line 189. The attribute's comment: “module_lower_shriek_inverse_image_structure_sheaf”.
Stacks 04CC(2), étale case. The inverse image of the structure sheaf of the big étale site over
Sis the structure sheaf of the big étale site overT.
public theorem bigEtaleInverseImageRing_eq :
Stacks.SheafOfModules.inverseImageRing
(BigEtaleOver.topology B T.obj T.property)
(BigEtaleOver.topology B S.obj S.property) (Over.map f)
(BigEtaleOver.structureSheaf B S.obj S.property) =
BigEtaleOver.structureSheaf B T.obj T.property
AlgebraicGeometry.bigEtaleLowerShriekModulesAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesLowerShriek/ModuleLowerShriek.lean, line 219. The attribute's comment: “module_lower_shriek_adjunction”.
Stacks 04CC(2), étale case.
f_big^*on sheaves of modules of the big étale sites hasf_big!as a left adjoint.
public def bigEtaleLowerShriekModulesAdjunction :
bigEtaleLowerShriekModules B T S f ⊣ bigEtaleInverseImageModules B T S f
AlgebraicGeometry.bigEtaleLowerShriekModulesToSheafIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesLowerShriek/ModuleLowerShriek.lean, line 229. The attribute's comment: “module_lower_shriek_agrees_on_abelian_sheaves”.
Stacks 04CC(2), étale case. The two
f_big!agree on underlying sheaves of abelian groups.
public def bigEtaleLowerShriekModulesToSheafIso :
SheafOfModules.toSheaf.{u + 1} (BigEtaleOver.structureSheaf B T.obj T.property) ⋙
(Over.map f).sheafPullback AddCommGrpCat.{u + 1}
(BigEtaleOver.topology B T.obj T.property)
(BigEtaleOver.topology B S.obj S.property) ≅
bigEtaleLowerShriekModules B T S f ⋙
SheafOfModules.toSheaf.{u + 1} (BigEtaleOver.structureSheaf B S.obj S.property)
AlgebraicGeometry.bigEtaleLowerShriekModules_preservesFiniteLimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesLowerShriek/ModuleLowerShriek.lean, line 245. The attribute's comment: “module_lower_shriek_exact”.
Stacks 04CC(2), étale case.
f_big!on sheaves of modules of the big étale sites preserves finite limits. Lower shriek on abelian sheaves does, and forgetting the module structure both preserves and reflects finite limits.
public theorem bigEtaleLowerShriekModules_preservesFiniteLimits :
PreservesFiniteLimits (bigEtaleLowerShriekModules B T S f)
AlgebraicGeometry.bigEtaleLowerShriekModules_preservesFiniteColimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesLowerShriek/ModuleLowerShriek.lean, line 255. The attribute's comment: “module_lower_shriek_exact”.
Stacks 04CC(2), étale case.
f_big!on sheaves of modules of the big étale sites preserves finite colimits: it is a left adjoint.
public theorem bigEtaleLowerShriekModules_preservesFiniteColimits :
PreservesFiniteColimits (bigEtaleLowerShriekModules B T S f)
AlgebraicGeometry.bigFppfInverseImageRing_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesLowerShriek/ModuleLowerShriek.lean, line 273. The attribute's comment: “module_lower_shriek_inverse_image_structure_sheaf”.
Stacks 04CC(2), fppf case. The inverse image of the structure sheaf of the big fppf site over
Sis the structure sheaf of the big fppf site overT.
public theorem bigFppfInverseImageRing_eq :
Stacks.SheafOfModules.inverseImageRing
(B.topology.over T)
(B.topology.over S) (Over.map f)
(BigFppfOver.structureSheaf B S.1 S.property) =
BigFppfOver.structureSheaf B T.1 T.property
AlgebraicGeometry.bigFppfLowerShriekModulesAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesLowerShriek/ModuleLowerShriek.lean, line 303. The attribute's comment: “module_lower_shriek_adjunction”.
Stacks 04CC(2), fppf case.
f_big^*on sheaves of modules of the big fppf sites hasf_big!as a left adjoint.
public def bigFppfLowerShriekModulesAdjunction :
bigFppfLowerShriekModules B T S f ⊣ bigFppfInverseImageModules B T S f
AlgebraicGeometry.bigFppfLowerShriekModulesToSheafIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesLowerShriek/ModuleLowerShriek.lean, line 313. The attribute's comment: “module_lower_shriek_agrees_on_abelian_sheaves”.
Stacks 04CC(2), fppf case. The two
f_big!agree on underlying sheaves of abelian groups.
public def bigFppfLowerShriekModulesToSheafIso :
SheafOfModules.toSheaf.{u + 1} (BigFppfOver.structureSheaf B T.1 T.property) ⋙
(Over.map f).sheafPullback AddCommGrpCat.{u + 1}
(B.topology.over T)
(B.topology.over S) ≅
bigFppfLowerShriekModules B T S f ⋙
SheafOfModules.toSheaf.{u + 1} (BigFppfOver.structureSheaf B S.1 S.property)
AlgebraicGeometry.bigFppfLowerShriekModules_preservesFiniteLimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesLowerShriek/ModuleLowerShriek.lean, line 329. The attribute's comment: “module_lower_shriek_exact”.
Stacks 04CC(2), fppf case.
f_big!on sheaves of modules of the big fppf sites preserves finite limits. Lower shriek on abelian sheaves does, and forgetting the module structure both preserves and reflects finite limits.
public theorem bigFppfLowerShriekModules_preservesFiniteLimits :
PreservesFiniteLimits (bigFppfLowerShriekModules B T S f)
AlgebraicGeometry.bigFppfLowerShriekModules_preservesFiniteColimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesLowerShriek/ModuleLowerShriek.lean, line 339. The attribute's comment: “module_lower_shriek_exact”.
Stacks 04CC(2), fppf case.
f_big!on sheaves of modules of the big fppf sites preserves finite colimits: it is a left adjoint.
public theorem bigFppfLowerShriekModules_preservesFiniteColimits :
PreservesFiniteColimits (bigFppfLowerShriekModules B T S f)
AlgebraicGeometry.bigSmoothInverseImageRing_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesLowerShriek/ModuleLowerShriek.lean, line 357. The attribute's comment: “module_lower_shriek_inverse_image_structure_sheaf”.
Stacks 04CC(2), smooth case. The inverse image of the structure sheaf of the big smooth site over
Sis the structure sheaf of the big smooth site overT.
public theorem bigSmoothInverseImageRing_eq :
Stacks.SheafOfModules.inverseImageRing
(BigSmoothOver.topology B T.1 T.2)
(BigSmoothOver.topology B S.1 S.2) (Over.map f)
(BigSmoothOver.structureSheaf B S.1 S.2) =
BigSmoothOver.structureSheaf B T.1 T.2
AlgebraicGeometry.bigSmoothLowerShriekModulesAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesLowerShriek/ModuleLowerShriek.lean, line 387. The attribute's comment: “module_lower_shriek_adjunction”.
Stacks 04CC(2), smooth case.
f_big^*on sheaves of modules of the big smooth sites hasf_big!as a left adjoint.
public def bigSmoothLowerShriekModulesAdjunction :
bigSmoothLowerShriekModules B T S f ⊣ bigSmoothInverseImageModules B T S f
AlgebraicGeometry.bigSmoothLowerShriekModulesToSheafIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesLowerShriek/ModuleLowerShriek.lean, line 397. The attribute's comment: “module_lower_shriek_agrees_on_abelian_sheaves”.
Stacks 04CC(2), smooth case. The two
f_big!agree on underlying sheaves of abelian groups.
public def bigSmoothLowerShriekModulesToSheafIso :
SheafOfModules.toSheaf.{u + 1} (BigSmoothOver.structureSheaf B T.1 T.2) ⋙
(Over.map f).sheafPullback AddCommGrpCat.{u + 1}
(BigSmoothOver.topology B T.1 T.2)
(BigSmoothOver.topology B S.1 S.2) ≅
bigSmoothLowerShriekModules B T S f ⋙
SheafOfModules.toSheaf.{u + 1} (BigSmoothOver.structureSheaf B S.1 S.2)
AlgebraicGeometry.bigSmoothLowerShriekModules_preservesFiniteLimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesLowerShriek/ModuleLowerShriek.lean, line 413. The attribute's comment: “module_lower_shriek_exact”.
Stacks 04CC(2), smooth case.
f_big!on sheaves of modules of the big smooth sites preserves finite limits. Lower shriek on abelian sheaves does, and forgetting the module structure both preserves and reflects finite limits.
public theorem bigSmoothLowerShriekModules_preservesFiniteLimits :
PreservesFiniteLimits (bigSmoothLowerShriekModules B T S f)
AlgebraicGeometry.bigSmoothLowerShriekModules_preservesFiniteColimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesLowerShriek/ModuleLowerShriek.lean, line 423. The attribute's comment: “module_lower_shriek_exact”.
Stacks 04CC(2), smooth case.
f_big!on sheaves of modules of the big smooth sites preserves finite colimits: it is a left adjoint.
public theorem bigSmoothLowerShriekModules_preservesFiniteColimits :
PreservesFiniteColimits (bigSmoothLowerShriekModules B T S f)
AlgebraicGeometry.bigSyntomicInverseImageRing_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesLowerShriek/ModuleLowerShriek.lean, line 441. The attribute's comment: “module_lower_shriek_inverse_image_structure_sheaf”.
Stacks 04CC(2), syntomic case. The inverse image of the structure sheaf of the big syntomic site over
Sis the structure sheaf of the big syntomic site overT.
public theorem bigSyntomicInverseImageRing_eq :
Stacks.SheafOfModules.inverseImageRing
(BigSyntomicOver.topology B T.1 T.2)
(BigSyntomicOver.topology B S.1 S.2) (Over.map f)
(BigSyntomicOver.structureSheaf B S.1 S.2) =
BigSyntomicOver.structureSheaf B T.1 T.2
AlgebraicGeometry.bigSyntomicLowerShriekModulesAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesLowerShriek/ModuleLowerShriek.lean, line 472. The attribute's comment: “module_lower_shriek_adjunction”.
Stacks 04CC(2), syntomic case.
f_big^*on sheaves of modules of the big syntomic sites hasf_big!as a left adjoint.
public def bigSyntomicLowerShriekModulesAdjunction :
bigSyntomicLowerShriekModules B T S f ⊣ bigSyntomicInverseImageModules B T S f
AlgebraicGeometry.bigSyntomicLowerShriekModulesToSheafIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesLowerShriek/ModuleLowerShriek.lean, line 482. The attribute's comment: “module_lower_shriek_agrees_on_abelian_sheaves”.
Stacks 04CC(2), syntomic case. The two
f_big!agree on underlying sheaves of abelian groups.
public def bigSyntomicLowerShriekModulesToSheafIso :
SheafOfModules.toSheaf.{u + 1} (BigSyntomicOver.structureSheaf B T.1 T.2) ⋙
(Over.map f).sheafPullback AddCommGrpCat.{u + 1}
(BigSyntomicOver.topology B T.1 T.2)
(BigSyntomicOver.topology B S.1 S.2) ≅
bigSyntomicLowerShriekModules B T S f ⋙
SheafOfModules.toSheaf.{u + 1} (BigSyntomicOver.structureSheaf B S.1 S.2)
AlgebraicGeometry.bigSyntomicLowerShriekModules_preservesFiniteLimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesLowerShriek/ModuleLowerShriek.lean, line 498. The attribute's comment: “module_lower_shriek_exact”.
Stacks 04CC(2), syntomic case.
f_big!on sheaves of modules of the big syntomic sites preserves finite limits. Lower shriek on abelian sheaves does, and forgetting the module structure both preserves and reflects finite limits.
public theorem bigSyntomicLowerShriekModules_preservesFiniteLimits :
PreservesFiniteLimits (bigSyntomicLowerShriekModules B T S f)
AlgebraicGeometry.bigSyntomicLowerShriekModules_preservesFiniteColimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesLowerShriek/ModuleLowerShriek.lean, line 508. The attribute's comment: “module_lower_shriek_exact”.
Stacks 04CC(2), syntomic case.
f_big!on sheaves of modules of the big syntomic sites preserves finite colimits: it is a left adjoint.
public theorem bigSyntomicLowerShriekModules_preservesFiniteColimits :
PreservesFiniteColimits (bigSyntomicLowerShriekModules B T S f)
Declarations registered for the tag:
Functor.sheafPullbackConstruction.sheafAdjunctionContinuousregistered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/EtaleCohomology/BigSitesLowerShriek/AbelianExact.lean, line 93 (StacksFrontier): “abelian_lower_shriek_exact”.
Tag 07AJ, a lemma
Tag 07AJ in the Stacks Project.
AlgebraicGeometry.isIso_lowerShriekStructureSheafHom_of_isClosedUnderAffineLine, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/SubcategoryAffineLineClosure.lean, line 236. The attribute's comment: “part (b)”.
Let
C₁ ⊆ C₂be full subcategories of the big fppf category over a schemeX, letC₁contain the base objectX/Xand the affine line over each of its objects, and letg : Sh(C₁) ⟶ Sh(C₂)be the morphism of topoi of the inclusion. Then the canonical mapg_!O₁ ⟶ O₂from the lower shriek of the restricted structure sheaf to the structure sheaf is an isomorphism.The sheaf condition on the structure presheaf of
C₂and the existence ofg_!, a left adjoint of the pushforward along the inclusion, are taken as hypotheses.
theorem isIso_lowerShriekStructureSheafHom_of_isClosedUnderAffineLine
{P₁ P₂ : ObjectProperty (BigFppfOver B X hX)} (h₁₂ : P₁ ≤ P₂)
(J₁ : GrothendieckTopology P₁.FullSubcategory)
(J₂ : GrothendieckTopology P₂.FullSubcategory)
(hsh : Presheaf.IsSheaf J₂ (P₂.ι.op ⋙ bigOverPresheafAb B X hX))
[(ObjectProperty.ιOfLE h₁₂).IsContinuous J₁ J₂]
[((ObjectProperty.ιOfLE h₁₂).sheafPushforwardContinuous
AddCommGrpCat.{t} J₁ J₂).IsRightAdjoint]
(hbase : P₁ (Over.mk (𝟙 (B.obj hX)))) (hline : IsClosedUnderAffineLine P₁) :
IsIso (lowerShriekStructureSheafHom h₁₂ J₁ J₂ hsh)
AlgebraicGeometry.fullyFaithful_isContinuous_isCocontinuous_ιOfLE_baseOverTopology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/SubcategoryBigFppfLowerShriek.lean, line 373. The attribute's comment: “part (a), at the inherited topologies, for every τ”.
Stacks 07AJ (a). Let
τbe any of the Zariski, étale, smooth, syntomic and fppf topologies, and letC₁ ⊆ C₂be full subcategories of the big category overX, each with the topology it inherits from the bigτ-site overX, both satisfying the closure condition (1)(a) of the source. Then the inclusionC₁ ⊆ C₂is fully faithful, continuous and cocontinuous.Full faithfulness holds for any inclusion of full subcategories; continuity and cocontinuity are
AlgebraicGeometry.isContinuous_ιOfLE_baseOverTopologyandAlgebraicGeometry.isCocontinuous_ιOfLE_baseOverTopology.
theorem fullyFaithful_isContinuous_isCocontinuous_ιOfLE_baseOverTopology (τ : CoveringTopology)
{P₁ P₂ : ObjectProperty (BigFppfOver B X hX)} (h₁₂ : P₁ ≤ P₂)
(hcov₁ : IsClosedUnderCoverings τ P₁) (hcov₂ : IsClosedUnderCoverings τ P₂) :
(ObjectProperty.ιOfLE h₁₂).Full ∧ (ObjectProperty.ιOfLE h₁₂).Faithful ∧
(ObjectProperty.ιOfLE h₁₂).IsContinuous
(P₁.ι.inheritedTopology (BigFppfOver.baseOverTopology B X hX τ.toSiteKind))
(P₂.ι.inheritedTopology (BigFppfOver.baseOverTopology B X hX τ.toSiteKind)) ∧
(ObjectProperty.ιOfLE h₁₂).IsCocontinuous
(P₁.ι.inheritedTopology (BigFppfOver.baseOverTopology B X hX τ.toSiteKind))
(P₂.ι.inheritedTopology (BigFppfOver.baseOverTopology B X hX τ.toSiteKind))
AlgebraicGeometry.isIso_lowerShriekStructureSheafHom_baseOverTopology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/SubcategoryBigFppfLowerShriek.lean, line 465. The attribute's comment: “part (b), at the inherited topologies, for every τ”.
Stacks 07AJ (b). Let
τbe any of the Zariski, étale, smooth, syntomic and fppf topologies, and letC₁ ⊆ C₂be full subcategories of the big category over a schemeX, each with the topology it inherits from the bigτ-site overX, both satisfying the closure condition (1)(a) of the source, and letC₁contain the base objectX/Xand the affine line over each of its objects — conditions (2) and (1)(b). Writingg : Sh(C₁) ⟶ Sh(C₂)for the morphism of topoi of the inclusion, the canonical mapg_!O₁ ⟶ O₂from the lower shriek of the restriction of the structure sheaf to the structure sheaf is an isomorphism.The continuity of the inclusion that
gandg_!refer to isAlgebraicGeometry.isContinuous_ιOfLE_baseOverTopology; the existence ofg_!is instance search on the essential smallness of the two sites; the descent witness for the structure presheaf ofC₂isAlgebraicGeometry.isSheaf_inheritedTopology_bigOverPresheafAb. With those three supplied, the assertion isAlgebraicGeometry.isIso_lowerShriekStructureSheafHom_of_isClosedUnderAffineLineread at the inherited topologies.
theorem isIso_lowerShriekStructureSheafHom_baseOverTopology (τ : CoveringTopology)
{P₁ P₂ : ObjectProperty (BigFppfOver B X hX)} (h₁₂ : P₁ ≤ P₂)
(hcov₁ : IsClosedUnderCoverings τ P₁) (hcov₂ : IsClosedUnderCoverings τ P₂)
(hbase : P₁ (Over.mk (𝟙 (B.obj hX)))) (hline : IsClosedUnderAffineLine P₁) :
letI : (ObjectProperty.ιOfLE h₁₂).IsContinuous
(P₁.ι.inheritedTopology (BigFppfOver.baseOverTopology B X hX τ.toSiteKind))
(P₂.ι.inheritedTopology (BigFppfOver.baseOverTopology B X hX τ.toSiteKind)) :=
isContinuous_ιOfLE_baseOverTopology τ h₁₂ hcov₁
IsIso (lowerShriekStructureSheafHom h₁₂
(P₁.ι.inheritedTopology (BigFppfOver.baseOverTopology B X hX τ.toSiteKind))
(P₂.ι.inheritedTopology (BigFppfOver.baseOverTopology B X hX τ.toSiteKind))
(isSheaf_inheritedTopology_bigOverPresheafAb τ hcov₂))
Declarations registered for the tag:
ObjectProperty.fullyFaithfulιOfLEregistered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Topologies/SubcategoryAffineLineClosure.lean, line 257 (StacksFrontier): “part (a), full faithfulness”.ObjectProperty.isContinuous_ιOfLE_inheritedTopologyregistered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Topologies/SubcategoryAffineLineClosure.lean, line 259 (StacksFrontier): “part (a), continuity”.ObjectProperty.isCocontinuous_ιOfLE_inheritedTopologyregistered withadd_to_stacksin StacksFrontier/AlgebraicGeometry/Topologies/SubcategoryAffineLineClosure.lean, line 261 (StacksFrontier): “part (a), cocontinuity”.
Sources
Section59.50 Étale cohomology#
Section 59.50 of the Stacks Project, Tag 03Q3. 2 tags here are carried by 11 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0A50, a lemma
Tag 0A50 in the Stacks Project.
Stacks.EtaleCohomology.MayerVietoris.cohomologySequence_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/MayerVietoris.lean, line 325. The attribute's comment: “exactness of each six-term window”.
Stacks 0A50. The Mayer--Vietoris sequence in étale cohomology is exact: for open subschemes
U,Vof a schemeXand an abelian sheafFon the small étale site ofX, every six-term window of
⋯ ⟶ Hⁿ(U ⊔ V, F) ⟶ Hⁿ(U, F) ⊞ Hⁿ(V, F) ⟶ Hⁿ(U ⊓ V, F) ⟶ Hⁿ⁺¹(U ⊔ V, F) ⟶ ⋯is exact.
theorem cohomologySequence_exact (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁) :
(cohomologySequence F U V n₀ n₁ h).Exact
Stacks.EtaleCohomology.MayerVietoris.initialSequence_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/MayerVietoris.lean, line 343. The attribute's comment: “the long exact sequence, with its leading zero”.
Stacks 0A50. The Mayer--Vietoris sequence in étale cohomology is exact at its initial segment, leading zero included: the sum of the two restriction maps
H⁰(U ⊔ V, F) ⟶ H⁰(U, F) ⊞ H⁰(V, F)is injective.
theorem initialSequence_exact : (initialSequence F U V).Exact
Stacks.EtaleCohomology.MayerVietoris.mayerVietoris_longExactSequence_etaleCohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/MayerVietorisAbsolute.lean, line 582.
Stacks 0A50: Mayer--Vietoris for étale cohomology. For open subschemes
U,Vof a schemeXand an abelian sheafFon the small étale site ofX, the sequence
0 ⟶ H⁰(U ∪ V, F) ⟶ H⁰(U, F) ⊞ H⁰(V, F) ⟶ H⁰(U ∩ V, F) ⟶ H¹(U ∪ V, F) ⟶ H¹(U, F) ⊞ H¹(V, F) ⟶ H¹(U ∩ V, F) ⟶ ⋯of absolute étale cohomology groups of the open subschemes
U ∪ V,U,V,U ∩ Vis a long exact sequence, functorial inF. That is the conjunction of the clauses stated here:
- its initial segment is exact, leading zero included, which is exactness at
H⁰(U ∪ V, F), the one place no six-term window reaches;- every six-term window of it is exact, which is exactness at
Hⁿ(U, F) ⊞ Hⁿ(V, F)and atHⁿ(U ∩ V, F)for everyn, and atHⁿ(U ∪ V, F)for everyn ≥ 1;- each of the three families of maps of the sequence — the connecting morphisms, the sum of the two restriction maps and their difference — is natural in
F, so that a morphism of abelian sheaves induces a morphism of long exact sequences: this is the functoriality the source asserts.The first two clauses together are exactness at every term of the sequence.
The terms are the étale cohomology of the schemes
U ∪ V,U,V,U ∩ Vwith coefficients in the restriction ofFto their small étale sites. The comparison with the cohomology over those opens read as objects of the small étale site ofX, which is where the exactness is proved, isStacks.EtaleCohomology.MayerVietoris.h'OpensIsoH, and the arrows of the sequence are the arrows ofStacks.EtaleCohomology.MayerVietoris.mayerVietoris_longExactSequenceread through it.The statement is made for arbitrary open subschemes
U,V, so it is more general than the source, whose hypothesis isX = U ∪ V: in that case the open subschemeU ⊔ VisXitself, and the same ambient terms are identified with the global étale cohomology groupsHⁿ(F)on the small étale site ofXdirectly byStacks.EtaleCohomology.MayerVietoris.cohomologySupIsoH.
theorem mayerVietoris_longExactSequence_etaleCohomology :
(absoluteInitialSequence F U V).Exact ∧
(∀ (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁), (absoluteSequence F U V n₀ n₁ h).Exact) ∧
(∀ (G' : Sheaf (topology X) AddCommGrpCat.{u + 1}) (f : F ⟶ G') (n₀ n₁ : ℕ)
(h : n₀ + 1 = n₁),
opensCohomologyMap X (U ⊓ V) n₀ f ≫ absoluteDelta G' U V n₀ n₁ h =
absoluteDelta F U V n₀ n₁ h ≫ opensCohomologyMap X (U ⊔ V) n₁ f) ∧
(∀ (G' : Sheaf (topology X) AddCommGrpCat.{u + 1}) (f : F ⟶ G') (n : ℕ),
opensCohomologyMap X (U ⊔ V) n f ≫ absoluteToBiprod G' U V n =
absoluteToBiprod F U V n ≫
biprod.map (opensCohomologyMap X U n f) (opensCohomologyMap X V n f)) ∧
∀ (G' : Sheaf (topology X) AddCommGrpCat.{u + 1}) (f : F ⟶ G') (n : ℕ),
biprod.map (opensCohomologyMap X U n f) (opensCohomologyMap X V n f) ≫
absoluteFromBiprod G' U V n =
absoluteFromBiprod F U V n ≫ opensCohomologyMap X (U ⊓ V) n f
Stacks.EtaleCohomology.MayerVietoris.mayerVietoris_longExactSequence_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/MayerVietorisAbsolute.lean, line 829. The attribute's comment: “the source's own statement: the hypothesis X = U ∪ V, with the ambient terms of the sequence the global étale cohomology groups of X itself”.
Stacks 0A50: Mayer--Vietoris for étale cohomology, as the source states it. Let
Xbe a scheme which is the unionX = U ∪ Vof two open subschemes and letFbe an abelian sheaf on the small étale site ofX. Then
0 ⟶ H⁰(X, F) ⟶ H⁰(U, F) ⊞ H⁰(V, F) ⟶ H⁰(U ∩ V, F) ⟶ H¹(X, F) ⟶ H¹(U, F) ⊞ H¹(V, F) ⟶ H¹(U ∩ V, F) ⟶ ⋯is a long exact sequence, functorial in
F. That is the conjunction of the clauses stated here:
- its initial segment is exact, leading zero included, which is exactness at
H⁰(X, F), the one place no six-term window reaches;- every six-term window of it is exact, which is exactness at
Hⁿ(U, F) ⊞ Hⁿ(V, F)and atHⁿ(U ∩ V, F)for everyn, and atHⁿ(X, F)for everyn ≥ 1;- each of the three families of maps of the sequence — the connecting morphisms, the sum of the two restriction maps and their difference — is natural in
F, so that a morphism of abelian sheaves induces a morphism of long exact sequences: this is the functoriality the source asserts.The first two clauses together are exactness at every term of the sequence.
The ambient terms are the global étale cohomology groups of
Xitself, which is the hypothesisU ⊔ V = ⊤being used: the other terms are the étale cohomology of the schemesU,V,U ∩ Vwith coefficients in the restriction ofFto their small étale sites.This is the statement of
Stacks.EtaleCohomology.MayerVietoris.mayerVietoris_longExactSequence_etaleCohomology, which makes no hypothesis onUandVand whose ambient terms are therefore the étale cohomology of the open subschemeU ∪ V, transported along the comparisonsupIsoGlobalHof those terms with the global étale cohomology ofX. Nothing of the Mayer--Vietoris sequence is reproved.
theorem mayerVietoris_longExactSequence_cover (hUV : U ⊔ V = ⊤) :
(coverInitialSequence F U V hUV).Exact ∧
(∀ (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁), (coverSequence F U V hUV n₀ n₁ h).Exact) ∧
(∀ (G' : Sheaf (topology X) AddCommGrpCat.{u + 1}) (f : F ⟶ G') (n₀ n₁ : ℕ)
(h : n₀ + 1 = n₁),
opensCohomologyMap X (U ⊓ V) n₀ f ≫ coverDelta G' U V hUV n₀ n₁ h =
coverDelta F U V hUV n₀ n₁ h ≫ globalCohomologyMap X n₁ f) ∧
(∀ (G' : Sheaf (topology X) AddCommGrpCat.{u + 1}) (f : F ⟶ G') (n : ℕ),
globalCohomologyMap X n f ≫ coverToBiprod G' U V hUV n =
coverToBiprod F U V hUV n ≫
biprod.map (opensCohomologyMap X U n f) (opensCohomologyMap X V n f)) ∧
∀ (G' : Sheaf (topology X) AddCommGrpCat.{u + 1}) (f : F ⟶ G') (n : ℕ),
biprod.map (opensCohomologyMap X U n f) (opensCohomologyMap X V n f) ≫
absoluteFromBiprod G' U V n =
absoluteFromBiprod F U V n ≫ opensCohomologyMap X (U ⊓ V) n f
Tag 0EYK, a lemma
Tag 0EYK in the Stacks Project.
Stacks.EtaleCohomology.RelativeMayerVietoris.toCover, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/RelativeMayerVietoris.lean, line 659. The attribute's comment: “the map Rⁿf_F → Rⁿa_(F|_U) ⊕ Rⁿb_*(F|_V)”.
The first map of the Mayer--Vietoris sequence in degree
n,Rⁿf_*F ⟶ Rⁿa_*(F|_U) ⊕ Rⁿb_*(F|_V), as a natural transformation of functors inF: that naturality is the functoriality asserted by the statement.
def toCover (n : ℕ) :
higherDirectImage.{u, v} f n ⟶
restrictedHigherDirectImage.{u, v} f U n ⊞
restrictedHigherDirectImage.{u, v} f V n
Stacks.EtaleCohomology.RelativeMayerVietoris.toIntersection, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/RelativeMayerVietoris.lean, line 670. The attribute's comment: “the map Rⁿa_(F|_U) ⊕ Rⁿb_(F|_V) → Rⁿc_*(F|_{U ∩ V})”.
The second map of the Mayer--Vietoris sequence in degree
n,Rⁿa_*(F|_U) ⊕ Rⁿb_*(F|_V) ⟶ Rⁿc_*(F|_{U ∩ V}), as a natural transformation of functors inF.
def toIntersection (n : ℕ) :
restrictedHigherDirectImage.{u, v} f U n ⊞
restrictedHigherDirectImage.{u, v} f V n ⟶
restrictedHigherDirectImage.{u, v} f (U ⊓ V) n
Stacks.EtaleCohomology.RelativeMayerVietoris.boundary, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/RelativeMayerVietoris.lean, line 681. The attribute's comment: “the connecting map Rⁿc_(F|_{U ∩ V}) → Rⁿ⁺¹f_F”.
The connecting map of the Mayer--Vietoris sequence,
Rⁿc_*(F|_{U ∩ V}) ⟶ Rⁿ⁺¹f_*F, as a natural transformation of functors inF.
def boundary (hUV : U ⊔ V = ⊤) (n : ℕ) :
restrictedHigherDirectImage.{u, v} f (U ⊓ V) n ⟶
higherDirectImage.{u, v} f (n + 1)
Stacks.EtaleCohomology.RelativeMayerVietoris.cohomologySequence_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/RelativeMayerVietoris.lean, line 698. The attribute's comment: “exactness of the long sequence”.
Stacks Project, Tag 0EYK (relative Mayer--Vietoris), exactness. For a morphism
f : X ⟶ Yof schemes, two open subschemesUandVcoveringX, and every abelian sheafFon the small étale site ofX, the six-term window
Rⁿf_*F ⟶ Rⁿa_*(F|_U) ⊕ Rⁿb_*(F|_V) ⟶ Rⁿc_*(F|_{U ∩ V}) ⟶ Rⁿ⁺¹f_*F ⟶ ⋯of the Mayer--Vietoris sequence is exact, for every
n. Since the three maps are natural transformations of functors ofF, the sequence is functorial inF.
theorem cohomologySequence_exact (hUV : U ⊔ V = ⊤) (n : ℕ)
(F : Sheaf X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v}) :
(ComposableArrows.mk₅ ((toCover.{u, v} f U V n).app F)
((toIntersection.{u, v} f U V n).app F) ((boundary.{u, v} f U V hUV n).app F)
((toCover.{u, v} f U V (n + 1)).app F)
((toIntersection.{u, v} f U V (n + 1)).app F)).Exact
Stacks.EtaleCohomology.RelativeMayerVietoris.mono_toCover_zero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/RelativeMayerVietoris.lean, line 736. The attribute's comment: “the sequence begins with 0 ⟶ f_*F”.
Stacks Project, Tag 0EYK (relative Mayer--Vietoris), the left end. The Mayer--Vietoris sequence starts with
0 ⟶ f_*F: the degree-zero mapf_*F ⟶ a_*(F|_U) ⊕ b_*(F|_V)is a monomorphism.
theorem mono_toCover_zero (hUV : U ⊔ V = ⊤)
(F : Sheaf X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v}) :
Mono ((toCover.{u, v} f U V 0).app F)
Stacks.EtaleCohomology.RelativeMayerVietoris.higherDirectImageZeroIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/RelativeMayerVietoris.lean, line 753. The attribute's comment: “the degree-zero term is f_*F”.
The degree-zero term of the sequence is the direct image itself. The direct image along
fis left exact, being a right adjoint, soR⁰f_* ≅ f_*; this is what makes the sequence of the statement begin with0 ⟶ f_*F.
def higherDirectImageZeroIso :
higherDirectImage.{u, v} f 0 ≅ etaleAbelianDirectImage.{u, v} f
Stacks.EtaleCohomology.RelativeMayerVietoris.restrictedHigherDirectImageZeroIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/RelativeMayerVietoris.lean, line 761. The attribute's comment: “the degree-zero restricted term is a_*(F|_U)”.
The degree-zero restricted term of the sequence is the pushed-forward restriction itself,
R⁰(F ↦ a_*(F|_U)) ≅ (F ↦ a_*(F|_U)): restriction toUis exact and the direct image alonga = f|_Uis left exact.
def restrictedHigherDirectImageZeroIso :
restrictedHigherDirectImage.{u, v} f U 0 ≅ restrictedPushforward.{u, v} f U
Sources
Section59.51 Colimits#
Section 59.51 of the Stacks Project, Tag 03Q4. 10 tags here are carried by 40 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0EZL, a definition
Tag 0EZL in the Stacks Project.
Stacks.EtaleCohomology.inverseImageSystem, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Colimits/InverseImageSystem.lean, line 111. The attribute's comment: “the system of INVERSE IMAGES of a single sheaf: for a cocone on the inverse system with vertex S and an abelian sheaf on the small etale site of S, the system 𝒢_i = (D_i ⟶ S)^{-1} ℱ together with its cocycle condition, constructed and not assumed. Coefficients are Ab.{u + 1} on Mathlib's Scheme.smallEtaleTopology, which is where the inverse image of abelian sheaves exists unconditionally”.
The system of inverse images of a single sheaf, constructed. Let
Dbe an inverse system of schemes, letdbe a cocone on it with vertexS— so everyD_icarries a morphismD_i ⟶ Scompatible with the transitions — and letℱbe an abelian sheaf on the small étale site ofS. The inverse images(D_i ⟶ S)^{-1} ℱ, with the transition maps supplied bycoconeInverseImageComp, form a system of sheaves onDin the sense of Stacks 0EZL.The cocycle condition is the associativity pentagon
smallEtalePullbackAbCompIso'_assocof the inverse-image comparison, at the three morphismsD_i ⟶ D_j ⟶ D_k ⟶ S.
def inverseImageSystem : EtaleSheafSystem D Ab.{u + 1}
Stacks.EtaleCohomology.EtaleSheafSystem, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Colimits/SheafSystems.lean, line 110.
A system of sheaves on an inverse system of schemes
D: a sheaf on the small étale site of each member, together with a map from the inverse image of the sheaf at an index to the sheaf at any larger index, compatible with composition of the transition morphisms through the canonical comparisonStacks.EtaleCohomology.systemPullbackComp.
public structure EtaleSheafSystem
Tag 0EYL, a lemma
Tag 0EYL in the Stacks Project.
Stacks.EtaleCohomology.affineEtaleSiteColimit, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Colimits/AffineEtaleSites/ColimitSite.lean, line 40. The attribute's comment: “canonical site system”.
Stacks 0EYL. Let
Ibe a directed set, let(X_i, f_{i'i})be an inverse system of schemes overIwith affine transition morphisms and letX = lim X_i. ThenX_{affine, étale} = colim (X_i)_{affine, étale}as sites in the sense of Stacks 09YL.
public noncomputable def affineEtaleSiteColimit (hc : IsLimit c)
[∀ {i j : Iᵒᵖ} (a : i ⟶ j), IsAffineHom (D.map a)] :
AffineEtaleSiteColimit D c B hD hX
Stacks.EtaleCohomology.affineEtaleSiteColimit_level_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Colimits/AffineEtaleSites/ColimitSite.lean, line 88. The attribute's comment: “level coverings”.
The level equivalences identify the Grothendieck topologies: a presieve is covering at a stage exactly when its image generates a covering sieve of the corresponding affine étale site. Finiteness is not imposed here, since an equivalence can identify distinct isomorphic source objects and need not reflect finiteness of a particular presieve.
public theorem affineEtaleSiteColimit_level_cover
(i : (affineEtaleSiteColimit D c B hD hX hc).system.I)
(Y : (affineEtaleSiteColimit D c B hD hX hc).system.C i) (R : Presieve Y) :
R ∈ ((affineEtaleSiteColimit D c B hD hX hc).system.J i).toPrecoverage Y ↔
R.map ((affineEtaleSiteColimit D c B hD hX hc).levelEquiv i).functor ∈
(AlgebraicGeometry.SmallAffineEtale.topology B
(D.obj ((affineEtaleSiteColimit D c B hD hX hc).indexEquiv.functor.obj i))
(hD ((affineEtaleSiteColimit D c B hD hX hc).indexEquiv.functor.obj
i))).toPrecoverage
(((affineEtaleSiteColimit D c B hD hX hc).levelEquiv i).functor.obj Y)
Stacks.EtaleCohomology.affineEtaleSiteColimit_levelEquiv_isDenseSubsite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Colimits/AffineEtaleSites/ColimitSite.lean, line 112. The attribute's comment: “level coverings, as a dense subsite”.
The level equivalences identify the Grothendieck topologies, in the form of a dense subsite. The topology of a level is the topology induced on the category of representatives by the level equivalence, so that equivalence's functor is a dense subsite of the small affine étale site of the corresponding
X_i.This is
affineEtaleSiteColimit_level_coverin the form typeclass inference consumes. The covering correspondence is a statement about presieves; transporting sheaves across a level needs continuity of the functor as an instance, andCategoryTheory.Functor.IsDenseSubsitecarries both that and the cover-lifting direction. Nothing is asserted beyond the covering correspondence: the content is that it holds for sieves at every object, which is what makes the induced topology the topology of the level.
public theorem affineEtaleSiteColimit_levelEquiv_isDenseSubsite
(i : (affineEtaleSiteColimit D c B hD hX hc).system.I) :
((affineEtaleSiteColimit D c B hD hX hc).levelEquiv i).functor.IsDenseSubsite
((affineEtaleSiteColimit D c B hD hX hc).system.J i)
(AlgebraicGeometry.SmallAffineEtale.topology B
(D.obj ((affineEtaleSiteColimit D c B hD hX hc).indexEquiv.functor.obj i))
(hD ((affineEtaleSiteColimit D c B hD hX hc).indexEquiv.functor.obj i)))
Stacks.EtaleCohomology.affineEtaleSiteColimit_levelToSmallEtale_isContinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Colimits/AffineEtaleSites/ColimitSite.lean, line 133. The attribute's comment: “levels as morphisms of sites to the small étale sites”.
A level of the system, carried into the small étale site of its scheme, is a morphism of sites. The composite of the level equivalence with the inclusion of Stacks 04HR is continuous from the topology of the level to the small étale topology of
X_i.This is the level-side counterpart of
Stacks.EtaleCohomology.AffineLimitCohomology.isContinuous_limitToSmallEtale, and unlike that one it is not a universe raising followed by 04HR: a level of this system is a category of representatives, equivalent to the small affine étale site ofX_ibut not equal to it, so the first factor is the level equivalence and its continuity isaffineEtaleSiteColimit_levelEquiv_isDenseSubsite. Without this a sheaf on the small étale site ofX_icannot be read on the level at all.
public theorem affineEtaleSiteColimit_levelToSmallEtale_isContinuous
(i : (affineEtaleSiteColimit D c B hD hX hc).system.I) :
(((affineEtaleSiteColimit D c B hD hX hc).levelEquiv i).functor ⋙
AlgebraicGeometry.SmallAffineEtale.inclusion B
(D.obj ((affineEtaleSiteColimit D c B hD hX hc).indexEquiv.functor.obj i))
(hD ((affineEtaleSiteColimit D c B hD hX hc).indexEquiv.functor.obj
i))).IsContinuous
((affineEtaleSiteColimit D c B hD hX hc).system.J i)
(AlgebraicGeometry.SmallEtale.topology B
(D.obj ((affineEtaleSiteColimit D c B hD hX hc).indexEquiv.functor.obj i))
(hD ((affineEtaleSiteColimit D c B hD hX hc).indexEquiv.functor.obj i)))
Stacks.EtaleCohomology.affineEtaleSiteColimit_levelToSmallEtale_sheafEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Colimits/AffineEtaleSites/ColimitSite.lean, line 155. The attribute's comment: “sheaves of a level are sheaves of the small étale site of its scheme”.
Restriction of sheaves of sets from the small étale site of
X_ito a level is an equivalence. Both factors of the crossing are: the level equivalence byaffineEtaleSiteColimit_levelEquiv_isDenseSubsite, and the inclusion of the small affine étale site by Stacks 04HR.This says that reading a sheaf of a level as the restriction of a sheaf on the small étale site of
X_iis no restriction on the level sheaf: every one of them is isomorphic to such a restriction, and every map of them to a map of those.
public theorem affineEtaleSiteColimit_levelToSmallEtale_sheafEquiv
(i : (affineEtaleSiteColimit D c B hD hX hc).system.I) :
letI := affineEtaleSiteColimit_levelToSmallEtale_isContinuous D c B hD hX hc i
((((affineEtaleSiteColimit D c B hD hX hc).levelEquiv i).functor ⋙
AlgebraicGeometry.SmallAffineEtale.inclusion B
(D.obj ((affineEtaleSiteColimit D c B hD hX hc).indexEquiv.functor.obj i))
(hD ((affineEtaleSiteColimit D c B hD hX hc).indexEquiv.functor.obj
i))).sheafPushforwardContinuous (Type (max u v + 1))
((affineEtaleSiteColimit D c B hD hX hc).system.J i)
(AlgebraicGeometry.SmallEtale.topology B
(D.obj ((affineEtaleSiteColimit D c B hD hX hc).indexEquiv.functor.obj i))
(hD ((affineEtaleSiteColimit D c B hD hX hc).indexEquiv.functor.obj
i)))).IsEquivalence
Stacks.EtaleCohomology.affineEtaleSiteColimit_obj_descends, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Colimits/AffineEtaleSites/ColimitSite.lean, line 180. The attribute's comment: “objects”.
Every affine étale object over the limit descends to a finite stage.
public theorem affineEtaleSiteColimit_obj_descends
(Z : AlgebraicGeometry.SmallAffineEtale B c.pt hX) :
∃ (i : (affineEtaleSiteColimit D c B hD hX hc).system.I)
(Y : (affineEtaleSiteColimit D c B hD hX hc).system.C i),
((affineEtaleSiteColimit D c B hD hX hc).toLimit i).obj Y = Z
Stacks.EtaleCohomology.affineEtaleSiteColimit_hom_descends, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Colimits/AffineEtaleSites/ColimitSite.lean, line 190. The attribute's comment: “morphisms”.
Every morphism between objects descended from one stage descends after increasing the stage.
public theorem affineEtaleSiteColimit_hom_descends
(i : (affineEtaleSiteColimit D c B hD hX hc).system.I)
(X Y : (affineEtaleSiteColimit D c B hD hX hc).system.C i)
(f : ((affineEtaleSiteColimit D c B hD hX hc).toLimit i).obj X ⟶
((affineEtaleSiteColimit D c B hD hX hc).toLimit i).obj Y) :
∃ (j : (affineEtaleSiteColimit D c B hD hX hc).system.I) (a : j ⟶ i)
(g : ((affineEtaleSiteColimit D c B hD hX hc).system.u a).obj X ⟶
((affineEtaleSiteColimit D c B hD hX hc).system.u a).obj Y),
((affineEtaleSiteColimit D c B hD hX hc).toLimit j).map g =
eqToHom (Functor.congr_obj
((affineEtaleSiteColimit D c B hD hX hc).toLimit_transition a) X) ≫ f ≫
eqToHom (Functor.congr_obj
((affineEtaleSiteColimit D c B hD hX hc).toLimit_transition a) Y).symm
Stacks.EtaleCohomology.affineEtaleSiteColimit_hom_eventually_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Colimits/AffineEtaleSites/ColimitSite.lean, line 334. The attribute's comment: “faithfulness”.
Two morphisms that agree over the limit agree after increasing the stage.
public theorem affineEtaleSiteColimit_hom_eventually_eq
(i : (affineEtaleSiteColimit D c B hD hX hc).system.I)
(X Y : (affineEtaleSiteColimit D c B hD hX hc).system.C i)
(f g : X ⟶ Y)
(hfg : ((affineEtaleSiteColimit D c B hD hX hc).toLimit i).map f =
((affineEtaleSiteColimit D c B hD hX hc).toLimit i).map g) :
∃ (j : (affineEtaleSiteColimit D c B hD hX hc).system.I) (a : j ⟶ i),
((affineEtaleSiteColimit D c B hD hX hc).system.u a).map f =
((affineEtaleSiteColimit D c B hD hX hc).system.u a).map g
Stacks.EtaleCohomology.affineEtaleSiteColimit_mem_precoverage_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Colimits/AffineEtaleSites/ColimitSite.lean, line 569. The attribute's comment: “coverings”.
Coverings of the small affine étale site of the limit are exactly the images of finite coverings from a stage.
public theorem affineEtaleSiteColimit_mem_precoverage_iff
(Z : AlgebraicGeometry.SmallAffineEtale B c.pt hX) (R : Presieve Z) :
R ∈ AlgebraicGeometry.SmallAffineEtale.precoverage B c.pt hX Z ↔
∃ (i : (affineEtaleSiteColimit D c B hD hX hc).system.I)
(Y : (affineEtaleSiteColimit D c B hD hX hc).system.C i)
(h : ((affineEtaleSiteColimit D c B hD hX hc).toLimit i).obj Y = Z)
(S : Presieve Y),
S ∈ ((affineEtaleSiteColimit D c B hD hX hc).system.J i).toPrecoverage Y ∧
S ∈ Precoverage.finite ((affineEtaleSiteColimit D c B hD hX hc).system.C i) Y ∧
R = h ▸ S.map ((affineEtaleSiteColimit D c B hD hX hc).toLimit i)
Stacks.EtaleCohomology.affineEtaleSiteColimit_isColimitPrecoverage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Colimits/AffineEtaleSites/ColimitSite.lean, line 626. The attribute's comment: “colimit site”.
Stacks 0EYL, the clause "as sites in the sense of Stacks 09YL". The standard étale precoverage of the small affine étale site of the limit
X = lim X_iis the colimit precoverage that Stacks 09YL produces from the canonical system: its coverings are exactly the images of the finite coverings of the stages, and it therefore satisfies the three axioms of a site in the sense of Stacks 00VH — a one-element family given by an isomorphism is a covering, coverings are stable under refinement by coverings, and the fibre products of a covering along any morphism exist and again form a covering.
public theorem affineEtaleSiteColimit_isColimitPrecoverage :
(∀ (Z : AlgebraicGeometry.SmallAffineEtale B c.pt hX) (R : Presieve Z),
R ∈ AlgebraicGeometry.SmallAffineEtale.precoverage B c.pt hX Z ↔
∃ (i : (affineEtaleSiteColimit D c B hD hX hc).system.I)
(Y : (affineEtaleSiteColimit D c B hD hX hc).system.C i)
(h : ((affineEtaleSiteColimit D c B hD hX hc).toLimit i).obj Y = Z)
(S : Presieve Y),
S ∈ ((affineEtaleSiteColimit D c B hD hX hc).system.J i).toPrecoverage Y ∧
S ∈ Precoverage.finite
((affineEtaleSiteColimit D c B hD hX hc).system.C i) Y ∧
R = h ▸ S.map ((affineEtaleSiteColimit D c B hD hX hc).toLimit i)) ∧
(AlgebraicGeometry.SmallAffineEtale.precoverage B c.pt hX).HasIsos ∧
(∀ (Z : AlgebraicGeometry.SmallAffineEtale B c.pt hX) (R : Presieve Z)
(T : ∀ ⦃Y : AlgebraicGeometry.SmallAffineEtale B c.pt hX⦄ (f : Y ⟶ Z),
R f → Presieve Y),
R ∈ AlgebraicGeometry.SmallAffineEtale.precoverage B c.pt hX Z →
(∀ ⦃Y : AlgebraicGeometry.SmallAffineEtale B c.pt hX⦄ (f : Y ⟶ Z) (hf : R f),
T f hf ∈ AlgebraicGeometry.SmallAffineEtale.precoverage B c.pt hX Y) →
R.bind T ∈ AlgebraicGeometry.SmallAffineEtale.precoverage B c.pt hX Z) ∧
∃ _ : (AlgebraicGeometry.SmallAffineEtale.precoverage B c.pt hX).HasPullbacks,
∀ (Z W : AlgebraicGeometry.SmallAffineEtale B c.pt hX) (f : W ⟶ Z)
(R : Presieve Z) [R.HasPullbacks f],
R ∈ AlgebraicGeometry.SmallAffineEtale.precoverage B c.pt hX Z →
R.pullbackArrows f ∈
AlgebraicGeometry.SmallAffineEtale.precoverage B c.pt hX W
AlgebraicGeometry.smallEtaleStagesCoveringsRefine_of_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Colimits/SmallEtaleCoveringsRefine.lean, line 382. The attribute's comment: “coverings of the final object, for the small étale site”.
Stacks 0EYL for the small étale site. Let
X = lim X_ibe the limit of a directed inverse system of quasi-compact, quasi-separated schemes with affine transition morphisms inside a big étale site. Every covering of the final object of the small étale site ofXis refined by the inverse image of a finite covering of the final object at some stage beyond a prescribed one.The hypotheses are the three geometric conditions the assertion needs and which
AlgebraicGeometry.SmallEtaleStagesCoveringsRefine, a predicate on an arbitrary cone, does not itself carry: the cone is limiting, the transition morphisms are affine, and the stages are quasi-compact and quasi-separated. Quasi-compactness is not cosmetic: the conclusion demands a finite refining family, and over a vertex which is an infinite disjoint union the covering by the components admits none.
public theorem smallEtaleStagesCoveringsRefine_of_isLimit (hc : IsLimit c)
(haff : ∀ {p q : Iᵒᵖ} (e : p ⟶ q), IsAffineHom (B.inclusion.map (Dg.map e)))
(hqc : ∀ p : I, CompactSpace (Dg.obj (op p)).obj)
(hqs : ∀ p : I, QuasiSeparatedSpace (Dg.obj (op p)).obj) :
SmallEtaleStagesCoveringsRefine B Dg c hX
Tag 09YQ, a theorem
Tag 09YQ in the Stacks Project.
Stacks.EtaleCohomology.AffineLimitCohomology.transitionImage_isoLevelTerminal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Colimits/AffineEtaleCohomologyColimit.lean, line 444. The attribute's comment: “the affine case: the transition image of the terminal object X_i is the terminal object X_j, so the value of the cohomology diagram at a : j ⟶ i is the cohomology over X_j”.
Stacks 09YQ, the diagram values. The transition image of
X_iat a leveljbelowiisX_j: the value of the cohomology diagram ata : j ⟶ iis the cohomology ofF_jover the terminal object of the site ofX_j, that is overX_jitself.
def transitionImage_isoLevelTerminal {i j : (sys D c B hD hX hc).I} (a : j ⟶ i) :
((sys D c B hD hX hc).u a).obj (levelTerminal D c B hD hX hc i) ≅
levelTerminal D c B hD hX hc j
Stacks.EtaleCohomology.AffineLimitCohomology.toLimitImage_isoLimitTerminal, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Colimits/AffineEtaleCohomologyColimit.lean, line 457. The attribute's comment: “the affine case: the image of the terminal object X_i in the site of the limit is the terminal object X, so the vertex of the cohomology cocone is the cohomology over X”.
Stacks 09YQ, the cocone vertex. The image of
X_iin the site of the limit isX: the vertex of the cohomology cocone is the cohomology of𝒢over the terminal object of the site ofX, that is overXitself.
def toLimitImage_isoLimitTerminal (i : (sys D c B hD hX hc).I) :
(toLimitSmall D c B hD hX hc i).obj (levelTerminal D c B hD hX hc i) ≅
limitTerminal D c B hX hc
Stacks.EtaleCohomology.AffineLimitCohomology.etaleCohomologyColimit_isColimit_of_affine, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Colimits/AffineEtaleCohomologyColimit.lean, line 487. The attribute's comment: “the affine case: the schemes X_i of the system are affine, so that X_i is itself an object of its own small affine etale site and is the terminal one; the sites are the small AFFINE etale sites and the cohomology of THIS statement is the right-derived sheafSections of Stacks 09YP on them. The comparison across Stacks 04HR that turns those groups into the library's mainstream etale cohomology of a scheme is Stacks.EtaleCohomology.AffineLimitCohomology.limitCohomologyFunctorIsoEtaleCohomology at the limit and ...levelTerminalCohomologyIsoEtaleCohomology at a level”.
Stacks 09YQ, the affine case. Let
Ibe a directed set, let(X_i)be an inverse system of affine schemes overIwith affine transition morphisms, and letX = lim X_i. LetFbe a system of abelian sheaves on the small affine etale sites of theX_i, let𝒢on the small affine etale site ofXpresent the colimitcolim f_i^{-1} F_i, and letpbe a degree. ThenH^p(X, 𝒢)is the filtered colimit, over the arrowsa : j ⟶ i, of the groupsH^p(X_j, F_j): the canonical cocone is a colimit cocone.The base object is
levelTerminal i, which isX_i(levelTerminal_isTerminal); its image in the site of the limit isX(toLimitImage_isoLimitTerminal) and its transition image at a leveljisX_j(transitionImage_isoLevelTerminal), so the vertex and the values of the diagram are the cohomology groups of the schemes of the system.This is Stacks 09YP, applied to the colimit of sites of Stacks 0EYL through
mem_limitSitePrecoverage_iffand the three descent clauses above.
def etaleCohomologyColimit_isColimit_of_affine
(F : InverseSystemOfFiniteSites.AbelianSheafSystem.{v, v, max u v + 1, max u v + 1}
(sys D c B hD hX hc))
(𝒢 : Sheaf (limitSitePrecoverage D c B hX).toGrothendieck Ab.{max u v + 1})
(ι : ∀ j, (F.obj j).obj ⟶ (toLimitSmall D c B hD hX hc j).op ⋙ 𝒢.obj)
(hcolim : IsColimitPresentation.{v, v, max u v + 1, max u v + 1}
(sys D c B hD hX hc) (toLimitSmall D c B hD hX hc)
(toLimitSmall_transition D c B hD hX hc) (limitSitePrecoverage D c B hX) F 𝒢 ι)
(i : (sys D c B hD hX hc).I) (p : ℕ)
(E : CohomologyCocone.{v, v, max u v + 1, max u v + 1}
(sys D c B hD hX hc) (toLimitSmall D c B hD hX hc)
(toLimitSmall_transition D c B hD hX hc) (limitSitePrecoverage D c B hX) F 𝒢 ι i
(levelTerminal D c B hD hX hc i) p) :
IsColimit E.cocone
Stacks.EtaleCohomology.AffineLimitCohomology.etaleCohomologyColimit_isColimit_of_affine_colimitSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Colimits/AffineEtaleCohomologyColimit.lean, line 550. The attribute's comment: “the affine case with the colimit sheaf CONSTRUCTED: the sheaf 𝒢 presenting colim f_i^{-1} F_i on the site of the limit, its legs and its universal property are the left Kan extension of the system and are no longer hypotheses. The system F itself is still given, and the cohomology of THIS statement is the right-derived sheafSections of Stacks 09YP on the small AFFINE etale sites; AffineLimitCohomology.etaleCohomologyColimit_isColimit_of_affine_etaleVertex is the same colimit with its vertex the library's mainstream etale cohomology of the limit.”.
Stacks 09YQ in the affine case, with the colimit sheaf constructed. Let
(X_i)be an inverse system of affine schemes with affine transitions,X = lim X_i, and letFbe a system of abelian sheaves on their small affine etale sites. Then
H^p(X, colim_i f_i^{-1} F_i) = colim_i H^p(X_i, F_i).This is
etaleCohomologyColimit_isColimit_of_affinewith the sheaf presenting the colimit, its legs and its universal property no longer hypotheses but the constructionscolimitSheaf,colimitSheafLegsandisColimitPresentation_colimitSheaf.
def etaleCohomologyColimit_isColimit_of_affine_colimitSheaf
(E : CohomologyCocone.{v, v, max u v + 1, max u v + 1} (sys D c B hD hX hc)
(toLimitSmall D c B hD hX hc) (toLimitSmall_transition D c B hD hX hc)
(limitSitePrecoverage D c B hX) F (colimitSheaf D c B hD hX hc F)
(colimitSheafLegs D c B hD hX hc F) i (levelTerminal D c B hD hX hc i) p :=
cohomologyCoconeOfColimitSheaf D c B hD hX hc F i p) :
IsColimit E.cocone
Stacks.EtaleCohomology.QcqsLimitCohomology.etaleCohomologyColimit_isColimit, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Colimits/QcqsEtaleCohomologyColimit.lean, line 233. The attribute's comment: “the general case of the levels: the schemes X_i are arbitrary — only the transition morphisms are affine — and the cohomology is taken over an arbitrary object Z of the small affine etale site of X_i, whose transition images and whose image in the site of the limit carry the groups of the diagram and the vertex. For an affine X_i the terminal object of that site is X_i itself and this specializes to the affine case already recorded in Stacks.EtaleCohomology.AffineLimitCohomology; for a merely quasi-compact and quasi-separated X_i, which is NOT an object of its own small affine etale site, the identification of this cohomology with H^p(X_i, F_i) is the Cech / Mayer-Vietoris descent along a finite affine cover and is NOT performed here — only the covering input is, in exists_finite_jointlySurjective_smallAffineEtale. The sites are the small AFFINE etale sites and the cohomology is the right-derived sheafSections of the weak-system Stacks 09YP on them, not the library's mainstream etale cohomology of a scheme, the comparison across Stacks 04HR not being performed here. No hypothesis of this statement is an instance of its own conclusion.”.
Stacks 09YQ for arbitrary levels, over an arbitrary object of a level. Let
Ibe a directed set, let(X_i)be an inverse system of schemes overIwhose transition morphisms are affine, and letX = lim X_i. LetFbe a system of abelian sheaves on the small affine etale sites of theX_i, let𝒢on the small affine etale site ofXpresent the colimitcolim f_i^{-1} F_i, letZbe an object of the small affine etale site ofX_iand letpbe a degree. ThenH^p(Z_X, 𝒢), the cohomology over the image ofZin the site of the limit, is the filtered colimit, over the arrowsa : j ⟶ i, of the groupsH^p(Z_j, F_j)over the transition images ofZ: the canonical cocone is a colimit cocone.The schemes
X_iare arbitrary here; only the transition morphisms are affine. This is Stacks 09YP, in its weak-system form, applied to the colimit of sites of Stacks 0EYL throughmem_limitSitePrecoverage_iffand the three descent clauses of that file, none of which uses any affineness of the levels.Specialized to affine
X_iandZthe terminal object of the site ofX_i, the objects carrying the cohomology areX_jandX, which is the affine caseStacks.EtaleCohomology.AffineLimitCohomology.etaleCohomologyColimit_isColimit_of_affine. For a merely quasi-compact and quasi-separatedX_ithere is no such terminal object, and the passage from the chartsZtoX_iis the Cech / Mayer-Vietoris step along a finite affine cover; this file supplies only its covering input,exists_finite_jointlySurjective_smallAffineEtale.
def etaleCohomologyColimit_isColimit
(F : InverseSystemOfFiniteSites.AbelianSheafSystem.{v, v, max u v + 1, max u v + 1}
(sys D c B hD hX hc))
(𝒢 : Sheaf (limitSitePrecoverage D c B hX).toGrothendieck Ab.{max u v + 1})
(ι : ∀ j, (F.obj j).obj ⟶ (toLimitSmall D c B hD hX hc j).op ⋙ 𝒢.obj)
(hcolim : IsColimitPresentation.{v, v, max u v + 1, max u v + 1}
(sys D c B hD hX hc) (toLimitSmall D c B hD hX hc)
(toLimitSmall_transition D c B hD hX hc) (limitSitePrecoverage D c B hX) F 𝒢 ι)
(i : (sys D c B hD hX hc).I) (Z : (sys D c B hD hX hc).C i) (p : ℕ)
(E : CohomologyCocone.{v, v, max u v + 1, max u v + 1}
(sys D c B hD hX hc) (toLimitSmall D c B hD hX hc)
(toLimitSmall_transition D c B hD hX hc) (limitSitePrecoverage D c B hX) F 𝒢 ι i Z p) :
IsColimit E.cocone
Stacks.EtaleCohomology.EtaleSheafSystem.isSystemColimit_etaleCohomologyPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Colimits/SheafSystemCohomologyColimit.lean, line 453.
Étale cohomology commutes with limits of quasi-compact quasi-separated schemes with affine transition morphisms ([Stacks, Tag 09YQ]). Let
X = lim X_ibe the limit of a directed inverse system of quasi-compact and quasi-separated schemes with affine transition morphisms,(F_i, φ_{i'i})a system of abelian sheaves on the small étale sites of theX_i, andι_i : f_i⁻¹F_i ⟶ 𝓕a colimit of the system of the inverse images on the small étale site ofX. Then for everypthe pull back mapsH^p(X_i, F_i) ⟶ H^p(X, 𝓕)exhibitH^p(X, 𝓕)as the colimit of the system of theH^p(X_i, F_i).
theorem EtaleSheafSystem.isSystemColimit_etaleCohomologyPullback (p : ℕ)
(F : EtaleSheafSystem D Ab.{u + 1}) (𝓕 : Sheaf (smallEtaleTopology c.pt) Ab.{u + 1})
(ι : ∀ i : Iᵒᵖ, (smallEtalePullbackAb (c.π.app i)).obj (F.obj i) ⟶ 𝓕)
(hι : LimitHigherDirectImage.IsPullbackCocone c F ι)
(hpres : LimitHigherDirectImage.IsPullbackColimitPresentation c 𝓕 F ι) :
IsSystemColimit (fun i => AddCommGrpCat.of (Sheaf.H.{u + 1} (F.obj i) p))
(fun a => AddCommGrpCat.ofHom (etaleCohomologyPullback (D.map a) (F.map a) p))
(AddCommGrpCat.of (Sheaf.H.{u + 1} 𝓕 p))
(fun i => AddCommGrpCat.ofHom (etaleCohomologyPullback (c.π.app i) (ι i) p))
Stacks.EtaleCohomology.SmallEtaleLimitCohomology.isCohomologyColimit_of_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Colimits/SmallEtaleColimitUnconditional.lean, line 132. The attribute's comment: “the whole tag, for ALL degrees p ≥ 0 and every system of abelian sheaves in the sense of Tag 0EZL, with no hypothesis beyond the source's. The source assumes a directed set, affine transition morphisms, X = lim X_i and that every X_i is quasi-compact and quasi-separated; those are IsDirected, IsAffineHom (D.map a), hc : IsLimit c, and the per-level CompactSpace/QuasiSeparatedSpace instances. The big etale site B with hD/hX is a SIZE device and not a source hypothesis: it fixes which small sites are meant, and AlgebraicGeometry.BigEtaleSite.exists_contains_of_small produces one for any small family. The corresponding instances on the VERTEX are derived, not assumed. The conclusion is the tag's equality of groups in elementwise form -- joint surjectivity of the legs together with eventual vanishing, which for a filtered index and abelian coefficients is exactly the assertion that the cocone is colimiting -- and Stacks.EtaleCohomology.SmallEtaleLimitCohomology.isColimit_stableCohomologyCocone transports it, in both directions, to a genuine CategoryTheory.Limits.IsColimit whose vertex is the full H^p(X, 𝒢). No identity law is used: Definition 59.51.1 imposes only the cocycle condition, so the naive diagram i ↦ H^p(X_i, F_i) is not a functor in general, and hasCohomologyIdentityLaw_iff_forall_stableCohomologySubgroup_eq_top says precisely when the two spellings coincide. No hypothesis of this statement is an instance of its own conclusion.”.
[Stacks, Tag 09YQ] on Mathlib's small étale sites, in every degree, unconditionally. Let
Ibe a nonempty directed index, let(X_i)be an inverse system of schemes overIᵒᵖwith affine transition morphisms and everyX_iquasi-compact and quasi-separated, letcbe a limit cone with vertexX, and let all theX_iandXbe objects of a big étale siteB. Then for every presented systemE— a system(F_i)of abelian sheaves on Mathlib's small étale sites of theX_iin the sense of [Stacks, Tag 0EZL], together with an abelian sheaf𝒢on the small étale site ofXand legsι_i : f_i^{-1}F_i ⟶ 𝒢exhibiting𝒢 = colim_i f_i^{-1}F_i— and every degreep, the cohomologyH^p(X, 𝒢)is the filtered colimit of theH^p(X_i, F_i)along the legs.This is
isCohomologyColimit_of_degreeZero_of_affineOpensAcyclicwith all four of its hypotheses supplied; the module docstring says which theorem supplies each, and how the two instances on the vertex are derived rather than assumed.No identity law on the system of [Stacks, Tag 0EZL] is used or available: Definition 59.51.1 of that tag imposes only the cocycle condition, and none of the four suppliers asks for more.
theorem isCohomologyColimit_of_isLimit (p : ℕ)
(E : PresentedSystem (c := c) IsColimitPresentation) : IsCohomologyColimit E p
Tag 03Q5, a lemma
Tag 03Q5 in the Stacks Project.
Stacks.EtaleCohomology.isIso_colimit_post_rightDerived_Γ_smallEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FilteredColimitsOfEtaleCohomology.lean, line 305.
Stacks 03Q5. Let
Xbe a quasi-compact and quasi-separated scheme. For every degreepand every filtered systemFof abelian sheaves on the small étale site ofX, the canonical map
colim_i H^p_étale(X, F_i) ⟶ H^p_étale(X, colim_i F_i)is an isomorphism: taking cohomology of the étale site of
Xcommutes with filtered colimits.Étale cohomology is the right derived functor of global sections, which is sections over the final object
X ⟶ Xof the small étale site; that object is quasi-compact and separated overX, so this is the caseU = XofStacks.EtaleCohomology.isIso_colimit_post_rightDerived_sheafSections_smallEtale.
theorem isIso_colimit_post_rightDerived_Γ_smallEtale (X : Scheme.{u})
[CompactSpace X] [QuasiSeparatedSpace X] (p : ℕ)
{I : Type (max (u + 1) v)} [SmallCategory I] [IsFiltered I]
(F : I ⥤ Sheaf X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v}) :
IsIso (colimit.post F
((Sheaf.Γ X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v}).rightDerived p))
AlgebraicGeometry.isIso_vanishingCyclesFibreMap_app_constantComplex_of_isColimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/LocalAcyclicity/LocallyConstantCoefficientsUnconditional.lean, line 337. The attribute's comment: “for the canonical map of Tag 0GJN at a variety of vanishing cycles, in the unbounded derived category: the locus where the map is invertible on constant coefficients is closed under filtered colimits of the coefficient group”.
Stacks 03Q5 for the canonical map of Tag 0GJN on constant coefficients. The locus where the canonical map
α_{K,x,t}is an isomorphism on constant coefficients is closed under filtered colimits of the coefficient group: ifMis the colimit of a filtered systemNof abelian groups andαis invertible on the constant complex with valueN ifor everyi, then it is invertible on the constant complex with valueM.A map of
D(Ab)is invertible as soon as it is so on cohomology in every degree, and in each degree both sides are functors of the coefficient group commuting with filtered colimits: below degree zero both vanish, and in degreep ≥ 0the stalk side isM ↦ (constant sheaf M)_xplaced in degree zero while the sections side isH^p_étale(F_{x,t}, -)of the inverse image of the constant sheaf. The variety of vanishing cycles is affine, hence quasi-compact and quasi-separated, so [Stacks, Tag 03Q5] on its small étale site applies.See the module docstring for why this is not phrased as preservation of filtered colimits by
α.
theorem isIso_vanishingCyclesFibreMap_app_constantComplex_of_isColimit
(B : BigEtaleSite.{u}) {X S : Scheme.{u}} (hX : B.Contains X) (hS : B.Contains S)
(f : X ⟶ S) (x : GeometricPoint X)
(t : GeometricPoint (strictHenselization B S hS (x.map f)))
{I : Type (u + 1)} [SmallCategory I] [IsFiltered I] (N : I ⥤ Ab.{u + 1})
(c : Cocone N) (hc : IsColimit c)
(hi : ∀ i, IsIso ((vanishingCyclesFibreMap B hX hS f x t).app
(smallEtaleConstantComplexAb X (N.obj i)))) :
IsIso ((vanishingCyclesFibreMap B hX hS f x t).app
(smallEtaleConstantComplexAb X c.pt))
Tag 03Q6, a lemma
Tag 03Q6 in the Stacks Project.
Stacks.EtaleCohomology.ColimitBaseChange.isIso_colimitDesc_algebraCohomologyCocone, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Colimits/AlgebraColimitCohomology.lean, line 159.
Let
Abe a ring,(B_i)a directed system ofA-algebras with colimitB,f : X ⟶ Spec Aquasi-compact and quasi-separated, andFan abelian sheaf onX_étale. WithY_i = Spec B_i ×_{Spec A} X,Y = Spec B ×_{Spec A} XandG_i,Gthe inverse images ofF, the restriction maps exhibitH^p(Y, G)ascolim_i H^p(Y_i, G_i), for everyp.
theorem isIso_colimitDesc_algebraCohomologyCocone [Nonempty I] [IsDirected I (· ≤ ·)]
(hcB : IsColimit cB) [QuasiCompact f] [QuasiSeparated f] (n : ℕ) :
IsIso (colimit.desc (algebraCohomologyDiagram A B f F n)
(algebraCohomologyCocone A B cB f F n))
Stacks.EtaleCohomology.BaseChangeAlgebraSystem.etaleCohomologyColimit_baseChange_systemLimit_isColimit, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Colimits/BaseChangeAlgebraSystemCohomology.lean, line 622. The attribute's comment: “the case of an AFFINE X: the source allows X ⟶ Spec(A) quasi-compact and quasi-separated, and the passage from an affine X to a general qcqs one is the Cech descent along a finite affine cover, which this library does not carry. The system is geometric rather than ring-level: T, the Z_i and X are affine schemes over T, and A, B_i, B = colim B_i are reached through Spec(colim B_i) = lim Spec B_i of Stacks 01YW, no CommRingCat-level wrapper taking a ring and a functor I ⟶ CommRingCat being stated. The base change is written Z_i ×_T X. The cohomology is the right-derived sheafSections of Stacks 09YP on the small AFFINE etale sites, inherited from etaleCohomologyColimit_isColimit_of_affine, and is NOT yet identified with the mainstream Stacks.EtaleCohomology.etaleCohomologyFunctor: the 04HR half of that identification is supplied here by affineEtaleCohomologyFunctorIso, but transporting cohomology across AsSmall.equiv onto the universe-raised site Stacks 09YP is stated on does not exist in this library”.
Stacks 03Q6 for an affine
X, at the canonical limit. This isetaleCohomologyColimit_baseChange_isColimitinstantiated atcY = systemLimitCone T X Z, so that the scheme the cohomology on the left is taken over is the honestY = (lim_i Z_i) ×_T X: withT = Spec A,Z_i = Spec B_iandB = colim_i B_ithis isSpec B ×_{Spec A} X, by Stacks 01YW (AlgebraicGeometry.Scheme.affineLimitCone, throughoverLimitCone_pt_iso).
def etaleCohomologyColimit_baseChange_systemLimit_isColimit
(T : Scheme.{u}) (X : Over T) (Z : Iᵒᵖ ⥤ Over T)
[IsAffine T] [IsAffine X.left] [∀ i, IsAffine (Z.obj i).left]
(B : AlgebraicGeometry.BigEtaleSite.{u})
(hD : ∀ i, B.Contains ((baseChange T X Z).obj i))
(hY : B.Contains (systemLimitCone T X Z).pt)
(F : InverseSystemOfFiniteSites.AbelianSheafSystem.{u, u, u + 1, u + 1}
(bcSys T X Z (systemLimitCone T X Z) (isLimitSystemLimitCone T X Z) B hD hY))
(𝒢 : Sheaf (bcPrecoverage T X Z (systemLimitCone T X Z)
(isLimitSystemLimitCone T X Z) B hD hY).toGrothendieck Ab.{u + 1})
(ι : ∀ j, (F.obj j).obj ⟶ (bcToLimitSmall T X Z (systemLimitCone T X Z)
(isLimitSystemLimitCone T X Z) B hD hY j).op ⋙ 𝒢.obj)
(hcolim : IsColimitPresentation.{u, u, u + 1, u + 1}
(bcSys T X Z (systemLimitCone T X Z) (isLimitSystemLimitCone T X Z) B hD hY)
(bcToLimitSmall T X Z (systemLimitCone T X Z) (isLimitSystemLimitCone T X Z) B hD hY)
(bcToLimitSmall_transition T X Z (systemLimitCone T X Z)
(isLimitSystemLimitCone T X Z) B hD hY)
(bcPrecoverage T X Z (systemLimitCone T X Z) (isLimitSystemLimitCone T X Z) B hD hY) F 𝒢 ι)
(i : (bcSys T X Z (systemLimitCone T X Z) (isLimitSystemLimitCone T X Z) B hD hY).I) (p : ℕ)
(E : CohomologyCocone.{u, u, u + 1, u + 1}
(bcSys T X Z (systemLimitCone T X Z) (isLimitSystemLimitCone T X Z) B hD hY)
(bcToLimitSmall T X Z (systemLimitCone T X Z) (isLimitSystemLimitCone T X Z) B hD hY)
(bcToLimitSmall_transition T X Z (systemLimitCone T X Z)
(isLimitSystemLimitCone T X Z) B hD hY)
(bcPrecoverage T X Z (systemLimitCone T X Z) (isLimitSystemLimitCone T X Z) B hD hY) F 𝒢 ι i
(bcLevelTerminal T X Z (systemLimitCone T X Z)
(isLimitSystemLimitCone T X Z) B hD hY i) p) :
IsColimit E.cocone
Stacks.EtaleCohomology.etaleCohomology_specBaseChange_colimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Colimits/BaseChangeAlgebraSystemQcqs.lean, line 431. The attribute's comment: “the whole lemma, at the source's hypotheses: a ring A, a directed set I (nonempty, as directed sets are in the source), a system of A-algebras B : I ⥤ Under A with a colimit cocone cB (so B = colim B_i is cB.pt), a quasi-compact and quasi-separated g : X ⟶ Spec A, an abelian sheaf F on Mathlib's small etale site of X and every degree p. Y_i and Y are the fibre products Spec B_i ×_{Spec A} X and Spec B ×_{Spec A} X (the factors in Mathlib's pullback order), G_i, G the inverse images of F along their projections to X, and the cohomology is the library's etale cohomology Sheaf.H on the small etale sites, with coefficients in AddCommGrpCat.{u + 1}, the first universe in which these sites have sheafification. The equality of the source is stated as the elementwise form of a filtered colimit of abelian groups along the restriction maps: joint surjectivity of the maps H^p(Y_i, G_i) to H^p(Y, G) and eventual vanishing of a class killed on Y, which over a directed index is exactly the assertion that the cohomology cocone is colimiting. The proof is the source's, Tag 09YQ at the inverse system of base changes.”.
[Stacks, Tag 03Q6]. Let
Abe a ring,Ia nonempty directed set,(B_i)a system ofA-algebras overI(a functorB : I ⥤ Under A) andcBa colimit cocone of it, with vertexB = colim_i B_i. Letg : X ⟶ Spec(A)be quasi-compact and quasi-separated andFan abelian sheaf onX_étale. WriteY_i = Spec(B_i) ×_{Spec A} X,Y = Spec(B) ×_{Spec A} XandG_i,Gfor the inverse images ofFalong the projections toX. Then for everyp,
H^p_étale(Y, G) = colim_i H^p_étale(Y_i, G_i),the colimit taken along the restriction maps of the morphisms
Y_j ⟶ Y_i(fori ≤ j) andY ⟶ Y_i. The colimit is stated elementwise, which over a directed index and with abelian groups is the assertion that the cocone is a colimit: every class onYcomes from someY_i(the inverse image ofG_ionYidentified withGby the composition isomorphism of inverse images), and a class onY_iwhich dies onYalready dies on someY_j,j ≥ i.The proof is the source's: this is [Stacks, Tag 09YQ] at the inverse system of the
Y_i(Stacks.EtaleCohomology.etaleCohomologyBaseChangeColimit), the limitSpec(B) = lim Spec(B_i)being the image of the colimitBunderSpec.
theorem etaleCohomology_specBaseChange_colimit (A : CommRingCat.{u}) (I : Type u) [Preorder I]
[Nonempty I] [IsDirected I (· ≤ ·)] (B : I ⥤ Under A) (cB : Cocone B) (hcB : IsColimit cB)
(X : Scheme.{u}) (g : X ⟶ Spec A) [QuasiCompact g] [QuasiSeparated g]
(F : Sheaf X.smallEtaleTopology AddCommGrpCat.{u + 1}) (p : ℕ) :
(∀ η : Sheaf.H.{u + 1}
((etaleAbelianInverseImage.{u, 0} (pullback.snd (Spec.map cB.pt.hom) g)).obj F) p,
∃ (i : I)
(ξ : Sheaf.H.{u + 1}
((etaleAbelianInverseImage.{u, 0} (pullback.snd (Spec.map (B.obj i).hom) g)).obj F) p),
(etaleCohomologyRestrictionMap.{u, 0, u + 1}
(pullback.map (Spec.map cB.pt.hom) g (Spec.map (B.obj i).hom) g
(Spec.map (cB.ι.app i).right) (𝟙 X) (𝟙 (Spec A))
(by rw [Category.comp_id, ← Spec.map_comp, Under.w]; rfl) (by simp)) _ p ξ).comp
(Ext.mk₀ ((etaleAbelianInverseImageCompIso'.{u, 0}
(pullback.map (Spec.map cB.pt.hom) g (Spec.map (B.obj i).hom) g
(Spec.map (cB.ι.app i).right) (𝟙 X) (𝟙 (Spec A))
(by rw [Category.comp_id, ← Spec.map_comp, Under.w]; rfl) (by simp))
(pullback.snd (Spec.map (B.obj i).hom) g) (pullback.snd (Spec.map cB.pt.hom) g)
(by simp only [pullback.map, pullback.lift_snd, Category.comp_id])).app F).inv)
(add_zero p) = η) ∧
(∀ (i : I)
(ξ : Sheaf.H.{u + 1}
((etaleAbelianInverseImage.{u, 0} (pullback.snd (Spec.map (B.obj i).hom) g)).obj F) p),
etaleCohomologyRestrictionMap.{u, 0, u + 1}
(pullback.map (Spec.map cB.pt.hom) g (Spec.map (B.obj i).hom) g
(Spec.map (cB.ι.app i).right) (𝟙 X) (𝟙 (Spec A))
(by rw [Category.comp_id, ← Spec.map_comp, Under.w]; rfl) (by simp)) _ p ξ = 0 →
∃ (j : I) (a : i ⟶ j),
etaleCohomologyRestrictionMap.{u, 0, u + 1}
(pullback.map (Spec.map (B.obj j).hom) g (Spec.map (B.obj i).hom) g
(Spec.map (B.map a).right) (𝟙 X) (𝟙 (Spec A))
(by rw [Category.comp_id, ← Spec.map_comp, Under.w]) (by simp)) _ p ξ = 0)
Tag 03Q8, a lemma
Tag 03Q8 in the Stacks Project.
Stacks.HigherDirectImage.higherDirectImageComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Comparison/HigherDirectImage.lean, line 460. The attribute's comment: “abelian sheaves”.
Stacks 03Q8 for abelian sheaves. The higher direct image
R^p f_*is the sheafification of the presheafV ↦ H^p_ét(X ×_Y V, F), by a natural isomorphism whose components are the counit-normalized objectwise comparisonhigherDirectImageSheafificationIso, and whose cohomology presheaf has the derived restriction maps of sections.
public def higherDirectImageComparison (p : ℕ) :
HigherDirectImageComparison.{u, w} B f p
Stacks.HigherDirectImage.derivedPushforwardComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Comparison/HigherDirectImageDerived.lean, line 273. The attribute's comment: “unbounded complexes”.
Stacks 03Q8, unbounded complexes. The canonical comparison of
Rf_*with the sheafified derived presheaf of sections over the étale base changes is invertible, evaluating the derived presheaf of sections atVis the total right derived functor of sections overX ×_Y V, and the restriction maps of the hypercohomology presheaf are the derived restriction maps of sections.
public theorem derivedPushforwardComparison : DerivedPushforwardComparison.{u, w} B f
Stacks.HigherDirectImage.higherDirectImageStalkCohomologyPresheafIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/HigherDirectImageStalkColimit.lean, line 103. The attribute's comment: “the stalk form: the stalk at a geometric point s of R^p f_* F is the stalk at s of the cohomology presheaf V ↦ H^p(X ×_Y V, F), hence the colimit of that presheaf over the étale neighbourhoods of s. This is the first display in the source's proof of Stacks 03Q9, which the source attributes to this tag. The base, the morphism f and the geometric point are arbitrary. It is NOT Stacks 03Q9: that tag identifies the colimit with the cohomology of the base change of X to Spec(O^{sh}_{Y,s}), which is Stacks 03Q6 and is not available in a consumable shape”. References: SGA 4 VIII (5.1), “partial”; SGA 4½ Arcata (2.3.3).
Stacks 03Q8 at a geometric point. The stalk at
sof thep-th higher direct image ofFalongfis the stalk atsof the cohomology presheafV ↦ H^p_ét(X ×_Y V, F), which by definition of the stalk is the colimit of that presheaf over the étale neighbourhoods ofs.This is the objectwise comparison of Stacks 03Q8,
higherDirectImageSheafificationIso, followed by the invariance of a stalk under sheafification,AlgebraicGeometry.etaleStalkSheafificationIso.
public def higherDirectImageStalkCohomologyPresheafIso
(F : Sheaf (JX B (X := X)) AddCommGrpCat.{w}) (p : ℕ) :
etaleStalk B Y.obj Y.property s (((pushforward.{u, w} B f).rightDerived p).obj F).obj ≅
etaleStalk B Y.obj Y.property s (preimageCohomologyPresheaf.{u, w} B f F p)
Tag 09Z1, a lemma
Tag 09Z1 in the Stacks Project.
Stacks.EtaleCohomology.FixedBaseHigherDirectImage.transitionMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Colimits/LimitHigherDirectImageFixedBase.lean, line 128. The attribute's comment: “the transition maps ψ_{i'i} : R^p g_{i, *} ℱ_i ⟶ R^p g_{i', *} ℱ_{i'} of the diagram whose colimit the lemma computes, constructed from the base change map on higher direct images of Stacks 0F02 for the square over the fixed base and the transition map of the system of sheaves. The cocycle condition ψ_{i''i} = ψ_{i''i'} ∘ ψ_{i'i} is NOT proved here: the pasting law it reduces to, Stacks.EtaleCohomology.higherBaseChangeMapAb_paste_app, is unconditional, and the cocycle condition for the transition maps of a system of bases is Stacks.EtaleCohomology.LimitHigherDirectImage.transitionMap_comp, but neither is transported to the fixed base, where the comparisons of the inverse image along 𝟙_S have to be moved past them. The colimit assertion R^p g_* ℱ = colim_i R^p g_{i, *} ℱ_i is NOT proved either; it additionally needs Theorem 09YQ at quasi-compact quasi-separated levels and the comparison of Stacks 04HR at the level of cohomology, the carriers of 09YQ in this repository being stated for the right-derived CategoryTheory.sheafSections of the small AFFINE étale sites.”.
The transition map
ψ_{i'i} : R^p g_{i, *} ℱ_i ⟶ R^p g_{i', *} ℱ_{i'}: the base change maphigherBaseChangeMapAbfor the squareg_{i'} ≫ 𝟙_S = f_{i'i} ≫ g_i, read through the identification of the inverse image along𝟙_Swith the identity functor, followed byR^p g_{i', *}of the transition mapφ_{i'i} : f_{i'i}^{-1}ℱ_i ⟶ ℱ_{i'}of the system of sheaves.
def transitionMap (F : EtaleSheafSystem D Ab.{u + 1}) {i j : Iᵒᵖ} (a : i ⟶ j)
(w : g i = D.map a ≫ g j) :
stage g p F j ⟶ stage g p F i
Stacks.EtaleCohomology.FixedBaseHigherDirectImage.projectionMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Colimits/LimitHigherDirectImageFixedBase.lean, line 171. The attribute's comment: “the cocone maps ψ_i : R^p g_{i, *} ℱ_i ⟶ R^p g_* ℱ whose universality the lemma asserts, constructed from the base change map on higher direct images of Stacks 0F02 for the square over the fixed base and the map ι_i : f_i^{-1}ℱ_i ⟶ ℱ presenting the colimit. The compatibility ψ_{i'} ∘ ψ_{i'i} = ψ_i, which would exhibit these maps as a cocone, is NOT proved, for the reason recorded on Stacks.EtaleCohomology.FixedBaseHigherDirectImage.transitionMap. The colimit assertion R^p g_* ℱ = colim_i R^p g_{i, *} ℱ_i is NOT proved.”.
The map
ψ_i : R^p g_{i, *} ℱ_i ⟶ R^p g_* ℱ: the base change maphigherBaseChangeMapAbfor the squareg ≫ 𝟙_S = f_i ≫ g_i, read through the identification of the inverse image along𝟙_Swith the identity functor, followed byR^p g_*of the mapι_i : f_i^{-1}ℱ_i ⟶ ℱpresentingℱascolim f_i^{-1}ℱ_i.
def projectionMap (F : EtaleSheafSystem D Ab.{u + 1})
(ι : ∀ i : Iᵒᵖ, (smallEtalePullbackAb (c.π.app i)).obj (F.obj i) ⟶ 𝓕) (i : Iᵒᵖ)
(w : gX = c.π.app i ≫ g i) :
stage g p F i ⟶ ((smallEtalePushforwardAb gX).rightDerived p).obj 𝓕
Stacks.EtaleCohomology.FixedBaseHigherDirectImage.isSystemColimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Colimits/LimitHigherDirectImageFixedBaseColimit.lean, line 169. References: SGA 4 VII (5.11), “special case”.
Let
X = lim X_ibe the limit of a directed inverse system of schemes overSwith affine transition morphisms and quasi-compact and quasi-separated structure morphismsg_i : X_i ⟶ S, letg : X ⟶ Sbe the structure morphism of the limit, and letι_i : f_i⁻¹ℱ_i ⟶ ℱpresentℱ = colim f_i⁻¹ℱ_ifor a system(ℱ_i, φ_{i'i})of abelian sheaves. Then for everypthe mapsψ_i : R^p g_{i, *}ℱ_i ⟶ R^p g_*ℱpresentR^p g_*ℱ = colim_i R^p g_{i, *}ℱ_i, the transition maps being theψ_{i'i}.
theorem isSystemColimit (p : ℕ) (F : EtaleSheafSystem D Ab.{u + 1})
(𝓕 : Sheaf (smallEtaleTopology c.pt) Ab.{u + 1})
(ι : ∀ i : Iᵒᵖ, (smallEtalePullbackAb (c.π.app i)).obj (F.obj i) ⟶ 𝓕)
(hι : ∀ {i j : Iᵒᵖ} (a : i ⟶ j),
(conePullbackComp c a).inv.app (F.obj j) ≫
(smallEtalePullbackAb (c.π.app i)).map (F.map a) ≫ ι i = ι j)
(hpres : LimitHigherDirectImage.IsPullbackColimitPresentation c 𝓕 F ι) :
IsSystemColimit (stage g p F) (fun {_i _j} a => transitionMap g p F a (hg a))
(((smallEtalePushforwardAb gX).rightDerived p).obj 𝓕)
(fun i => projectionMap g p c gX 𝓕 F ι i (w i))
Tag 0EYM, a lemma
Tag 0EYM in the Stacks Project.
Stacks.EtaleCohomology.LimitHigherDirectImage.transitionMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Colimits/LimitHigherDirectImage.lean, line 143. The attribute's comment: “the transition maps ψ_{i'i} : h_{i'i}^{-1} R^p g_{i, *} ℱ_i ⟶ R^p g_{i', *} ℱ_{i'} of the first paragraph of the proof, constructed from the base change map on higher direct images of Stacks 0F02 and the transition map of the system of sheaves. The cocycle condition ψ_{i''i} = ψ_{i''i'} ∘ h_{i''i'}^{-1}ψ_{i'i}, which the source gets from Stacks 0E47, is NOT proved: pasting of base change maps is carried for ringed topoi on sheaves of modules and for the unbounded derived étale base change map, but not for the bounded below Stacks.EtaleCohomology.smallEtaleDerivedBaseChangeAb that Stacks.EtaleCohomology.higherBaseChangeMapAb descends from. The colimit assertion R^p g_* ℱ = colim_i h_i^{-1} R^p g_{i, *} ℱ_i is NOT proved either; it additionally needs the comparison of Stacks 04HR at the level of cohomology, the carried Stacks 09YQ being stated for the right-derived sheafSections of the small AFFINE étale sites.”.
The transition maps of Stacks 0EYM,
ψ\_\{i'i} : h\_\{i'i}^\{-1} R^p g\_\{i, *} ℱ\_i ⟶ R^p g\_\{i', *} ℱ\_\{i'}: the base change map of the transition squareg_{i'} ≫ h_{i'i} = f_{i'i} ≫ g_ion higher direct images, followed byR^p g_{i', *}of the transition mapφ_{i'i} : f_{i'i}^{-1}ℱ_i ⟶ ℱ_{i'}of the system of sheaves.
def transitionMap (F : EtaleSheafSystem DX Ab.{u + 1}) {i j : Iᵒᵖ} (a : i ⟶ j) :
(smallEtalePullbackAb (DS.map a)).obj
(((smallEtalePushforwardAb (γ.app j)).rightDerived p).obj (F.obj j)) ⟶
((smallEtalePushforwardAb (γ.app i)).rightDerived p).obj (F.obj i)
Stacks.EtaleCohomology.LimitHigherDirectImage.projectionMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Colimits/LimitHigherDirectImage.lean, line 179. The attribute's comment: “the cocone maps ψ_i : h_i^{-1} R^p g_{i, *} ℱ_i ⟶ R^p g_* ℱ of the first paragraph of the proof, constructed from the base change map on higher direct images of Stacks 0F02 and the map ι_i : f_i^{-1}ℱ_i ⟶ ℱ presenting the colimit. The compatibility ψ_{i'} ∘ h_{i'}^{-1}ψ_{i'i} = ψ_i, which the source gets from Stacks 0E47, is NOT proved, for the reason recorded on transitionMap; so these maps are not exhibited as a cocone. The colimit assertion R^p g_* ℱ = colim_i h_i^{-1} R^p g_{i, *} ℱ_i is NOT proved.”.
The cocone maps of Stacks 0EYM,
ψ_i : h_i^{-1} R^p g_{i, *} ℱ_i ⟶ R^p g_* ℱ: the base change map of the projection squareg ≫ h_i = f_i ≫ g_ion higher direct images, followed byR^p g_*of the mapι_i : f_i^{-1}ℱ_i ⟶ ℱpresentingℱascolim f_i^{-1}ℱ_i.
def projectionMap (F : EtaleSheafSystem DX Ab.{u + 1})
(ι : ∀ i : Iᵒᵖ, (smallEtalePullbackAb (cX.π.app i)).obj (F.obj i) ⟶ 𝓕) (i : Iᵒᵖ) :
(smallEtalePullbackAb (cS.π.app i)).obj
(((smallEtalePushforwardAb (γ.app i)).rightDerived p).obj (F.obj i)) ⟶
((smallEtalePushforwardAb (limitMorphism γ cX cS hcS)).rightDerived p).obj 𝓕
Stacks.EtaleCohomology.LimitHigherDirectImage.isHigherDirectImageColimit_of_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Colimits/LimitHigherDirectImageColimitAssertion.lean, line 280. References: SGA 4 VII (5.11), “more general”.
Let
Ibe a directed set, let(X_i, f_{i'i})and(S_i, h_{i'i})be inverse systems of schemes overIwith affine transition morphisms, letg_i : X_i ⟶ S_ibe a morphism of inverse systems with everyg_iquasi-compact and quasi-separated, letX = lim X_i,S = lim S_iandg : X ⟶ Sthe limit morphism. Let(F_i, φ_{i'i})be a system of abelian sheaves on(X_i, f_{i'i})andι_i : f_i^{-1}F_i ⟶ 𝓕maps, compatible with the transition maps, presenting𝓕 = colim f_i^{-1}F_i. Then for everyp ≥ 0
R^p g_* 𝓕 = colim_{i ∈ I} h_i^{-1} R^p g_{i, *}F_i:every family of maps out of the
h_i^{-1} R^p g_{i, *}F_icompatible with the mapsh_{i'}^{-1}ψ_{i'i}induced by the transition mapsψ_{i'i} : h_{i'i}^{-1} R^p g_{i, *}F_i ⟶ R^p g_{i', *}F_{i'}factors uniquely through the cocone mapsψ_i : h_i^{-1} R^p g_{i, *}F_i ⟶ R^p g_* 𝓕, both families being built from the base change maps on higher direct images as in the source (Stacks.EtaleCohomology.LimitHigherDirectImage.transitionMap,Stacks.EtaleCohomology.LimitHigherDirectImage.projectionMap).
theorem isHigherDirectImageColimit_of_isLimit (p : ℕ)
(𝓕 : Sheaf (smallEtaleTopology cX.pt) Ab.{max u v + 1})
(F : EtaleSheafSystem DX Ab.{max u v + 1})
(ι : ∀ i : Iᵒᵖ, (smallEtalePullbackAb (cX.π.app i)).obj (F.obj i) ⟶ 𝓕)
(hι : ∀ {i j : Iᵒᵖ} (a : i ⟶ j),
(conePullbackComp cX a).inv.app (F.obj j) ≫
(smallEtalePullbackAb (cX.π.app i)).map (F.map a) ≫ ι i = ι j)
(hpres : IsPullbackColimitPresentation cX 𝓕 F ι) :
IsHigherDirectImageColimit γ p cX cS hcS 𝓕 F ι
Stacks.EtaleCohomology.LimitHigherDirectImage.higherDirectImageColimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Colimits/LimitHigherDirectImageColimitTheorem.lean, line 92. References: SGA 4 VII (5.11), “more general”.
Let
Ibe a directed set,g_i : X_i ⟶ S_ian inverse system of quasi-compact and quasi-separated morphisms of schemes with affine transition morphismsf_{i'i},h_{i'i},g : X ⟶ Sits limit with projectionsf_i,h_i,(ℱ_i, φ_{i'i})a system of abelian sheaves on(X_i, f_{i'i})andℱ = colim f_i⁻¹ℱ_i. Then for everyp
- the maps
ψ_{i'i} : h_{i'i}⁻¹R^p g_{i, *}ℱ_i ⟶ R^p g_{i', *}ℱ_{i'}satisfy the cocycle conditionψ_{i''i} = ψ_{i''i'} ∘ h_{i''i'}⁻¹ψ_{i'i};- the maps
ψ_i : h_i⁻¹R^p g_{i, *}ℱ_i ⟶ R^p g_*ℱsatisfyψ_{i'} ∘ h_{i'}⁻¹ψ_{i'i} = ψ_i;- they present
R^p g_*ℱ = colim_{i ∈ I} h_i⁻¹R^p g_{i, *}ℱ_i.
theorem higherDirectImageColimit (p : ℕ) (F : EtaleSheafSystem DX Ab.{u + 1})
(𝓕 : Sheaf (smallEtaleTopology cX.pt) Ab.{u + 1})
(ι : ∀ i : Iᵒᵖ, (smallEtalePullbackAb (cX.π.app i)).obj (F.obj i) ⟶ 𝓕)
(hι : ∀ {i j : Iᵒᵖ} (a : i ⟶ j),
(conePullbackComp cX a).inv.app (F.obj j) ≫
(smallEtalePullbackAb (cX.π.app i)).map (F.map a) ≫ ι i = ι j)
(hpres : IsPullbackColimitPresentation cX 𝓕 F ι) :
(∀ {i j k : Iᵒᵖ} (a : i ⟶ j) (b : j ⟶ k),
(systemPullbackComp DS Ab.{u + 1} a b).inv.app
(((smallEtalePushforwardAb (γ.app k)).rightDerived p).obj (F.obj k)) ≫
(systemPullback DS Ab.{u + 1} a).map (transitionMap γ p F b) ≫
transitionMap γ p F a =
transitionMap γ p F (a ≫ b)) ∧
(∀ {i j : Iᵒᵖ} (a : i ⟶ j),
(conePullbackComp cS a).inv.app
(((smallEtalePushforwardAb (γ.app j)).rightDerived p).obj (F.obj j)) ≫
(smallEtalePullbackAb (cS.π.app i)).map (transitionMap γ p F a) ≫
projectionMap γ cX cS hcS p 𝓕 F ι i =
projectionMap γ cX cS hcS p 𝓕 F ι j) ∧
IsHigherDirectImageColimit γ p cX cS hcS 𝓕 F ι
Tag 0EYN, a lemma
Tag 0EYN in the Stacks Project.
Stacks.EtaleCohomology.directImageSystem, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Colimits/DirectImageSystem.lean, line 342. The attribute's comment: “the system of sheaves”.
Let
(X_i, f_{i'i})be an inverse system of schemes, letf_i : X ⟶ X_ibe the projections of a cone over it, and let𝓕be a sheaf on the small étale site ofX. The direct imagesf_{i,*}𝓕, with the canonical mapsφ_{i'i} : f_{i'i}^{-1} f_{i,*}𝓕 ⟶ f_{i',*}𝓕adjoint to the identificationf_{i,*}𝓕 ≅ f_{i'i,*} f_{i',*}𝓕given byf_i = f_{i'} ≫ f_{i'i}, form a system of sheaves on(X_i, f_{i'i})in the sense of Stacks 0EZL.
public def directImageSystem : EtaleSheafSystem D A
Stacks.EtaleCohomology.isPullbackColimitPresentation_directImageSystem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Colimits/DirectImageSystemColimitPresentation.lean, line 94. The attribute's comment: “the colimit 𝓕 = colim f_i⁻¹f_{i,*}𝓕”.
[Stacks, Tag 0EYN], the colimit. Let
X = lim X_ibe a directed limit of schemes with affine transition morphisms and projectionsf_i : X ⟶ X_i, and let𝓕be an abelian sheaf onX_étale. Then the counitsf_i⁻¹f_{i,*}𝓕 ⟶ 𝓕present𝓕 = colim f_i⁻¹f_{i,*}𝓕over the system of sheaves(f_{i,*}𝓕, φ_{i'i})ofStacks.EtaleCohomology.directImageSystem.
theorem isPullbackColimitPresentation_directImageSystem (hc : IsLimit c) :
LimitHigherDirectImage.IsPullbackColimitPresentation c 𝓕
(directImageSystem D Ab.{u + 1} c 𝓕) (coneDirectImageCounit c 𝓕)
Stacks.EtaleCohomology.isColimitPullbackDirectImageCocone, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Colimits/DirectImageSystemIsColimit.lean, line 377. The attribute's comment: “part (2): 𝓕 = colim_i f_i^{-1}f_{i,*}𝓕 for the system of part (1), on Mathlib's small étale site, for sheaves of sets”.
[Stacks, Tag 0EYN] (2), for sheaves of sets. Let
X = lim X_ibe a directed limit of schemes with affine transition morphismsf_{i'i}and projection morphismsf_i : X ⟶ X_i, and let𝓕be a sheaf of sets on the small étale site ofX. Then𝓕 = colim_i f_i^{-1}f_{i,*}𝓕: the cocone of counitsf_i^{-1}f_{i,*}𝓕 ⟶ 𝓕over the diagramStacks.EtaleCohomology.pullbackDirectImageDiagram, whose transition maps are built from the mapsφ_{i'i} : f_{i'i}^{-1}f_{i,*}𝓕 ⟶ f_{i',*}𝓕of the system of sheaves of part (1),Stacks.EtaleCohomology.directImageSystem, is a colimit cocone. Equivalently, the canonical mapcolim_i f_i^{-1}f_{i,*}𝓕 ⟶ 𝓕is an isomorphism.
def isColimitPullbackDirectImageCocone
(F : Sheaf (AlgebraicGeometry.Scheme.smallEtaleTopology c.pt) (Type (max u v + 1))) :
IsColimit (pullbackDirectImageCocone D (Type (max u v + 1)) c F)
Stacks.EtaleCohomology.AffineLimitCohomology.restrictionIsColimit_limitToSmallEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Colimits/SmallEtaleLimitColimitSheaf.lean, line 721. The attribute's comment: “part (2): F = colim_i p_i^{-1}p_{i,*}F, on the site of Stacks 021B”.
Stacks 0EYN, second half, on the small étale site of a limit of schemes. Let
(X_i)be an inverse system of schemes with affine transition morphisms over a nonempty directed index, all of them objects of a big étale siteB, letX = lim X_i, and letFbe a sheaf of sets on the small étale site ofX. Then
F = colim_i p_i^{-1} p_{i,*} F,in the form the inverse-system machinery proves it: every family of maps out of the restrictions of
Fto the levels of the system of sites of [Stacks, Tag 0EYL], compatible with the canonical transition maps, is the restriction of a unique map of sheaves out ofF. Those restrictions are thep_{i,*}Fread on the levels — they arelevelRestrict, whose sections over a level object are the sections ofFover its image in the site of the limit (levelRestrict_obj, anrfl), and that image is the base change of the level object alongp_i.This is the geometric instantiation of
CategoryTheory.Sites.InverseSystem.InverseSystemOfFiniteSites.descent_along_restrictionatΛ = limitToSmallEtale: the five site inputs of [Stacks, Tag 09YP] for the raised site aretoLimitSmall_transition,toLimitSmall_obj_descends,toLimitSmall_hom_descends,toLimitSmall_hom_eventually_eqandmem_limitSitePrecoverage_iff, and the two instances making restriction along the composite crossing fully faithful arefull_limitRestrictionandfaithful_limitRestriction.Why the conclusion is the named predicate. Written out, the telescope mentions
(sys D c B hD hX hc).I,.C iand.u asome thirty times and exceeds the heartbeat budget in the signature; the failure is a(deterministic) timeout at isDefEqinside the compatibility hypothesis of the familyg, before any proof runs. The docstring ofCategoryTheory.Sites.InverseSystem.InverseSystemOfFiniteSites.RestrictionIsColimitrecords the rule and the three other places in this development where it was needed.Why
hKis supplied byrwand not as a term.mem_limitSitePrecoverage_iffstates exactly the required equivalence, but its last clause is a transportR = h ▸ S.map (toLimitSmall …)whose motive was elaborated against the concrete functor, while the motive the machinery's hypothesis carries is the one elaborated against its variableu. The two are definitionally equal and deciding them is another heartbeat timeout; rewriting the goal with the equivalence closes it outright instead.Part (1) of the tag, that the
p_{i,*}Fcarry canonical maps making them a system of sheaves in the sense of [Stacks, Tag 0EZL], isStacks.EtaleCohomology.directImageSystem, which states it on Mathlib's small étale site; that declaration and this one are the covering set of Tag 0EYN.
theorem restrictionIsColimit_limitToSmallEtale
(F : Sheaf (AlgebraicGeometry.SmallEtale.topology B c.pt hX) (Type (max u v + 1))) :
InverseSystemOfFiniteSites.RestrictionIsColimit
(AlgebraicGeometry.SmallEtale.topology B c.pt hX) (sys D c B hD hX hc)
(fun i => toLimitSmall D c B hD hX hc i ⋙ limitToSmallEtale D c B hX)
(InverseSystemOfFiniteSites.compTransitionIso (limitToSmallEtale D c B hX)
(sys D c B hD hX hc) (toLimitSmall D c B hD hX hc)
(toLimitSmall_transition D c B hD hX hc)) F
Tag 0DV2, a lemma
Tag 0DV2 in the Stacks Project.
Stacks.EtaleCohomology.LimitHigherDirectImage.isColimit_pushforwardStage_of_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Colimits/PushforwardStageColimit.lean, line 76. The attribute's comment: “the colimit assertion for the canonical diagram and the canonical cocone, with the cocycle condition of the diagram and the cocone identity of its legs”.
Stacks 0DV2. Let
Ibe a directed set, let(X_i, f_{i'i})and(S_i, h_{i'i})be inverse systems of schemes with affine transition morphisms, letg_i : X_i ⟶ S_ibe a morphism of the first system into the second with everyg_iquasi-compact and quasi-separated, letf_i : X ⟶ X_iandh_i : S ⟶ S_ibe the projections of limit cones over the two systems, letg : X ⟶ Sbe the limit morphism, and let𝓕be an abelian sheaf on the small étale site ofX. Then
R^p g_* 𝓕 = colim_{i ∈ I} h_i^{-1} R^p g_{i, *}(f_{i, *}𝓕):the objects
h_i^{-1} R^p g_{i, *}(f_{i, *}𝓕)with the maps induced by the transition mapsψ_{i'i}of [Stacks, Tag 0EYM] satisfy the cocycle condition, the mapsψ_iof the same source form a cocone on them, and that cocone is a colimit.The counits present
𝓕 = colim_i f_i^{-1}f_{i, *}𝓕by the colimit half of [Stacks, Tag 0EYN],Stacks.EtaleCohomology.isPullbackColimitPresentation_directImageSystem; they are compatible with the transition maps ofStacks.EtaleCohomology.directImageSystembyStacks.EtaleCohomology.coneDirectImageCounit_cocone, and [Stacks, Tag 0EYM],Stacks.EtaleCohomology.LimitHigherDirectImage.isHigherDirectImageColimit, applies.
theorem isColimit_pushforwardStage_of_isLimit [Nonempty I] [IsDirected I (· ≤ ·)]
[∀ {i j : Iᵒᵖ} (a : i ⟶ j), IsAffineHom (DX.map a)]
[∀ {i j : Iᵒᵖ} (a : i ⟶ j), IsAffineHom (DS.map a)]
[∀ i : Iᵒᵖ, QuasiCompact (γ.app i)] [∀ i : Iᵒᵖ, QuasiSeparated (γ.app i)]
(hcX : IsLimit cX) :
(∀ {i j k : Iᵒᵖ} (a : i ⟶ j) (b : j ⟶ k),
(systemPullbackComp DS Ab.{u + 1} a b).inv.app
(((smallEtalePushforwardAb (γ.app k)).rightDerived p).obj
((directImageSystem DX Ab.{u + 1} cX 𝓕).obj k)) ≫
(systemPullback DS Ab.{u + 1} a).map (pushforwardStageTransition cX 𝓕 γ p b) ≫
pushforwardStageTransition cX 𝓕 γ p a =
pushforwardStageTransition cX 𝓕 γ p (a ≫ b)) ∧
(∀ {i j : Iᵒᵖ} (a : i ⟶ j),
(conePullbackComp cS a).inv.app
(((smallEtalePushforwardAb (γ.app j)).rightDerived p).obj
((directImageSystem DX Ab.{u + 1} cX 𝓕).obj j)) ≫
(smallEtalePullbackAb (cS.π.app i)).map (pushforwardStageTransition cX 𝓕 γ p a) ≫
pushforwardStageLeg cX 𝓕 γ cS hcS p i =
pushforwardStageLeg cX 𝓕 γ cS hcS p j) ∧
IsHigherDirectImageColimit γ p cX cS hcS 𝓕 (directImageSystem DX Ab.{u + 1} cX 𝓕)
(coneDirectImageCounit cX 𝓕)
Sources
Section59.52 Colimits and complexes#
Section 59.52 of the Stacks Project, Tag 0GIR. 6 tags here are carried by 9 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 0EZM, a lemma
Tag 0EZM in the Stacks Project.
Stacks.EtaleCohomology.EtaleComplexSystem.isSystemColimit_etaleHypercohomologyPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Colimits/ComplexSystemCohomologyColimit.lean, line 651.
Étale cohomology commutes with colimits of bounded below systems of complexes over a limit of schemes ([Stacks, Tag 0EZM]). Let
X = lim X_ibe the limit of a directed inverse system of quasi-compact and quasi-separated schemes with affine transition morphisms,(ℱ_i^•, φ_{i'i})a system of complexes of abelian sheaves on the small étale sites of theX_iwithℱ_i^n = 0forn < a,aindependent ofi, andι_i : f_i⁻¹ℱ_i^• ⟶ ℱ^•maps of complexes, compatible with the transition maps, which present every termℱ^nas the colimitcolim f_i⁻¹ℱ_i^n. Then for everyp ∈ ℤthe pull back mapsH^p(X_i, ℱ_i^•) ⟶ H^p(X, ℱ^•)exhibitH^p(X, ℱ^•)as the colimit of the system of theH^p(X_i, ℱ_i^•).
theorem isSystemColimit_etaleHypercohomologyPullback (a : ℤ) [∀ i, (F.obj i).IsStrictlyGE a]
(𝓕 : CochainComplex (Sheaf (smallEtaleTopology c.pt) Ab.{u + 1}) ℤ)
(ι : ∀ i : Iᵒᵖ, ((smallEtalePullbackAb (c.π.app i)).mapHomologicalComplex _).obj (F.obj i) ⟶ 𝓕)
(hι : F.IsPullbackCocone c ι)
(hpres : ∀ n, LimitHigherDirectImage.IsPullbackColimitPresentation c (𝓕.X n) (F.term n)
(fun i => (ι i).f n)) (p : ℤ) :
IsSystemColimit
(fun i => AddCommGrpCat.of
(etaleHypercohomology (D.obj i) (DerivedCategory.Q.obj (F.obj i)) p))
(fun a => AddCommGrpCat.ofHom (etaleHypercohomologyPullback (D.map a) (F.map a) p))
(AddCommGrpCat.of (etaleHypercohomology c.pt (DerivedCategory.Q.obj 𝓕) p))
(fun i => AddCommGrpCat.ofHom (etaleHypercohomologyPullback (c.π.app i) (ι i) p))
Tag 0GIS, a lemma
Tag 0GIS in the Stacks Project.
Stacks.EtaleCohomology.preservesColimit_rightDerivedFunctorPlus_Γ_smallEtale_of_isGE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BoundedBelowDirectSumsGlobalSections.lean, line 101. The attribute's comment: “RΓ(X, ⨁ K_i) = ⨁ RΓ(X, K_i) for a family of D⁺(X_étale) with common lower bound a, on a quasi-compact quasi-separated scheme. The global sections case of the machinery behind Tag 0GIW; unlike that tag nothing is carried, the input that H^q_étale(X, -) commutes with direct sums being preservesColimitsOfShape_discrete_rightDerived_Γ_smallEtale. The index type lies in Type (max (u+1) v), the universe at which the abelian sheaves on the small étale site are Grothendieck abelian: the termwise direct sum of the resolutions is formed inside that category, so the index universe and the Grothendieck universe are the same.”.
[Stacks, Tag 0GIS]. Let
Xbe a quasi-compact and quasi-separated scheme, letK : I → D⁺(X_étale)be a family of objects of the bounded below derived category of abelian sheaves on the small étale site ofXand leta : ℤbe such thatH^n(K i) = 0forn < aand alli, that is(K i).IsGE a. ThenRΓ(X, ⨁ i, K i) = ⨁ i, RΓ(X, K i).Nothing is assumed: the one input of the argument beyond the injective resolutions bounded below by
aof [Stacks, Tag 07D9] and Leray's acyclicity lemma [Stacks, Tag 015E] is that eachH^q_étale(X, -)commutes with the direct sum, which isStacks.EtaleCohomology.preservesColimitsOfShape_discrete_rightDerived_Γ_smallEtale, and that is where the quasi-compactness and quasi-separatedness ofXare used.The source states the lemma in
D(X_étale); its hypothesis places everyK iinD⁺, and the module docstring records why the statement is read there and why the index universe ismax (u + 1) v.
theorem preservesColimit_rightDerivedFunctorPlus_Γ_smallEtale_of_isGE
(X : Scheme.{u}) [CompactSpace X] [QuasiSeparatedSpace X] {I : Type (max (u + 1) v)}
(K : I → DerivedCategory.Plus (Sheaf X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v}))
(a : ℤ) (hK : ∀ i, (K i).IsGE a) :
PreservesColimit (Discrete.functor K)
(Sheaf.Γ X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v}).rightDerivedFunctorPlus
Tag 0GIT, a lemma
Tag 0GIT in the Stacks Project.
Stacks.EtaleCohomology.isSystemColimit_etaleHypercohomologyMap_of_isLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Colimits/ComplexSystemCohomologyColimit.lean, line 758.
Étale cohomology of a bounded below complex pulled back to a limit of schemes ([Stacks, Tag 0GIT]). Let
Sbe a scheme,X = lim X_ithe limit of a directed inverse system of quasi-compact and quasi-separated schemes overS, with structure morphismsι_i : X_i ⟶ S,g : X ⟶ Sand affine transition morphisms, andK ∈ D^+(S_étale). Then for everyp ∈ ℤthe pull back mapsH^p(X_i, K|_{X_i}) ⟶ H^p(X, K|_X)exhibitH^p(X, K|_X)as the colimit of the system of theH^p(X_i, K|_{X_i}). HereK|_{X_i}is the derived inverse image ofKalongι_i, and the transition maps are induced by the comparisonsf_{i'i}⁻¹ ι_i⁻¹ ≅ ι_{i'}⁻¹andf_i⁻¹ ι_i⁻¹ ≅ g⁻¹of inverse images along composites.
theorem isSystemColimit_etaleHypercohomologyMap_of_isLimit (ι : ∀ i, D.obj i ⟶ S)
(hι : ∀ {i j : Iᵒᵖ} (a : i ⟶ j), D.map a ≫ ι j = ι i) (g : c.pt ⟶ S)
(hg : ∀ i, c.π.app i ≫ ι i = g)
(K : DerivedCategory.Plus (Sheaf (smallEtaleTopology S) Ab.{u + 1})) (p : ℤ) :
IsSystemColimit
(fun i => AddCommGrpCat.of (etaleHypercohomology (D.obj i)
((smallEtalePullbackAb (ι i)).mapDerivedCategory.obj K.obj) p))
(fun {i j} a => AddCommGrpCat.ofHom (etaleHypercohomologyMap (D.map a)
((Functor.mapDerivedCategoryIsoComp _ _ _
(smallEtalePullbackAbComp' (D.map a) (ι j) (ι i) (hι a).symm)).inv.app K.obj) p))
(AddCommGrpCat.of (etaleHypercohomology c.pt
((smallEtalePullbackAb g).mapDerivedCategory.obj K.obj) p))
(fun i => AddCommGrpCat.ofHom (etaleHypercohomologyMap (c.π.app i)
((Functor.mapDerivedCategoryIsoComp _ _ _
(smallEtalePullbackAbComp' (c.π.app i) (ι i) g (hg i).symm)).inv.app K.obj) p))
Tag 0GIU, a lemma
Tag 0GIU in the Stacks Project.
Stacks.EtaleCohomology.LimitHigherDirectImage.pullbackProjectionMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Colimits/LimitHigherDirectImageDerived.lean, line 276. The attribute's comment: “the comparison maps h_i^{-1} R^p g_{i, *} K_i ⟶ R^p g_* K of the assertion, for all p ∈ ℤ, with K_i the derived pullback of K_0 ∈ D^+(X_{0, étale}) to X_i, built from the derived base change comparison of Stacks 0F02 together with exactness of h_i^{-1}; their naturality in K_0 is derivedProjectionMap_naturality. The colimit assertion R^p g_* K = colim_{i ≥ 0} h_i^{-1} R^p g_{i, *} K_i is NOT proved, and cannot be: it is a formal consequence (by the dimension-shifting induction of the source over the triangle H^a(K_0)[-a] → K_0 → τ_{≥ a+1}K_0) of the colimit assertion of Stacks 0EYM, which the carrier Stacks.EtaleCohomology.LimitHigherDirectImage.projectionMap of that tag states in its own clause string is not proved; indeed the colimit itself cannot be formed, since that needs the cocycle condition of Stacks 0E47 which 0EYM's carrier also leaves open. EXTRA HYPOTHESIS: the pullback K of K_0 to X and the isomorphisms κ_i : R f_i^{-1} K_i ≅ K are taken as data, as ℱ and ι_i are in 0EYM's carrier and as K is given data in the source; this is a generalization, since in the source's situation those data exist.”.
The comparison map of Stacks 0GIU,
h_i^{-1} R^p g_{i, *} K_i ⟶ R^p g_* K, forK_0 ∈ D^+(X_{0, étale}),K_ithe pullback ofK_0toX_iandKthe pullback ofK_0toX: the derived comparison mapderivedProjectionMapatL = K_i,M = Kandκ = κ_i : R f_i^{-1} K_i ≅ K.
def pullbackProjectionMap (K₀ : PlusAb (DX.obj i₀)) (K : PlusAb cX.pt) {i : Iᵒᵖ} (a : i ⟶ i₀)
(κ : (derivedPullbackAb (cX.π.app i)).obj (derivedLevelPullback a K₀) ≅ K) :
(smallEtalePullbackAb (cS.π.app i)).obj
((homologyAb (DS.obj i) p).obj
((derivedPushforwardAb (γ.app i)).obj (derivedLevelPullback a K₀))) ⟶
(homologyAb cS.pt p).obj
((derivedPushforwardAb (limitMorphism γ cX cS hcS)).obj K)
Stacks.EtaleCohomology.LimitHigherDirectImage.derivedPullbackHigherDirectImageColimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Colimits/LimitHigherDirectImageDerivedColimit.lean, line 510. References: SGA 4 VII (5.11), “more general”.
Let
Ibe a directed set,g_i : X_i ⟶ S_ian inverse system of quasi-compact and quasi-separated morphisms of schemes with affine transition morphismsf_{i'i},h_{i'i}, andg : X ⟶ Sits limit with projectionsf_i,h_i. Let0 = i₀ ∈ I,K_0 ∈ D^+(X_{0, étale}),K_i = R f_{i0}^{-1}K_0its pullback toX_ifori ≥ 0andK = R f_0^{-1}K_0its pullback toX. Then for everyp ∈ ℤthe mapsh_{i'i}^{-1}R^pg_{i, *}K_i ⟶ R^pg_{i', *}K_{i'}(the derived base change maps of the transition squares composed withR^pg_{i', *}ofR f_{i'i}^{-1}K_i ≅ K_{i'}), pulled back toS, satisfy the cocycle condition, the mapsh_i^{-1}R^pg_{i, *}K_i ⟶ R^pg_*K(the derived base change maps of the projection squares composed withR^pg_*ofR f_i^{-1}K_i ≅ K) are compatible with them, and they presentR^pg_*K = colim_{i ≥ 0} h_i^{-1}R^pg_{i, *}K_i.
theorem derivedPullbackHigherDirectImageColimit (K₀ : PlusAb (DX.obj (op i₀))) (p : ℤ) :
(∀ {j j' j'' : (Set.Ici i₀)ᵒᵖ} (c : j ⟶ j') (c' : j' ⟶ j''),
derivedPullbackTransition γ cS i₀ p K₀ (c ≫ c') =
derivedPullbackTransition γ cS i₀ p K₀ c' ≫ derivedPullbackTransition γ cS i₀ p K₀ c) ∧
(∀ {j j' : (Set.Ici i₀)ᵒᵖ} (c : j ⟶ j'),
derivedPullbackTransition γ cS i₀ p K₀ c ≫ derivedPullbackLeg γ cX cS i₀ p K₀
(limitMorphism γ cX cS hcS) (fun j => limitMorphism_comp_π γ cX cS hcS _) j =
derivedPullbackLeg γ cX cS i₀ p K₀ (limitMorphism γ cX cS hcS)
(fun j => limitMorphism_comp_π γ cX cS hcS _) j') ∧
IsSystemColimit (derivedPullbackTerm γ cS i₀ p K₀)
(fun {j j'} c => derivedPullbackTransition γ cS i₀ p K₀ (j := j) (j' := j') c)
((homologyAb cS.pt p).obj ((derivedPushforwardAb (limitMorphism γ cX cS hcS)).obj
((derivedPullbackAb (cX.π.app (op i₀))).obj K₀)))
(derivedPullbackLeg γ cX cS i₀ p K₀ (limitMorphism γ cX cS hcS)
(fun j => limitMorphism_comp_π γ cX cS hcS _))
Tag 0GIV, a lemma
Tag 0GIV in the Stacks Project.
Stacks.EtaleCohomology.LimitHigherDirectImage.complexHigherDirectImageColimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Colimits/ComplexHigherDirectImageColimitTheorem.lean, line 438. References: SGA 4 VII (5.11), “more general”.
[Stacks, Tag 0GIV]. Let
Ibe a directed set,g_i : X_i ⟶ S_ian inverse system of quasi-compact and quasi-separated morphisms of schemes with affine transition morphismsf_{i'i},h_{i'i}, andg : X ⟶ Sits limit with projectionsf_i,h_i. Let(ℱ_i^•, φ_{i'i})be a system of complexes of abelian sheaves on theX_{i, étale}, withℱ_i^n = 0forn < aand alli, andℱ^• = colim f_i^{-1}ℱ_i^•, presented by maps of complexesι_i : f_i^{-1}ℱ_i^• ⟶ ℱ^•compatible with the transition maps and presenting every termℱ^nascolim f_i^{-1}ℱ_i^n. Then for everyp ∈ ℤthe mapsh_i^{-1}R^pg_{i, *}ℱ_i^• ⟶ R^pg_*ℱ^•(the derived base change maps of the projection squares followed byR^pg_*ι_i) are compatible with the mapsh_{i'i}^{-1}R^pg_{i, *}ℱ_i^• ⟶ R^pg_{i', *}ℱ_{i'}^•of the system of theR^pg_{i, *}ℱ_i^•and presentR^pg_*ℱ^• = colim_i h_i^{-1}R^pg_{i, *}ℱ_i^•.
theorem complexHigherDirectImageColimit (F : EtaleComplexSystem DX) (a : ℤ)
[∀ i, (F.obj i).IsStrictlyGE a]
(𝓕 : CochainComplex (Sheaf (smallEtaleTopology cX.pt) Ab.{u + 1}) ℤ)
(ι : ∀ i : Iᵒᵖ, ((smallEtalePullbackAb (cX.π.app i)).mapHomologicalComplex _).obj (F.obj i) ⟶ 𝓕)
(hι : F.IsPullbackCocone cX ι)
(hpres : ∀ n, IsPullbackColimitPresentation cX (𝓕.X n) (F.term n) (fun i => (ι i).f n))
(p : ℤ) :
haveI := F.isStrictlyGE_of_isPullbackColimitPresentation a hpres
(∀ {i j : Iᵒᵖ} (c : i ⟶ j),
(complexHigherDirectImageSystem γ p a F).pullbackDiagramMap cS (i := i) (j := j) c ≫
complexLeg γ p a F cX cS hcS 𝓕 ι i = complexLeg γ p a F cX cS hcS 𝓕 ι j) ∧
IsComplexHigherDirectImageColimit γ p a F cX cS hcS 𝓕 ι
Stacks.EtaleCohomology.LimitHigherDirectImage.complexProjectionMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/Colimits/LimitHigherDirectImageDerived.lean, line 368. The attribute's comment: “the comparison maps h_i^{-1} R^p g_{i, *} ℱ_i^• ⟶ R^p g_* ℱ^• of the assertion, for all p ∈ ℤ, where R^p g_* of a complex is the degree-p cohomology of the total right derived direct image of its class in D^+; built from the derived base change comparison of Stacks 0F02, exactness of h_i^{-1}, and — for the pullback of the complex — the invertibility of the right-derived-functor unit of the exact functor f_i^{-1}. The uniform lower bound a of the source (ℱ_i^n = 0 for n < a, a independent of i) is carried as CochainComplex.IsStrictlyGE; naturality is derivedProjectionMap_naturality. The colimit assertion R^p g_*(colim f_i^{-1}ℱ_i^•) = colim_{i ≥ 0} h_i^{-1} R^p g_{i, *} ℱ_i^• is NOT proved, and cannot be: it is a formal consequence (by the two spectral sequences of a Cartan-Eilenberg resolution, Stacks 015J) of the colimit assertion of Stacks 0EYM, which the carrier Stacks.EtaleCohomology.LimitHigherDirectImage.projectionMap of that tag states in its own clause string is not proved; indeed the colimit itself cannot be formed, since that needs the cocycle condition of Stacks 0E47 which 0EYM's carrier also leaves open. EXTRA HYPOTHESIS: the complex ℱ^• = colim f_i^{-1}ℱ_i^• and the maps of complexes ι_i : f_i^{-1}ℱ_i^• ⟶ ℱ^• are taken as data, as ℱ and ι_i are in 0EYM's carrier and as the colimit is given data in the source; this is a generalization, since in the source's situation those data exist. The transition maps φ_{i'i} and their cocycle condition are the data of the system; the transition form of the comparison map is derivedTransitionMap.”.
The comparison map of Stacks 0GIV,
h_i^{-1} R^p g_{i, *} ℱ_i^• ⟶ R^p g_* ℱ^•, for a complexℱ_i^•of abelian sheaves onX_{i, étale}vanishing in degrees< a, a complexℱ^•onX_étalevanishing in degrees< a, and a map of complexesι_i : f_i^{-1}ℱ_i^• ⟶ ℱ^•: the derived comparison mapderivedProjectionMapat the classes of the two complexes in the bounded below derived categories, withκthe comparisoncomplexPullbackComparison.
def complexProjectionMap (i : Iᵒᵖ)
(F : CochainComplex (Sheaf (smallEtaleTopology (DX.obj i)) Ab.{u + 1}) ℤ) [F.IsStrictlyGE a]
(G : CochainComplex (Sheaf (smallEtaleTopology cX.pt) Ab.{u + 1}) ℤ) [G.IsStrictlyGE a]
(ι : complexPullbackObj cX i F ⟶ G) :
(smallEtalePullbackAb (cS.π.app i)).obj
((homologyAb (DS.obj i) p).obj
((derivedPushforwardAb (γ.app i)).obj (plusComplexObj a F))) ⟶
(homologyAb cS.pt p).obj
((derivedPushforwardAb (limitMorphism γ cX cS hcS)).obj (plusComplexObj a G))
Tag 0GIW, a lemma
Tag 0GIW in the Stacks Project.
Stacks.EtaleCohomology.preservesColimit_etaleModuleDerivedDirectImage_of_isGE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BoundedBelowDirectSums.lean, line 316. The attribute's comment: “Rf_(⨁ K_i) = ⨁ Rf_ K_i for a family of D⁺(X_étale, Λ) with common lower bound a. Tag 09Z1, that each R^q f_* on the small étale site commutes with direct sums, is carried as the hypothesis hsums, since it is not proved in this library; everything else the source cites is proved. The index type lies in Type (max (u+1) r), the universe at which the sheaves of Λ-modules on the small étale sites are Grothendieck abelian: the termwise direct sum of the resolutions is formed inside those categories, so the index universe and the Grothendieck universe are the same. For Λ a general ring.”.
[Stacks, Tag 0GIW]. Let
Λbe a ring, letf : X ⟶ Ybe a quasi-compact and quasi-separated morphism of schemes, letK : I → D⁺(X_étale, Λ)be a family of objects and leta : ℤbe such thatH^n(K i) = 0forn < aand alli, that is(K i).IsGE a. ThenRf_*(⨁ i, K i) = ⨁ i, Rf_*(K i).The one input that is carried rather than used is
hsums: that each ordinary higher direct imageR^q f_*on the small étale site commutes with the direct sum. That is [Stacks, Tag 09Z1], which is not proved in this repository, so it appears here as a hypothesis, in the shape in which the source cites it. Nothing else is assumed: thatf_*itself commutes with the direct sum is proved fromhsumsatq = 0, and the rest of the argument of the source — the injective resolutions bounded below byaof [Stacks, Tag 07D9], the right acyclicity of their termwise direct sum, and Leray's acyclicity lemma [Stacks, Tag 015E] identifyingRf_*with the termwise image on each of them — is proved.Quasi-compactness and quasi-separatedness of
fare the hypotheses under which the source's proof invokes [Stacks, Tag 09Z1]; they are carried here even though the argument consumes them only throughhsums, so that the statement is the source's.The source states the lemma in
D(X_étale); its hypothesis places everyK_iinD⁺, and the module docstring records why the statement is read there, why the coefficients are an arbitrary ring, and why the index universe ismax (u + 1) r.
theorem preservesColimit_etaleModuleDerivedDirectImage_of_isGE
{X Y : Scheme.{u}} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f]
{I : Type (max (u + 1) r)}
(hsums : ∀ p : ℕ, PreservesColimitsOfShape (Discrete I)
((etaleModuleDirectImage.{u, r} Λ f).rightDerived p))
(K : I → DerivedCategory.Plus (EtaleModules.{u, r} Λ X)) (a : ℤ)
(hK : ∀ i, (K i).IsGE a) :
PreservesColimit (Discrete.functor K) (etaleModuleDerivedDirectImage.{u, r} Λ f)
Stacks.EtaleCohomology.preservesColimit_etaleAbelianDerivedDirectImage_of_isGE, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/DerivedDirectImageBoundedBelowSums.lean, line 193.
[Stacks, Tag 0GIW]. Let
f : X ⟶ Ybe a quasi-compact and quasi-separated morphism of schemes, letK : I → D(X_étale)be a family of objects of the derived category of abelian sheaves on the small étale site ofX, and leta : ℤbe such thatH^n(K i) = 0forn < aand alli, that is(K i).IsGE a. ThenRf_*(⨁ i, K i) = ⨁ i, Rf_*(K i): the unbounded derived direct imageRf_* : D(X_étale) ⥤ D(Y_étale)preserves the direct sum of the family.Nothing is assumed beyond the source's hypotheses. That each
R^q f_*commutes with direct sums ispreservesColimitsOfShape_discrete_rightDerived_etaleAbelianDirectImage, where quasi-compactness and quasi-separatedness offare used.
theorem preservesColimit_etaleAbelianDerivedDirectImage_of_isGE
{X Y : Scheme.{u}} (f : X ⟶ Y) [QuasiCompact f] [QuasiSeparated f]
{I : Type (max (u + 1) v)}
(K : I → DerivedCategory (Sheaf X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v}))
(a : ℤ) (hK : ∀ i, (K i).IsGE a) :
PreservesColimit (Discrete.functor K) (etaleAbelianDerivedDirectImage.{u, v} f)
Sources
Section59.53 Stalks of higher direct images#
Section 59.53 of the Stacks Project, Tag 03Q7. 2 tags here are carried by 11 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 03Q9, a theorem
Tag 03Q9 in the Stacks Project.
AlgebraicGeometry.higherBaseChangeStalkHom_comp_higherDirectImageStalkIso_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/BaseChangeHigher/StrictHenselizationCriterionCommSq.lean, line 571. The attribute's comment: “compatibility of the isomorphisms with the base change map of a commutative square”.
Stacks 03Q9, compatibility with base change along a commutative square. Write
θ = AlgebraicGeometry.higherDirectImageStalkIsofor the isomorphisms(R^q g_* F)_{f(x)} ≅ H^q(T ×_S Spec(𝒪^{sh}_{S,f(x)}), F)and(R^q h_* e⁻¹F)_x ≅ H^q(Y ×_X Spec(𝒪^{sh}_{X,x}), e⁻¹F). For a commutative squareh ≫ f = e ≫ gwithg,hquasi-compact and quasi-separated,θatxafter the stalkbatxof the base change mapf⁻¹ R^q g_* F ⟶ R^q h_* e⁻¹ Fisθatf(x)followed by the pull backρalongκ = AlgebraicGeometry.strictHenselizationBaseChangeSquareMap, the morphismY ×_X Spec(𝒪^{sh}_{X,x}) ⟶ T ×_S Spec(𝒪^{sh}_{S,f(x)})given byeand by the morphismmof strict henselizations:θ ∘ b = ρ ∘ θ.
theorem higherBaseChangeStalkHom_comp_higherDirectImageStalkIso_hom (q : ℕ)
(F : Sheaf (smallEtaleTopology T) Ab.{u + 1}) :
((higherBaseChangeStalkHom f g h e w x.hom).app q).app F ≫
(higherDirectImageStalkIso B₁ hX h x q ((smallEtalePullbackAb e).obj F)).hom =
(higherDirectImageStalkIso B₂ hS g (x.map f) q F).hom ≫
AddCommGrpCat.ofHom (etaleCohomologyPullback
(strictHenselizationBaseChangeSquareMap B₁ B₂ hX hS w x m hm)
((strictHenselizationBaseChangeSquarePullbackHom B₁ B₂ hX hS w x m hm).app F) q)
AlgebraicGeometry.stalkHigherDirectImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/StalkHigherDirectImageStrictHenselization.lean, line 282. The attribute's comment: “first assertion, for an abelian sheaf F on X_étale: (R^n f_* F)_s = H^n_ét(X ×_S Spec(𝒪^{sh}_{S,s}), p^{-1}F), with R^n Mathlib's right derived functors of direct image and of global sections on the small étale sites; the strict henselization is taken inside a big étale site B containing S”. References: SGA 4 IX (4.1.1), “more general”.
For
f : X ⟶ Squasi-compact and quasi-separated,sa geometric point ofSandp : X ×_S Spec(𝒪^{sh}_{S,s}) ⟶ Xthe projection,(R^n f_* F)_s ≅ H^n_ét(X ×_S Spec(𝒪^{sh}_{S,s}), p⁻¹F)for every abelian sheafFonX_étaleand everyn.
def stalkHigherDirectImageIso (F : Sheaf (smallEtaleTopology X) Ab.{u + 1}) (n : ℕ) :
(smallEtaleStalkAb s.hom).obj (((smallEtalePushforwardAb f).rightDerived n).obj F) ≅
((Sheaf.Γ (smallEtaleTopology (strictHenselizationBaseChange B hS f s))
Ab.{u + 1}).rightDerived n).obj
((smallEtalePullbackAb (strictHenselizationBaseChangeToSource B hS f s)).obj F)
AlgebraicGeometry.stalkDerivedPushforwardHomologyIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/StalkHigherDirectImageStrictHenselization.lean, line 295. The attribute's comment: “second assertion, for K in D^+(X_étale) and n in ℤ: (R^n f_* K)_s = H^n_ét(X ×_S Spec(𝒪^{sh}_{S,s}), p^{-1}K), the cohomology objects of the right derived functors on the bounded below derived categories”.
For
f : X ⟶ Squasi-compact and quasi-separated,KinD⁺(X_étale)andn : ℤ,(R^n f_* K)_s ≅ H^n(X ×_S Spec(𝒪^{sh}_{S,s}), p⁻¹K).
def stalkDerivedPushforwardHomologyIso
(K : DerivedCategory.Plus (Sheaf (smallEtaleTopology X) Ab.{u + 1})) (n : ℤ) :
(smallEtaleStalkAb s.hom).obj ((DerivedCategory.Plus.homologyFunctor _ n).obj
((smallEtalePushforwardAb f).rightDerivedFunctorPlus.obj K)) ≅
(DerivedCategory.Plus.homologyFunctor Ab.{u + 1} n).obj
((Sheaf.Γ (smallEtaleTopology (strictHenselizationBaseChange B hS f s))
Ab.{u + 1}).rightDerivedFunctorPlus.obj
((smallEtalePullbackAb
(strictHenselizationBaseChangeToSource B hS f s)).mapDerivedCategoryPlus.obj K))
AlgebraicGeometry.stalkDerivedPushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/StalkHigherDirectImageStrictHenselization.lean, line 312. The attribute's comment: “third assertion: (Rf_* K)_s = RΓ_ét(X ×_S Spec(𝒪^{sh}_{S,s}), p^{-1}K) in D^+(Ab), as an isomorphism of functors on D^+(X_étale), the stalk and p^{-1} acting degreewise”.
For
f : X ⟶ Squasi-compact and quasi-separated,(Rf_* K)_s ≅ RΓ(X ×_S Spec(𝒪^{sh}_{S,s}), p⁻¹K)inD⁺(Ab), naturally inK ∈ D⁺(X_étale).
def stalkDerivedPushforwardIso :
(smallEtalePullbackAb
(strictHenselizationBaseChangeToSource B hS f s)).mapDerivedCategoryPlus ⋙
(Sheaf.Γ (smallEtaleTopology (strictHenselizationBaseChange B hS f s))
Ab.{u + 1}).rightDerivedFunctorPlus ≅
(smallEtalePushforwardAb f).rightDerivedFunctorPlus ⋙
(smallEtaleStalkAb s.hom).mapDerivedCategoryPlus
AlgebraicGeometry.higherDirectImageStalkIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/StalkOfHigherDirectImage.lean, line 809. The attribute's comment: “the first assertion: abelian sheaves”. References: SGA 4 IX (4.1.1), “more general”.
Stacks 03Q9: the stalks of the higher direct images. Let
g : T ⟶ Sbe a quasi-compact and quasi-separated morphism of schemes,Fan abelian sheaf onT_étaleandsa geometric point ofS. Then(R^n g_* F)_s = H^n_étale(T ×_S Spec(𝒪^{sh}_{S,s}), p⁻¹F), wherep : T ×_S Spec(𝒪^{sh}_{S,s}) ⟶ Tis the projection. The isomorphism is natural inF, compatible with the connecting morphisms (it is the component ofAlgebraicGeometry.higherDirectImageStalkComparison), and in degree zero it is the canonical mapAlgebraicGeometry.pushforwardStalkToStrictHenselizationSectionsAb.
def higherDirectImageStalkIso (n : ℕ) (F : Sheaf (smallEtaleTopology T) Ab.{u + 1}) :
(smallEtaleStalkAb s.hom).obj (((smallEtalePushforwardAb g).rightDerived n).obj F) ≅
AddCommGrpCat.of (Sheaf.H.{u + 1}
((smallEtalePullbackAb (strictHenselizationBaseChangeToSource B hS g s)).obj F) n)
Stacks.StrictlyHenselian.higherDirectImageEtaleStalkIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/StrictlyHenselianDirectImageStalk.lean, line 105. The attribute's comment: “conditional on the base being Spec R for a strictly henselian local ring R and the geometric point lying over its closed point, so that the strict henselization is R and the base change of the source is X itself”.
Stacks 03Q9 over a strictly henselian base. The stalk at
sof then-th higher direct image ofFalongf : X ⟶ Spec Ris then-th étale cohomology group ofXwith coefficients inF.
public def higherDirectImageEtaleStalkIso
(hs : s.LiesOver (IsLocalRing.closedPoint R)) (n : ℕ)
(F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{u + 1}) :
etaleStalk B (Spec (.of R)) hS s ((higherDirectImage B R hS f n).obj F).obj ≅
((smallEtaleGlobalSections B X).rightDerived n).obj F
Tag 0GIX, a remark
Tag 0GIX in the Stacks Project.
AlgebraicGeometry.strictHenselizationSectionsToFibreSectionsViaBaseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/DerivedStalkFibreBaseChangeMaps.lean, line 448. The attribute's comment: “the second map: global sections of the base change map for the left square”.
Stacks 0GIX, the second map. The canonical map
RΓ(X ×_S Spec(𝒪^{sh}_{S,s}), p⁻¹K) ⟶ RΓ(X_s, K|_{X_s}), natural inK ∈ D(X_étale), defined as the source defines it: from the derived base change mapi⁻¹Rf'_*(p⁻¹K) ⟶ Rf_{s,*}(K|_{X_s})of the left squareX_s ----> X ×_S Spec(𝒪^{sh}_{S,s}) |f_s |f' v v s ---i--> Spec(𝒪^{sh}_{S,s})by taking global sections: it is the identification
RΓ(X ×_S Spec(𝒪^{sh}_{S,s}), -) ≅ RΓ(Spec(𝒪^{sh}_{S,s}), Rf'_* -), restriction of derived global sections alongi(an isomorphism over the strictly henselian base), derived global sections onsof the base change map, the identificationRΓ(s, Rf_{s,*} -) ≅ RΓ(X_s, -), and the identification of the restriction ofp⁻¹KtoX_swithK|_{X_s}.Every derived functor here is the total right derived functor on the whole unbounded homotopy category; their existence is not assumed but supplied by the instances
Stacks.EtaleCohomology.smallEtaleGlobalSectionsAb_hasRightDerivedFunctorandStacks.EtaleCohomology.hasRightDerivedFunctor_smallEtalePushforwardAb(abelian sheaves on a small étale site have K-injective resolutions).
def strictHenselizationSectionsToFibreSectionsViaBaseChange :
smallEtaleDerivedPullbackAb (strictHenselizationBaseChangeToSource B hS f s) ⋙
smallEtaleDerivedGlobalSections (strictHenselizationBaseChange B hS f s) ⟶
smallEtaleDerivedPullbackAb (geometricFibreToSource f s) ⋙
smallEtaleDerivedGlobalSections (geometricFibre f s)
AlgebraicGeometry.derivedPushforwardStalkToStrictHenselizationSectionsViaBaseChange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/DerivedStalkFibreBaseChangeMaps.lean, line 709. The attribute's comment: “the first map: global sections of the base change map for the right square”.
Stacks 0GIX, the first map. The canonical map
(Rf_*K)_s ⟶ RΓ(X ×_S Spec(𝒪^{sh}_{S,s}), p⁻¹K), natural inK ∈ D(X_étale), defined as the source defines it: from the derived base change mapj⁻¹Rf_*K ⟶ Rf'_*(p⁻¹K)of the right squareX ×_S Spec(𝒪^{sh}_{S,s}) --p--> X |f' |f v v Spec(𝒪^{sh}_{S,s}) ---j---> Sby taking global sections over the strict henselization: it is the comparison
(Rf_*K)_s ⟶ RΓ(Spec(𝒪^{sh}_{S,s}), j⁻¹Rf_*K)of the stalk with derived sections over the strict henselization (AlgebraicGeometry.vanishingCyclesMap, an isomorphism byAlgebraicGeometry.isIso_vanishingCyclesMap_id), derived global sections over the strict henselization of the base change map, and the identificationRΓ(Spec(𝒪^{sh}_{S,s}), Rf'_* -) ≅ RΓ(X ×_S Spec(𝒪^{sh}_{S,s}), -). The structure morphismjis written𝟙 ≫ j, the form in which the comparison of the stalk with sections presents it.Every derived functor here is the total right derived functor on the whole unbounded homotopy category; their existence is not assumed but supplied by the instances
Stacks.EtaleCohomology.smallEtaleGlobalSectionsAb_hasRightDerivedFunctorandStacks.EtaleCohomology.hasRightDerivedFunctor_smallEtalePushforwardAb(abelian sheaves on a small étale site have K-injective resolutions).
def derivedPushforwardStalkToStrictHenselizationSectionsViaBaseChange :
smallEtaleDerivedPushforwardAb f ⋙ smallEtaleDerivedStalkAb s.hom ⟶
smallEtaleDerivedPullbackAb (strictHenselizationBaseChangeToSource B hS f s) ⋙
smallEtaleDerivedGlobalSections (strictHenselizationBaseChange B hS f s)
AlgebraicGeometry.derivedPushforwardStalkToStrictHenselizationSectionsViaBaseChange_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/DerivedStalkFibreBaseChangeMaps.lean, line 771. The attribute's comment: “the composition is the base change map”.
Stacks 0GIX, the composition clause. For a morphism of schemes
f : X ⟶ Sand a geometric pointsofS, the composite of the two canonical maps
(Rf_*K)_s ⟶ RΓ(X ×_S Spec(𝒪^{sh}_{S,s}), p⁻¹K) ⟶ RΓ(X_s, K|_{X_s})obtained by taking global sections of the base change maps of the right and of the left square (
AlgebraicGeometry.derivedPushforwardStalkToStrictHenselizationSectionsViaBaseChangeandAlgebraicGeometry.strictHenselizationSectionsToFibreSectionsViaBaseChange) is the usual base change map(Rf_*K)_s ⟶ RΓ(X_s, K|_{X_s}): the identification of the stalk atswith global sections onsof the inverse image, followed by global sections onsof the derived base change maps⁻¹Rf_*K ⟶ Rq_*(K|_{X_s})of Stacks 0A2A for the cartesian square defining the geometric fibre (q : X_s ⟶ sits structure morphism), and by the identificationRΓ(s, Rq_* -) ≅ RΓ(X_s, -)of Stacks 0D6H. This holds as an equality of natural transformations on the whole unbounded derived categoryD(X_étale); nothing is assumed offor ofs, and the existence of the unbounded derived functors involved is supplied by instances, not assumed.The two maps agree with the ones this library constructs directly (
AlgebraicGeometry.derivedPushforwardStalkToStrictHenselizationSections_eq_baseChangeandAlgebraicGeometry.strictHenselizationSectionsToFibreSections_eq_baseChange), whose composite is computed byAlgebraicGeometry.derivedPushforwardStalkToStrictHenselizationSections_comp_fibreSections.
theorem derivedPushforwardStalkToStrictHenselizationSectionsViaBaseChange_comp :
derivedPushforwardStalkToStrictHenselizationSectionsViaBaseChange B hS f s ≫
strictHenselizationSectionsToFibreSectionsViaBaseChange B hS f s =
Functor.whiskerLeft (smallEtaleDerivedPushforwardAb f)
(derivedGeometricStalkToPullbackSections s.hom) ≫
(Functor.associator _ _ _).inv ≫
Functor.whiskerRight (geometricFibreDerivedBaseChangeAb f s)
(smallEtaleDerivedGlobalSections s.source) ≫
(Functor.associator _ _ _).hom ≫
Functor.whiskerLeft (smallEtaleDerivedPullbackAb (geometricFibreToSource f s))
(smallEtaleDerivedGlobalSectionsPushforwardIsoAb (geometricFibreToPoint f s)).hom
AlgebraicGeometry.strictHenselizationSectionsToFibreSections, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/StalkOfDerivedPushforward.lean, line 445. The attribute's comment: “the map to the fibre”.
Stacks 0GIX, the map to the fibre. The canonical map
RΓ(X ×_S Spec(𝒪^{sh}_{S,s}), p⁻¹K) ⟶ RΓ(X_s, K|_{X_s})for an object
Kof the unbounded derived category of abelian sheaves on the small étale site ofX, natural inK, wherep : X ×_S Spec(𝒪^{sh}_{S,s}) ⟶ Xis the projection.It is the derived restriction map along the canonical morphism
X_s ⟶ X ×_S Spec(𝒪^{sh}_{S,s})overX, after identifying the inverse image along that morphism ofp⁻¹Kwith the restriction ofKto the geometric fibre.
def strictHenselizationSectionsToFibreSections :
smallEtaleDerivedPullbackAb (strictHenselizationBaseChangeToSource B hS f s) ⋙
smallEtaleDerivedGlobalSections (strictHenselizationBaseChange B hS f s) ⟶
smallEtaleDerivedPullbackAb (geometricFibreToSource f s) ⋙
smallEtaleDerivedGlobalSections (geometricFibre f s)
AlgebraicGeometry.derivedPushforwardStalkToStrictHenselizationSections, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/StalkOfDerivedPushforward.lean, line 551. The attribute's comment: “the map from the stalk”.
Stacks 0GIX, the map from the stalk. The canonical map
(Rf_*K)_s ⟶ RΓ(X ×_S Spec(𝒪^{sh}_{S,s}), p⁻¹K)for an object
Kof the unbounded derived category of abelian sheaves on the small étale site ofX, natural inK, wherep : X ×_S Spec(𝒪^{sh}_{S,s}) ⟶ Xis the projection.The stalk of the derived direct image is a right derived functor of the stalk of the direct image, the stalk functor having a right adjoint, so the map on sheaves
AlgebraicGeometry.pushforwardStalkToStrictHenselizationSectionsAbextends uniquely to a map of unbounded derived categories factoring it through the units.
def derivedPushforwardStalkToStrictHenselizationSections :
smallEtaleDerivedPushforwardAb f ⋙ smallEtaleDerivedStalkAb s.hom ⟶
smallEtaleDerivedPullbackAb (strictHenselizationBaseChangeToSource B hS f s) ⋙
smallEtaleDerivedGlobalSections (strictHenselizationBaseChange B hS f s)
Sources
Section59.54 The Leray spectral sequence#
Section 59.54 of the Stacks Project, Tag 03QA. 2 tags here are carried by 4 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 03QB, a lemma
Tag 03QB in the Stacks Project.
AlgebraicGeometry.pushforward_injective_cechCohomology_isZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PushforwardAcyclic/CechVanishing.lean, line 43. The attribute's comment: “cech_vanishing”.
Stacks 03QB. The direct image of an injective abelian sheaf on the small étale site of
Xhas vanishing positive-degree Čech cohomology for every family of morphisms in the small étale site ofY.
public theorem pushforward_injective_cechCohomology_isZero
(B : BigEtaleSite.{u}) {X Y : B.Scheme} (f : X ⟶ Y)
(I : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{u + 1})
[Injective I]
(E : Covering.{u + 1, u, u + 1} (SmallEtale B Y.obj Y.property))
(p : ℕ) (hp : 0 < p) :
IsZero (Stacks.CechSite.cechCohomology E.2
(((smallEtaleBaseChange B f).sheafPushforwardContinuous
AddCommGrpCat.{u + 1}
(SmallEtale.topology B Y.obj Y.property)
(SmallEtale.topology B X.obj X.property)).obj I).obj p)
AlgebraicGeometry.pushforward_injective_rightAcyclic_pushforward_of_smallEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PushforwardAcyclic/Pushforward.lean, line 120. The attribute's comment: “pushforward_acyclic”.
Stacks 03QB, with no homological-algebra side condition. The direct image of an injective abelian étale sheaf is acyclic for a further direct image.
This is
AlgebraicGeometry.pushforward_injective_rightAcyclic_pushforwardwith all three of its instance binders discharged, exactly as inAlgebraicGeometry.pushforward_injective_rightAcyclic_sections_of_smallEtale: sheafification comes from Mathlib's plus construction at the coefficient universeu + 1and the enough injectives fromAlgebraicGeometry.SmallEtale.isGrothendieckAbelian_sheaf_succ.
public theorem pushforward_injective_rightAcyclic_pushforward_of_smallEtale
(B : BigEtaleSite.{u}) {X Y Z : B.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z)
(I : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{u + 1})
[Injective I] :
((smallEtaleBaseChange B g).sheafPushforwardContinuous
AddCommGrpCat.{u + 1}
(SmallEtale.topology B Z.obj Z.property)
(SmallEtale.topology B Y.obj Y.property)).rightAcyclic
(((smallEtaleBaseChange B f).sheafPushforwardContinuous
AddCommGrpCat.{u + 1}
(SmallEtale.topology B Y.obj Y.property)
(SmallEtale.topology B X.obj X.property)).obj I)
AlgebraicGeometry.pushforward_injective_rightAcyclic_sections_of_smallEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/PushforwardAcyclic/Sections.lean, line 105. The attribute's comment: “sections_acyclic”.
Stacks 03QB, with no homological-algebra side condition. The direct image of an injective abelian étale sheaf is acyclic for sections over any object of the small étale site of the target.
This is
AlgebraicGeometry.pushforward_injective_rightAcyclic_sectionswith both of its instance binders discharged: abelian presheaves on the small étale site of a scheme inScheme.{u}have a sheafification with coefficients inAddCommGrpCat.{u + 1}by Mathlib's plus construction, the site having its objects inType (u + 1), and the resulting abelian category of sheaves has enough injectives becauseAlgebraicGeometry.SmallEtale.isGrothendieckAbelian_sheaf_succmakes it Grothendieck abelian at that coefficient universe.
public theorem pushforward_injective_rightAcyclic_sections_of_smallEtale
(B : BigEtaleSite.{u}) {X Y : B.Scheme} (f : X ⟶ Y)
(I : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{u + 1})
[Injective I] (V : SmallEtale B Y.obj Y.property) :
((sheafSections (SmallEtale.topology B Y.obj Y.property)
AddCommGrpCat.{u + 1}).obj (Opposite.op V)).rightAcyclic
(((smallEtaleBaseChange B f).sheafPushforwardContinuous
AddCommGrpCat.{u + 1}
(SmallEtale.topology B Y.obj Y.property)
(SmallEtale.topology B X.obj X.property)).obj I)
Tag 03QC, a proposition
Tag 03QC in the Stacks Project.
AlgebraicGeometry.exists_abutsTo_leraySpectralSequence_smallEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/LeraySpectralSequence.lean, line 226. References: SGA 4½ Arcata (2.3.4), “first spectral sequence”; SGA 4 V (5.3), “small étale sites”; SGA 4 V (5.4), “étale sites, Z = point”; SGA 4 VII (1.5), “H^p(Y,R^qf_*F) SS”; SGA 4 IX (4.2), “more general”; SGA 4½ Th finitude (1.3), “partial”.
The Leray spectral sequence for the small étale site (Stacks 03QC). Let
f : X ⟶ Ybe a morphism in a big étale site and letFbe an abelian sheaf on the small étale site ofX. There is a cohomological spectral sequence with second pageE₂^{p,q} ≅ H^p_ét(Y, R^q f_* F),the étale cohomology of
Ywith coefficients in the higher direct images ofF, which abuts to the graded familyn ↦ H^n_ét(X, F)of étale cohomology groups ofX: some finite decreasing filtration of eachH^n_ét(X, F)has the termsE_∞^{p,n-p}as its graded pieces.Both the second page and the abutment are taken in the derived-functor form of étale cohomology,
CategoryTheory.Functor.rightDerivedPlusof global sections, andR^q f_*is theq-th right derived functor of direct image.This is
exists_abutsTo_leraySpectralSequence_smallEtale_sectionsfor the final object of the small étale site ofY, whose base change is a final object of the small étale site ofX.
public theorem exists_abutsTo_leraySpectralSequence_smallEtale
(F : Sheaf (SmallEtale.topology B X.obj X.property) AddCommGrpCat.{u + 1}) :
∃ E : CohomologicalSpectralSequence AddCommGrpCat.{u + 1} 0,
(∀ p q : ℤ, Nonempty ((E.page 2 zero_le_two).X (p, q) ≅
((smallEtaleGlobalSections B Y).rightDerivedPlus p).obj
((Stacks.HigherDirectImage.pushforward.{u, u + 1} B f).rightDerivedPlus q |>.obj
F))) ∧
SpectralSequence.AbutsTo E
(fun n => ((smallEtaleGlobalSections B X).rightDerivedPlus n).obj F)
Sources
Section59.55 Vanishing of finite higher direct images#
Section 59.55 of the Stacks Project, Tag 03QN. 6 tags here are carried by 20 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.
Tag 03QO, a lemma
Tag 03QO in the Stacks Project.
Stacks.StrictlyHenselian.subsingleton_etaleCohomology_smallEtaleTopology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/StrictlyHenselianSmallEtaleVanishing.lean, line 92. The attribute's comment: “vanishing of positive-degree étale cohomology, on the small étale site”.
Positive-degree étale cohomology of an abelian sheaf on the small étale site of the spectrum of a strictly henselian local ring vanishes.
public theorem subsingleton_etaleCohomology_smallEtaleTopology
(R : Type u) [CommRing R] [StrictlyHenselianLocalRing R]
[HasExt.{w} (Sheaf (Spec (.of R)).smallEtaleTopology AddCommGrpCat.{u + 1})]
(F : Sheaf (Spec (.of R)).smallEtaleTopology AddCommGrpCat.{u + 1})
(p : ℕ) (hp : 1 ≤ p) :
Subsingleton (Sheaf.H.{w, u + 1} F p)
Stacks.StrictlyHenselian.isIso_globalSectionsToEtaleStalk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/StrictlyHenselianVanishing.lean, line 560. The attribute's comment: “global sections equal the closed geometric stalk”. References: SGA 4 VIII (8.6), “strictly henselian, n=0”.
For a strictly henselian local ring, the canonical global-sections-to-stalk map is an isomorphism for every sheaf of sets.
public theorem isIso_globalSectionsToEtaleStalk
[StrictlyHenselianLocalRing R]
(hs : s.LiesOver (IsLocalRing.closedPoint R))
[HasWeakSheafify (SmallEtale.topology B (Spec (.of R)) hS)
(Type (u + 1))]
(F : Sheaf (SmallEtale.topology B (Spec (.of R)) hS)
(Type (u + 1))) :
IsIso (globalSectionsToEtaleStalk B R hS s F)
Stacks.StrictlyHenselian.globalSections_preservesFiniteColimits, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/StrictlyHenselianVanishing.lean, line 647. The attribute's comment: “exactness of global sections”.
Global sections of abelian étale sheaves on a strictly henselian local scheme are exact. As a right adjoint, this functor already preserves limits.
public instance globalSections_preservesFiniteColimits
[StrictlyHenselianLocalRing R]
[HasSheafify (SmallEtale.topology B (Spec (.of R)) hS)
AddCommGrpCat.{u + 1}] :
PreservesFiniteColimits
(Sheaf.Γ (SmallEtale.topology B (Spec (.of R)) hS)
AddCommGrpCat.{u + 1})
Stacks.StrictlyHenselian.subsingleton_etaleCohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/StrictlyHenselianVanishing.lean, line 665. The attribute's comment: “vanishing of positive-degree étale cohomology”. References: SGA 4 VIII (8.6), “strictly henselian, p≥1”.
Positive-degree étale cohomology of an abelian sheaf over a strictly henselian local scheme vanishes.
public theorem subsingleton_etaleCohomology
[StrictlyHenselianLocalRing R]
[HasSheafify (SmallEtale.topology B (Spec (.of R)) hS)
AddCommGrpCat.{u + 1}]
[HasExt.{w} (Sheaf (SmallEtale.topology B (Spec (.of R)) hS)
AddCommGrpCat.{u + 1})]
(F : Sheaf (SmallEtale.topology B (Spec (.of R)) hS)
AddCommGrpCat.{u + 1}) (p : ℕ) (hp : 1 ≤ p) :
Subsingleton (Sheaf.H.{w, u + 1} F p)
Tag 03QP, a proposition
Tag 03QP in the Stacks Project.
AlgebraicGeometry.SmallEtale.etalePushforward_exact_of_isFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Etale/DerivedLowerShriekQuasiFinite.lean, line 264. The attribute's comment: “exactness of direct image along a finite morphism”.
Direct image of abelian étale sheaves along a finite morphism is exact.
public theorem etalePushforward_exact_of_isFinite :
exactFunctor _ _ (etalePushforward.{u, u + 1} B fbar)
AlgebraicGeometry.finitePushforwardStalkToProduct_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FinitePushforwardStalk/Bijectivity.lean, line 691. The attribute's comment: “part (1): the stalk of a finite pushforward, for sheaves of sets”.
Stacks Project, Tag 03QP, part (1), sheaves of sets. For a finite morphism the comparison map from the stalk of a direct image to the product of the stalks over the lifts of the geometric point is bijective.
public theorem finitePushforwardStalkToProduct_bijective
(B : BigEtaleSite.{u}) {X Y : B.Scheme} (f : X ⟶ Y)
[IsFinite (B.inclusion.map f)] (y : GeometricPoint Y.1)
(F : Sheaf (SmallEtale.topology B X.1 X.property) (Type (u + 1))) :
Function.Bijective (finitePushforwardStalkToProduct B f y F)
AlgebraicGeometry.finitePushforwardStalkEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FinitePushforwardStalk/Bijectivity.lean, line 709. The attribute's comment: “part (1): the stalk of a finite pushforward, for sheaves of sets”. References: SGA 4 VIII (5.5), “partial”.
Stacks Project, Tag 03QP, part (1), sheaves of sets. The stalk at a geometric point
yof the direct image of a sheaf of sets along a finite morphism is the product of the stalks of the sheaf over the lifts ofy.
public def finitePushforwardStalkEquiv
(B : BigEtaleSite.{u}) {X Y : B.Scheme} (f : X ⟶ Y)
[IsFinite (B.inclusion.map f)] (y : GeometricPoint Y.1)
(F : Sheaf (SmallEtale.topology B X.1 X.property) (Type (u + 1))) :
etaleStalk B Y.1 Y.property y
(((smallEtaleBaseChange B f).sheafPushforwardContinuous (Type (u + 1))
(SmallEtale.topology B Y.1 Y.property)
(SmallEtale.topology B X.1 X.property)).obj F).obj ≃
(∀ x : {g : y.source ⟶ X.1 // g ≫ B.inclusion.map f = y.hom},
etaleStalk B X.1 X.property
(geometricPointLift (B.inclusion.map f) y x) F.obj)
AlgebraicGeometry.finitePushforwardStalkEquiv_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FinitePushforwardStalk/Bijectivity.lean, line 726. The attribute's comment: “part (1): the stalk of a finite pushforward, for sheaves of sets”.
Stacks Project, Tag 03QP, part (1), sheaves of sets. Each component of the product decomposition of the stalk is the canonical stalk map at the corresponding lift.
public theorem finitePushforwardStalkEquiv_apply
(B : BigEtaleSite.{u}) {X Y : B.Scheme} (f : X ⟶ Y)
[IsFinite (B.inclusion.map f)] (y : GeometricPoint Y.1)
(F : Sheaf (SmallEtale.topology B X.1 X.property) (Type (u + 1)))
(z : etaleStalk B Y.1 Y.property y
(((smallEtaleBaseChange B f).sheafPushforwardContinuous (Type (u + 1))
(SmallEtale.topology B Y.1 Y.property)
(SmallEtale.topology B X.1 X.property)).obj F).obj)
(x : {g : y.source ⟶ X.1 // g ≫ B.inclusion.map f = y.hom}) :
finitePushforwardStalkEquiv B f y F z x =
finitePushforwardStalkComponent B f y F x z
AlgebraicGeometry.stalkPushforwardIsoDirectSum, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FinitePushforwardStalk/DirectSum.lean, line 560. The attribute's comment: “part (1): the stalk of a finite pushforward, for abelian sheaves”.
The stalk of a finite direct image is canonically the direct sum of its stalks at the geometric lifts.
public noncomputable def stalkPushforwardIsoDirectSum
[IsFinite (B.inclusion.map f)]
(F : Sheaf (SmallEtale.topology B X.1 X.property) AddCommGrpCat.{u + 1}) :
AlgebraicGeometry.etaleStalk B Y.1 Y.property y
(((smallEtaleBaseChange B f).sheafPushforwardContinuous
AddCommGrpCat.{u + 1}
(SmallEtale.topology B Y.1 Y.property)
(SmallEtale.topology B X.1 X.property)).obj F).obj ≅
∐ fun x : GeometricLifts B f y =>
AlgebraicGeometry.etaleStalk B X.1 X.property
(geometricPointLift
(B.inclusion.map f) y x) F.obj
AlgebraicGeometry.stalkPushforwardIsoDirectSum_germ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FinitePushforwardStalk/DirectSum.lean, line 601. The attribute's comment: “part (1): the stalk of a finite pushforward, for abelian sheaves”.
On each component, the finite direct-image stalk decomposition takes a section over a neighborhood of
yto its germ at a liftx, after pulling the neighborhood back toX. The auxiliary neighborhoodVis any étale neighborhood ofxmapping to that pullback and carrying the specified point.
public theorem stalkPushforwardIsoDirectSum_germ
[IsFinite (B.inclusion.map f)]
(F : Sheaf (SmallEtale.topology B X.1 X.property) AddCommGrpCat.{u + 1})
(x : GeometricLifts B f y)
(U : (geometricPointFiber B Y.1 Y.property y).Elements)
(V : (geometricPointFiber B X.1 X.property
(geometricPointLift
(B.inclusion.map f) y x)).Elements)
(t : V.1 ⟶ (smallEtaleBaseChange B f).obj U.1)
(hU : V.2.1 ≫ (SmallEtale.toScheme B X.1 X.property).map t ≫
B.inclusion.map (pullback.fst U.1.obj.hom f) = U.2.1)
(hX : V.2.1 ≫ (SmallEtale.toScheme B X.1 X.property).map t ≫
B.inclusion.map (pullback.snd U.1.obj.hom f) = x.1) :
colimit.ι
((CategoryOfElements.π (geometricPointFiber B Y.1 Y.property y)).op ⋙
(((smallEtaleBaseChange B f).sheafPushforwardContinuous
AddCommGrpCat.{u + 1}
(SmallEtale.topology B Y.1 Y.property)
(SmallEtale.topology B X.1 X.property)).obj F).obj)
(op U) ≫
(stalkPushforwardIsoDirectSum B f y F).hom ≫
(by classical exact Limits.Sigma.π _ x) =
F.obj.map t.op ≫
colimit.ι
((CategoryOfElements.π (geometricPointFiber B X.1 X.property
(geometricPointLift
(B.inclusion.map f) y x))).op ⋙ F.obj)
(op V)
AlgebraicGeometry.stalkPushforwardIsoDirectSum_natural, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FinitePushforwardStalk/DirectSum.lean, line 635. The attribute's comment: “part (1): the stalk of a finite pushforward, for abelian sheaves”.
The finite direct-sum decomposition is natural in the abelian sheaf.
public theorem stalkPushforwardIsoDirectSum_natural
[IsFinite (B.inclusion.map f)]
{F G : Sheaf (SmallEtale.topology B X.1 X.property) AddCommGrpCat.{u + 1}}
(α : F ⟶ G) :
etaleStalkMap B Y.1 Y.property y
(((smallEtaleBaseChange B f).sheafPushforwardContinuous
AddCommGrpCat.{u + 1}
(SmallEtale.topology B Y.1 Y.property)
(SmallEtale.topology B X.1 X.property)).map α) ≫
(stalkPushforwardIsoDirectSum B f y G).hom =
(stalkPushforwardIsoDirectSum B f y F).hom ≫
Limits.Sigma.map (fun x : GeometricLifts B f y =>
etaleStalkMap B X.1 X.property
(geometricPointLift
(B.inclusion.map f) y x) α)
Stacks.EtaleCohomology.isZero_rightDerived_smallEtalePushforwardAb_of_isIntegralHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/IntegralHigherDirectImage.lean, line 55. The attribute's comment: “part (2): vanishing of the positive higher direct images”. References: SGA 4 Vbis (4.3.4); SGA 4½ Arcata (2.3.6).
The positive higher direct images along an integral morphism vanish. For a finite morphism this is the acyclicity half of Stacks Project Tag 03QP, finiteness implying integrality.
public theorem isZero_rightDerived_smallEtalePushforwardAb_of_isIntegralHom
{X Y : Scheme.{u}} (f : X ⟶ Y) [IsIntegralHom f]
(F : Sheaf (smallEtaleTopology X) Ab.{u + 1}) (q : ℕ) (hq : 0 < q) :
IsZero (((smallEtalePushforwardAb f).rightDerived q).obj F)
Stacks.EtaleCohomology.isZero_rightDerived_etaleAbelianDirectImage_of_isIntegralHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/ProperBaseChange/IntegralDirectImageAcyclic.lean, line 167. The attribute's comment: “part (2) at the coefficients of proper base change”. References: SGA 4 VIII (5.5), “more general”; SGA 4 VIII (5.6); SGA 4 Vbis (4.3.4); SGA 4 XII (5.3bis), “special case”; SGA 4 XIV (1.11), “partial”; SGA 4 XVII (4.3.1), “special case”; SGA 4½ Arcata (2.3.6).
Stacks 03QP, part (2), at the coefficients of the proper base change development. The positive higher direct images of an abelian sheaf along an integral morphism of schemes vanish: an integral morphism — a finite morphism, for instance — is acyclic for étale cohomology.
Direct image is exact, and applying an exact functor degreewise to an injective resolution gives a resolution again, so the homology of the image complex vanishes in positive degrees.
public theorem isZero_rightDerived_etaleAbelianDirectImage_of_isIntegralHom
(f : X ⟶ Y) [IsIntegralHom f]
(F : Sheaf X.smallEtaleTopology AddCommGrpCat.{max (u + 1) v}) (q : ℕ) (hq : 0 < q) :
IsZero (((etaleAbelianDirectImage.{u, v} f).rightDerived q).obj F)
Stacks.EtaleCohomology.TorsionModules.isZero_rightDerived_modulePushforward_of_isIntegralHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/TorsionModulesCurves/FinitePushforwardAcyclic.lean, line 156. The attribute's comment: “part (2), for sheaves of Λ-modules on the small étale sites of Tag 021B”. References: SGA 4 VIII (5.5), “more general”; SGA 4 VIII (5.6), “more general”; SGA 4 Vbis (4.3.4), “more general”; SGA 4 XIV (1.11), “partial”; SGA 4½ Arcata (2.3.6), “more general”.
Stacks 03QP, part (2), for sheaves of
Λ-modules on the small étale sites of Stacks 021B. Forfwith integral underlying morphism of schemes — a finite morphism, for instance — the higher direct images of a sheaf ofΛ-modules alongfvanish:R^q f_*ℱ = 0for everyq > 0. The direct image is exact bymodulePushforward_exact_of_isIntegralHom, and the higher right derived functors of an exact functor vanish.
theorem isZero_rightDerived_modulePushforward_of_isIntegralHom
[IsIntegralHom (B.inclusion.map f)]
(ℱ : Sheaf (SmallEtale.topology B X.obj X.property) (ModuleCat.{max (u + 1) w r} Λ))
(q : ℕ) (hq : 0 < q) :
IsZero (((modulePushforward.{u, max w r} B Λ f).rightDerived q).obj ℱ)
Tag 0959, a lemma
Tag 0959 in the Stacks Project.
AlgebraicGeometry.isIso_smallEtaleBaseChangeNatTrans, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FinitePushforwardBaseChange.lean, line 709.
Consider a cartesian square
of schemes of a big étale site withX' --g'--> X |f' |f v v Y' --g---> Yffinite, and a sheaf of setsFon the small étale site ofX. Then the canonical comparisong⁻¹ f_* F ⟶ f'_* (g')⁻¹ Fis an isomorphism.
theorem isIso_smallEtaleBaseChangeNatTrans
(sq : IsPullback (B.inclusion.map g') (B.inclusion.map f') (B.inclusion.map f)
(B.inclusion.map g))
[IsFinite (B.inclusion.map f)] (h : g' ≫ f = f' ≫ g)
(F : Sheaf (SmallEtale.topology B X.1 X.property) (Type (u + 1))) :
IsIso ((smallEtaleBaseChangeNatTrans B g' f' f g h).app F)
Stacks.EtaleCohomology.isIso_smallEtaleBaseChangeAb_of_isFinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/SmallEtaleBaseChangeAbFinite.lean, line 307. The attribute's comment: “for abelian sheaves, at the comparison smallEtaleBaseChangeAb of [Stacks, Tag 0F02]; the morphism is finite, not merely integral, so this is 0959 and not 0EYP”.
Base change of an abelian direct image along a finite morphism, at the comparison
Stacks.EtaleCohomology.smallEtaleBaseChangeAb. For a cartesian squareof schemes withY' --π'--> Y |e' |e v v T' --π---> Tπfinite, the canonical comparisone⁻¹ π_* ⟶ π'_* (e')⁻¹of abelian sheaves on the small étale sites is an isomorphism.This is [Stacks, Tag 0959] for abelian coefficients, stated at the comparison which the higher-direct-image development of [Stacks, Tag 0F02] uses. The abelian statement at the comparison of the proper base change development is
Stacks.EtaleCohomology.isIso_etaleAbelianBaseChange_of_isFinite; the passage between the two comparisons isStacks.EtaleCohomology.isIso_smallEtaleBaseChangeAb_of_isIso_etaleAbelianBaseChange, and no big étale site occurs in the hypotheses.[Stacks, Tag 0EYP] is this statement with
πmerely integral. It does not follow from this one: the source's passage from a finite morphism to an integral one presents the comparison as a colimit of the comparisons for the finite stages of the integral morphism, and that presentation is not available in this library for abelian coefficients.
public theorem isIso_smallEtaleBaseChangeAb_of_isFinite {Y Y' T T' : Scheme.{u}} (e : Y ⟶ T)
(π : T' ⟶ T) (π' : Y' ⟶ Y) (e' : Y' ⟶ T') (sq : IsPullback π' e' e π) [IsFinite π] :
IsIso (smallEtaleBaseChangeAb e π π' e' sq.w)
Tag 0EYP, a lemma
Tag 0EYP in the Stacks Project.
AlgebraicGeometry.isIso_smallEtaleBaseChangeNatTrans_of_isIntegralHom_univ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/IntegralPushforwardBaseChangeLimitUnconditional.lean, line 621. References: SGA 4 VIII (5.5), “more general”.
Stacks Project, Tag 0EYP. Consider a cartesian square
of schemes of a big étale site withX' --g'--> X |f' |f v v Y' --g---> Yfintegral, and a sheaf of setsFon the small étale site ofX, with values inType (max (u + 1) v)for any universev. Then the canonical comparisong⁻¹ f_* F ⟶ f'_* (g')⁻¹ Fis an isomorphism.The comparison is checked on stalks at the geometric points
y'ofY'. Both stalks embed into the product of the stalks ofFover the lifts ofy', because for an integral morphism the stalk of a direct image is detected at the lifts (AlgebraicGeometry.finitePushforwardStalkComponent_injective_univ); this gives injectivity. For surjectivity, an affine open neighbourhoodVof the image ofy'inYis chosen, the integral morphismX ×_Y V ⟶ Vis written as a limit of finite morphisms (Stacks 09YZ), the family of germs attached to an element of the target is shown to be given by stage sections on cylinders of lifts (AlgebraicGeometry.exists_stage_forall_cylinderGerm_eq_univ), finitely many cylinders cover the lifts (AlgebraicGeometry.exists_finset_forall_exists_comp_eq_of_isLimit), and the finite case of the stalk computation, Stacks 03QP, at a common stage produces the required germ off_* F.
theorem isIso_smallEtaleBaseChangeNatTrans_of_isIntegralHom_univ
(sq : IsPullback (B.inclusion.map g') (B.inclusion.map f') (B.inclusion.map f)
(B.inclusion.map g))
[IsIntegralHom (B.inclusion.map f)] (h : g' ≫ f = f' ≫ g)
(F : Sheaf (SmallEtale.topology B X.1 X.property) (Type (max (u + 1) v))) :
IsIso ((smallEtaleBaseChangeNatTransUniv B g' f' f g h).app F)
Tag 09Z2, a lemma
Tag 09Z2 in the Stacks Project.
Stacks.EtaleCohomology.exists_cechSheafSpectralSequence_functorial, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FiniteDescent/SpectralSequenceFunctorial.lean, line 476.
[Stacks, Tag 09Z2]. Let
f : X ⟶ Ybe a surjective finite morphism of schemes, letf_n : X_n ⟶ Ybe the structure map of the(n + 1)-fold fibre product ofXoverY, and for an abelian sheafFon the small étale site ofYputF_n = f_{n,*}f_n^{-1}F. Then:
- there is an exact sequence
0 → F → F_0 → F_1 → F_2 → ⋯onY_étale, with augmentation the canonical mapF ⟶ f_*f^{-1}F;- there is a cohomological spectral sequence with
E_1^{p,q} = H^q_étale(X_p, f_p^{-1}F)converging toH^{p+q}(Y_étale, F), convergence meaning that eachH^n(Y_étale, F)carries a finite decreasing filtrationFilwhose graded pieces are the stable terms of the spectral sequence;- this spectral sequence is functorial in
F: it is produced by a functorEofF, the first-page identification is an isomorphism of functors ofF, and the filtration of the abutment is carried into itself by the map a morphismF ⟶ Ginduces on cohomology.The exact sequence is
Stacks.EtaleCohomology.exists_exact_cechSheafSequence; the functor isStacks.EtaleCohomology.cechSpectralSequenceFunctor, the augmented cobar complex of the monadf_*f^{-1}followed by the hyper-Extspectral sequence of [Stacks, Tag 0AVI].
public theorem exists_cechSheafSpectralSequence_functorial [IsFinite f] [Surjective f] :
(∀ F : Sheaf (smallEtaleTopology Y) Ab.{u + 1},
∃ (d : ∀ n : ℕ, cechSheaf f F n ⟶ cechSheaf f F (n + 1))
(haug : cechAug f F ≫ d 0 = 0) (hdd : ∀ n : ℕ, d n ≫ d (n + 1) = 0),
Mono (cechAug f F) ∧ (ShortComplex.mk _ _ haug).Exact ∧
∀ n : ℕ, (ShortComplex.mk _ _ (hdd n)).Exact) ∧
∃ E : Sheaf (smallEtaleTopology Y) Ab.{u + 1} ⥤
CohomologicalSpectralSequence AddCommGrpCat.{u + 1} 1,
(∀ p q : ℕ, Nonempty (E ⋙
CategoryTheory.SpectralSequence.pageFunctor AddCommGrpCat.{u + 1} _ 1 1 (le_refl 1) ⋙
HomologicalComplex.eval AddCommGrpCat.{u + 1} _ ((p : ℤ), (q : ℤ)) ≅
smallEtalePullbackAb (cechProjection f p) ⋙
sheafHFunctor (cechScheme f p) q)) ∧
∃ (Fil : ∀ (_p : ℤ) (n : ℕ) (F : Sheaf (smallEtaleTopology Y) Ab.{u + 1}),
Subobject ((sheafHFunctor Y n).obj F))
(hFil : ∀ (p p' : ℤ) (n : ℕ) (F : Sheaf (smallEtaleTopology Y) Ab.{u + 1}),
p ≤ p' → Fil p' n F ≤ Fil p n F),
(∀ (p : ℤ) (n : ℕ) (F G : Sheaf (smallEtaleTopology Y) Ab.{u + 1}) (φ : F ⟶ G),
(Subobject.«exists» ((sheafHFunctor Y n).map φ)).obj (Fil p n F) ≤
Fil p n G) ∧
(∀ (n : ℕ) (F : Sheaf (smallEtaleTopology Y) Ab.{u + 1}),
∃ s t : ℤ, s ≤ t ∧ Fil s n F = ⊤ ∧ Fil t n F = ⊥) ∧
∀ (p q : ℤ) (n : ℕ) (F : Sheaf (smallEtaleTopology Y) Ab.{u + 1}),
p + q = (n : ℤ) → ∃ r₀ : ℤ, 1 ≤ r₀ ∧
∀ (r : ℤ) (hr : 1 ≤ r), r₀ ≤ r →
((E.obj F).page r hr).d (p, q) (p + r, q + 1 - r) = 0 ∧
((E.obj F).page r hr).d (p - r, q + r - 1) (p, q) = 0 ∧
Nonempty (((E.obj F).page r hr).X (p, q) ≅
cokernel (Subobject.ofLE (Fil (p + 1) n F) (Fil p n F)
(hFil p (p + 1) n F (by omega))))
AlgebraicGeometry.mono_smallEtaleUnitAb_of_isFinite_of_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/FiniteSurjectiveAbelianUnit.lean, line 100. The attribute's comment: “exactness at ℱ of 0 → ℱ → ℱ₀ → ℱ₁ → ⋯, i.e. injectivity of the augmentation ℱ ⟶ ℱ₀ = f_*f^{-1}ℱ; exactness in the higher degrees and the spectral sequence are not proved here”.
Stacks 09Z2, exactness at
ℱ. For a finite surjective morphism of schemes the unitℱ ⟶ f_* f^{-1}ℱof the inverse-image/direct-image adjunction on abelian sheaves on the small étale sites is a monomorphism. The zeroth level of the Čech nerve offbeingXitself, this is injectivity of the augmentationℱ ⟶ ℱ₀.
public theorem mono_smallEtaleUnitAb_of_isFinite_of_surjective
[IsFinite (B.inclusion.map f)] [Surjective (B.inclusion.map f)]
(G : Sheaf (SmallEtale.topology B Y.1 Y.property) AddCommGrpCat.{u + 1}) :
Mono (((smallEtaleBaseChange B f).sheafAdjunctionContinuous AddCommGrpCat.{u + 1}
(SmallEtale.topology B Y.1 Y.property)
(SmallEtale.topology B X.1 X.property)).unit.app G)
Tag 09Z3, a remark
Tag 09Z3 in the Stacks Project.
Stacks.EtaleCohomology.globalSectionsPullback_isEqualizer_of_isFinite_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/GlobalSectionsClosed/FiniteSurjectiveDescent.lean, line 1344. The attribute's comment: “the displayed equality Γ(Y, 𝒢) = Equalizer (Γ(X₀, f₀⁻¹𝒢) ⇉ Γ(X₁, f₁⁻¹𝒢)), for a finite surjective f : X ⟶ Y and a sheaf of sets 𝒢 on the small étale site of Y, with X₀ = X, f₀ = f, X₁ = X ×_Y X and f₁ the structure morphism of X₁: the canonical comparison on global sections is injective with image exactly the equalizer”. References: SGA 1 XIII (1.11), “partial”.
[Stacks, Tag 09Z3]. Let
f : X ⟶ Ybe a finite surjective morphism of schemes and let𝒢be a sheaf of sets on the small étale site ofY. The first two levels of the Čech nerve offareX₀ = Xwithf₀ = f, andX₁ = X ×_Y Xwithf₁ = pr₀ ≫ f = pr₁ ≫ f. Then
Γ(Y, 𝒢) = Equalizer (Γ(X₀, f₀⁻¹𝒢) ⇉ Γ(X₁, f₁⁻¹𝒢)):the canonical comparison
Γ(Y, 𝒢) ⟶ Γ(X₀, f₀⁻¹𝒢)on global sections is injective, and a section off₀⁻¹𝒢overX₀is in its image exactly when its two pullbacks toX₁agree.The comparison is
Stacks.EtaleCohomology.etaleGlobalPullback, which is by definition the component at𝒢ofStacks.EtaleCohomology.globalSectionsSmallEtaleInverseImageComparison; the two parallel arrows are the two instances ofStacks.EtaleCohomology.relativeGlobalSectionsMapattached to the two factorizationsf₁ = pr₀ ≫ fandf₁ = pr₁ ≫ fof the structure morphism ofX₁.
public theorem globalSectionsPullback_isEqualizer_of_isFinite_surjective
{X Y : Scheme.{u}} (f : X ⟶ Y) [IsFinite f] [Surjective f]
(G : Sheaf (Scheme.smallEtaleTopology Y) (Type (max (u + 1) v))) :
Function.Injective (etaleGlobalPullback f G) ∧
∀ t : (etaleGlobalSections X).obj ((smallEtaleInverseImage.{u, v} f).obj G),
relativeGlobalSectionsMap f (pullback.fst f f) (pullback.fst f f ≫ f) rfl G t =
relativeGlobalSectionsMap f (pullback.snd f f) (pullback.fst f f ≫ f)
pullback.condition G t ↔
∃ s : (etaleGlobalSections Y).obj G, etaleGlobalPullback f G s = t
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.