84 More on Cohomology of Spaces

Chapter 84 of the Stacks Project, More on Cohomology of Spaces, Tag 0DFR: the 6 sections of its 8 with a tag that a declaration carries, one article each, in the Stacks Project's order. Their 33 tags are carried by 97 declarations of the repository (all in StacksFrontier) and 12 registered declarations.

Section84.3 Transporting results from schemes #

Section 84.3 of the Stacks Project, Tag 0DFU. 1 tag here is carried by 6 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0DFV, a lemma

Tag 0DFV in the Stacks Project.

AlgebraicGeometry.etaleSchemeToSpace_isSpecialCocontinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SchemeToSpaceSites.lean, line 1216. The attribute's comment: “étale case”.

Stacks 0DFV, étale case. The inclusion of schemes into algebraic spaces is special cocontinuous for the big étale sites.

public theorem etaleSchemeToSpace_isSpecialCocontinuous
    {S : Scheme.{u}} (T : AlgebraicGeometry.BigEtaleSpaceSite S)
    (h : T.schemeSite.cutoff = T.fppfSite.cutoff) :
    IsSpecialCocontinuous
      (AlgebraicGeometry.BigEtaleOver.topology T.schemeSite S T.scheme_mem)
      T.topology (etaleSchemeToSpace T h)

AlgebraicGeometry.fppfSchemeToSpace_isSpecialCocontinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SchemeToSpaceSites.lean, line 1233. The attribute's comment: “fppf case”.

Stacks 0DFV, fppf case. The Yoneda inclusion of schemes into algebraic spaces is special cocontinuous for the big fppf sites.

public theorem fppfSchemeToSpace_isSpecialCocontinuous
    {S : Scheme.{u}} (T : AlgebraicGeometry.BigFppfSpaceSite S) :
    IsSpecialCocontinuous
      (AlgebraicGeometry.BigFppfOver.topology T.schemeSite S T.scheme_mem)
      T.topology
      (AlgebraicGeometry.schemeSpaceFunctor T.schemeSite S T.scheme_mem)

AlgebraicGeometry.phSchemeToSpace_isSpecialCocontinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SchemeToSpaceSites.lean, line 1261. The attribute's comment: “ph case”.

Stacks 0DFV, ph case. The inclusion of schemes into algebraic spaces is special cocontinuous for the big ph sites.

public theorem phSchemeToSpace_isSpecialCocontinuous
    {S : Scheme.{u}} (T : AlgebraicGeometry.BigPHSpaceSite S) :
    IsSpecialCocontinuous
      (AlgebraicGeometry.BigPHOver.topology T.schemeSite S T.scheme_mem)
      T.topology T.schemeToSpace

AlgebraicGeometry.etaleSchemeToSpaceSheafEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SchemeToSpaceSites.lean, line 1277. The attribute's comment: “étale case, equivalence of topoi”.

Stacks 0DFV, étale case: the identification of topoi. The inclusion of schemes into algebraic spaces induces an equivalence between the big étale topos of the scheme site and the big étale topos of the algebraic-space site.

public noncomputable def etaleSchemeToSpaceSheafEquiv {S : Scheme.{u}}
    (T : AlgebraicGeometry.BigEtaleSpaceSite S)
    (h : T.schemeSite.cutoff = T.fppfSite.cutoff) :
    Sheaf (AlgebraicGeometry.BigEtaleOver.topology T.schemeSite S T.scheme_mem)
        (Type (u + 1)) ≌
      Sheaf T.topology (Type (u + 1))

AlgebraicGeometry.fppfSchemeToSpaceSheafEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SchemeToSpaceSites.lean, line 1291. The attribute's comment: “fppf case, equivalence of topoi”.

Stacks 0DFV, fppf case: the identification of topoi. The Yoneda inclusion of schemes into algebraic spaces induces an equivalence between the big fppf topos of the scheme site and the big fppf topos of the algebraic-space site.

public noncomputable def fppfSchemeToSpaceSheafEquiv {S : Scheme.{u}}
    (T : AlgebraicGeometry.BigFppfSpaceSite S) :
    Sheaf (AlgebraicGeometry.BigFppfOver.topology T.schemeSite S T.scheme_mem)
        (Type (u + 1)) ≌
      Sheaf T.topology (Type (u + 1))

AlgebraicGeometry.phSchemeToSpaceSheafEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SchemeToSpaceSites.lean, line 1305. The attribute's comment: “ph case, equivalence of topoi”.

Stacks 0DFV, ph case: the identification of topoi. The inclusion of schemes into algebraic spaces induces an equivalence between the big ph topos of the scheme site and the big ph topos of the algebraic-space site.

public noncomputable def phSchemeToSpaceSheafEquiv {S : Scheme.{u}}
    (T : AlgebraicGeometry.BigPHSpaceSite S) :
    Sheaf (AlgebraicGeometry.BigPHOver.topology T.schemeSite S T.scheme_mem)
        (Type (u + 1)) ≌
      Sheaf T.topology (Type (u + 1))

Sources

LeanAlgebraicGeometry.etaleSchemeToSpace_isSpecialCocontinuous · AlgebraicGeometry.fppfSchemeToSpace_isSpecialCocontinuous · AlgebraicGeometry.phSchemeToSpace_isSpecialCocontinuous · AlgebraicGeometry.etaleSchemeToSpaceSheafEquiv · AlgebraicGeometry.fppfSchemeToSpaceSheafEquiv · AlgebraicGeometry.phSchemeToSpaceSheafEquiv

Section84.4 Proper base change #

Section 84.4 of the Stacks Project, Tag 0DFW. 9 tags here are carried by 10 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0DFX, a lemma

Tag 0DFX in the Stacks Project.

AlgebraicGeometry.Space.unit_comp_smallToposDescentMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SmallEtaleDescentFork.lean, line 92. The attribute's comment: “the unit equalizes the two restrictions”.

Stacks 0DFX. The unit of f followed by the restriction along p is the unit of p ≫ f.

Applied to the two projections p₁, p₂ : Y ×_X Y ⟶ Y of a self-intersection, where p₁ ≫ f = p₂ ≫ f, this says that the unit equalizes the two restrictions to Y ×_X Y.

theorem unit_comp_smallToposDescentMap {P Y X : AlgebraicSpaces B S hS}
    (p : P ⟶ Y) (f : Y ⟶ X)
    (F : Sheaf (SmallEtale.topology B S hS X.1) (Type (u + 1))) :
    (smallToposMorphism B S hS f).adj.unit.app F ≫ smallToposDescentMap B S hS p f F =
      (smallToposMorphism B S hS (p ≫ f)).adj.unit.app F

AlgebraicGeometry.Space.unit_equalizes, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SmallEtaleDescentUnit.lean, line 135. The attribute's comment: “the unit equalizes the two restrictions”.

Stacks 0DFX. The fork of Stacks 0DFX commutes: the adjunction unit F ⟶ f_* f⁻¹ F has equal composites with the two restriction maps f_* f⁻¹ F ⟶ g_* g⁻¹ F coming from the two projections of Y ×_X Y, where g is its structure morphism to X. Neither surjectivity nor properness of f is needed for this.

theorem unit_equalizes {Y X : AlgebraicSpaces B S hS} (f : Y ⟶ X)
    (F : Sheaf (SmallEtale.topology B S hS X.1) (Type (u + 1))) :
    let P := AlgebraicSpaces.fiberProduct B S hS f f
    let p₁ : P ⟶ Y := ObjectProperty.homMk (pullback.fst f.hom f.hom)
    let p₂ : P ⟶ Y := ObjectProperty.homMk (pullback.snd f.hom f.hom)
    let g : P ⟶ X := p₁ ≫ f
    (smallToposMorphism B S hS f).adj.unit.app F ≫
        descentMapOver B S hS p₁ f g rfl F =
      (smallToposMorphism B S hS f).adj.unit.app F ≫
        descentMapOver B S hS p₂ f g
          (AlgebraicSpaces.isPullback_fiberProduct B S hS f f).w.symm F

AlgebraicGeometry.Space.nonempty_isLimit_unitFork_of_isProper_isSurjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SpacesEtaleProperSurjectiveEqualizer.lean, line 70.

Stacks 0DFX. Let f : Y ⟶ X be a surjective proper morphism of algebraic spaces over S, let F be a sheaf on X_étale (the spaces-étale site of X, Stacks 03G1), and let g : Y ×_X Y ⟶ X be the structure morphism. Then F ⟶ f_* f⁻¹ F is injective with image the equalizer of the two maps f_* f⁻¹ F ⇉ g_* g⁻¹ F induced by the two projections Y ×_X Y ⟶ Y: the fork formed by the unit of f⁻¹ ⊣ f_* and these two maps is a limit.

theorem nonempty_isLimit_unitFork_of_isProper_isSurjective {X Y : AlgebraicSpaces B S hS}
    (f : Y ⟶ X) (hs : IsSurjective B S hS f.hom) (hp : IsProper B S hS f.hom)
    (F : Sheaf (SpacesEtale.topology B S hS X) (Type (u + 1))) :
    Nonempty (IsLimit (Fork.ofι ((spacesEtalePseudofunctorAdjunction B S hS f).unit.app F)
      ((Pseudofunctor.unit_comp_unitForkRestriction _ f (spacesChosenPullback B S hS f f)
          (spacesEtalePseudofunctorAdjunction B S hS f)
          (spacesEtalePseudofunctorAdjunction B S hS (spacesChosenPullback B S hS f f).p)
          (spacesChosenPullback B S hS f f).p₁ (spacesChosenPullback B S hS f f).hp₁ F).trans
        (Pseudofunctor.unit_comp_unitForkRestriction _ f (spacesChosenPullback B S hS f f)
          (spacesEtalePseudofunctorAdjunction B S hS f)
          (spacesEtalePseudofunctorAdjunction B S hS (spacesChosenPullback B S hS f f).p)
          (spacesChosenPullback B S hS f f).p₂ (spacesChosenPullback B S hS f f).hp₂ F).symm) :
      Fork (Pseudofunctor.unitForkRestriction _ f (spacesChosenPullback B S hS f f)
          (spacesEtalePseudofunctorAdjunction B S hS f)
          (spacesEtalePseudofunctorAdjunction B S hS (spacesChosenPullback B S hS f f).p)
          (spacesChosenPullback B S hS f f).p₁ (spacesChosenPullback B S hS f f).hp₁ F)
        (Pseudofunctor.unitForkRestriction _ f (spacesChosenPullback B S hS f f)
          (spacesEtalePseudofunctorAdjunction B S hS f)
          (spacesEtalePseudofunctorAdjunction B S hS (spacesChosenPullback B S hS f f).p)
          (spacesChosenPullback B S hS f f).p₂ (spacesChosenPullback B S hS f f).hp₂ F)))

Tag 0DFY, a lemma

Tag 0DFY in the Stacks Project.

AlgebraicGeometry.Space.isIso_globalSectionsRestriction_closedFibre_of_henselianPair, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/ProperHenselianPairSections.lean, line 162.

[Stacks, Tag 0DFY]. Let (A, I) be a henselian pair, let X be an algebraic space over A whose structure morphism f : X ⟶ Spec A is proper, and let i : X₀ ⟶ X be the inclusion of X₀ = X ×_{Spec A} Spec (A ⧸ I). For every sheaf of sets ℱ on X_étale, Γ(X, ℱ) = Γ(X₀, i⁻¹ ℱ): restriction of global sections along i, natural in ℱ, is an isomorphism.

theorem isIso_globalSectionsRestriction_closedFibre_of_henselianPair (hI : HenselianPair A I)
    (hf : IsProper B (Spec (.of A)) hA f.hom) :
    IsIso (globalSectionsRestriction B (Spec (.of A)) hA (closedFibreInclusion A I hA X f))

Tag 0DFZ, a lemma

Tag 0DFZ in the Stacks Project.

AlgebraicGeometry.Space.isIso_globalSectionsRestriction_closedFibre_of_henselianLocalRing, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/ProperHenselianLocalSections.lean, line 51. References: SGA 4 XII (5.5), “more general”.

[Stacks, Tag 0DFZ]. Let A be a henselian local ring, let X be an algebraic space over A whose structure morphism f : X ⟶ Spec A is proper, and let i : X₀ ⟶ X be the inclusion of the fibre X₀ = X ×_{Spec A} Spec (A ⧸ 𝔪) of f over the closed point (A ⧸ 𝔪 is the residue field of A). For every sheaf of sets ℱ on X_étale, Γ(X, ℱ) = Γ(X₀, ℱ|_{X₀}): restriction of global sections along i, natural in ℱ, is an isomorphism.

theorem isIso_globalSectionsRestriction_closedFibre_of_henselianLocalRing
    (hf : IsProper B (Spec (.of A)) hA f.hom) :
    IsIso (globalSectionsRestriction B (Spec (.of A)) hA
      (closedFibreInclusion A (maximalIdeal A) hA X f))

Tag 0DG0, a lemma

Tag 0DG0 in the Stacks Project.

AlgebraicGeometry.Space.isIso_properBaseChangeMap_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/ProperBaseChangeSmallEtale.lean, line 244.

Let S be a scheme, let f : X ⟶ Y and g : Y' ⟶ Y be morphisms of algebraic spaces over S with f proper, and let
X' --g'--> X
|f'        |f
v          v
Y' --g---> Y
be cartesian, that is X' = Y' ×_Y X with projections f' and g'. Then for every sheaf of sets ℱ on X_étale the canonical map g⁻¹ f_* ℱ ⟶ f'_* (g')⁻¹ ℱ is an isomorphism, naturally in ℱ: the base-change map AlgebraicGeometry.Space.properBaseChangeMap of the small étale topoi is invertible.

theorem isIso_properBaseChangeMap_of_isProper (f : X ⟶ Y) (hf : IsProper B S hS f.hom)
    (g : Y' ⟶ Y) (f' : X' ⟶ Y') (g' : X' ⟶ X) (sq : IsPullback g' f' f g) :
    IsIso (properBaseChangeMap B S hS f g f' g' sq)

Tag 0DG1, a lemma

Tag 0DG1 in the Stacks Project.

AlgebraicGeometry.Space.bijective_geometricFibreSectionsMap_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/ProperGeometricFibreSections.lean, line 117.

[Stacks, Tag 0DG1]. Let S be a scheme, let f : Y ⟶ X be a proper morphism of algebraic spaces over S and let x̄ be a geometric point of X, with geometric fibre Y_x̄ = Y ×_{X, x̄} Spec(k) and projection p : Y_x̄ ⟶ Y. For every sheaf of sets ℱ on Y_étale the canonical map (f_* ℱ)_x̄ ⟶ Γ(Y_x̄, ℱ_x̄), ℱ_x̄ = p⁻¹ ℱ, is bijective.

The proof is the source's: the base-change map of the geometric fibre square is invertible by proper base change, Stacks 0DG0 (AlgebraicGeometry.Space.isIso_properBaseChangeMap_of_isProper).

theorem bijective_geometricFibreSectionsMap_of_isProper (f : Y ⟶ X)
    (hf : IsProper B S hS f.hom) (x : GeometricPoint B S hS X.obj)
    (ℱ : Sheaf (SmallEtale.topology B S hS Y.obj) (Type (u + 1))) :
    Function.Bijective ((geometricFibreSectionsMap B S hS f x).app ℱ)

Tag 0DG2, a theorem

Tag 0DG2 in the Stacks Project.

Declarations registered for the tag:

AlgebraicGeometry.BigEtaleSpaceSite.isIso_spacesEtaleDerivedBaseChange_app_singleFunctor_of_isProper, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SpacesEtaleProperBaseChange.lean, line 15 (StacksFrontier): “proper base change for algebraic spaces: g⁻¹ R f_ F ≅ R f'_ (g')⁻¹ F for f proper and F an abelian torsion sheaf”.

Tag 0DG3, a lemma

Tag 0DG3 in the Stacks Project.

Declarations registered for the tag:

AlgebraicGeometry.BigEtaleSpaceSite.isIso_spacesEtaleDerivedBaseChange_app_of_isProper, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SpacesEtaleProperBaseChangeBoundedBelow.lean, line 15 (StacksFrontier): “proper base change for algebraic spaces: g⁻¹ R f_ E ≅ R f'_ (g')⁻¹ E for f proper and E bounded below with torsion cohomology sheaves”.

Tag 0DG4, a lemma

Tag 0DG4 in the Stacks Project.

AlgebraicGeometry.BigEtaleSpaceSite.abelianSheafFiberHomologyDerivedPushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/GeometricPointStalkProperBaseChange.lean, line 62. The attribute's comment: “(2)”. References: SGA 4 XVI (2.1), “more general”; SGA 4 XVI (2.2), “more general”.

Let f : Y ⟶ X be a proper morphism of algebraic spaces over a scheme S and x̄ : Spec Ω ⟶ X a geometric point, with geometric fibre Y_x̄ = Y ×_X Spec Ω and projection g' : Y_x̄ ⟶ Y. For an object E of D⁺(Y_étale) with torsion cohomology sheaves, (Hⁿ(Rf_* E))_x̄ ≅ Hⁿ(RΓ(Y_x̄, E_x̄)) for every n, where E_x̄ = (g')⁻¹ E.

def abelianSheafFiberHomologyDerivedPushforwardIso
    (hf : Space.IsProper T.fppfSite S T.fppf_mem f.hom)
    (E : DerivedCategory (Sheaf (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem Y)
      Ab.{u + 1})) (m : ℤ) (hE : E.IsGE m) (hT : HasTorsionCohomology T E) (n : ℤ) :
    ((spacesEtaleSitePoint x).sheafFiber (A := Ab.{u + 1})).obj
      ((DerivedCategory.homologyFunctor
        (Sheaf (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem X) Ab.{u + 1}) n).obj
          ((totalRightDerived (smallEtalePushforward T f)).obj E)) ≅
    (DerivedCategory.homologyFunctor Ab.{u + 1} n).obj
      ((totalRightDerived (Sheaf.Γ (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem
          (pullback f (geometricPointHom x))) Ab.{u + 1})).obj
        ((CategoryTheory.Sites.abelianInverseImage
          (smallEtaleMorphism T (pullback.fst f (geometricPointHom x)))).mapDerivedCategory.obj
            E))

AlgebraicGeometry.BigEtaleSpaceSite.abelianSheafFiberRightDerivedPushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/GeometricPointStalkProperBaseChange.lean, line 90. The attribute's comment: “(1)”. References: SGA 4 XII (5.2), “more general”; SGA 4 XVI (2.1), “more general”; SGA 4 XVI (2.2), “more general”; SGA 4½ Arcata (4.1.1), “more general”.

Let f : Y ⟶ X be a proper morphism of algebraic spaces over a scheme S and x̄ : Spec Ω ⟶ X a geometric point, with geometric fibre Y_x̄ = Y ×_X Spec Ω and projection g' : Y_x̄ ⟶ Y. For a torsion abelian sheaf F on Y_étale, (Rⁿf_* F)_x̄ ≅ Hⁿ_étale(Y_x̄, F_x̄) for every n, where F_x̄ = (g')⁻¹ F.

def abelianSheafFiberRightDerivedPushforwardIso
    (hf : Space.IsProper T.fppfSite S T.fppf_mem f.hom)
    (F : Sheaf (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem Y) Ab.{u + 1})
    (hF : Stacks.Torsion.torsionSheafProperty
      (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem Y) F) (n : ℕ) :
    ((spacesEtaleSitePoint x).sheafFiber (A := Ab.{u + 1})).obj
      (((smallEtalePushforward T f).rightDerived n).obj F) ≅
    AddCommGrpCat.of (Sheaf.H.{u + 1} ((CategoryTheory.Sites.abelianInverseImage
      (smallEtaleMorphism T (pullback.fst f (geometricPointHom x)))).obj F) n)

Tag 0DG5, a lemma

Tag 0DG5 in the Stacks Project.

AlgebraicGeometry.BigEtaleSpaceSite.spacesEtaleCohomologyRestrictionMap_bijective_of_isSepClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SpacesSeparablyClosedFieldExtension.lean, line 126. References: SGA 4 XII (5.4), “more general”; SGA 4 XVI (1.6), “Abelian clause”.

Étale cohomology of a proper algebraic space does not change under an extension of separably closed ground fields. Let K/k be an extension of separably closed fields and p : X ⟶ Spec k a proper morphism of algebraic spaces; write X_K = X ×_{Spec k} Spec K with projection g' : X_K ⟶ X. Then for every torsion abelian sheaf F on X_étale and every q ≥ 0 the restriction map H^q_étale(X, F) ⟶ H^q_étale(X_K, F|_{X_K}) is bijective.

The base change map g⁻¹ R p_* E ⟶ R p_{K,*} (g')⁻¹ E is invertible at every bounded below E with torsion cohomology sheaves by Stacks 0DG3 (isIso_spacesEtaleDerivedBaseChange_app_of_isProper_of_representable, with Stacks 0A3U and Stacks 095T for schemes supplied).

theorem spacesEtaleCohomologyRestrictionMap_bijective_of_isSepClosed {X : T.Spaces}
    (p : X ⟶ yonedaSpace T.fppfSite S T.fppf_mem (BigFppfOver.mk T.fppfSite S T.fppf_mem hk s))
    (hp : Space.IsProper T.fppfSite S T.fppf_mem p.hom)
    [HasExt.{w} (Sheaf (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem X) Ab.{u + 1})]
    [HasExt.{w} (Sheaf (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem
      (pullback p (fieldExtensionSpaceHom T k K hk hK s))) Ab.{u + 1})]
    (F : Sheaf (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem X) Ab.{u + 1})
    (hF : Stacks.Torsion.torsionSheafProperty
      (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem X) F) (q : ℕ) :
    Function.Bijective (spacesEtaleCohomologyRestrictionMap.{u, w} T
      (pullback.fst p (fieldExtensionSpaceHom T k K hk hK s)) F q)

Sources

LeanAlgebraicGeometry.Space.unit_comp_smallToposDescentMap · AlgebraicGeometry.Space.unit_equalizes · AlgebraicGeometry.Space.nonempty_isLimit_unitFork_of_isProper_isSurjective · AlgebraicGeometry.Space.isIso_globalSectionsRestriction_closedFibre_of_henselianPair · AlgebraicGeometry.Space.isIso_globalSectionsRestriction_closedFibre_of_henselianLocalRing · AlgebraicGeometry.Space.isIso_properBaseChangeMap_of_isProper · AlgebraicGeometry.Space.bijective_geometricFibreSectionsMap_of_isProper · AlgebraicGeometry.BigEtaleSpaceSite.isIso_spacesEtaleDerivedBaseChange_app_singleFunctor_of_isProper

Section84.5 Comparing big and small topoi #

Section 84.5 of the Stacks Project, Tag 0DG6. 7 tags here are carried by 39 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0DG7, a lemma

Tag 0DG7 in the Stacks Project.

AlgebraicGeometry.BigEtaleSpaceSite.bigToSmall_inverseImageFactorizationIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigToSmallEtalePullback.lean, line 52. The attribute's comment: “transitivity of inverse image”.

Transitivity of inverse image for f_small = π_X ∘ i_f: the adjunction mate of the direct-image factorization of Tag 0DF6, part (4).

noncomputable def bigToSmall_inverseImageFactorizationIso :
    (bigToSmallEtaleMorphism T X).inverseImage ⋙ (smallToBigEtaleMorphism T f).inverseImage ≅
      (smallEtaleMorphism T f).inverseImage

AlgebraicGeometry.BigEtaleSpaceSite.bigToSmall_inverseImageFactorizationIso_hom_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigToSmallEtalePullback.lean, line 64. The attribute's comment: “the components of the transitivity isomorphism”.

The transitivity isomorphism is determined by the adjunction unit of f_small and the direct-image factorization of Tag 0DF6: it is the morphism whose adjoint transpose is the unit followed by that factorization.

theorem bigToSmall_inverseImageFactorizationIso_hom_app
    (F : Sheaf (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem X) (Type (u + 1))) :
    (bigToSmall_inverseImageFactorizationIso T f).hom.app F =
      (((bigToSmallEtaleMorphism T X).comp
        (smallToBigEtaleMorphism T f)).adj.homEquiv _ _).symm
        ((smallEtaleMorphism T f).adj.unit.app F ≫
          (smallEtale_pushforwardIsoDirectFactorization T f).hom.app
            ((smallEtaleMorphism T f).inverseImage.obj F))

AlgebraicGeometry.BigEtaleSpaceSite.smallToBig_inverseImageSectionsIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigToSmallEtalePullback.lean, line 84. The attribute's comment: “global sections after restriction are evaluation at f”.

Taking global sections on the spaces-étale site of Y after restriction along i_f is evaluation at the object f : Y ⟶ X of the big étale site of X.

noncomputable def smallToBig_inverseImageSectionsIso :
    (smallToBigEtaleMorphism T f).inverseImage ⋙
        Sheaf.Γ (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem Y) (Type (u + 1)) ≅
      (sheafSections (T.bigEtaleTopology X) (Type (u + 1))).obj (op (Over.mk f))

AlgebraicGeometry.BigEtaleSpaceSite.bigToSmall_inverseImageSectionsIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigToSmallEtalePullback.lean, line 132. The attribute's comment: “the section rule for the pullback”.

The sections of the inverse image π_X⁻¹F of a sheaf on the spaces-étale site of X over the object f : Y ⟶ X of the big étale site of X are the global sections of the small-site pullback f_small⁻¹F on the spaces-étale site of Y, naturally in F.

noncomputable def bigToSmall_inverseImageSectionsIso :
    (bigToSmallEtaleMorphism T X).inverseImage ⋙
        (sheafSections (T.bigEtaleTopology X) (Type (u + 1))).obj (op (Over.mk f)) ≅
      (smallEtaleMorphism T f).inverseImage ⋙
        Sheaf.Γ (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem Y) (Type (u + 1))

AlgebraicGeometry.BigEtaleSpaceSite.bigToSmall_inverseImageSectionsIso_hom_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigToSmallEtalePullback.lean, line 146. The attribute's comment: “the components of the section rule”.

The section rule is the global-sections image of the transitivity isomorphism, after identifying evaluation at f with global sections of the restriction along i_f.

theorem bigToSmall_inverseImageSectionsIso_hom_app
    (F : Sheaf (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem X) (Type (u + 1))) :
    (bigToSmall_inverseImageSectionsIso T f).hom.app F =
      (smallToBig_inverseImageSectionsIso T f).inv.app
          ((bigToSmallEtaleMorphism T X).inverseImage.obj F) ≫
        (Sheaf.Γ (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem Y)
          (Type (u + 1))).map ((bigToSmall_inverseImageFactorizationIso T f).hom.app F)

AlgebraicGeometry.BigEtaleSpaceSite.inverseImage_isSheafFor_smooth_syntomic_fppf_fpqc, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigToSmallEtaleSheafConditions.lean, line 73. The attribute's comment: “Moreover: the sheaf condition for smooth, syntomic, fppf and fpqc coverings”.

Stacks 0DG7, the sheaf conditions for smooth, syntomic, fppf and fpqc coverings. Let F be a sheaf on the spaces-étale site of X. Then π_X⁻¹F satisfies the sheaf condition for every family of the slice over X whose underlying family of algebraic spaces is a smooth, syntomic, fppf or fpqc covering.

theorem inverseImage_isSheafFor_smooth_syntomic_fppf_fpqc :
    (∀ (U : Over X) (E : PreZeroHypercover.{v} U),
      Space.IsSmoothCovering T.fppfSite S T.fppf_mem
        (fun i ↦ ((E.map (Over.forget X)).X i).obj) (fun i ↦ ((E.map (Over.forget X)).f i).hom) →
      Presieve.IsSheafFor ((bigToSmallEtaleMorphism T X).inverseImage.obj F).obj E.presieve₀) ∧
    (∀ (U : Over X) (E : PreZeroHypercover.{v} U),
      Space.IsSyntomicCovering T.fppfSite S T.fppf_mem
        (fun i ↦ ((E.map (Over.forget X)).X i).obj) (fun i ↦ ((E.map (Over.forget X)).f i).hom) →
      Presieve.IsSheafFor ((bigToSmallEtaleMorphism T X).inverseImage.obj F).obj E.presieve₀) ∧
    (∀ (U : Over X) (E : PreZeroHypercover.{v} U),
      Space.IsFppfCovering T.fppfSite S T.fppf_mem
        (fun i ↦ ((E.map (Over.forget X)).X i).obj) (fun i ↦ ((E.map (Over.forget X)).f i).hom) →
      Presieve.IsSheafFor ((bigToSmallEtaleMorphism T X).inverseImage.obj F).obj E.presieve₀) ∧
    (∀ (U : Over X) (E : PreZeroHypercover.{v} U),
      Space.IsFpqcCovering T.fppfSite S T.fppf_mem (fun i ↦ ((E.map (Over.forget X)).f i).hom) →
      Presieve.IsSheafFor ((bigToSmallEtaleMorphism T X).inverseImage.obj F).obj E.presieve₀)

Declarations registered for the tag:

AlgebraicGeometry.BigPHSpaceSite.isSheaf_bigToSmallEtale_inverseImage, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigToSmallEtaleSheafConditions.lean, line 104 (StacksFrontier): “Moreover: the sheaf condition for ph coverings”.

Tag 0DG8, a lemma

Tag 0DG8 in the Stacks Project.

AlgebraicGeometry.BigEtaleSpaceSite.injective_smallEtaleRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigSmallEtaleRestriction.lean, line 176. The attribute's comment: “part (1), injectives restrict along i_f”.

Stacks 0DG8, part (1). The inverse image along i_f of an injective abelian sheaf on the big étale site of X is an injective abelian sheaf on the spaces-étale site of Y.

theorem injective_smallEtaleRestriction {X Y : T.Spaces} (f : Y ⟶ X)
    (I : Sheaf (T.bigEtaleTopology X) Ab.{u + 1}) [Injective I] :
    Injective ((smallEtaleRestriction T f).obj I)

AlgebraicGeometry.BigEtaleSpaceSite.injective_bigToSmallEtaleRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigSmallEtaleRestriction.lean, line 195. The attribute's comment: “part (1), injectives restrict to the small site”.

Stacks 0DG8, part (1). The restriction to the spaces-étale site of X of an injective abelian sheaf on the big étale site of X is injective.

theorem injective_bigToSmallEtaleRestriction (X : T.Spaces)
    (I : Sheaf (T.bigEtaleTopology X) Ab.{u + 1}) [Injective I] :
    Injective ((bigToSmallEtaleRestriction T X).obj I)

AlgebraicGeometry.BigEtaleSpaceSite.isKInjective_smallEtaleRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigSmallEtaleRestriction.lean, line 215. The attribute's comment: “part (2), K-injectivity restricts along i_f”.

Stacks 0DG8, part (2). The inverse image along i_f of a K-injective complex of abelian sheaves on the big étale site of X is a K-injective complex on the spaces-étale site of Y.

theorem isKInjective_smallEtaleRestriction {X Y : T.Spaces} (f : Y ⟶ X)
    (I : CochainComplex (Sheaf (T.bigEtaleTopology X) Ab.{u + 1}) ℤ) [I.IsKInjective] :
    CochainComplex.IsKInjective
      (((smallEtaleRestriction T f).mapHomologicalComplex (ComplexShape.up ℤ)).obj I)

AlgebraicGeometry.BigEtaleSpaceSite.isKInjective_bigToSmallEtaleRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigSmallEtaleRestriction.lean, line 233. The attribute's comment: “part (2), K-injectivity restricts to the small site”.

Stacks 0DG8, part (2). The restriction to the spaces-étale site of X of a K-injective complex of abelian sheaves on the big étale site of X is K-injective.

theorem isKInjective_bigToSmallEtaleRestriction (X : T.Spaces)
    (I : CochainComplex (Sheaf (T.bigEtaleTopology X) Ab.{u + 1}) ℤ) [I.IsKInjective] :
    ((bigToSmallEtaleRestrictionComplex T X).obj I).IsKInjective

AlgebraicGeometry.BigEtaleSpaceSite.injective_spacesEtaleRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigToSmallEtaleKInjective.lean, line 103. The attribute's comment: “injective_restriction”.

Stacks Project, Tag 0DG8, part (1)(b). Restriction of an injective abelian sheaf from the big étale site of X to the spaces-étale site of X is injective.

theorem injective_spacesEtaleRestriction (X : T.Spaces)
    (I : Sheaf (T.bigEtaleTopology X) Ab.{u + 1}) [Injective I] :
    Injective
      (((Space.SpacesEtale.inclusion T.fppfSite S T.fppf_mem X).sheafPushforwardContinuous
        Ab.{u + 1} (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem X)
        (T.bigEtaleTopology X)).obj I)

AlgebraicGeometry.BigEtaleSpaceSite.injective_spacesEtaleRestrictionAlong, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigToSmallEtaleKInjective.lean, line 126. The attribute's comment: “injective_pullback”.

Stacks Project, Tag 0DG8, part (1)(a). Restriction of an injective abelian sheaf from the big étale site of X to the spaces-étale site of Y along a morphism f : Y ⟶ X — the inverse image of i_f — is injective.

theorem injective_spacesEtaleRestrictionAlong {X Y : T.Spaces} (f : Y ⟶ X)
    (I : Sheaf (T.bigEtaleTopology X) Ab.{u + 1}) [Injective I] :
    Injective
      (((inclusionFunctor T f).sheafPushforwardContinuous Ab.{u + 1}
        (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem Y)
        (T.bigEtaleTopology X)).obj I)

AlgebraicGeometry.BigEtaleSpaceSite.isKInjective_spacesEtaleRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigToSmallEtaleKInjective.lean, line 149. The attribute's comment: “kinjective_restriction”.

Stacks Project, Tag 0DG8, part (2)(b). Restriction of a K-injective complex of abelian sheaves from the big étale site of X to the spaces-étale site of X is K-injective.

theorem isKInjective_spacesEtaleRestriction (X : T.Spaces)
    (I : CochainComplex (Sheaf (T.bigEtaleTopology X) Ab.{u + 1}) ℤ)
    (hI : I.IsKInjective) :
    CochainComplex.IsKInjective
      ((((Space.SpacesEtale.inclusion T.fppfSite S T.fppf_mem X).sheafPushforwardContinuous
        Ab.{u + 1} (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem X)
        (T.bigEtaleTopology X)).mapHomologicalComplex (ComplexShape.up ℤ)).obj I)

AlgebraicGeometry.BigEtaleSpaceSite.isKInjective_spacesEtaleRestrictionAlong, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigToSmallEtaleKInjective.lean, line 177. The attribute's comment: “kinjective_pullback”.

Stacks Project, Tag 0DG8, part (2)(a). Restriction of a K-injective complex of abelian sheaves from the big étale site of X to the spaces-étale site of Y along a morphism f : Y ⟶ X — the inverse image of i_f — is K-injective.

theorem isKInjective_spacesEtaleRestrictionAlong {X Y : T.Spaces} (f : Y ⟶ X)
    (I : CochainComplex (Sheaf (T.bigEtaleTopology X) Ab.{u + 1}) ℤ)
    (hI : I.IsKInjective) :
    CochainComplex.IsKInjective
      ((((inclusionFunctor T f).sheafPushforwardContinuous Ab.{u + 1}
        (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem Y)
        (T.bigEtaleTopology X)).mapHomologicalComplex (ComplexShape.up ℤ)).obj I)

Tag 0DG9, an equation

Tag 0DG9 in the Stacks Project.

AlgebraicGeometry.BigEtaleSpaceSite.bigSmallEtale_restrictPushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigSmallEtalePushforwardModules.lean, line 255. The attribute's comment: “the comparison for sheaves of sets”.

Stacks 0DG9. The restriction to the spaces-étale site of X of the big étale direct image along f is the small étale direct image along f of the restriction to the spaces-étale site of Y.

def bigSmallEtale_restrictPushforwardIso (f : Y ⟶ X) :
    (bigEtaleMorphism T f).pushforward ⋙ (bigToSmallEtaleMorphism T X).pushforward ≅
      (bigToSmallEtaleMorphism T Y).pushforward ⋙ (smallEtaleMorphism T f).pushforward

AlgebraicGeometry.BigEtaleSpaceSite.bigSmallEtale_restrictPushforwardModulesIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigSmallEtalePushforwardModules.lean, line 263. The attribute's comment: “the comparison for sheaves of modules”.

Stacks 0DG9. For a sheaf of 𝒪-modules the comparison of the previous isomorphism is an isomorphism of 𝒪_X-modules on the spaces-étale site of X.

def bigSmallEtale_restrictPushforwardModulesIso (f : Y ⟶ X) :
    bigEtaleModulePushforward.{u, m} T f ⋙ restrictModules.{u, m} T X ≅
      restrictModules.{u, m} T Y ⋙ smallEtaleModulePushforward.{u, m} T f

AlgebraicGeometry.BigEtaleSpaceSite.bigSmallEtale_restrictPushforwardModulesIso_hom_app_val_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigSmallEtalePushforwardModules.lean, line 275. The attribute's comment: “the comparison for sheaves of modules, on sections”.

Stacks 0DG9. On sections over an algebraic space étale over X, the comparison of sheaves of modules is restriction along the comparison isomorphism of the two cartesian squares of Tag 0DF6.

theorem bigSmallEtale_restrictPushforwardModulesIso_hom_app_val_app (f : Y ⟶ X)
    (M : BigEtaleModules.{u, m} T Y)
    (U : (Space.SpacesEtale T.fppfSite S T.fppf_mem X)ᵒᵖ) (x) :
    ((bigSmallEtale_restrictPushforwardModulesIso.{u, m} T f).hom.app M).val.app U x =
      M.val.map ((smallBaseChange_comp_inclusionIso T f).hom.app U.unop).op x

Tag 0DGA, a lemma

Tag 0DGA in the Stacks Project.

AlgebraicGeometry.BigEtaleSpaceSite.derivedBigEtaleBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigSmallEtaleDerivedBaseChange.lean, line 118. The attribute's comment: “big_base_change_abelian”.

For a cartesian square of algebraic spaces of the big étale site, the inverse image along g_big of the derived big étale direct image along f agrees naturally with the derived big étale direct image along f' of the inverse image along g'_big.

def derivedBigEtaleBaseChangeIso {X Y X' Y' : T.Spaces} (f : Y ⟶ X) (g : X' ⟶ X)
    (g' : Y' ⟶ Y) (f' : Y' ⟶ X') (h : IsPullback g' f' f g) :
    ((bigEtalePushforward T f).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
          DerivedCategory.Qh).totalRightDerived DerivedCategory.Qh
            (HomotopyCategory.quasiIso
              (Sheaf (T.bigEtaleTopology Y) Ab.{u + 1}) (ComplexShape.up ℤ)) ⋙
        (bigEtalePullback T g).mapDerivedCategory ≅
      (bigEtalePullback T g').mapDerivedCategory ⋙
        ((bigEtalePushforward T f').mapHomotopyCategory (ComplexShape.up ℤ) ⋙
          DerivedCategory.Qh).totalRightDerived DerivedCategory.Qh
            (HomotopyCategory.quasiIso
              (Sheaf (T.bigEtaleTopology Y') Ab.{u + 1}) (ComplexShape.up ℤ))

AlgebraicGeometry.BigEtaleSpaceSite.derivedSmallEtaleBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigSmallEtaleDerivedBaseChange.lean, line 159. The attribute's comment: “small_base_change_abelian”.

For a cartesian square of algebraic spaces of the big étale site, the restriction to the spaces-étale site of X' of the derived big étale direct image along f agrees naturally with the derived small étale direct image along f' of the restriction to the spaces-étale site of Y'. Both restrictions are the inverse image i_g^{-1} resp. i_{g'}^{-1} of Tag 0DF2, written as the inverse image along g_big resp. g'_big followed by restriction to the spaces-étale site.

def derivedSmallEtaleBaseChangeIso {X Y X' Y' : T.Spaces} (f : Y ⟶ X) (g : X' ⟶ X)
    (g' : Y' ⟶ Y) (f' : Y' ⟶ X') (h : IsPullback g' f' f g) :
    ((bigEtalePushforward T f).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
          DerivedCategory.Qh).totalRightDerived DerivedCategory.Qh
            (HomotopyCategory.quasiIso
              (Sheaf (T.bigEtaleTopology Y) Ab.{u + 1}) (ComplexShape.up ℤ)) ⋙
        (bigEtalePullback T g).mapDerivedCategory ⋙
          (spacesEtaleRestrictionAb T X').mapDerivedCategory ≅
      (bigEtalePullback T g').mapDerivedCategory ⋙
        (spacesEtaleRestrictionAb T Y').mapDerivedCategory ⋙
          ((smallEtalePushforward T f').mapHomotopyCategory (ComplexShape.up ℤ) ⋙
            DerivedCategory.Qh).totalRightDerived DerivedCategory.Qh
              (HomotopyCategory.quasiIso
                (Sheaf (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem Y')
                  Ab.{u + 1}) (ComplexShape.up ℤ))

AlgebraicGeometry.BigEtaleSpaceSite.derivedBigEtaleModuleBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigSmallEtaleDerivedBaseChange.lean, line 262. The attribute's comment: “big_base_change_modules”.

For a cartesian square of algebraic spaces of the big étale site, the inverse image of sheaves of 𝒪-modules along g_big of the derived big étale direct image along f agrees naturally with the derived big étale direct image along f' of the inverse image along g'_big.

def derivedBigEtaleModuleBaseChangeIso {X Y X' Y' : T.Spaces} (f : Y ⟶ X) (g : X' ⟶ X)
    (g' : Y' ⟶ Y) (f' : Y' ⟶ X') (h : IsPullback g' f' f g) :
    (homotopyToDerived (bigEtaleRelocalizationPushforward T f)).totalRightDerived
          DerivedCategory.Qh
          (HomotopyCategory.quasiIso
            (SheafOfModules.{u + 1} ((globalRingSheaf T).over Y)) (ComplexShape.up ℤ)) ⋙
        (bigEtaleModulePullback T g).mapDerivedCategory ≅
      (bigEtaleModulePullback T g').mapDerivedCategory ⋙
        (homotopyToDerived (bigEtaleRelocalizationPushforward T f')).totalRightDerived
          DerivedCategory.Qh
          (HomotopyCategory.quasiIso
            (SheafOfModules.{u + 1} ((globalRingSheaf T).over Y')) (ComplexShape.up ℤ))

AlgebraicGeometry.BigEtaleSpaceSite.derivedSmallEtaleModuleBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigSmallEtaleDerivedBaseChange.lean, line 604. The attribute's comment: “small_base_change_modules”.

For a cartesian square of algebraic spaces of the big étale site, the restriction to the spaces-étale site of X' of the derived big étale direct image of sheaves of 𝒪-modules along f agrees naturally with the derived small étale direct image along f' of the restriction to the spaces-étale site of Y'. The two restrictions are the inverse images i_g^* and i_{g'}^* of Tag 0DF2 on sheaves of 𝒪-modules.

def derivedSmallEtaleModuleBaseChangeIso (f : Y ⟶ X) (g : X' ⟶ X) (g' : Y' ⟶ Y) (f' : Y' ⟶ X')
    (h : IsPullback g' f' f g) :
    derivedPushforward.{u + 1} (bigEtaleRingedSiteHom T f) ⋙
        (spacesEtaleRestrictionAlongRingedHom T g).pushforwardTopos.mapDerivedCategory ≅
      (spacesEtaleRestrictionAlongRingedHom T g').pushforwardTopos.mapDerivedCategory ⋙
        derivedPushforward.{u + 1} (smallEtaleRingedSiteHom T f')

AlgebraicGeometry.BigEtaleSpaceSite.derivedBigSmallEtalePushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigSmallEtaleDerivedPushforward.lean, line 292. The attribute's comment: “big_small_abelian”.

Derived direct image commutes with restriction to the small étale site. Derived big-site direct image followed by restriction to the small étale site agrees naturally with restriction followed by derived small-site direct image.

public def derivedBigSmallEtalePushforwardIso :
    (((bigEtalePushforward T f).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
      DerivedCategory.Qh).totalRightDerived DerivedCategory.Qh
        (HomotopyCategory.quasiIso
          (Sheaf (T.bigEtaleTopology Y) Ab.{u + 1})
          (ComplexShape.up ℤ))) ⋙
      ((Space.SpacesEtale.inclusion T.fppfSite S T.fppf_mem X).sheafPushforwardContinuous
        Ab.{u + 1} (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem X)
        (T.bigEtaleTopology X)).mapDerivedCategory ≅
    ((Space.SpacesEtale.inclusion T.fppfSite S T.fppf_mem Y).sheafPushforwardContinuous
        Ab.{u + 1} (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem Y)
        (T.bigEtaleTopology Y)).mapDerivedCategory ⋙
      (((smallEtalePushforward T f).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
        DerivedCategory.Qh).totalRightDerived DerivedCategory.Qh
          (HomotopyCategory.quasiIso
            (Sheaf (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem Y)
              Ab.{u + 1}) (ComplexShape.up ℤ)))

AlgebraicGeometry.BigEtaleSpaceSite.derivedBigSmallEtaleModulePushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigSmallEtaleDerivedPushforwardModules.lean, line 323. The attribute's comment: “big_small_modules”.

Stacks Project, Tag 0DGA, part (2). Derived big étale direct image of sheaves of 𝒪-modules followed by restriction to the small étale site of X agrees naturally with restriction to the small étale site of Y followed by derived small étale direct image.

def derivedBigSmallEtaleModulePushforwardIso (f : Y ⟶ X) :
    derivedPushforward.{u + 1} (bigEtaleRingedSiteHom T f) ⋙
        (spacesEtaleRestrictionRingedHom T X).pushforwardTopos.mapDerivedCategory ≅
      (spacesEtaleRestrictionRingedHom T Y).pushforwardTopos.mapDerivedCategory ⋙
        derivedPushforward.{u + 1} (smallEtaleRingedSiteHom T f)

Declarations registered for the tag:

Stacks.Cohomology.Localization.derivedOverPushforwardBaseChangeIso, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Simplicial/BigEtaleBaseChange.lean, line 34 (StacksFrontier): “big_base_change_abelian”.

Tag 0DGB, a lemma

Tag 0DGB in the Stacks Project.

AlgebraicGeometry.BigEtaleSpaceSite.bigSmallEtaleCohomologyIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigSmallEtaleCohomology.lean, line 176. The attribute's comment: “part (5), big-site cohomology over Y of a big complex”.

Étale cohomology over Y of a complex of abelian sheaves on the big étale site of X is the cohomology on the spaces-étale site of Y of its restriction along i_f: the right-derived sections functor at f : Y ⟶ X is restriction followed by derived global sections, naturally in the derived coefficient object.

noncomputable def bigSmallEtaleCohomologyIso :
    (((bigEtaleSections T f).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
      DerivedCategory.Qh).totalRightDerived DerivedCategory.Qh
        (HomotopyCategory.quasiIso
          (Sheaf (T.bigEtaleTopology X) Ab.{u + 1}) (ComplexShape.up ℤ))) ≅
    ((smallEtaleRestriction T f).mapDerivedCategory ⋙
      (((Sheaf.Γ (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem Y)
        Ab.{u + 1}).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
        DerivedCategory.Qh).totalRightDerived DerivedCategory.Qh
          (HomotopyCategory.quasiIso
            (Sheaf (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem Y) Ab.{u + 1})
            (ComplexShape.up ℤ))))

AlgebraicGeometry.BigEtaleSpaceSite.bigSmallEtaleCohomologyIsoAt, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigSmallEtaleCohomology.lean, line 232. The attribute's comment: “part (5), in each degree”.

In every degree, étale cohomology over Y of a complex on the big étale site of X agrees with the cohomology on the spaces-étale site of Y of its restriction along i_f.

noncomputable def bigSmallEtaleCohomologyIsoAt
    (M : DerivedCategory (Sheaf (T.bigEtaleTopology X) Ab.{u + 1})) (n : ℤ) :
    (DerivedCategory.homologyFunctor Ab.{u + 1} n).obj
      ((((bigEtaleSections T f).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
        DerivedCategory.Qh).totalRightDerived DerivedCategory.Qh
          (HomotopyCategory.quasiIso
            (Sheaf (T.bigEtaleTopology X) Ab.{u + 1}) (ComplexShape.up ℤ))).obj M) ≅
    (DerivedCategory.homologyFunctor Ab.{u + 1} n).obj
      (((smallEtaleRestriction T f).mapDerivedCategory ⋙
        (((Sheaf.Γ (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem Y)
          Ab.{u + 1}).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
          DerivedCategory.Qh).totalRightDerived DerivedCategory.Qh
            (HomotopyCategory.quasiIso
              (Sheaf (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem Y) Ab.{u + 1})
              (ComplexShape.up ℤ)))).obj M)

AlgebraicGeometry.BigEtaleSpaceSite.pulledSmallEtaleCohomologyIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigSmallEtaleCohomology.lean, line 276. The attribute's comment: “part (3), cohomology of a pullback from the small site”.

Étale cohomology over Y of a complex pulled back from the spaces-étale site of X to the big étale site of X is the cohomology on the spaces-étale site of Y of its pullback along f_small.

noncomputable def pulledSmallEtaleCohomologyIso :
    ((CategoryTheory.Sites.abelianInverseImage
      (bigToSmallEtaleMorphism T X)).mapDerivedCategory ⋙
      (((bigEtaleSections T f).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
        DerivedCategory.Qh).totalRightDerived DerivedCategory.Qh
          (HomotopyCategory.quasiIso
            (Sheaf (T.bigEtaleTopology X) Ab.{u + 1}) (ComplexShape.up ℤ)))) ≅
    ((CategoryTheory.Sites.abelianInverseImage
      (smallEtaleMorphism T f)).mapDerivedCategory ⋙
      (((Sheaf.Γ (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem Y)
        Ab.{u + 1}).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
        DerivedCategory.Qh).totalRightDerived DerivedCategory.Qh
          (HomotopyCategory.quasiIso
            (Sheaf (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem Y) Ab.{u + 1})
            (ComplexShape.up ℤ))))

AlgebraicGeometry.BigEtaleSpaceSite.pulledSmallEtaleCohomologyIsoAt, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigSmallEtaleCohomology.lean, line 300. The attribute's comment: “part (3), in each degree”.

In every degree, étale cohomology over Y of a complex pulled back from the spaces-étale site of X agrees with the cohomology on the spaces-étale site of Y of its pullback along f_small.

noncomputable def pulledSmallEtaleCohomologyIsoAt
    (K : DerivedCategory
      (Sheaf (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem X) Ab.{u + 1})) (n : ℤ) :
    (DerivedCategory.homologyFunctor Ab.{u + 1} n).obj
      (((CategoryTheory.Sites.abelianInverseImage
        (bigToSmallEtaleMorphism T X)).mapDerivedCategory ⋙
        (((bigEtaleSections T f).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
          DerivedCategory.Qh).totalRightDerived DerivedCategory.Qh
            (HomotopyCategory.quasiIso
              (Sheaf (T.bigEtaleTopology X) Ab.{u + 1}) (ComplexShape.up ℤ)))).obj K) ≅
    (DerivedCategory.homologyFunctor Ab.{u + 1} n).obj
      (((CategoryTheory.Sites.abelianInverseImage
        (smallEtaleMorphism T f)).mapDerivedCategory ⋙
        (((Sheaf.Γ (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem Y)
          Ab.{u + 1}).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
          DerivedCategory.Qh).totalRightDerived DerivedCategory.Qh
            (HomotopyCategory.quasiIso
              (Sheaf (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem Y) Ab.{u + 1})
              (ComplexShape.up ℤ)))).obj K)

AlgebraicGeometry.BigEtaleSpaceSite.overXSmallEtaleCohomologyIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigSmallEtaleCohomology.lean, line 382. The attribute's comment: “part (1), cohomology over X of a pullback”.

Étale cohomology over X of a complex pulled back from the spaces-étale site of X to the big étale site of X is its cohomology on the spaces-étale site of X.

noncomputable def overXSmallEtaleCohomologyIso :
    ((CategoryTheory.Sites.abelianInverseImage
      (bigToSmallEtaleMorphism T X)).mapDerivedCategory ⋙
      (((bigEtaleSections T (𝟙 X)).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
        DerivedCategory.Qh).totalRightDerived DerivedCategory.Qh
          (HomotopyCategory.quasiIso
            (Sheaf (T.bigEtaleTopology X) Ab.{u + 1}) (ComplexShape.up ℤ)))) ≅
    (((Sheaf.Γ (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem X)
      Ab.{u + 1}).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
      DerivedCategory.Qh).totalRightDerived DerivedCategory.Qh
        (HomotopyCategory.quasiIso
          (Sheaf (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem X) Ab.{u + 1})
          (ComplexShape.up ℤ)))

AlgebraicGeometry.BigEtaleSpaceSite.overXSmallEtaleCohomologyIsoAt, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigSmallEtaleCohomology.lean, line 402. The attribute's comment: “part (1), in each degree”.

In every degree, étale cohomology over X of a complex pulled back from the spaces-étale site of X agrees with its small-site cohomology.

noncomputable def overXSmallEtaleCohomologyIsoAt
    (K : DerivedCategory
      (Sheaf (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem X) Ab.{u + 1})) (n : ℤ) :
    (DerivedCategory.homologyFunctor Ab.{u + 1} n).obj
      (((CategoryTheory.Sites.abelianInverseImage
        (bigToSmallEtaleMorphism T X)).mapDerivedCategory ⋙
        (((bigEtaleSections T (𝟙 X)).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
          DerivedCategory.Qh).totalRightDerived DerivedCategory.Qh
            (HomotopyCategory.quasiIso
              (Sheaf (T.bigEtaleTopology X) Ab.{u + 1}) (ComplexShape.up ℤ)))).obj K) ≅
    (DerivedCategory.homologyFunctor Ab.{u + 1} n).obj
      ((((Sheaf.Γ (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem X)
        Ab.{u + 1}).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
        DerivedCategory.Qh).totalRightDerived DerivedCategory.Qh
          (HomotopyCategory.quasiIso
            (Sheaf (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem X) Ab.{u + 1})
            (ComplexShape.up ℤ))).obj K)

AlgebraicGeometry.BigEtaleSpaceSite.moduleOverXSmallEtaleCohomologyIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigSmallEtaleCohomologyModuleOverX.lean, line 250. The attribute's comment: “part (2), cohomology over X of a derived pullback of modules from the small site”.

Stacks 0DGB, part (2). Étale cohomology over X of the derived pullback Lπ_X^*K to the big étale site of X of a complex of sheaves of 𝒪_X-modules on the spaces-étale site of X is the cohomology of K on that site, naturally in the derived coefficient object.

def moduleOverXSmallEtaleCohomologyIso :
    (derivedModulePullbackPi T X ⋙
      (SheafOfModules.toSheaf.{u + 1} (bigEtaleRingSheaf T X)).mapDerivedCategory ⋙
      (((bigEtaleSections T (𝟙 X)).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
        DerivedCategory.Qh).totalRightDerived DerivedCategory.Qh
          (HomotopyCategory.quasiIso
            (Sheaf (T.bigEtaleTopology X) Ab.{u + 1}) (ComplexShape.up ℤ)))) ≅
    ((SheafOfModules.toSheaf.{u + 1} (spacesEtaleRingSheaf T X)).mapDerivedCategory ⋙
      (((Sheaf.Γ (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem X)
          Ab.{u + 1}).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
          DerivedCategory.Qh).totalRightDerived DerivedCategory.Qh
            (HomotopyCategory.quasiIso
              (Sheaf (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem X) Ab.{u + 1})
              (ComplexShape.up ℤ))))

AlgebraicGeometry.BigEtaleSpaceSite.moduleOverXSmallEtaleCohomologyIsoAt, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigSmallEtaleCohomologyModuleOverX.lean, line 272. The attribute's comment: “part (2), in each degree”.

Stacks 0DGB, part (2). In every degree, étale cohomology over X of the derived pullback Lπ_X^*K of a complex of sheaves of 𝒪_X-modules on the spaces-étale site of X agrees with the cohomology of K on that site.

def moduleOverXSmallEtaleCohomologyIsoAt
    (K : DerivedCategory (SpacesEtaleModules.{u, u + 1} T X)) (n : ℤ) :
    (DerivedCategory.homologyFunctor Ab.{u + 1} n).obj
      ((derivedModulePullbackPi T X ⋙
        (SheafOfModules.toSheaf.{u + 1} (bigEtaleRingSheaf T X)).mapDerivedCategory ⋙
        (((bigEtaleSections T (𝟙 X)).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
          DerivedCategory.Qh).totalRightDerived DerivedCategory.Qh
            (HomotopyCategory.quasiIso
              (Sheaf (T.bigEtaleTopology X) Ab.{u + 1}) (ComplexShape.up ℤ)))).obj K) ≅
    (DerivedCategory.homologyFunctor Ab.{u + 1} n).obj
      (((SheafOfModules.toSheaf.{u + 1} (spacesEtaleRingSheaf T X)).mapDerivedCategory ⋙
        (((Sheaf.Γ (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem X)
            Ab.{u + 1}).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
            DerivedCategory.Qh).totalRightDerived DerivedCategory.Qh
              (HomotopyCategory.quasiIso
                (Sheaf (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem X) Ab.{u + 1})
                (ComplexShape.up ℤ)))).obj K)

AlgebraicGeometry.BigEtaleSpaceSite.modulePulledSmallEtaleCohomologyIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigSmallEtaleCohomologyModulePullback.lean, line 267. The attribute's comment: “part (4), cohomology over Y of a derived pullback from the small site”.

Étale cohomology over Y of the derived pullback Lπ_X^*K of a complex of sheaves of 𝒪_X-modules on the spaces-étale site of X is naturally isomorphic to the cohomology on the spaces-étale site of Y of Lf_small^*K, as total right derived functors.

noncomputable def modulePulledSmallEtaleCohomologyIso :
    (derivedModulePullbackPi T X ⋙
      (SheafOfModules.toSheaf.{u + 1} (bigEtaleRingSheaf T X)).mapDerivedCategory ⋙
      (((bigEtaleSections T f).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
        DerivedCategory.Qh).totalRightDerived DerivedCategory.Qh
          (HomotopyCategory.quasiIso
            (Sheaf (T.bigEtaleTopology X) Ab.{u + 1}) (ComplexShape.up ℤ)))) ≅
    (derivedModulePullbackSmallEtale T f ⋙
      (SheafOfModules.toSheaf.{u + 1} (spacesEtaleRingSheaf T Y)).mapDerivedCategory ⋙
      (((Sheaf.Γ (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem Y)
          Ab.{u + 1}).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
          DerivedCategory.Qh).totalRightDerived DerivedCategory.Qh
            (HomotopyCategory.quasiIso
              (Sheaf (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem Y) Ab.{u + 1})
              (ComplexShape.up ℤ))))

AlgebraicGeometry.BigEtaleSpaceSite.modulePulledSmallEtaleCohomologyIsoAt, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigSmallEtaleCohomologyModulePullback.lean, line 290. The attribute's comment: “part (4), in each degree”.

In every degree, étale cohomology over Y of the derived pullback Lπ_X^*K of a complex of sheaves of 𝒪_X-modules on the spaces-étale site of X agrees with the cohomology on the spaces-étale site of Y of Lf_small^*K.

noncomputable def modulePulledSmallEtaleCohomologyIsoAt
    (K : DerivedCategory (SpacesEtaleModules.{u, u + 1} T X)) (n : ℤ) :
    (DerivedCategory.homologyFunctor Ab.{u + 1} n).obj
      ((derivedModulePullbackPi T X ⋙
        (SheafOfModules.toSheaf.{u + 1} (bigEtaleRingSheaf T X)).mapDerivedCategory ⋙
        (((bigEtaleSections T f).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
          DerivedCategory.Qh).totalRightDerived DerivedCategory.Qh
            (HomotopyCategory.quasiIso
              (Sheaf (T.bigEtaleTopology X) Ab.{u + 1}) (ComplexShape.up ℤ)))).obj K) ≅
    (DerivedCategory.homologyFunctor Ab.{u + 1} n).obj
      ((derivedModulePullbackSmallEtale T f ⋙
        (SheafOfModules.toSheaf.{u + 1} (spacesEtaleRingSheaf T Y)).mapDerivedCategory ⋙
        (((Sheaf.Γ (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem Y)
            Ab.{u + 1}).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
            DerivedCategory.Qh).totalRightDerived DerivedCategory.Qh
              (HomotopyCategory.quasiIso
                (Sheaf (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem Y) Ab.{u + 1})
                (ComplexShape.up ℤ)))).obj K)

AlgebraicGeometry.BigEtaleSpaceSite.moduleBigSmallEtaleCohomologyIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigSmallEtaleCohomologyModules.lean, line 107. The attribute's comment: “part (6), big-site cohomology over Y of a complex of modules”.

Stacks 0DGB, part (6). Étale cohomology over Y of a complex of sheaves of 𝒪-modules on the big étale site of X is the cohomology on the spaces-étale site of Y of its inverse image along i_f: the right-derived sections functor at f : Y ⟶ X is i_f^* followed by derived global sections, naturally in the derived coefficient object.

noncomputable def moduleBigSmallEtaleCohomologyIso :
    ((SheafOfModules.toSheaf.{u + 1} (bigEtaleRingSheaf T X)).mapDerivedCategory ⋙
      (((bigEtaleSections T f).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
        DerivedCategory.Qh).totalRightDerived DerivedCategory.Qh
          (HomotopyCategory.quasiIso
            (Sheaf (T.bigEtaleTopology X) Ab.{u + 1}) (ComplexShape.up ℤ)))) ≅
    ((restrictModulesAlong T f).mapDerivedCategory ⋙
      (SheafOfModules.toSheaf.{u + 1} (spacesEtaleRingSheaf T Y)).mapDerivedCategory ⋙
      (((Sheaf.Γ (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem Y)
        Ab.{u + 1}).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
        DerivedCategory.Qh).totalRightDerived DerivedCategory.Qh
          (HomotopyCategory.quasiIso
            (Sheaf (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem Y) Ab.{u + 1})
            (ComplexShape.up ℤ))))

AlgebraicGeometry.BigEtaleSpaceSite.moduleBigSmallEtaleCohomologyIsoAt, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigSmallEtaleCohomologyModules.lean, line 130. The attribute's comment: “part (6), in each degree”.

Stacks 0DGB, part (6). In every degree, étale cohomology over Y of a complex of sheaves of 𝒪-modules on the big étale site of X agrees with the cohomology on the spaces-étale site of Y of its inverse image along i_f.

noncomputable def moduleBigSmallEtaleCohomologyIsoAt
    (M : DerivedCategory (BigEtaleModules.{u, u + 1} T X)) (n : ℤ) :
    (DerivedCategory.homologyFunctor Ab.{u + 1} n).obj
      (((SheafOfModules.toSheaf.{u + 1} (bigEtaleRingSheaf T X)).mapDerivedCategory ⋙
        (((bigEtaleSections T f).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
          DerivedCategory.Qh).totalRightDerived DerivedCategory.Qh
            (HomotopyCategory.quasiIso
              (Sheaf (T.bigEtaleTopology X) Ab.{u + 1}) (ComplexShape.up ℤ)))).obj M) ≅
    (DerivedCategory.homologyFunctor Ab.{u + 1} n).obj
      (((restrictModulesAlong T f).mapDerivedCategory ⋙
        (SheafOfModules.toSheaf.{u + 1} (spacesEtaleRingSheaf T Y)).mapDerivedCategory ⋙
        (((Sheaf.Γ (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem Y)
          Ab.{u + 1}).mapHomotopyCategory (ComplexShape.up ℤ) ⋙
          DerivedCategory.Qh).totalRightDerived DerivedCategory.Qh
            (HomotopyCategory.quasiIso
              (Sheaf (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem Y) Ab.{u + 1})
              (ComplexShape.up ℤ)))).obj M)

Tag 0DGC, a lemma

Tag 0DGC in the Stacks Project.

AlgebraicGeometry.BigEtaleSpaceSite.bigToSmall_inverseImage_comp_pushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SmallEtaleCohomologicalDescent.lean, line 88. The attribute's comment: “the composite is the identity, for sheaves of sets”.

Stacks 0DGC. Restricting back to the spaces-étale site of X the inverse image of a sheaf of sets along π_X returns that sheaf: π_{X,*} ∘ π_X⁻¹ is the identity functor.

noncomputable def bigToSmall_inverseImage_comp_pushforwardIso :
    (bigToSmallEtaleMorphism T X).inverseImage ⋙ (bigToSmallEtaleMorphism T X).pushforward ≅
      𝟭 (Sheaf (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem X) (Type (u + 1)))

AlgebraicGeometry.BigEtaleSpaceSite.bigToSmall_abelianInverseImage_comp_restrictionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SmallEtaleCohomologicalDescent.lean, line 110. The attribute's comment: “the composite is the identity, for abelian sheaves”.

Stacks 0DGC. The same composite identity for abelian sheaves: restricting the abelian inverse image along π_X back to the spaces-étale site of X returns the sheaf.

noncomputable def bigToSmall_abelianInverseImage_comp_restrictionIso :
    CategoryTheory.Sites.abelianInverseImage (bigToSmallEtaleMorphism T X) ⋙
        bigToSmallEtaleRestriction T X ≅
      𝟭 (Sheaf (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem X) Ab.{u + 1})

AlgebraicGeometry.BigEtaleSpaceSite.isIso_bigToSmallEtaleDerivedAdjunction_unit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/SmallEtaleCohomologicalDescent.lean, line 144. The attribute's comment: “the derived unit is an isomorphism”.

Stacks 0DGC. For every complex K on the spaces-étale site of X the canonical map K ⟶ Rπ_{X,*}π_X⁻¹K is an isomorphism.

theorem isIso_bigToSmallEtaleDerivedAdjunction_unit
    (K : DerivedCategory
      (Sheaf (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem X) Ab.{u + 1})) :
    IsIso ((bigToSmallEtaleDerivedAdjunction T X).unit.app K)

Tag 0DGD, a lemma

Tag 0DGD in the Stacks Project.

AlgebraicGeometry.BigEtaleSpaceSite.bigToSmallEtale_pushforward_baseChange_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigSmallEtalePushforwardBaseChange.lean, line 114.

Stacks 0DGD. Let S be a scheme and f : Y ⟶ X a proper morphism of algebraic spaces over S (objects of the big étale site T of algebraic spaces over S). Write π_X : Sh((Spaces/X)_étale) ⟶ Sh(X_étale) (bigToSmallEtaleMorphism T X) for the comparison of the big étale topos with the small étale topos Sh(X_étale) (the spaces-étale site of X). Then:

the canonical base change map π_X⁻¹ ∘ f_{small,*} ⟶ f_{big,*} ∘ π_Y⁻¹ of functors from sheaves of sets on Y_étale to sheaves of sets on (Spaces/X)_étale (bigToSmallEtaleBaseChange T f; its target f_{big,*} is restriction along Y ×_X - : Spaces/X ⥤ Spaces/Y) is an isomorphism;

for every K in D⁺(Y_étale) (K.IsGE n for some n) whose cohomology sheaves are torsion, the canonical base change map π_X⁻¹ R f_{small,*} K ⟶ R f_{big,*} π_Y⁻¹ K of Stacks 07A7 (bigToSmallEtaleDerivedBaseChange T f, on the derived categories of abelian sheaves) is an isomorphism;

if f is finite, the canonical base change map π_X⁻¹ R f_{small,*} K ⟶ R f_{big,*} π_Y⁻¹ K is an isomorphism for every K in the unbounded derived category D(Y_étale).

theorem bigToSmallEtale_pushforward_baseChange_of_isProper {X Y : T.Spaces} (f : Y ⟶ X)
    (hf : Space.IsProper T.fppfSite S T.fppf_mem f.hom) :
    IsIso (bigToSmallEtaleBaseChange T f) ∧
      (∀ (K : DerivedCategory
          (Sheaf (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem Y) Ab.{u + 1})) (n : ℤ),
        K.IsGE n → HasTorsionCohomology T K →
          IsIso ((bigToSmallEtaleDerivedBaseChange T f).app K)) ∧
      (Space.IsFinite T.fppfSite S T.fppf_mem f.hom →
        ∀ K : DerivedCategory
          (Sheaf (Space.SpacesEtale.topology T.fppfSite S T.fppf_mem Y) Ab.{u + 1}),
          IsIso ((bigToSmallEtaleDerivedBaseChange T f).app K))

Sources

LeanAlgebraicGeometry.BigEtaleSpaceSite.bigToSmall_inverseImageFactorizationIso · AlgebraicGeometry.BigEtaleSpaceSite.bigToSmall_inverseImageFactorizationIso_hom_app · AlgebraicGeometry.BigEtaleSpaceSite.smallToBig_inverseImageSectionsIso · AlgebraicGeometry.BigEtaleSpaceSite.bigToSmall_inverseImageSectionsIso · AlgebraicGeometry.BigEtaleSpaceSite.bigToSmall_inverseImageSectionsIso_hom_app · AlgebraicGeometry.BigEtaleSpaceSite.inverseImage_isSheafFor_smooth_syntomic_fppf_fpqc · AlgebraicGeometry.BigPHSpaceSite.isSheaf_bigToSmallEtale_inverseImage · AlgebraicGeometry.BigEtaleSpaceSite.injective_smallEtaleRestriction

Section84.6 Comparing fppf and étale topologies #

Section 84.6 of the Stacks Project, Tag 0DGE. 7 tags here are carried by 18 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0DGF, a lemma

Tag 0DGF in the Stacks Project.

AlgebraicGeometry.BigFppfSpaceSite.isIso_fppfToSmallEtale_units_and_isZero_rightDerived, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigFppfToSmallEtaleUnconditional.lean, line 74.

Stacks 0DGF. Let X be an algebraic space over S. (1) For a sheaf of sets F on X_étale, ε_{X,*}a_X⁻¹F = π_X⁻¹F and a_{X,*}a_X⁻¹F = F: the units π_X⁻¹F ⟶ ε_{X,*}ε_X⁻¹π_X⁻¹F and F ⟶ a_{X,*}a_X⁻¹F are isomorphisms. (2) For an abelian sheaf F on X_étale, R^iε_{X,*}(a_X⁻¹F) = 0 for i > 0.

theorem isIso_fppfToSmallEtale_units_and_isZero_rightDerived (X : T.Spaces) :
    (IsIso (Functor.whiskerLeft (E.bigToSmallEtaleMorphism (etaleSpace T E h X)).inverseImage
        (fppfToBigEtaleMorphism T E h X).adj.unit) ∧
      IsIso (fppfToSmallEtaleMorphism T E h X).adj.unit) ∧
    ∀ (F : Sheaf (Space.SpacesEtale.topology E.fppfSite S E.fppf_mem (etaleSpace T E h X))
      AddCommGrpCat.{u + 1}) (i : ℕ), 0 < i →
      IsZero ((((Over.postEquiv (canonicalSpaceEquivalence T E h).1
        (X := X)).inverse.sheafPushforwardContinuous
        AddCommGrpCat.{u + 1} (E.bigEtaleTopology (etaleSpace T E h X))
        (BigFppfSpaceOver.topology T X)).rightDerived i).obj
          ((CategoryTheory.Sites.abelianInverseImage (fppfToSmallEtaleMorphism T E h X)).obj F))

Tag 0DGG, a lemma

Tag 0DGG in the Stacks Project.

AlgebraicGeometry.BigFppfSpaceSite.isIso_fppfToSmallEtale_derivedUnits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigFppfToSmallEtaleUnconditional.lean, line 101.

Stacks 0DGG. For K in D⁺(X_étale) the maps π_X⁻¹K ⟶ Rε_{X,*}a_X⁻¹K and K ⟶ Ra_{X,*}a_X⁻¹K are isomorphisms: the units of the derived adjunctions ε_X⁻¹ ⊣ Rε_{X,*} at π_X⁻¹K and a_X⁻¹ ⊣ Ra_{X,*} at K.

theorem isIso_fppfToSmallEtale_derivedUnits
    (K : DerivedCategory.Plus (Sheaf (Space.SpacesEtale.topology E.fppfSite S E.fppf_mem
      (etaleSpace T E h X)) AddCommGrpCat.{u + 1})) :
    IsIso ((Stacks.ComparingTopologies.derivedPlusAdjunction
        (fppfToBigEtaleAbelianAdjunction T E h X)).unit.app
          ((CategoryTheory.Sites.abelianInverseImage
            (E.bigToSmallEtaleMorphism (etaleSpace T E h X))).mapDerivedCategoryPlus.obj K)) ∧
      IsIso ((Stacks.ComparingTopologies.derivedPlusAdjunction
        (fppfToSmallEtaleAbelianAdjunction T E h X)).unit.app K)

Tag 0DGH, a lemma

Tag 0DGH in the Stacks Project.

AlgebraicGeometry.BigFppfSpaceSite.isIso_etaleToFppfCohomology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigFppfToSmallEtaleUnconditional.lean, line 125. The attribute's comment: “(2)”.

Stacks 0DGH, part (2). For K in D⁺(X_étale), H^q(X_étale, K) = H^q_fppf(X, a_X⁻¹K) for every q: the map induced on H^q by the canonical map AlgebraicGeometry.BigFppfSpaceSite.etaleToFppfDerivedGlobalSections is an isomorphism, naturally in K.

theorem isIso_etaleToFppfCohomology (q : ℤ) :
    IsIso (Functor.whiskerRight (etaleToFppfDerivedGlobalSections T E h X)
      (DerivedCategory.Plus.homologyFunctor AddCommGrpCat.{u + 1} q))

AlgebraicGeometry.BigFppfSpaceSite.etaleCohomologyIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigFppfToSmallEtaleUnconditional.lean, line 166. The attribute's comment: “(1)”.

Stacks 0DGH, part (1). For an abelian sheaf F on X_étale, H^q(X_étale, F) = H^q_fppf(X, a_X⁻¹F) for every q, by the canonical map AlgebraicGeometry.BigFppfSpaceSite.etaleToFppfDerivedGlobalSections at F[0].

def etaleCohomologyIso (X : T.Spaces)
    (F : Sheaf (Space.SpacesEtale.topology E.fppfSite S E.fppf_mem (etaleSpace T E h X))
      AddCommGrpCat.{u + 1}) (q : ℕ) :
    ((etaleGlobalSections T E h X).rightDerived q).obj F ≅
      ((fppfGlobalSections T X).rightDerived q).obj
        ((CategoryTheory.Sites.abelianInverseImage (fppfToSmallEtaleMorphism T E h X)).obj F)

AlgebraicGeometry.BigFppfSpaceSite.etaleCohomologyConstantIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigFppfToSmallEtaleUnconditional.lean, line 177. The attribute's comment: “the example of an abelian group”.

The example of Stacks 0DGH. For an abelian group A, H^q_étale(X, A) = H^q_fppf(X, A) for the constant sheaves.

def etaleCohomologyConstantIso (X : T.Spaces) (A : AddCommGrpCat.{u + 1}) (q : ℕ) :
    ((etaleGlobalSections T E h X).rightDerived q).obj
        ((constantSheaf (Space.SpacesEtale.topology E.fppfSite S E.fppf_mem (etaleSpace T E h X))
          AddCommGrpCat.{u + 1}).obj A) ≅
      ((fppfGlobalSections T X).rightDerived q).obj
        ((constantSheaf (BigFppfSpaceOver.topology T X) AddCommGrpCat.{u + 1}).obj A)

Tag 0DGI, a lemma

Tag 0DGI in the Stacks Project.

AlgebraicGeometry.BigFppfSpaceSite.canonicalSpaceEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigFppfToSmallEtale.lean, line 62. The attribute's comment: “identification of the underlying algebraic spaces”.

The identification of the category of algebraic spaces a big fppf site of algebraic spaces is built on with the one a big étale site of algebraic spaces over the same big fppf site of schemes is built on, together with the facts that it is the identity on objects and on morphisms.

def canonicalSpaceEquivalence :
    { G : T.Spaces ≌ E.Spaces //
      (∀ X : T.Spaces, HEq X.1 (G.functor.obj X).1) ∧
      (∀ {X Y : T.Spaces} (f : X ⟶ Y), HEq f.hom (G.functor.map f).hom) }

AlgebraicGeometry.BigFppfSpaceSite.fppfToBigEtale_isContinuous, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigFppfToSmallEtale.lean, line 84. The attribute's comment: “continuity of the change-of-topology functor”.

The identity-on-spaces functor from the big étale slice at X to the big fppf slice at X is continuous.

instance fppfToBigEtale_isContinuous (X : T.Spaces) :
    ((Over.postEquiv (canonicalSpaceEquivalence T E h).1 (X := X)).inverse).IsContinuous
      (E.bigEtaleTopology (etaleSpace T E h X)) (BigFppfSpaceOver.topology T X)

AlgebraicGeometry.BigFppfSpaceSite.fppfToBigEtaleMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigFppfToSmallEtale.lean, line 134. The attribute's comment: “the fppf-to-big-étale morphism”.

The change-of-topology morphism ε_X from the big fppf topos of X to its big étale topos, induced by the identity-on-spaces functor of slice categories.

def fppfToBigEtaleMorphism (X : T.Spaces) :
    MorphismOfTopoi (Sheaf (BigFppfSpaceOver.topology T X) (Type (u + 1)))
      (Sheaf (E.bigEtaleTopology (etaleSpace T E h X)) (Type (u + 1)))

AlgebraicGeometry.BigFppfSpaceSite.fppfToBigEtale_pushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigFppfToSmallEtale.lean, line 146. The attribute's comment: “direct image of the fppf-to-big-étale morphism”.

The direct image of ε_X is restriction along the identity-on-spaces functor of slice categories.

def fppfToBigEtale_pushforwardIso (X : T.Spaces) :
    (fppfToBigEtaleMorphism T E h X).pushforward ≅
      ((Over.postEquiv (canonicalSpaceEquivalence T E h).1
        (X := X)).inverse).sheafPushforwardContinuous (Type (u + 1))
        (E.bigEtaleTopology (etaleSpace T E h X)) (BigFppfSpaceOver.topology T X)

AlgebraicGeometry.BigFppfSpaceSite.pullbackChangeOfTopologyIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigFppfToSmallEtale.lean, line 156. The attribute's comment: “canonical base-change comparison on the big sites”.

Base change along f commutes with the identity-on-spaces change-of-topology functor of slice categories.

def pullbackChangeOfTopologyIso {X Y : T.Spaces} (f : Y ⟶ X) :
    Over.pullback (etaleMap T E h f) ⋙
        (Over.postEquiv (canonicalSpaceEquivalence T E h).1 (X := Y)).inverse ≅
      (Over.postEquiv (canonicalSpaceEquivalence T E h).1 (X := X)).inverse ⋙
        Over.pullback f

AlgebraicGeometry.BigFppfSpaceSite.fppfToSmallEtaleMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigFppfToSmallEtale.lean, line 173. The attribute's comment: “the factorization through big étale”.

The morphism a_X from the big fppf topos of X to its small étale topos: the composite of ε_X with the big-to-small étale morphism π_X ([Stacks, Tag 0DF3]).

def fppfToSmallEtaleMorphism (X : T.Spaces) :
    MorphismOfTopoi (Sheaf (BigFppfSpaceOver.topology T X) (Type (u + 1)))
      (Sheaf (Space.SpacesEtale.topology E.fppfSite S E.fppf_mem (etaleSpace T E h X))
        (Type (u + 1)))

AlgebraicGeometry.BigFppfSpaceSite.bigFppfBigEtale_pushforwardCommIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigFppfToSmallEtale.lean, line 182. The attribute's comment: “the big fppf–big étale square”.

The big fppf–big étale square: for a morphism f : Y ⟶ X of algebraic spaces the direct images of ε_X ∘ f_{big, fppf} and of f_{big, étale} ∘ ε_Y are canonically isomorphic.

def bigFppfBigEtale_pushforwardCommIso {X Y : T.Spaces} (f : Y ⟶ X) :
    ((E.bigEtaleMorphism (etaleMap T E h f)).comp (fppfToBigEtaleMorphism T E h Y)).pushforward ≅
      ((fppfToBigEtaleMorphism T E h X).comp (bigFppfMorphism T f)).pushforward

AlgebraicGeometry.BigFppfSpaceSite.bigFppfSmallEtale_pushforwardCommIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigFppfToSmallEtale.lean, line 240. The attribute's comment: “the big fppf–small étale square”.

The big fppf–small étale square: for a morphism f : Y ⟶ X of algebraic spaces the direct images of a_X ∘ f_{big, fppf} and of f_{small} ∘ a_Y are canonically isomorphic.

def bigFppfSmallEtale_pushforwardCommIso {X Y : T.Spaces} (f : Y ⟶ X) :
    ((E.smallEtaleMorphism (etaleMap T E h f)).comp
        (fppfToSmallEtaleMorphism T E h Y)).pushforward ≅
      ((fppfToSmallEtaleMorphism T E h X).comp (bigFppfMorphism T f)).pushforward

Tag 0DGJ, a lemma

Tag 0DGJ in the Stacks Project.

AlgebraicGeometry.BigFppfSpaceSite.fppfToSmallEtalePushforwardIsosOfIsProper, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigFppfToSmallEtaleAbelianProperPushforward.lean, line 121. The attribute's comment: “(1)”.

Let f : Y ⟶ X be a proper morphism of algebraic spaces over S, and a = π ∘ ε the comparison morphisms from the big fppf topoi to the small étale topoi of Stacks 0DGI. Then a_X⁻¹ ∘ f_{small,*} = f_{big,fppf,*} ∘ a_Y⁻¹, as functors from sheaves of sets on the small étale site of Y to sheaves of sets on the big fppf site of X, and likewise for abelian sheaves. Both isomorphisms are the canonical base change maps, the mates of the commutative square of Stacks 0DGI: AlgebraicGeometry.BigFppfSpaceSite.fppfToSmallEtaleBaseChange and AlgebraicGeometry.BigFppfSpaceSite.fppfToSmallEtaleAbelianBaseChange.

def fppfToSmallEtalePushforwardIsosOfIsProper
    (hf : Space.IsProper T.schemeSite S T.scheme_mem f.hom) :
    ((E.smallEtaleMorphism (etaleMap T E h f)).pushforward ⋙
        (fppfToSmallEtaleMorphism T E h X).inverseImage ≅
      (fppfToSmallEtaleMorphism T E h Y).inverseImage ⋙ (bigFppfMorphism T f).pushforward) ×
    (E.smallEtalePushforward (etaleMap T E h f) ⋙
        CategoryTheory.Sites.abelianInverseImage (fppfToSmallEtaleMorphism T E h X) ≅
      CategoryTheory.Sites.abelianInverseImage (fppfToSmallEtaleMorphism T E h Y) ⋙
        fppfAbelianPushforward T f)

AlgebraicGeometry.BigFppfSpaceSite.isIso_fppfToSmallEtaleBaseChange_of_isProper, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigFppfToSmallEtaleProperPushforward.lean, line 278. The attribute's comment: “(1)”.

Proper base change for the big fppf topos. For a proper morphism f : Y ⟶ X of algebraic spaces, the canonical base change map a_X⁻¹ ∘ f_{small,*} ⟶ f_{big,fppf,*} ∘ a_Y⁻¹ of functors from sheaves on the small étale site of Y to sheaves on the big fppf site of X is an isomorphism.

theorem isIso_fppfToSmallEtaleBaseChange_of_isProper {X Y : T.Spaces} (f : Y ⟶ X)
    (hf : Space.IsProper T.schemeSite S T.scheme_mem f.hom) :
    IsIso (fppfToSmallEtaleBaseChange T E h f)

AlgebraicGeometry.BigFppfSpaceSite.isIso_fppfToSmallEtaleProperDerivedBaseChange_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigFppfToSmallEtaleUnconditional.lean, line 204. The attribute's comment: “(2)”.

Stacks 0DGJ, part (2). For a proper morphism f : Y ⟶ X of algebraic spaces and K in D⁺(Y_étale) with torsion cohomology sheaves, a_X⁻¹(Rf_{small,*}K) = Rf_{big,fppf,*}(a_Y⁻¹K): the comparison map AlgebraicGeometry.BigFppfSpaceSite.fppfToSmallEtaleProperDerivedBaseChange is an isomorphism at K.

theorem isIso_fppfToSmallEtaleProperDerivedBaseChange_app
    (hf : Space.IsProper T.schemeSite S T.scheme_mem f.hom)
    (K : DerivedCategory.Plus (Sheaf (Space.SpacesEtale.topology E.fppfSite S E.fppf_mem
      (etaleSpace T E h Y)) AddCommGrpCat.{u + 1}))
    (hK : BigEtaleSpaceSite.HasTorsionCohomology E (DerivedCategory.Plus.ι.obj K)) :
    IsIso ((fppfToSmallEtaleProperDerivedBaseChange T E h f).app K)

Tag 0DGK, a lemma

Tag 0DGK in the Stacks Project.

AlgebraicGeometry.BigFppfSpaceSite.isIso_fppfToSmallEtaleDerivedBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigFppfToSmallEtaleUnconditional.lean, line 149.

Stacks 0DGK. For a finite morphism f : Y ⟶ X of algebraic spaces, a_X⁻¹(Rf_{small,*}K) = Rf_{big,fppf,*}(a_Y⁻¹K) for K in D⁺(Y_étale): the base change map AlgebraicGeometry.BigFppfSpaceSite.fppfToSmallEtaleDerivedBaseChange, the mate of Rf_{small,*} ∘ Ra_{Y,*} = Ra_{X,*} ∘ Rf_{big,fppf,*}, is an isomorphism.

theorem isIso_fppfToSmallEtaleDerivedBaseChange
    (hf : Space.IsFinite T.schemeSite S T.scheme_mem f.hom) :
    IsIso (fppfToSmallEtaleDerivedBaseChange T E h f)

Tag 0DGL, a lemma

Tag 0DGL in the Stacks Project.

AlgebraicGeometry.BigFppfSpaceSite.isEquivalence_fppfSmallEtaleTripleFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigFppfSmallEtaleDescent.lean, line 338.

Fppf descent of small étale sheaves. Let f : X ⟶ Y be a morphism of algebraic spaces over S which is flat, locally of finite presentation and surjective. Then the functor Sh(Y_étale) ⥤ {(G, H, α)}, F ↦ (f_small⁻¹F, a_Y⁻¹F, can), into the category of triples with G ∈ Sh(X_étale), H ∈ Sh((Spaces/Y)_fppf) and α : a_X⁻¹G ⟶ f_{big,fppf}⁻¹H an isomorphism, is an equivalence of categories.

The category of triples is the two-fibre product a_X⁻¹ ⊡ f_{big,fppf}⁻¹ (CategoryTheory.Limits.CategoricalPullback), whose objects are exactly the triples, and the functor is AlgebraicGeometry.BigFppfSpaceSite.fppfSmallEtaleTripleFunctor, built from the canonical isomorphism can = AlgebraicGeometry.BigFppfSpaceSite.fppfSmallEtaleInverseImageCommIso.

theorem isEquivalence_fppfSmallEtaleTripleFunctor {X Y : T.Spaces} (f : X ⟶ Y)
    (hf : Space.IsFlat T.schemeSite S T.scheme_mem f.hom)
    (hlfp : Space.IsLocallyOfFinitePresentation T.schemeSite S T.scheme_mem f.hom)
    (hsurj : Space.IsSurjective T.schemeSite S T.scheme_mem f.hom) :
    (fppfSmallEtaleTripleFunctor T E h f).IsEquivalence

Sources

LeanAlgebraicGeometry.BigFppfSpaceSite.isIso_fppfToSmallEtale_units_and_isZero_rightDerived · AlgebraicGeometry.BigFppfSpaceSite.isIso_fppfToSmallEtale_derivedUnits · AlgebraicGeometry.BigFppfSpaceSite.isIso_etaleToFppfCohomology · AlgebraicGeometry.BigFppfSpaceSite.etaleCohomologyIso · AlgebraicGeometry.BigFppfSpaceSite.etaleCohomologyConstantIso · AlgebraicGeometry.BigFppfSpaceSite.canonicalSpaceEquivalence · AlgebraicGeometry.BigFppfSpaceSite.fppfToBigEtale_isContinuous · AlgebraicGeometry.BigFppfSpaceSite.fppfToBigEtaleMorphism

Section84.7 Comparing fppf and étale topologies: modules #

Section 84.7 of the Stacks Project, Tag 0DGM. 4 tags here are carried by 7 declarations of the repository (all in StacksFrontier) and 8 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0DGN, a lemma

Tag 0DGN in the Stacks Project.

AlgebraicGeometry.Space.associatedSectionsEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigEtaleAssociatedModule.lean, line 303. The attribute's comment: “the value of the rule 𝓕 ↦ 𝓕ᵃ at an object (f : Y ⟶ X) of the big étale site of an algebraic space X is Γ(Y, f^*𝓕), the global sections of the inverse image of 𝓕 along f”.

The value of 𝓕ᵃ at (f : Y ⟶ X) is Γ(Y, f^*𝓕): the morphisms f^*𝒪_X ⟶ f^*𝓕 of 𝒪_Y-modules correspond to the global sections of f^*𝓕.

The inverse image of the structure sheaf is the structure sheaf (AlgebraicGeometry.Space.modulePullbackUnitIso), and a morphism out of the structure sheaf is a global section (CategoryTheory.SheafOfModules.unitHomEquiv).

noncomputable def associatedSectionsEquiv {X : AlgebraicSpaces B S hS}
    (F : Modules.{u, u} B S hS X.1 X.2) (Y : Over X) :
    ((modulePullback B S hS Y.hom).obj (SheafOfModules.unit _ :
          Modules.{u, u} B S hS X.1 X.2) ⟶
        (modulePullback B S hS Y.hom).obj F) ≃
      ((modulePullback B S hS Y.hom).obj F).sections

AlgebraicGeometry.BigEtaleSpaceSite.associatedPresheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigEtaleAssociatedModule.lean, line 351. The attribute's comment: “the construction of the rule 𝓕 ↦ 𝓕ᵃ as a presheaf of abelian groups on the big étale site of an algebraic space; none of the seven assertions the source makes about it”.

Stacks 0DGN, the rule 𝓕ᵃ on the big étale site of an algebraic space. For an 𝒪_X-module 𝓕 on the small étale site of an algebraic space X of a big étale space site of Stacks 0DBX, the presheaf of abelian groups on the category underlying the big étale site of X whose value at (f : Y ⟶ X) is Γ(Y, f^*𝓕).

This is AlgebraicGeometry.Space.associatedPresheaf read on that category; the identification of its value with Γ(Y, f^*𝓕) is AlgebraicGeometry.Space.associatedSectionsEquiv.

noncomputable def BigEtaleSpaceSite.associatedPresheaf {S : Scheme.{u}}
    (T : BigEtaleSpaceSite S) (X : T.Spaces)
    (F : Space.Modules.{u, u} T.fppfSite S T.fppf_mem X.1 X.2) :
    (Over X)ᵒᵖ ⥤ AddCommGrpCat.{u + 1}

AlgebraicGeometry.Space.isSheafFor_associatedPresheaf_of_isFpqcCovering, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigEtaleAssociatedModuleFpqcSheaf.lean, line 508. The attribute's comment: “(1): for 𝓕 a quasi-coherent 𝒪_X-module, 𝓕ᵃ satisfies the sheaf condition for every fpqc covering {U_i → U} of an object of (Spaces/X)_étale; the fppf and étale cases are isSheafFor_associatedPresheaf_of_isFppfCovering and isSheafFor_associatedPresheaf_of_isEtaleCovering”.

Stacks 0DGN, clause (1): 𝓕ᵃ is an fpqc sheaf. For a quasi-coherent 𝒪_X-module 𝓕 on an algebraic space X over S, the rule 𝓕ᵃ : (f : Y ⟶ X) ↦ Γ(Y, f^*𝓕) (AlgebraicGeometry.Space.associatedPresheaf) satisfies the sheaf condition for every family {Y i ⟶ Y} of morphisms of algebraic spaces over X which is an fpqc covering of Y.

This is AlgebraicGeometry.Space.isSheafFor_associatedPresheaf_ofArrows_overMk for the members (g i).left of the family, each Y i being the object Over.mk (Y i).hom of Over X.

theorem isSheafFor_associatedPresheaf_of_isFpqcCovering {Y : Over X} {Yi : I → Over X}
    (g : ∀ i, Yi i ⟶ Y) (F : Modules.{u, u} B S hS X.1 X.2) [F.IsQuasicoherentOnSite]
    (hg : IsFpqcCovering B S hS fun i ↦ (g i).left.hom) :
    (Presieve.ofArrows Yi g).IsSheafFor (associatedPresheaf F ⋙ forget AddCommGrpCat)

AlgebraicGeometry.BigEtaleSpaceSite.isSheaf_associatedPresheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigEtaleAssociatedModuleStatement.lean, line 70. The attribute's comment: “(1), a fortiori for étale coverings: 𝓕ᵃ is a sheaf on (Spaces/X)_étale, for 𝓕 a quasi-coherent 𝒪_X-module; the fpqc sheaf condition is Space.isSheafFor_associatedPresheaf_of_isFpqcCovering”.

The rule 𝓕ᵃ is a sheaf on (Spaces/X)_étale (the étale case of Stacks 0DGN, clause (1)). For a quasi-coherent 𝒪_X-module 𝓕 on an algebraic space X of a big étale site, the rule 𝓕ᵃ : (f : Y ⟶ X) ↦ Γ(Y, f^*𝓕) is a sheaf of abelian groups on the big étale site of X: it is isomorphic to the underlying presheaf of the sheaf of modules π_X^*𝓕 (clause (2)).

theorem BigEtaleSpaceSite.isSheaf_associatedPresheaf {S : Scheme.{u}} (T : BigEtaleSpaceSite S)
    (X : T.Spaces) (F : Space.Modules.{u, u} T.fppfSite S T.fppf_mem X.1 X.2)
    [F.IsQuasicoherentOnSite] :
    Presheaf.IsSheaf (T.bigEtaleTopology X) (T.associatedPresheaf X F)

AlgebraicGeometry.BigFppfSpaceSite.isSheaf_associatedPresheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigEtaleAssociatedModuleStatement.lean, line 86. The attribute's comment: “(1), a fortiori for fppf coverings: 𝓕ᵃ is a sheaf on (Spaces/X)_fppf, for 𝓕 a quasi-coherent 𝒪_X-module; the fpqc sheaf condition is Space.isSheafFor_associatedPresheaf_of_isFpqcCovering”.

The rule 𝓕ᵃ is a sheaf on (Spaces/X)_fppf (the fppf case of Stacks 0DGN, clause (1)). For a quasi-coherent 𝒪_X-module 𝓕 on an algebraic space X of a big fppf site, the rule 𝓕ᵃ : (f : Y ⟶ X) ↦ Γ(Y, f^*𝓕) is a sheaf of abelian groups on the big fppf site of X: it is isomorphic to the underlying presheaf of the sheaf of modules a_X^*𝓕 (clause (3)).

theorem BigFppfSpaceSite.isSheaf_associatedPresheaf {S : Scheme.{u}} (T : BigFppfSpaceSite S)
    (X : T.Spaces) (F : Space.Modules.{u, u} T.schemeSite S T.scheme_mem X.1 X.2)
    [F.IsQuasicoherentOnSite] :
    Presheaf.IsSheaf (BigFppfSpaceOver.topology T X) (Space.associatedPresheaf F)

Declarations registered for the tag:

BigEtaleSpaceSite.associatedPresheafIsoPullback registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigEtaleAssociatedModuleStatement.lean, line 94 (StacksFrontier): “(2): 𝓕ᵃ ≅ π_X^*𝓕 on (Spaces/X)_étale, for 𝓕 a quasi-coherent 𝒪_X-module read on the spaces-étale site through ι”.
BigFppfSpaceSite.nonempty_associatedPresheaf_iso_pullback registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigEtaleAssociatedModuleStatement.lean, line 98 (StacksFrontier): “(3): 𝓕ᵃ ≅ a_X^*𝓕 on (Spaces/X)_fppf, for 𝓕 a quasi-coherent 𝒪_X-module read on the spaces-étale site through ι”.
BigEtaleSpaceSite.quasicoherentPullbackEquivalence registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigEtaleAssociatedModuleStatement.lean, line 102 (StacksFrontier): “(4): 𝓕 ↦ 𝓕ᵃ = π_X^𝓕 is an equivalence between quasi-coherent 𝒪_X-modules and quasi-coherent modules on ((Spaces/X)_étale, 𝒪), with quasi-inverse π_{X,}”.
BigFppfSpaceSite.quasicoherentPullbackEquivalence registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigEtaleAssociatedModuleStatement.lean, line 106 (StacksFrontier): “(5): 𝓕 ↦ 𝓕ᵃ = a_X^𝓕 is an equivalence between quasi-coherent 𝒪_X-modules and quasi-coherent modules on ((Spaces/X)_fppf, 𝒪), with quasi-inverse a_{X,}”.
BigFppfSpaceSite.pushforward_pullback_of_quasicoherent registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigEtaleAssociatedModuleStatement.lean, line 110 (StacksFrontier): “(6): ε_{X,}a_X^𝓕 ≅ π_X^𝓕 and 𝓕 ≅ a_{X,}a_X^*𝓕 (the unit is an isomorphism) for 𝓕 a quasi-coherent 𝒪_X-module”.
BigFppfSpaceSite.isZero_rightDerived_pushforward_pullback_of_quasicoherent registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigEtaleAssociatedModuleStatement.lean, line 114 (StacksFrontier): “(7): R^i ε_{X,}(a_X^𝓕) = 0 and R^i a_{X,}(a_X^𝓕) = 0 for i > 0 and 𝓕 a quasi-coherent 𝒪_X-module”.

Tag 0DGP, a lemma

Tag 0DGP in the Stacks Project.

AlgebraicGeometry.BigFppfSpaceSite.isIso_bigEtalePullbackToPushforwardPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigFppfModuleRightAcyclicCanonical.lean, line 127. The attribute's comment: “(1) the canonical map π_X^𝓕 ⟶ ε_{X,}a_X^𝓕 (unit of ε_X^ ⊣ ε_{X,} and a_X = π_X ∘ ε_X) is an isomorphism, and ε_{X,}a_X^𝓕 ⟶ Rε_{X,}a_X^*𝓕 is an isomorphism”.

Stacks 0DGP: the map π_X^*𝓕 ⟶ Rε_{X,*}(a_X^*𝓕) is an isomorphism for a quasi-coherent 𝒪_X-module 𝓕: the canonical map π_X^*𝓕 ⟶ ε_{X,*}(a_X^*𝓕) is an isomorphism (Stacks 0DGN (6)) and a_X^*𝓕 is right acyclic for ε_{X,*} (Stacks 0DGN (7)), so that the canonical map ε_{X,*}(a_X^*𝓕) ⟶ Rε_{X,*}(a_X^*𝓕) is an isomorphism too.

theorem isIso_bigEtalePullbackToPushforwardPullback
    (F : SheafOfModules.{u + 1}
      (Stacks.SheafOfModules.Tensor.ringSheaf
        (Space.spacesEtaleRingedSite T.schemeSite S T.scheme_mem X).O))
    [hF : F.IsQuasicoherentOnSite] :
    IsIso (bigEtalePullbackToPushforwardPullback T E h X F) ∧
      Functor.rightAcyclic.{u + 2, u + 2}
        (fppfToBigEtaleRingedHom T E h X).toRingedToposSiteHom.pushforwardTopos
        ((fppfToSpacesEtaleRingedSiteHom T X).toRingedToposSiteHom.pullbackTopos.obj F)

Declarations registered for the tag:

AlgebraicGeometry.BigFppfSpaceSite.isIso_derivedPushforward_pullback_of_quasicoherent, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigFppfQuasicoherentTags.lean, line 28 (StacksFrontier): “both maps: π_X^𝓕 ≅ ε_{X,}a_X^𝓕 ⟶ Rε_{X,}a_X^𝓕 and 𝓕 ≅ a_{X,}a_X^𝓕 ⟶ Ra_{X,}a_X^*𝓕, the second map in each being the canonical (right acyclicity) isomorphism”.

Tag 0DGQ, a lemma

Tag 0DGQ in the Stacks Project.

Declarations registered for the tag:

AlgebraicGeometry.BigFppfSpaceSite.homology_pullback_of_quasicoherent, declared in the repository, registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigFppfQuasicoherentTags.lean, line 32 (StacksFrontier).

Tag 0DGR, a lemma

Tag 0DGR in the Stacks Project.

AlgebraicGeometry.BigFppfSpaceSite.isIso_derivedUnits_of_quasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigFppfToSmallEtaleDerivedUnitQuasicoherent.lean, line 173.

Stacks 0DGR. Let S be a scheme and X an algebraic space over S. For K in D_QCoh(𝒪_X), an object of D(X_{spaces,étale}, 𝒪_X) all of whose cohomology sheaves are quasi-coherent, the maps

Lπ_X^*K ⟶ Rε_{X,*}(La_X^*K) and K ⟶ Ra_{X,*}(La_X^*K)

are isomorphisms, where a_X = π_X ∘ ε_X : ((Spaces/X)_fppf, 𝒪) ⟶ (X_{spaces,étale}, 𝒪_X). The first map is the unit of Lε_X^* ⊣ Rε_{X,*} at Lπ_X^*K followed by Rε_{X,*} of the comparison Lε_X^*Lπ_X^*K ⟶ La_X^*K of Stacks 0D6D; the second is the unit of La_X^* ⊣ Ra_{X,*} at K.

theorem isIso_derivedUnits_of_quasicoherent
    (X : T.Spaces)
    (K : DerivedCategory (SheafOfModules.{u + 1} (Stacks.SheafOfModules.Tensor.ringSheaf
      (Space.spacesEtaleRingedSite E.fppfSite S E.fppf_mem (etaleSpace T E h X)).O)))
    (hK : ∀ i : ℤ, ((DerivedCategory.homologyFunctor _ i).obj K).IsQuasicoherentOnSite) :
    IsIso ((derivedAdjunction (epsilonHom T E h X)
        (fppfToBigEtaleRingedHom T E h X).isMorphismOfSites).unit.app
          ((derivedPullback (BigEtaleSpaceSite.spacesEtaleRestrictionRingedSiteHom E
            (etaleSpace T E h X)).toRingedToposSiteHom).obj K) ≫
      (derivedPushforward (epsilonHom T E h X)).map
        ((derivedPullbackCompComparison (epsilonHom T E h X)
          (BigEtaleSpaceSite.spacesEtaleRestrictionRingedSiteHom E
            (etaleSpace T E h X)).toRingedToposSiteHom).app K)) ∧
    IsIso ((derivedAdjunction ((BigEtaleSpaceSite.spacesEtaleRestrictionRingedSiteHom E
        (etaleSpace T E h X)).toRingedToposSiteHom.comp (epsilonHom T E h X))
        (RingedToposSiteHom.isMorphismOfSites_comp_u _ _
          (fppfToBigEtaleRingedHom T E h X).isMorphismOfSites
          (BigEtaleSpaceSite.spacesEtaleRestrictionRingedSiteHom E
            (etaleSpace T E h X)).isMorphismOfSites)).unit.app K)

Sources

LeanAlgebraicGeometry.Space.associatedSectionsEquiv · AlgebraicGeometry.BigEtaleSpaceSite.associatedPresheaf · AlgebraicGeometry.Space.isSheafFor_associatedPresheaf_of_isFpqcCovering · AlgebraicGeometry.BigEtaleSpaceSite.isSheaf_associatedPresheaf · AlgebraicGeometry.BigFppfSpaceSite.isSheaf_associatedPresheaf · BigEtaleSpaceSite.associatedPresheafIsoPullback · BigFppfSpaceSite.nonempty_associatedPresheaf_iso_pullback · BigEtaleSpaceSite.quasicoherentPullbackEquivalence

Section84.8 Comparing ph and étale topologies #

Section 84.8 of the Stacks Project, Tag 0DGS. 5 tags here are carried by 17 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0DGT, a lemma

Tag 0DGT in the Stacks Project.

AlgebraicGeometry.BigPHSpaceSite.isIso_phToBigEtale_unit_app_inverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigPhSmallEtalePullbackSheaf.lean, line 134. The attribute's comment: “part (1), the equality ε_{X,*}a_X⁻¹ℱ = π_X⁻¹ℱ”.

Stacks 0DGT, part (1), ε_{X,*}a_X⁻¹ℱ = π_X⁻¹ℱ. For a sheaf of sets ℱ on X_étale the unit π_X⁻¹ℱ ⟶ ε_{X,*}ε_X⁻¹π_X⁻¹ℱ = ε_{X,*}a_X⁻¹ℱ is an isomorphism.

theorem isIso_phToBigEtale_unit_app_inverseImage
    (X : P.Spaces)
    (ℱ : Sheaf (Space.SpacesEtale.topology E.fppfSite S E.fppf_mem (etaleSpace P E h X))
      (Type (u + 1))) :
    IsIso ((phToBigEtaleMorphism P E h X).adj.unit.app
      ((E.bigToSmallEtaleMorphism (etaleSpace P E h X)).inverseImage.obj ℱ))

AlgebraicGeometry.BigPHSpaceSite.isIso_phToSmallEtale_unit_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigPhSmallEtalePullbackSheaf.lean, line 147. The attribute's comment: “part (1), the equality a_{X,*}a_X⁻¹ℱ = ℱ”.

Stacks 0DGT, part (1), a_{X,*}a_X⁻¹ℱ = ℱ. For a sheaf of sets ℱ on X_étale the unit ℱ ⟶ a_{X,*}a_X⁻¹ℱ is an isomorphism. It is the unit of π_X⁻¹ ⊣ π_{X,*}, an isomorphism by Stacks 0DF3, followed by π_{X,*} of the unit of ε_X⁻¹ ⊣ ε_{X,*} at π_X⁻¹ℱ.

theorem isIso_phToSmallEtale_unit_app
    (X : P.Spaces)
    (ℱ : Sheaf (Space.SpacesEtale.topology E.fppfSite S E.fppf_mem (etaleSpace P E h X))
      (Type (u + 1))) :
    IsIso ((phToSmallEtaleMorphism P E h X).adj.unit.app ℱ)

AlgebraicGeometry.BigPHSpaceSite.isZero_rightDerived_phToBigEtale_abelianInverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigPhSmallEtaleTorsionVanishing.lean, line 75. The attribute's comment: “part (2)”.

Stacks 0DGT, part (2). Let X be an algebraic space and ℱ a torsion abelian sheaf on X_étale. Then R^i ε_{X,*}(a_X⁻¹ℱ) = 0 for i > 0. Here ε_X : (Spaces/X)_ph ⟶ (Spaces/X)_étale is the comparison of Stacks 0DGW, ε_{X,*} is restriction of abelian sheaves along the identity-on-spaces functor of slices, a_X⁻¹ is the abelian inverse image (Stacks 04JC) of a_X = π_X ∘ ε_X, and R^i is the right derived functor.

public theorem isZero_rightDerived_phToBigEtale_abelianInverseImage (X : P.Spaces)
    (ℱ : Sheaf (Space.SpacesEtale.topology E.fppfSite S E.fppf_mem (etaleSpace P E h X))
      AddCommGrpCat.{u + 1})
    (hℱ : Stacks.Torsion.torsionSheafProperty
      (Space.SpacesEtale.topology E.fppfSite S E.fppf_mem (etaleSpace P E h X)) ℱ)
    (i : ℕ) (hi : 0 < i) :
    IsZero (((phToBigEtaleAbelianPushforward P E h X).rightDerived i).obj
      ((phToSmallEtaleAbelianInverseImage P E h X).obj ℱ))

Tag 0DGU, a lemma

Tag 0DGU in the Stacks Project.

AlgebraicGeometry.BigPHSpaceSite.isIso_phToSmallEtale_derivedUnits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigPhToSmallEtaleDerivedTorsion.lean, line 147.

Let X be an algebraic space over S and K an object of D⁺(X_étale) whose cohomology sheaves are torsion. Then the maps π_X⁻¹K ⟶ Rε_{X,*}a_X⁻¹K and K ⟶ Ra_{X,*}a_X⁻¹K are isomorphisms, for the comparison morphisms ε_X and a_X = π_X ∘ ε_X from the big ph topos of X (Stacks 0DGW). The two maps are the units of the derived adjunctions ε_X⁻¹ ⊣ Rε_{X,*} at π_X⁻¹K and a_X⁻¹ ⊣ Ra_{X,*} at K on bounded below derived categories.

theorem isIso_phToSmallEtale_derivedUnits
    (K : DerivedCategory.Plus (Sheaf (Space.SpacesEtale.topology E.fppfSite S E.fppf_mem
      (etaleSpace P E h X)) AddCommGrpCat.{u + 1}))
    (hK : ∀ i : ℤ, Stacks.Torsion.torsionSheafProperty _
      ((DerivedCategory.homologyFunctor _ i).obj (DerivedCategory.Plus.ι.obj K))) :
    IsIso ((Stacks.ComparingTopologies.derivedPlusAdjunction
        (phToBigEtaleAbelianAdjunction P E h X)).unit.app
          ((CategoryTheory.Sites.abelianInverseImage
            (E.bigToSmallEtaleMorphism (etaleSpace P E h X))).mapDerivedCategoryPlus.obj K)) ∧
      IsIso ((Stacks.ComparingTopologies.derivedPlusAdjunction
        (phToSmallEtaleAbelianAdjunction P E h X)).unit.app K)

Tag 0DGV, a lemma

Tag 0DGV in the Stacks Project.

AlgebraicGeometry.BigPHSpaceSite.etaleCohomologyDerivedIsoOfTorsion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigPhToSmallEtaleCohomology.lean, line 146. The attribute's comment: “(2)”.

Stacks 0DGV, part (2). For K in D⁺(X_étale) whose cohomology sheaves are torsion, H^q(X_étale, K) = H^q_ph(X, a_X⁻¹K) for every q, by the canonical map AlgebraicGeometry.BigPHSpaceSite.etaleToPhDerivedGlobalSections.

def etaleCohomologyDerivedIsoOfTorsion
    (K : DerivedCategory.Plus (Sheaf (Space.SpacesEtale.topology E.fppfSite S E.fppf_mem
      (etaleSpace P E h X)) AddCommGrpCat.{u + 1}))
    (hK : ∀ i : ℤ, Stacks.Torsion.torsionSheafProperty _
      ((DerivedCategory.homologyFunctor _ i).obj (DerivedCategory.Plus.ι.obj K))) (q : ℤ) :
    (DerivedCategory.Plus.homologyFunctor AddCommGrpCat.{u + 1} q).obj
        ((etaleGlobalSections P E h X).rightDerivedFunctorPlus.obj K) ≅
      (DerivedCategory.Plus.homologyFunctor AddCommGrpCat.{u + 1} q).obj
        ((phGlobalSections P X).rightDerivedFunctorPlus.obj
          ((CategoryTheory.Sites.abelianInverseImage
            (phToSmallEtaleMorphism P E h X)).mapDerivedCategoryPlus.obj K))

AlgebraicGeometry.BigPHSpaceSite.etaleCohomologyIsoOfTorsion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigPhToSmallEtaleCohomology.lean, line 164. The attribute's comment: “(1)”.

Stacks 0DGV, part (1). For a torsion abelian sheaf F on X_étale, H^q(X_étale, F) = H^q_ph(X, a_X⁻¹F) for every q.

def etaleCohomologyIsoOfTorsion
    (F : Sheaf (Space.SpacesEtale.topology E.fppfSite S E.fppf_mem (etaleSpace P E h X))
      AddCommGrpCat.{u + 1})
    (hF : Stacks.Torsion.torsionSheafProperty _ F) (q : ℕ) :
    ((etaleGlobalSections P E h X).rightDerived q).obj F ≅
      ((phGlobalSections P X).rightDerived q).obj
        ((CategoryTheory.Sites.abelianInverseImage (phToSmallEtaleMorphism P E h X)).obj F)

AlgebraicGeometry.BigPHSpaceSite.etaleCohomologyConstantIsoOfTorsion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigPhToSmallEtaleCohomology.lean, line 182. The attribute's comment: “the example of a torsion abelian group”.

The example of Stacks 0DGV. For a torsion abelian group A, H^q_étale(X, A) = H^q_ph(X, A) for the constant sheaves.

def etaleCohomologyConstantIsoOfTorsion (A : AddCommGrpCat.{u + 1}) (hA : IsAddTorsion A)
    (q : ℕ) :
    ((etaleGlobalSections P E h X).rightDerived q).obj
        ((constantSheaf (Space.SpacesEtale.topology E.fppfSite S E.fppf_mem (etaleSpace P E h X))
          AddCommGrpCat.{u + 1}).obj A) ≅
      ((phGlobalSections P X).rightDerived q).obj
        ((constantSheaf (BigPHSpaceOver.topology P X) AddCommGrpCat.{u + 1}).obj A)

Tag 0DGW, a lemma

Tag 0DGW in the Stacks Project.

AlgebraicGeometry.BigPHSpaceSite.phToBigEtaleMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigPhToSmallEtale.lean, line 192. The attribute's comment: “the comparison morphism ε from the big ph to the big étale topos”.

Stacks 0DGW. The change-of-topology morphism ε_X from the big ph topos of X to its big étale topos: the identity-on-spaces functor of slice categories is a morphism of sites, because it is continuous and representably flat.

def phToBigEtaleMorphism (X : P.Spaces) :
    MorphismOfTopoi (Sheaf (BigPHSpaceOver.topology P X) (Type (u + 1)))
      (Sheaf (E.bigEtaleTopology (etaleSpace P E h X)) (Type (u + 1)))

AlgebraicGeometry.BigPHSpaceSite.phToSmallEtaleMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigPhToSmallEtale.lean, line 230. The attribute's comment: “the comparison morphism a to the small étale topos, as the composite π ∘ ε”.

Stacks 0DGW. The morphism a_X from the big ph topos of X to its small étale topos, defined as the composite of ε_X with the big-to-small étale morphism π_X of Stacks 0DF3. The factorization a_X = π_X ∘ ε_X asserted by Stacks 0DGW is therefore definitional.

def phToSmallEtaleMorphism (X : P.Spaces) :
    MorphismOfTopoi (Sheaf (BigPHSpaceOver.topology P X) (Type (u + 1)))
      (Sheaf (Space.SpacesEtale.topology E.fppfSite S E.fppf_mem (etaleSpace P E h X))
        (Type (u + 1)))

AlgebraicGeometry.BigPHSpaceSite.bigPHBigEtale_pushforwardCommIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigPhToSmallEtale.lean, line 239. The attribute's comment: “the big ph–big étale square”.

Stacks 0DGW, the first diagram. For a morphism f : Y ⟶ X of algebraic spaces the direct images of ε_X ∘ f_{big, ph} and of f_{big, étale} ∘ ε_Y are canonically isomorphic.

def bigPHBigEtale_pushforwardCommIso {X Y : P.Spaces} (f : Y ⟶ X) :
    ((E.bigEtaleMorphism (etaleMap P E h f)).comp (phToBigEtaleMorphism P E h Y)).pushforward ≅
      ((phToBigEtaleMorphism P E h X).comp (bigPHMorphism P f)).pushforward

AlgebraicGeometry.BigPHSpaceSite.bigPHSmallEtale_pushforwardCommIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigPhToSmallEtale.lean, line 298. The attribute's comment: “the big ph–small étale square”.

Stacks 0DGW, the second diagram. For a morphism f : Y ⟶ X of algebraic spaces the direct images of a_X ∘ f_{big, ph} and of f_{small} ∘ a_Y are canonically isomorphic.

Since a is the composite of ε with π, this is the big square above pasted with the big–small étale square of Stacks 0DF6.

def bigPHSmallEtale_pushforwardCommIso {X Y : P.Spaces} (f : Y ⟶ X) :
    ((E.smallEtaleMorphism (etaleMap P E h f)).comp
        (phToSmallEtaleMorphism P E h Y)).pushforward ≅
      ((phToSmallEtaleMorphism P E h X).comp (bigPHMorphism P f)).pushforward

AlgebraicGeometry.BigPHSpaceSite.bigPHSmallEtaleCharts_pushforwardCommIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigPhToSmallEtale.lean, line 435. The attribute's comment: “the big ph–small étale square, for the small étale site of scheme charts”.

Stacks 0DGW, the second diagram, for the presentation of the small étale topos by the site of scheme charts. For a morphism f : X ⟶ Y of algebraic spaces of the ph site the direct images of f_{small} ∘ a_X and of a_Y ∘ f_{big, ph} are canonically isomorphic, where a is restriction along the chart functor smallEtaleToPH. No big étale site intervenes.

def bigPHSmallEtaleCharts_pushforwardCommIso {X Y : P.Spaces} (f : X ⟶ Y) :
    ((smallEtaleToPH P X).sheafPushforwardContinuous (Type (u + 1))
        (Space.SmallEtale.topology P.fppfSite S P.fppf_mem X.1)
        (BigPHSpaceOver.topology P X)) ⋙
      (Space.smallToposMorphism P.fppfSite S P.fppf_mem f).pushforward ≅
    (bigPHMorphism P f).pushforward ⋙
      (smallEtaleToPH P Y).sheafPushforwardContinuous (Type (u + 1))
        (Space.SmallEtale.topology P.fppfSite S P.fppf_mem Y.1)
        (BigPHSpaceOver.topology P Y)

AlgebraicGeometry.BigPHSpaceSite.bigPHBigEtale_inverseImageCommIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigPhToSmallEtaleInverseImage.lean, line 69. The attribute's comment: “the big ph–big étale square, on inverse images”.

The first diagram, on inverse images. For a morphism f : Y ⟶ X of algebraic spaces the inverse images of ε_X ∘ f_{big, ph} and of f_{big, étale} ∘ ε_Y are canonically isomorphic: f_{big, ph}⁻¹ ∘ ε_X⁻¹ ≅ ε_Y⁻¹ ∘ f_{big, étale}⁻¹. It is the conjugate of the direct-image isomorphism bigPHBigEtale_pushforwardCommIso.

def bigPHBigEtale_inverseImageCommIso {X Y : P.Spaces} (f : Y ⟶ X) :
    ((phToBigEtaleMorphism P E h X).comp (bigPHMorphism P f)).inverseImage ≅
      ((E.bigEtaleMorphism (etaleMap P E h f)).comp (phToBigEtaleMorphism P E h Y)).inverseImage

AlgebraicGeometry.BigPHSpaceSite.bigPHSmallEtale_inverseImageCommIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigPhToSmallEtaleInverseImage.lean, line 92. The attribute's comment: “the big ph–small étale square, on inverse images”.

The second diagram, on inverse images. For a morphism f : Y ⟶ X of algebraic spaces the inverse images of a_X ∘ f_{big, ph} and of f_{small} ∘ a_Y are canonically isomorphic: f_{big, ph}⁻¹ ∘ a_X⁻¹ ≅ a_Y⁻¹ ∘ f_{small}⁻¹, where a = π ∘ ε. It is the conjugate of the direct-image isomorphism bigPHSmallEtale_pushforwardCommIso.

def bigPHSmallEtale_inverseImageCommIso {X Y : P.Spaces} (f : Y ⟶ X) :
    ((phToSmallEtaleMorphism P E h X).comp (bigPHMorphism P f)).inverseImage ≅
      ((E.smallEtaleMorphism (etaleMap P E h f)).comp
        (phToSmallEtaleMorphism P E h Y)).inverseImage

AlgebraicGeometry.BigPHSpaceSite.bigPHSmallEtaleCharts_inverseImageCommIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigPhToSmallEtaleInverseImage.lean, line 134. The attribute's comment: “the big ph–small étale square, for the small étale site of scheme charts, on inverse images”.

The second diagram on inverse images, for the presentation of the small étale topos by the site of scheme charts. For a morphism f : X ⟶ Y of algebraic spaces of the ph site, with a the restriction along the chart functor smallEtaleToPH and a⁻¹ its left adjoint, f_{big, ph}⁻¹ ∘ a_Y⁻¹ ≅ a_X⁻¹ ∘ f_{small}⁻¹. It is the conjugate of the direct-image isomorphism bigPHSmallEtaleCharts_pushforwardCommIso.

def bigPHSmallEtaleCharts_inverseImageCommIso {X Y : P.Spaces} (f : X ⟶ Y) :
    (smallEtaleToPH P Y).sheafPullback (Type (u + 1))
        (Space.SmallEtale.topology P.fppfSite S P.fppf_mem Y.1)
        (BigPHSpaceOver.topology P Y) ⋙ (bigPHMorphism P f).inverseImage ≅
      (Space.smallToposMorphism P.fppfSite S P.fppf_mem f).inverseImage ⋙
        (smallEtaleToPH P X).sheafPullback (Type (u + 1))
          (Space.SmallEtale.topology P.fppfSite S P.fppf_mem X.1)
          (BigPHSpaceOver.topology P X)

Tag 0DGX, a lemma

Tag 0DGX in the Stacks Project.

AlgebraicGeometry.BigPHSpaceSite.phToSmallEtaleDerivedPushforwardIsoOfIsProper, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigPhSmallEtaleProperDerivedPushforward.lean, line 247. The attribute's comment: “(2)”.

Stacks 0DGX, part (2). Let f : Y ⟶ X be a proper morphism of algebraic spaces over S and K an object of D⁺(Y_étale) whose cohomology sheaves are torsion. Then a_X⁻¹(Rf_{small,*}K) = Rf_{big,ph,*}(a_Y⁻¹K), by the canonical comparison AlgebraicGeometry.BigPHSpaceSite.phToSmallEtaleDerivedBaseChange.

def phToSmallEtaleDerivedPushforwardIsoOfIsProper
    (hf : Space.IsProper P.fppfSite S P.fppf_mem f.hom)
    (K : DerivedCategory.Plus (Sheaf (Space.SpacesEtale.topology E.fppfSite S E.fppf_mem
      (etaleSpace P E h Y)) AddCommGrpCat.{u + 1}))
    (hK : ∀ i : ℤ, Stacks.Torsion.torsionSheafProperty _
      ((DerivedCategory.homologyFunctor _ i).obj (DerivedCategory.Plus.ι.obj K))) :
    (CategoryTheory.Sites.abelianInverseImage
        (phToSmallEtaleMorphism P E h X)).mapDerivedCategoryPlus.obj
        ((E.smallEtalePushforward (etaleMap P E h f)).rightDerivedFunctorPlus.obj K) ≅
      (phAbelianPushforward P f).rightDerivedFunctorPlus.obj
        ((CategoryTheory.Sites.abelianInverseImage
          (phToSmallEtaleMorphism P E h Y)).mapDerivedCategoryPlus.obj K)

AlgebraicGeometry.BigPHSpaceSite.phToSmallEtalePushforwardIsoOfIsProper, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Topologies/BigPhSmallEtaleProperPushforward.lean, line 224. The attribute's comment: “(1)”.

Stacks 0DGX, part (1). Let f : Y ⟶ X be a proper morphism of algebraic spaces over S, and let a = π ∘ ε be the comparison morphisms from the big ph topoi to the small étale topoi of Stacks 0DGW. Then a_X⁻¹ ∘ f_{small,*} = f_{big,ph,*} ∘ a_Y⁻¹ as functors from sheaves on the small étale site of Y to sheaves on the big ph site of X: the canonical base change map AlgebraicGeometry.BigPHSpaceSite.phToSmallEtaleBaseChange, the mate of the commutative square of Stacks 0DGW, is an isomorphism.

def phToSmallEtalePushforwardIsoOfIsProper
    (hf : Space.IsProper P.fppfSite S P.fppf_mem f.hom) :
    (E.smallEtaleMorphism (etaleMap P E h f)).pushforward ⋙
        (phToSmallEtaleMorphism P E h X).inverseImage ≅
      (phToSmallEtaleMorphism P E h Y).inverseImage ⋙ (bigPHMorphism P f).pushforward

Sources

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

84 More on Cohomology of Spaces

Section84.3 Transporting results from schemes#

Tag 0DFV, a lemma

Sources

Section84.4 Proper base change#

Tag 0DFX, a lemma

Tag 0DFY, a lemma

Tag 0DFZ, a lemma

Tag 0DG0, a lemma

Tag 0DG1, a lemma

Tag 0DG2, a theorem

Tag 0DG3, a lemma

Tag 0DG4, a lemma

Tag 0DG5, a lemma

Sources

Section84.5 Comparing big and small topoi#

Tag 0DG7, a lemma

Tag 0DG8, a lemma

Tag 0DG9, an equation

Tag 0DGA, a lemma

Tag 0DGB, a lemma

Tag 0DGC, a lemma

Tag 0DGD, a lemma

Sources

Section84.6 Comparing fppf and étale topologies#

Tag 0DGF, a lemma

Tag 0DGG, a lemma

Tag 0DGH, a lemma

Tag 0DGI, a lemma

Tag 0DGJ, a lemma

Tag 0DGK, a lemma

Tag 0DGL, a lemma

Sources

Section84.7 Comparing fppf and étale topologies: modules#

Tag 0DGN, a lemma

Tag 0DGP, a lemma

Tag 0DGQ, a lemma

Tag 0DGR, a lemma

Sources

Section84.8 Comparing ph and étale topologies#

Tag 0DGT, a lemma

Tag 0DGU, a lemma

Tag 0DGV, a lemma

Tag 0DGW, a lemma

Tag 0DGX, a lemma

Sources

Section84.3 Transporting results from schemes #

Section84.4 Proper base change #

Section84.5 Comparing big and small topoi #

Section84.6 Comparing fppf and étale topologies #

Section84.7 Comparing fppf and étale topologies: modules #

Section84.8 Comparing ph and étale topologies #