96.3 Presheaves to 96.15 Quasi-coherent sheaves on…

Section96.3 Presheaves#

Section 96.3 of the Stacks Project, Tag 06TI. 4 tags here are carried by 17 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06TJ, a definition

Tag 06TJ in the Stacks Project.

Declarations registered for the tag:

Tag 06TK, an equation

Tag 06TK in the Stacks Project.

AlgebraicGeometry.BigFppfOver.presheafAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AssociatedMorphismOfTopoi.lean, line 77. The attribute's comment: “presheaf pullback f^p, pushforward {}_pf, and the adjunction f^p ⊣ {}_pf”.

Stacks 06TK, the pullback and pushforward of presheaves and their adjointness. For a 1-morphism G : 𝒳 ⟶ 𝒴 of categories fibred in groupoids over the big fppf category of S, the pullback G^p : PSh(𝒴) ⥤ PSh(𝒳) of presheaves of sets is precomposition with G.op, so that G^p 𝒢 (x) = 𝒢 (G x) by definition, and the pushforward {}_pG : PSh(𝒳) ⥤ PSh(𝒴) is the right Kan extension along G.op; G^p is left adjoint to {}_pG.

noncomputable def presheafAdjunction :
    (Functor.whiskeringLeft _ _ (Type max v w t)).obj (CatFiberedInGroupoids.homFunctor G).op ⊣
      (CatFiberedInGroupoids.homFunctor G).op.ran

AlgebraicGeometry.BigFppfOver.presheafPushforwardObjObjIsoLimit, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AssociatedMorphismOfTopoi.lean, line 87. The attribute's comment: “the formula ({}_pf F)(y) = lim_{f(x) -> y} F(x) for the pushforward”.

Stacks 06TK, the formula ({}_pG ℱ)(y) = lim_{G(x) → y} ℱ(x) for the pushforward of a presheaf of sets ℱ on 𝒳 along a 1-morphism G : 𝒳 ⟶ 𝒴 of categories fibred in groupoids over the big fppf category of S, at an object y of 𝒴: the limit is indexed by the pairs of an object x of 𝒳 and a morphism G(x) → y.

noncomputable def presheafPushforwardObjObjIsoLimit (ℱ : 𝒳.val.objᵒᵖ ⥤ Type (max v w t))
    (y : 𝒴.val.obj) :
    ((CatFiberedInGroupoids.homFunctor G).op.ran.obj ℱ).obj (Opposite.op y) ≅
      Limits.limit (StructuredArrow.proj (Opposite.op y) (CatFiberedInGroupoids.homFunctor G).op ⋙
        ℱ)
Tag 06TL, a lemma

Tag 06TL in the Stacks Project.

CategoryTheory.Functor.ranOpCompIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInGroupoids/PresheafComp.lean, line 188. The attribute's comment: “the canonical isomorphism of pushforwards”.

Stacks 06TL: the canonical isomorphism {}_p(g ∘ f) ≅ {}_pg ∘ {}_pf of functors PSh(𝒳) ⥤ PSh(𝒵), namely the comparison of the two right adjoints {}_p(g ∘ f) and {}_pg ∘ {}_pf of (g ∘ f)^p = f^p ∘ g^p.

noncomputable def ranOpCompIso : (f ⋙ g).op.ran (H := A) ≅ f.op.ran ⋙ g.op.ran

CategoryTheory.Functor.homEquiv_comp_ranOpCompIso_hom_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInGroupoids/PresheafComp.lean, line 196. The attribute's comment: “compatibility of the canonical isomorphism with adjointness”.

Stacks 06TL: the isomorphism {}_p(g ∘ f) ≅ {}_pg ∘ {}_pf is compatible with adjointness of (f^p, {}_pf), (g^p, {}_pg) and ((g ∘ f)^p, {}_p(g ∘ f)): the square of hom-set bijections Mor(f^p g^p K, F) = Mor(g^p K, {}_pf F) = Mor(K, {}_pg {}_pf F) and Mor((g ∘ f)^p K, F) = Mor(K, {}_p(g ∘ f) F) commutes.

theorem homEquiv_comp_ranOpCompIso_hom_app (K : Zᵒᵖ ⥤ A) (F : Xᵒᵖ ⥤ A)
    (α : (f ⋙ g).op ⋙ K ⟶ F) :
    ((f ⋙ g).op.ranAdjunction A).homEquiv K F α ≫ (ranOpCompIso A f g).hom.app F =
      (ranCompAdjunction A f.op g.op).homEquiv K F α

Declarations registered for the tag:

Tag 06TM, a lemma

Tag 06TM in the Stacks Project.

CategoryTheory.CatFiberedInGroupoids.isIso_underlyingNatTrans_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Presheaves.lean, line 109. The attribute's comment: “invertibility of the two-morphism”.

Stacks 06TM. Every component of a two-morphism of categories fibred in groupoids lies over an identity, hence is invertible.

theorem isIso_underlyingNatTrans_app {f g : 𝒳 ⟶ 𝒴} (t : f ⟶ g) (x : 𝒳.based.obj) :
    IsIso (t.hom.toNatTrans.app x)

CategoryTheory.CatFiberedInGroupoids.pullbackIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Presheaves.lean, line 145. The attribute's comment: “canonical isomorphism on restriction functors”.

Stacks 06TM. Pullback of presheaves along the isomorphism of functors underlying a two-morphism, contravariant in the two-morphism.

noncomputable def pullbackIso :
    (whiskeringLeft 𝒳.based.objᵒᵖ 𝒴.based.objᵒᵖ A).obj
        (homFunctorOp g) ≅
      (whiskeringLeft 𝒳.based.objᵒᵖ 𝒴.based.objᵒᵖ A).obj
        (homFunctorOp f)

CategoryTheory.CatFiberedInGroupoids.pullbackIso_hom_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Presheaves.lean, line 155. The attribute's comment: “pointwise description of restriction”.

Stacks 06TM. On a presheaf and an object, the restriction comparison is evaluation on the component of the given two-morphism.

theorem pullbackIso_hom_app (P : 𝒴.based.objᵒᵖ ⥤ A) (x : 𝒳.based.obj) :
    ((pullbackIso A t).hom.app P).app (Opposite.op x) =
      P.map (t.hom.toNatTrans.app x).op

CategoryTheory.CatFiberedInGroupoids.pullbackIso_trans, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Presheaves.lean, line 163. The attribute's comment: “vertical composition on restriction”.

Stacks 06TM. Vertical composition of two-morphisms becomes composition of the induced restriction isomorphisms, in reverse order.

theorem pullbackIso_trans {h : 𝒳 ⟶ 𝒴} (s : g ⟶ h) :
    pullbackIso A (t ≫ s) = pullbackIso A s ≪≫ pullbackIso A t

CategoryTheory.CatFiberedInGroupoids.pullbackIso_hcomp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Presheaves.lean, line 176. The attribute's comment: “horizontal composition on restriction”.

Stacks 06TM. The restriction comparison for a horizontal composite acts pointwise by the two component maps, in the contravariant order.

theorem pullbackIso_hcomp {𝒵 : CatFiberedInGroupoids.{v₀, v₁, u₀, u₁} B}
    {h k : 𝒴 ⟶ 𝒵} (s : h ⟶ k) (P : 𝒵.based.objᵒᵖ ⥤ A) (x : 𝒳.based.obj) :
    ((pullbackIso (f := f ≫ h) (g := g ≫ k) A
      (Bicategory.whiskerRight t h ≫ Bicategory.whiskerLeft g s)).hom.app P).app
        (Opposite.op x) =
      P.map (s.hom.toNatTrans.app ((CatFiberedInGroupoids.homFunctor g).obj x)).op ≫
        P.map ((CatFiberedInGroupoids.homFunctor h).map (t.hom.toNatTrans.app x)).op

CategoryTheory.CatFiberedInGroupoids.pushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Presheaves.lean, line 225. The attribute's comment: “canonical isomorphism on right adjoints”.

Stacks 06TM. Direct image of presheaves along the isomorphism of functors underlying a two-morphism, obtained as the adjoint mate of the pullback isomorphism.

noncomputable def pushforwardIso :
    (homFunctorOp f).ran (H := A) ≅
      (homFunctorOp g).ran (H := A)

CategoryTheory.CatFiberedInGroupoids.pushforwardIso_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Presheaves.lean, line 234. The attribute's comment: “compatibility with adjunction”.

Stacks 06TM. The direct-image comparison is the mate of the restriction comparison, expressing compatibility with both adjunctions.

theorem pushforwardIso_hom :
    (pushforwardIso A t).hom =
      conjugateEquiv ((homFunctorOp f).ranAdjunction A)
        ((homFunctorOp g).ranAdjunction A)
        (pullbackIso A t).hom

CategoryTheory.CatFiberedInGroupoids.pushforwardIso_trans, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Presheaves.lean, line 243. The attribute's comment: “vertical composition on right adjoints”.

Stacks 06TM. Vertical composition of two-morphisms becomes composition of the corresponding direct-image isomorphisms.

theorem pushforwardIso_trans {h : 𝒳 ⟶ 𝒴} (s : g ⟶ h)
    [∀ (F : 𝒳.based.objᵒᵖ ⥤ A),
      (homFunctorOp h).HasRightKanExtension F] :
    pushforwardIso A (t ≫ s) = pushforwardIso A t ≪≫ pushforwardIso A s

CategoryTheory.CatFiberedInGroupoids.pushforwardIso_hcomp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Presheaves.lean, line 256. The attribute's comment: “horizontal composition on right adjoints”.

Stacks 06TM. The direct-image comparison for a horizontal composite, after identifying direct images of composites with successive direct images, is the horizontal composite of the two direct-image comparisons.

theorem pushforwardIso_hcomp {𝒵 : CatFiberedInGroupoids.{v₀, v₁, u₀, u₁} B}
    {h k : 𝒴 ⟶ 𝒵} (s : h ⟶ k)
    [∀ (P : 𝒴.based.objᵒᵖ ⥤ A),
      (homFunctorOp h).HasRightKanExtension P]
    [∀ (P : 𝒴.based.objᵒᵖ ⥤ A),
      (homFunctorOp k).HasRightKanExtension P]
    [∀ (F : 𝒳.based.objᵒᵖ ⥤ A),
      (homFunctorOp (f ≫ h)).HasRightKanExtension F]
    [∀ (F : 𝒳.based.objᵒᵖ ⥤ A),
      (homFunctorOp (g ≫ k)).HasRightKanExtension F]
    [∀ (F : 𝒳.based.objᵒᵖ ⥤ A),
      ((homFunctorOp f) ⋙
        (homFunctorOp h)).HasRightKanExtension F]
    [∀ (F : 𝒳.based.objᵒᵖ ⥤ A),
      ((homFunctorOp g) ⋙
        (homFunctorOp k)).HasRightKanExtension F] :
    pushforwardIso A (Bicategory.whiskerRight t h ≫ Bicategory.whiskerLeft g s) ≪≫
        ranCompIso (homFunctorOp g)
          (homFunctorOp k) A =
      ranCompIso (homFunctorOp f)
          (homFunctorOp h) A ≪≫
        Functor.isoWhiskerRight (pushforwardIso A t)
          ((homFunctorOp h).ran (H := A)) ≪≫
        Functor.isoWhiskerLeft ((homFunctorOp g).ran (H := A))
        (pushforwardIso A s)

CategoryTheory.CatFiberedInGroupoids.pushforwardIsoOfSets, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/PresheavesOfSets.lean, line 77. The attribute's comment: “canonical isomorphism of direct images of presheaves of sets”.

Stacks 06TM. The canonical isomorphism {}_pt : {}_pf ≅ {}_pg of direct images of presheaves of sets induced by a two-morphism t : f ⟶ g, namely the mate of the restriction comparison t^p : g^p ≅ f^p for the adjunctions (f^p, {}_pf) and (g^p, {}_pg). The direct images exist by instance search: Mathlib's pointwise right Kan extension, computed by limits in Type (max u₁ v₁ w).

noncomputable def pushforwardIsoOfSets :
    (homFunctorOp f).ran (H := Type (max u₁ v₁ w)) ≅ (homFunctorOp g).ran

CategoryTheory.CatFiberedInGroupoids.pushforwardIsoOfSets_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/PresheavesOfSets.lean, line 85. The attribute's comment: “compatibility with adjointness, for presheaves of sets”.

Stacks 06TM. The isomorphism {}_pt of direct images of presheaves of sets is compatible with adjointness of (f^p, {}_pf) and (g^p, {}_pg): it is the conjugate of t^p : g^p ≅ f^p for the two adjunctions.

theorem pushforwardIsoOfSets_hom :
    (pushforwardIsoOfSets.{w} t).hom =
      conjugateEquiv ((homFunctorOp f).ranAdjunction (Type (max u₁ v₁ w)))
        ((homFunctorOp g).ranAdjunction (Type (max u₁ v₁ w)))
        (pullbackIso (Type (max u₁ v₁ w)) t).hom

CategoryTheory.CatFiberedInGroupoids.pushforwardIsoOfSets_trans, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/PresheavesOfSets.lean, line 95. The attribute's comment: “vertical composition on direct images of presheaves of sets”.

Stacks 06TM. Vertical composition of two-morphisms becomes composition of the induced isomorphisms of direct images of presheaves of sets.

theorem pushforwardIsoOfSets_trans {h : 𝒳 ⟶ 𝒴} (s : g ⟶ h) :
    pushforwardIsoOfSets.{w} (t ≫ s) = pushforwardIsoOfSets.{w} t ≪≫ pushforwardIsoOfSets s

CategoryTheory.CatFiberedInGroupoids.pushforwardIsoOfSets_hcomp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/PresheavesOfSets.lean, line 103. The attribute's comment: “horizontal composition on direct images of presheaves of sets”.

Stacks 06TM. The isomorphism of direct images of presheaves of sets induced by a horizontal composite of two-morphisms, after identifying direct images along composites with successive direct images, is the horizontal composite of the two induced isomorphisms.

theorem pushforwardIsoOfSets_hcomp {𝒵 : CatFiberedInGroupoids.{v₀, v₁, u₀, u₁} B}
    {h k : 𝒴 ⟶ 𝒵} (s : h ⟶ k) :
    pushforwardIsoOfSets.{w} (Bicategory.whiskerRight t h ≫ Bicategory.whiskerLeft g s) ≪≫
        ranCompIso (homFunctorOp g) (homFunctorOp k) (Type (max u₁ v₁ w)) =
      ranCompIso (homFunctorOp f) (homFunctorOp h) (Type (max u₁ v₁ w)) ≪≫
        isoWhiskerRight (pushforwardIsoOfSets.{w} t)
          ((homFunctorOp h).ran (H := Type (max u₁ v₁ w))) ≪≫
        isoWhiskerLeft ((homFunctorOp g).ran (H := Type (max u₁ v₁ w)))
          (pushforwardIsoOfSets.{w} s)
Sources
LeanCategoryTheory.Functor.category · AlgebraicGeometry.BigFppfOver.presheafAdjunction · AlgebraicGeometry.BigFppfOver.presheafPushforwardObjObjIsoLimit · CategoryTheory.Functor.ranOpCompIso · CategoryTheory.Functor.homEquiv_comp_ranOpCompIso_hom_app · CategoryTheory.Functor.whiskeringLeft_obj_comp · CategoryTheory.CatFiberedInGroupoids.isIso_underlyingNatTrans_app · CategoryTheory.CatFiberedInGroupoids.pullbackIso

Section96.4 Sheaves#

Section 96.4 of the Stacks Project, Tag 06TN. 4 tags here are carried by 14 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06TP, a definition

Tag 06TP in the Stacks Project.

AlgebraicGeometry.Stack.associatedTopology, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AssociatedSite.lean, line 53.

The site associated to a category p : 𝒳 ⥤ (Sch/S) over the big fppf category of S and a topology τ on the underlying category of schemes of B: the topology 𝒳 inherits from the localization of τ at S.

abbrev associatedTopology {X : Type v} [Category.{w} X] (p : X ⥤ BigFppfOver B S hS)
    (τ : GrothendieckTopology B.Schemes) : GrothendieckTopology X
Tag 06TR, a definition

Tag 06TR in the Stacks Project.

AlgebraicGeometry.BigFppfOver.IsSheaf, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AssociatedSheaves.lean, line 99. The attribute's comment: “sheaf conditions for the five topologies”.

Stacks 06TR. A presheaf of sets on a category p : 𝒳 ⥤ (Sch/S) over the big fppf category of S is a sheaf for the topology τ when it is a sheaf on the associated site 𝒳_τ of Stacks 06TP. The five values of τ give the Zariski, étale, smooth, syntomic and fppf sheaf conditions of the source.

abbrev IsSheaf (τ : SiteKind) (F : Xᵒᵖ ⥤ Type t) : Prop

AlgebraicGeometry.BigFppfOver.AssociatedSheaf, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AssociatedSheaves.lean, line 106. The attribute's comment: “categories and morphisms of sheaves”.

Stacks 06TR. The category Sh(𝒳_τ) of sheaves of sets on the associated site 𝒳_τ of Stacks 06TP, for τ one of the five topologies. Its morphisms are morphisms of the underlying presheaves.

abbrev AssociatedSheaf (τ : SiteKind)
Tag 06TS, a lemma

Tag 06TS in the Stacks Project.

AlgebraicGeometry.BigFppfOver.isSheaf_comp_op_and_isSheaf_ran_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AssociatedMorphismOfTopoi.lean, line 101. The attribute's comment: “the functors f^p and {}_pf of presheaves of sets transform tau sheaves into tau sheaves”.

Stacks 06TS, preservation of sheaves. For a 1-morphism G : 𝒳 ⟶ 𝒴 of categories fibred in groupoids over the big fppf category of S and τ one of the five topologies, the pullback G^p 𝒢 = 𝒢 ∘ G of a τ sheaf of sets 𝒢 on 𝒴 is a τ sheaf on 𝒳, and the pushforward {}_pG ℱ, the right Kan extension of ℱ along G, of a τ sheaf of sets ℱ on 𝒳 is a τ sheaf on 𝒴.

theorem isSheaf_comp_op_and_isSheaf_ran_obj :
    (∀ 𝒢 : 𝒴.val.objᵒᵖ ⥤ Type t, IsSheaf B S hS 𝒴.val.p τ 𝒢 →
      IsSheaf B S hS 𝒳.val.p τ ((CatFiberedInGroupoids.homFunctor G).op ⋙ 𝒢)) ∧
    ∀ ℱ : 𝒳.val.objᵒᵖ ⥤ Type (max v w t), IsSheaf B S hS 𝒳.val.p τ ℱ →
      IsSheaf B S hS 𝒴.val.p τ ((CatFiberedInGroupoids.homFunctor G).op.ran.obj ℱ)

AlgebraicGeometry.BigFppfOver.morphismOfTopoi_associatedSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AssociatedMorphismOfTopoi.lean, line 121. The attribute's comment: “the morphism of topoi f : Sh(X_tau) -> Sh(Y_tau) defined by f^p and {}_pf, for sheaves of sets”.

Stacks 06TS, the morphism of topoi. A 1-morphism G : 𝒳 ⟶ 𝒴 of categories fibred in groupoids over the big fppf category of S defines, for each of the five topologies τ, a morphism of topoi f : Sh(𝒳_τ) ⟶ Sh(𝒴_τ) between the categories of sheaves of sets of Stacks 06TR: its inverse image f⁻¹ is the pullback G^p of sheaves, its direct image f_* is the pushforward {}_pG of sheaves, f⁻¹ is left adjoint to f_*, and f⁻¹ is left exact.

noncomputable def morphismOfTopoi_associatedSheaf :
    MorphismOfTopoi (AssociatedSheaf.{u, v, w, max v w t} B S hS 𝒳.val.p τ)
      (AssociatedSheaf.{u, v, w, max v w t} B S hS 𝒴.val.p τ)

AlgebraicGeometry.BigFppfOver.morphismOfTopoi_associatedSheaf_pushforwardCompSheafToPresheafIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AssociatedMorphismOfTopoi.lean, line 137. The attribute's comment: “the direct image of the morphism of topoi is the pushforward {}_pf of presheaves”.

Stacks 06TS, f_* = {}_pG. The direct image of the morphism of topoi AlgebraicGeometry.BigFppfOver.morphismOfTopoi_associatedSheaf is the pushforward of presheaves: on underlying presheaves it is the right Kan extension along G.op.

noncomputable def morphismOfTopoi_associatedSheaf_pushforwardCompSheafToPresheafIso :
    (morphismOfTopoi_associatedSheaf.{u, v, w, t} B S hS G τ).pushforward ⋙
        sheafToPresheaf (associatedTopology B S hS 𝒴.val.p τ) (Type max v w t) ≅
      sheafToPresheaf (associatedTopology B S hS 𝒳.val.p τ) (Type max v w t) ⋙
        (CatFiberedInGroupoids.homFunctor G).op.ran

AlgebraicGeometry.BigFppfOver.morphismOfTopoi_associatedSheaf_inverseImageCompSheafToPresheafIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AssociatedMorphismOfTopoi.lean, line 148. The attribute's comment: “the inverse image of the morphism of topoi is the pullback f^p of presheaves”.

Stacks 06TS, f⁻¹ = G^p. The inverse image of the morphism of topoi AlgebraicGeometry.BigFppfOver.morphismOfTopoi_associatedSheaf is the pullback of presheaves: on underlying presheaves it is precomposition with G.op.

noncomputable def morphismOfTopoi_associatedSheaf_inverseImageCompSheafToPresheafIso :
    (morphismOfTopoi_associatedSheaf.{u, v, w, t} B S hS G τ).inverseImage ⋙
        sheafToPresheaf (associatedTopology B S hS 𝒳.val.p τ) (Type max v w t) ≅
      sheafToPresheaf (associatedTopology B S hS 𝒴.val.p τ) (Type max v w t) ⋙
        (Functor.whiskeringLeft _ _ _).obj (CatFiberedInGroupoids.homFunctor G).op

AlgebraicGeometry.BigFppfOver.isContinuous_and_isCocontinuous_associatedTopology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AssociatedSheaves.lean, line 169. The attribute's comment: “preservation of sheaves by both functors”.

Stacks 06TS, preservation of sheaves by both functors. For each of the five topologies τ, the functor underlying a 1-morphism G : 𝒳 ⟶ 𝒴 of categories fibred in groupoids over the big fppf category of S is continuous and cocontinuous between the associated sites 𝒳_τ and 𝒴_τ of Stacks 06TP. Continuity says that G^p carries τ sheaves on 𝒴 to τ sheaves on 𝒳 and cocontinuity that {}_pG carries τ sheaves on 𝒳 to τ sheaves on 𝒴, which is the first assertion of the source.

This is the instance of Stacks 06NW (CategoryTheory.Functor.IsFibredOneMorphism.isContinuous_and_isCocontinuous_inheritedTopology) at the base site (Sch/S)_{fppf} with the localized topology of τ.

public theorem isContinuous_and_isCocontinuous_associatedTopology (G : 𝒳 ⟶ 𝒴) (τ : SiteKind) :
    (CatFiberedInGroupoids.homFunctor G).IsContinuous
        (associatedTopology B S hS 𝒳.val.p τ) (associatedTopology B S hS 𝒴.val.p τ) ∧
      (CatFiberedInGroupoids.homFunctor G).IsCocontinuous
        (associatedTopology B S hS 𝒳.val.p τ) (associatedTopology B S hS 𝒴.val.p τ)

AlgebraicGeometry.BigFppfOver.inverseImageCompSheafToPresheafIso_associatedTopology, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AssociatedSheaves.lean, line 187. The attribute's comment: “inverse image is restriction”.

Stacks 06TS, f⁻¹ = G^p. The inverse image of the induced morphism of topoi Sh(𝒳_τ) ⟶ Sh(𝒴_τ) is plain restriction along G.op: as a functor to presheaves on 𝒳 it is sheafToPresheaf followed by precomposition with G.op, with no sheafification intervening.

This is the instance of Stacks 06NW (CategoryTheory.Functor.IsFibredOneMorphism.inverseImageCompSheafToPresheafIso) at the five associated sites.

public def inverseImageCompSheafToPresheafIso_associatedTopology :
    letI := (isContinuous_and_isCocontinuous_associatedTopology B S hS G τ).1
    (CatFiberedInGroupoids.homFunctor G).sheafPushforwardContinuous A
          (associatedTopology B S hS 𝒳.val.p τ) (associatedTopology B S hS 𝒴.val.p τ) ⋙
        sheafToPresheaf (associatedTopology B S hS 𝒳.val.p τ) A ≅
      sheafToPresheaf (associatedTopology B S hS 𝒴.val.p τ) A ⋙
        (Functor.whiskeringLeft _ _ _).obj (CatFiberedInGroupoids.homFunctor G).op

AlgebraicGeometry.BigFppfOver.inverseImage_obj_obj_obj_associatedTopology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AssociatedSheaves.lean, line 206. The attribute's comment: “objectwise inverse image formula”.

Stacks 06TS, the objectwise formula f⁻¹(𝒢)(x) = 𝒢(G x): the sections of the inverse image of a τ sheaf 𝒢 on 𝒴 over an object x of 𝒳 are the sections of 𝒢 over G x.

This is the instance of Stacks 06NW (CategoryTheory.Functor.IsFibredOneMorphism.inverseImage_obj_obj_obj) at the five associated sites.

public theorem inverseImage_obj_obj_obj_associatedTopology :
    letI := (isContinuous_and_isCocontinuous_associatedTopology B S hS G τ).1
    ∀ (𝒢 : Sheaf (associatedTopology B S hS 𝒴.val.p τ) A) (x : 𝒳.val.obj),
      (((CatFiberedInGroupoids.homFunctor G).sheafPushforwardContinuous A
            (associatedTopology B S hS 𝒳.val.p τ)
            (associatedTopology B S hS 𝒴.val.p τ)).obj 𝒢).obj.obj (Opposite.op x) =
        𝒢.obj.obj (Opposite.op ((CatFiberedInGroupoids.homFunctor G).obj x))

AlgebraicGeometry.BigFppfOver.preservesFiniteLimits_inverseImage_associatedTopology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AssociatedSheaves.lean, line 223. The attribute's comment: “left exactness of inverse image”.

Stacks 06TS, exactness of the inverse image. The inverse image of the induced morphism of topoi preserves finite limits, which is the remaining clause in "morphism of topoi".

This is the instance of Stacks 06NW (CategoryTheory.Functor.IsFibredOneMorphism.preservesFiniteLimits_inverseImage) at the five associated sites.

public theorem preservesFiniteLimits_inverseImage_associatedTopology [Limits.HasFiniteLimits A] :
    letI := (isContinuous_and_isCocontinuous_associatedTopology B S hS G τ).1
    Limits.PreservesFiniteLimits ((CatFiberedInGroupoids.homFunctor G).sheafPushforwardContinuous A
      (associatedTopology B S hS 𝒳.val.p τ) (associatedTopology B S hS 𝒴.val.p τ))

AlgebraicGeometry.BigFppfOver.directImageCompSheafToPresheafIso_associatedTopology, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AssociatedSheaves.lean, line 238. The attribute's comment: “direct image is right Kan extension”.

Stacks 06TS, f_* = {}_pG. The direct image of the induced morphism of topoi is the right Kan extension along G.op, taken on sheaves: as a functor to presheaves on 𝒴 it is sheafToPresheaf followed by G.op.ran.

This is the instance of Stacks 06NW (CategoryTheory.Functor.IsFibredOneMorphism.directImageCompSheafToPresheafIso) at the five associated sites.

public noncomputable def directImageCompSheafToPresheafIso_associatedTopology
    [∀ (F : 𝒳.val.objᵒᵖ ⥤ A),
      (CatFiberedInGroupoids.homFunctor G).op.HasPointwiseRightKanExtension F] :
    letI := (isContinuous_and_isCocontinuous_associatedTopology B S hS G τ).2
    (CatFiberedInGroupoids.homFunctor G).sheafPushforwardCocontinuous A
          (associatedTopology B S hS 𝒳.val.p τ) (associatedTopology B S hS 𝒴.val.p τ) ⋙
        sheafToPresheaf (associatedTopology B S hS 𝒴.val.p τ) A ≅
      sheafToPresheaf (associatedTopology B S hS 𝒳.val.p τ) A ⋙
        (CatFiberedInGroupoids.homFunctor G).op.ran

AlgebraicGeometry.BigFppfOver.sheafAdjunction_associatedTopology, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AssociatedSheaves.lean, line 264. The attribute's comment: “adjunction defining the morphism of topoi”.

Stacks 06TS, the morphism of topoi itself. A 1-morphism G : 𝒳 ⟶ 𝒴 of categories fibred in groupoids over the big fppf category of S induces, for each of the five topologies τ, a morphism of topoi f : Sh(𝒳_τ) ⟶ Sh(𝒴_τ): this is the adjunction f⁻¹ ⊣ f_* between the two associated sites of Stacks 06TP, with f⁻¹ = G^p the restriction and f_* = {}_pG the right Kan extension. It is the actual adjunction, not an existence claim; together with AlgebraicGeometry.BigFppfOver.preservesFiniteLimits_inverseImage_associatedTopology it is a morphism of topoi in the source's sense.

This is the instance of Stacks 06NW (CategoryTheory.Functor.IsFibredOneMorphism.sheafAdjunctionInheritedTopology) at the five associated sites.

public noncomputable def sheafAdjunction_associatedTopology
    [∀ (F : 𝒳.val.objᵒᵖ ⥤ A),
      (CatFiberedInGroupoids.homFunctor G).op.HasPointwiseRightKanExtension F] :
    letI := (isContinuous_and_isCocontinuous_associatedTopology B S hS G τ).1
    letI := (isContinuous_and_isCocontinuous_associatedTopology B S hS G τ).2
    (CatFiberedInGroupoids.homFunctor G).sheafPushforwardContinuous A
        (associatedTopology B S hS 𝒳.val.p τ) (associatedTopology B S hS 𝒴.val.p τ) ⊣
      (CatFiberedInGroupoids.homFunctor G).sheafPushforwardCocontinuous A
        (associatedTopology B S hS 𝒳.val.p τ) (associatedTopology B S hS 𝒴.val.p τ)
Tag 06TT, a definition

Tag 06TT in the Stacks Project.

AlgebraicGeometry.BigFppfOver.sheafAdjunction_associatedSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AssociatedSheaves.lean, line 341. The attribute's comment: “the associated morphism of tau topoi f = (f^{-1}, f_*), for each of the five”.

Stacks 06TT. The associated morphism of τ topoi f = (f⁻¹, f_*) : Sh(𝒳_τ) ⟶ Sh(𝒴_τ) of a 1-morphism G : 𝒳 ⟶ 𝒴 of categories fibred in groupoids over the big fppf category of S, for each of the five topologies τ — the Zariski, étale, smooth, syntomic and fppf ones. It is the adjunction f⁻¹ ⊣ f_* between the two categories AlgebraicGeometry.BigFppfOver.AssociatedSheaf of sheaves of sets on the associated sites of Stacks 06TP, with f⁻¹ = G^p the restriction along G and f_* = {}_pG the right Kan extension along G.op.

The limits that compute f_* are supplied by AlgebraicGeometry.BigFppfOver.hasPointwiseRightKanExtension_op_homFunctor, a Type (max v w) having limits of the shapes that index them by CategoryTheory.Limits.Types.hasLimitsOfSize, so the data a reader must provide to obtain this morphism of topoi is a 1-morphism of categories fibred in groupoids over (Sch/S)_fppf and a choice among the five topologies, which is what the source provides. Left exactness of f⁻¹, the remaining clause of "morphism of topoi", is AlgebraicGeometry.BigFppfOver.preservesFiniteLimits_inverseImage_associatedTopology at these same coefficients.

public noncomputable def sheafAdjunction_associatedSheaf :
    letI := (isContinuous_and_isCocontinuous_associatedTopology B S hS G τ).1
    letI := (isContinuous_and_isCocontinuous_associatedTopology B S hS G τ).2
    (CatFiberedInGroupoids.homFunctor G).sheafPushforwardContinuous (Type max v w)
        (associatedTopology B S hS 𝒳.val.p τ) (associatedTopology B S hS 𝒴.val.p τ) ⊣
      (CatFiberedInGroupoids.homFunctor G).sheafPushforwardCocontinuous (Type max v w)
        (associatedTopology B S hS 𝒳.val.p τ) (associatedTopology B S hS 𝒴.val.p τ)
Sources
LeanAlgebraicGeometry.Stack.associatedTopology · AlgebraicGeometry.BigFppfOver.IsSheaf · AlgebraicGeometry.BigFppfOver.AssociatedSheaf · AlgebraicGeometry.BigFppfOver.isSheaf_comp_op_and_isSheaf_ran_obj · AlgebraicGeometry.BigFppfOver.morphismOfTopoi_associatedSheaf · AlgebraicGeometry.BigFppfOver.morphismOfTopoi_associatedSheaf_pushforwardCompSheafToPresheafIso · AlgebraicGeometry.BigFppfOver.morphismOfTopoi_associatedSheaf_inverseImageCompSheafToPresheafIso · AlgebraicGeometry.BigFppfOver.isContinuous_and_isCocontinuous_associatedTopology

Section96.5 Computing pushforward#

Section 96.5 of the Stacks Project, Tag 06W5. 4 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 06W6, an equation

Tag 06W6 in the Stacks Project.

CategoryTheory.Presheaf.pushforwardSectionsEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/PushforwardSections.lean, line 705. The attribute's comment: “canonical identification”.

The pushforward formula for a presheaf along a functor into a category fibred in groupoids. The projection from the two-fibre product to 𝒳 pulls the presheaf back by restriction; its global sections compute the right Kan extension at y.

public noncomputable def pushforwardSectionsEquiv
    (p𝒳 : 𝒳 ⥤ 𝒞) (p𝒴 : 𝒴 ⥤ 𝒞) (f : 𝒳 ⥤ 𝒴)
    (h𝒴 : p𝒴.IsFiberedInGroupoids)
    (hf : f ⋙ p𝒴 = p𝒳) (c : p𝒴.ChoiceOfPullbacks)
    {V : 𝒞} (y : p𝒴.Fiber V) (ℱ : 𝒳ᵒᵖ ⥤ Type w)
    [∀ (G : 𝒳ᵒᵖ ⥤ Type w), f.op.HasPointwiseRightKanExtension G] :
    (f.op.ran.obj ℱ).obj (op y.1) ≃
      Presheaf.globalSections
        ((TwoFibreProductOver.snd (Over.forget V) p𝒳 p𝒴 (c.sliceFunctor y) f).op ⋙ ℱ)

CategoryTheory.Presheaf.pushforwardSectionsEquiv_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/PushforwardSections.lean, line 721. The attribute's comment: “componentwise characterization by the right Kan counit”.

At a pair in the two-fibre product, the section corresponding to a pushforward section is obtained by restricting along the comparison arrow to y and then applying the counit of the right Kan extension.

public theorem pushforwardSectionsEquiv_apply
    (p𝒳 : 𝒳 ⥤ 𝒞) (p𝒴 : 𝒴 ⥤ 𝒞) (f : 𝒳 ⥤ 𝒴)
    (h𝒴 : p𝒴.IsFiberedInGroupoids)
    (hf : f ⋙ p𝒴 = p𝒳) (c : p𝒴.ChoiceOfPullbacks)
    {V : 𝒞} (y : p𝒴.Fiber V) (ℱ : 𝒳ᵒᵖ ⥤ Type w)
    [∀ (G : 𝒳ᵒᵖ ⥤ Type w), f.op.HasPointwiseRightKanExtension G]
    (s : (f.op.ran.obj ℱ).obj (op y.1))
    (P : TwoFibreProductOver (Over.forget V) p𝒳 p𝒴 (c.sliceFunctor y) f) :
    ((Presheaf.globalSectionsEquivSections
        ((TwoFibreProductOver.snd (Over.forget V) p𝒳 p𝒴 (c.sliceFunctor y) f).op ⋙ ℱ))
      (pushforwardSectionsEquiv p𝒳 p𝒴 f h𝒴 hf c y ℱ s)).1 (op P) =
      (f.op.ranCounit.app ℱ).app (op P.y)
        ((f.op.ran.obj ℱ).map (P.iso.inv ≫ c.map P.x.hom y).op s)

CategoryTheory.Presheaf.pushforwardSectionsEquiv_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/PushforwardSections.lean, line 739. The attribute's comment: “naturality in the presheaf”.

The pushforward identification commutes with maps of presheaves.

public theorem pushforwardSectionsEquiv_naturality
    (p𝒳 : 𝒳 ⥤ 𝒞) (p𝒴 : 𝒴 ⥤ 𝒞) (f : 𝒳 ⥤ 𝒴)
    (h𝒴 : p𝒴.IsFiberedInGroupoids)
    (hf : f ⋙ p𝒴 = p𝒳) (c : p𝒴.ChoiceOfPullbacks)
    {V : 𝒞} (y : p𝒴.Fiber V) (ℱ 𝒢 : 𝒳ᵒᵖ ⥤ Type w)
    [∀ (G : 𝒳ᵒᵖ ⥤ Type w), f.op.HasPointwiseRightKanExtension G]
    (η : ℱ ⟶ 𝒢) (s : (f.op.ran.obj ℱ).obj (op y.1)) :
    pushforwardSectionsEquiv p𝒳 p𝒴 f h𝒴 hf c y 𝒢
        (((f.op.ran.map η).app (op y.1)) s) =
      (pushforwardSectionsEquiv p𝒳 p𝒴 f h𝒴 hf c y ℱ s) ≫
        Functor.whiskerLeft
          (TwoFibreProductOver.snd (Over.forget V) p𝒳 p𝒴 (c.sliceFunctor y) f).op η
Tag 075B, a lemma

Tag 075B in the Stacks Project.

AlgebraicGeometry.Stack.abelianPresheafBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/HigherDirectImageBaseChange.lean, line 256. The attribute's comment: “abelian coefficients”.

Stacks 075B at abelian coefficients. For the canonical 2-cartesian square of categories fibred in groupoids over 𝒞, the base-change transformation g⁻¹f_* ⟶ f'_*(g')⁻¹ of presheaves of abelian groups is an isomorphism, naturally in the presheaf.

Direct image of presheaves is right Kan extension along the opposite functor and inverse image is restriction, so the transformation is CategoryTheory.TwoSquare.ranBaseChange of the opposite square, which is invertible because the square is Guitart exact. The library's CategoryTheory.TwoFibreProductOver.isIso_presheafRanBaseChange is the same statement at coefficients in Type t; both are instances of the one coefficient-free input CategoryTheory.TwoFibreProductOver.guitartExact_twoFibreProductSquare.

noncomputable def abelianPresheafBaseChangeIso
    (h𝒳 : p𝒳.IsFiberedInGroupoids) (h𝒴' : p𝒴'.IsFiberedInGroupoids)
    (h𝒴 : p𝒴.IsFiberedInGroupoids) (hfc : f ⋙ p𝒴 = p𝒳) (hgc : g ⋙ p𝒴 = p𝒴')
    [∀ G : 𝒳ᵒᵖ ⥤ AddCommGrpCat.{a}, f.op.HasPointwiseRightKanExtension G]
    [∀ G : (TwoFibreProductOver p𝒳 p𝒴' p𝒴 f g)ᵒᵖ ⥤ AddCommGrpCat.{a},
      (TwoFibreProductOver.snd p𝒳 p𝒴' p𝒴 f g).op.HasPointwiseRightKanExtension G] :
    f.op.ran ⋙ (Functor.whiskeringLeft _ _ AddCommGrpCat.{a}).obj g.op ≅
      (Functor.whiskeringLeft _ _ AddCommGrpCat.{a}).obj
          (TwoFibreProductOver.fst p𝒳 p𝒴' p𝒴 f g).op ⋙
        (TwoFibreProductOver.snd p𝒳 p𝒴' p𝒴 f g).op.ran

AlgebraicGeometry.Stack.modulePresheafBaseChangeIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/HigherDirectImageBaseChange.lean, line 659. The attribute's comment: “module coefficients, on underlying abelian presheaves”.

Stacks 075B at module coefficients. For the canonical 2-cartesian square of categories fibred in groupoids over the big fppf category of S and any topology τ on B.Schemes, the two composites f_* ⋙ g⁻¹ and (g')⁻¹ ⋙ f'_* of inverse- and direct-image functors of sheaves of modules are isomorphic on underlying abelian presheaves, naturally in the sheaf of modules.

Inverse image of sheaves of modules is objectwise restriction and direct image is the right Kan extension along the opposite 1-morphism, both on underlying abelian presheaves (AlgebraicGeometry.Stack.modulePullbackCompToPresheafIso and AlgebraicGeometry.Stack.moduleSheafPushforwardCompToPresheafIso), so both composites become the two ways round the square of a right Kan extension and a restriction, where they are identified by AlgebraicGeometry.Stack.abelianPresheafBaseChangeIso. Nothing here is special to modules: the Guitart exactness that identification rests on is coefficient-free.

noncomputable def modulePresheafBaseChangeIso
    (h𝒳 : p𝒳.IsFiberedInGroupoids) (h𝒴' : p𝒴'.IsFiberedInGroupoids)
    (h𝒴 : p𝒴.IsFiberedInGroupoids) (hfc : f ⋙ p𝒴 = p𝒳) (hgc : g ⋙ p𝒴 = p𝒴')
    [∀ G : 𝒳ᵒᵖ ⥤ AddCommGrpCat.{max (u + 1) v₁ w₁ v₂ w₂ v₃ w₃ a},
      f.op.HasPointwiseRightKanExtension G]
    [∀ G : (TwoFibreProductOver p𝒳 p𝒴' p𝒴 f g)ᵒᵖ ⥤ AddCommGrpCat.{max (u + 1) v₁ w₁ v₂ w₂ v₃ w₃ a},
      (TwoFibreProductOver.snd p𝒳 p𝒴' p𝒴 f g).op.HasPointwiseRightKanExtension G] :
    ((moduleSheafPushforward.{u, v₁, w₁, max (u + 1) v₂ w₂ a, v₃, w₃}
          B S hS p𝒳 p𝒴 h𝒳 h𝒴 f hfc τ hτ) ⋙
        (modulePullback.{u, v₂, w₂, max (u + 1) v₁ w₁ v₂ w₂ v₃ w₃ a, v₃, w₃}
          B S hS p𝒴' p𝒴 h𝒴' h𝒴 g hgc τ hτ)) ⋙
      (SheafOfModules.forget (ringStructureSheafCore B S hS p𝒴' h𝒴' τ hτ) ⋙
        PresheafOfModules.toPresheaf (ringStructureSheafCore B S hS p𝒴' h𝒴' τ hτ).obj) ≅
      ((modulePullback.{u, max (u + 1) v₁ v₂ w₃, max u w₁ w₂,
              max (u + 1) v₁ w₁ v₂ w₂ v₃ w₃ a, v₁, w₁}
          B S hS (TwoFibreProductOver.structureFunctor p𝒳 p𝒴' p𝒴 f g) p𝒳
          (TwoFibreProductOver.isFiberedInGroupoids p𝒳 p𝒴' p𝒴 f g h𝒳 h𝒴' h𝒴 hfc hgc)
            h𝒳 (TwoFibreProductOver.fst p𝒳 p𝒴' p𝒴 f g)
            TwoFibreProductOver.fst_comp_eq τ hτ) ⋙
        (moduleSheafPushforward.{u, max (u + 1) v₁ v₂ w₃, max u w₁ w₂,
              max v₃ a, v₂, w₂}
          B S hS (TwoFibreProductOver.structureFunctor p𝒳 p𝒴' p𝒴 f g) p𝒴'
          (TwoFibreProductOver.isFiberedInGroupoids p𝒳 p𝒴' p𝒴 f g h𝒳 h𝒴' h𝒴 hfc hgc)
            h𝒴' (TwoFibreProductOver.snd p𝒳 p𝒴' p𝒴 f g)
            TwoFibreProductOver.snd_comp_eq τ hτ)) ⋙
      (SheafOfModules.forget (ringStructureSheafCore B S hS p𝒴' h𝒴' τ hτ) ⋙
        PresheafOfModules.toPresheaf (ringStructureSheafCore B S hS p𝒴' h𝒴' τ hτ).obj)

CategoryTheory.TwoFibreProductOver.isIso_presheafRanBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedInGroupoids/PresheafBaseChange.lean, line 183.

Stacks 075B: in a 2-cartesian square of categories fibred in groupoids, the canonical base-change transformation g⁻¹ f_* ⟶ f'_* (g')⁻¹ for presheaves is an isomorphism, naturally in the presheaf.

theorem isIso_presheafRanBaseChange
    (pX : X ⥤ C) (pY' : Y' ⥤ C) (pY : Y ⥤ C)
    (f : X ⥤ Y) (g : Y' ⥤ Y)
    (hX : pX.IsFiberedInGroupoids) (hY' : pY'.IsFiberedInGroupoids)
    (hY : pY.IsFiberedInGroupoids)
    (hf : f ⋙ pY = pX) (hg : g ⋙ pY = pY')
    [∀ (F : Xᵒᵖ ⥤ Type t), f.op.HasPointwiseRightKanExtension F]
    [∀ (F : (TwoFibreProductOver pX pY' pY f g)ᵒᵖ ⥤ Type t),
      (TwoFibreProductOver.snd pX pY' pY f g).op.HasPointwiseRightKanExtension F] :
    IsIso ((TwoSquare.mk
      (TwoFibreProductOver.fst pX pY' pY f g)
      (TwoFibreProductOver.snd pX pY' pY f g) f g
      (TwoFibreProductOver.psiIso pX pY' pY f g).hom).op.ranBaseChange
        (D := Type t))
Tag 06W7, a lemma

Tag 06W7 in the Stacks Project.

AlgebraicGeometry.BigFppfOver.isRepresentableMorphism_iff_forall_isRepresentable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Representable.lean, line 344.

Stacks 06W7. A morphism of categories fibred in groupoids over the big fppf category of S is representable if and only if every presheaf x ↦ Hom(F x, y) on the source category is representable.

theorem isRepresentableMorphism_iff_forall_isRepresentable
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 𝒴 : Type v} [Category.{u + 1} 𝒳] [Category.{u + 1} 𝒴]
    (p𝒳 : 𝒳 ⥤ BigFppfOver B S hS)
    (p𝒴 : 𝒴 ⥤ BigFppfOver B S hS)
    (F : 𝒳 ⥤ 𝒴) (hF : F ⋙ p𝒴 = p𝒳)
    (h𝒳 : p𝒳.IsFiberedInGroupoids) (h𝒴 : p𝒴.IsFiberedInGroupoids) :
    Stacks.RepresentableMorphism.IsRepresentableMorphism p𝒳 p𝒴 F ↔
      ∀ y : 𝒴, (F.op ⋙ yoneda.obj y).IsRepresentable
Tag 06W8, a lemma

Tag 06W8 in the Stacks Project.

AlgebraicGeometry.BigFppfOver.isLeftAdjoint_of_isRepresentableMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/RepresentablePushforward.lean, line 74. The attribute's comment: “existence of the right adjoint”.

A representable 1-morphism of categories fibred in groupoids over the big fppf category of S has a right adjoint: its value at y is a representing object for the presheaf x ↦ Hom(F x, y), which exists by Stacks 06W7.

theorem isLeftAdjoint_of_isRepresentableMorphism (hF : F ⋙ p𝒴 = p𝒳)
    (h𝒳 : p𝒳.IsFiberedInGroupoids) (h𝒴 : p𝒴.IsFiberedInGroupoids)
    (hrep : Stacks.RepresentableMorphism.IsRepresentableMorphism p𝒳 p𝒴 F) :
    F.IsLeftAdjoint

AlgebraicGeometry.BigFppfOver.isContinuous_rightAdjoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/RepresentablePushforward.lean, line 93. The attribute's comment: “continuity of the right adjoint”.

The right adjoint of a representable 1-morphism is continuous for the topologies associated (Stacks 06TP) to a topology τ on the underlying category of schemes: F is cocontinuous by Stacks 06NW, and a right adjoint of a cocontinuous functor is continuous.

theorem isContinuous_rightAdjoint (τ : GrothendieckTopology B.Schemes) :
    letI : F.IsLeftAdjoint :=
      isLeftAdjoint_of_isRepresentableMorphism B S hS p𝒳 p𝒴 F hF h𝒳 h𝒴 hrep
    F.rightAdjoint.IsContinuous (Stack.associatedTopology B S hS p𝒴 τ)
      (Stack.associatedTopology B S hS p𝒳 τ)

AlgebraicGeometry.BigFppfOver.isMorphismOfSites_rightAdjoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/RepresentablePushforward.lean, line 112. The attribute's comment: “the morphism of sites”.

The right adjoint of a representable 1-morphism defines a morphism of sites from the associated site of 𝒳 to that of 𝒴: it is continuous, and the left exact left adjoint of its pushforward on sheaves is the pushforward along F.

theorem isMorphismOfSites_rightAdjoint (τ : GrothendieckTopology B.Schemes) :
    letI : F.IsLeftAdjoint :=
      isLeftAdjoint_of_isRepresentableMorphism B S hS p𝒳 p𝒴 F hF h𝒳 h𝒴 hrep
    IsMorphismOfSites.{u + 1} F.rightAdjoint (Stack.associatedTopology B S hS p𝒴 τ)
      (Stack.associatedTopology B S hS p𝒳 τ)

Declarations registered for the tag:

Sources
LeanCategoryTheory.Presheaf.pushforwardSectionsEquiv · CategoryTheory.Presheaf.pushforwardSectionsEquiv_apply · CategoryTheory.Presheaf.pushforwardSectionsEquiv_naturality · AlgebraicGeometry.Stack.abelianPresheafBaseChangeIso · AlgebraicGeometry.Stack.modulePresheafBaseChangeIso · CategoryTheory.TwoFibreProductOver.isIso_presheafRanBaseChange · AlgebraicGeometry.BigFppfOver.isRepresentableMorphism_iff_forall_isRepresentable · AlgebraicGeometry.BigFppfOver.isLeftAdjoint_of_isRepresentableMorphism

Section96.6 The structure sheaf#

Section 96.6 of the Stacks Project, Tag 06TU. 3 tags here are carried by 13 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06TV, a definition

Tag 06TV in the Stacks Project.

AlgebraicGeometry.Stack.structureSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/StructureSheaf.lean, line 108.

The structure sheaf of a category fibred in groupoids, given by inverse image of the commutative ring sheaf of the big site of schemes.

noncomputable def structureSheaf {X : Type v} [Category.{w} X]
    (p : X ⥤ BigFppfOver B S hS) (hp : p.IsFiberedInGroupoids)
    (τ : GrothendieckTopology B.Schemes) (hτ : τ ≤ B.topology) :
    Sheaf (associatedTopology B S hS p τ) CommRingCat.{u}
Tag 06TW, a lemma

Tag 06TW in the Stacks Project.

AlgebraicGeometry.FibredSite.inverseImageStructureSheaf_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/StructureSheafFunctoriality.lean, line 64. The attribute's comment: “canonical identification of structure sheaves”.

For a 1-morphism F of categories fibred in groupoids over the big fppf site, the inverse image along F of the structure sheaf of the target is the structure sheaf of the source, as a sheaf of commutative rings and on the nose.

theorem inverseImageStructureSheaf_eq
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X : Type v} [Category.{w} X] {Y : Type v'} [Category.{w'} Y]
    (p : X ⥤ BigFppfOver B S hS)
    (q : Y ⥤ BigFppfOver B S hS)
    (hp : p.IsFiberedInGroupoids) (hq : q.IsFiberedInGroupoids)
    (F : X ⥤ Y) (hF : p.IsFibredOneMorphism q F)
    (τ : SiteKind) :
    letI := hp.isFibered
    letI := hq.isFibered
    letI := (hF.isContinuous_and_isCocontinuous_inheritedTopology
      ((B.baseTopology τ).over (B.obj hS))).1
    (F.sheafPushforwardContinuous CommRingCat.{u}
      (BigFppfOver.associatedTopology B S hS p τ)
      (BigFppfOver.associatedTopology B S hS q τ)).obj
        (FibredSite.structureSheaf B S hS q hq τ) =
      FibredSite.structureSheaf B S hS p hp τ

AlgebraicGeometry.FibredSite.ringedToposMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/StructureSheafFunctoriality.lean, line 135. The attribute's comment: “morphism of ringed topoi”.

A 1-morphism F of categories fibred in groupoids over the big fppf site induces a morphism of ringed topoi in the sense of AlgebraicGeometry.RingedToposHom, between the two associated ringed topoi: the underlying morphism of topoi is the one F induces, and its structure map is the adjoint of the canonical identification AlgebraicGeometry.FibredSite.inverseImageStructureSheaf_eq.

noncomputable def ringedToposMorphism
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X : Type v} [Category.{w} X] {Y : Type v'} [Category.{w'} Y]
    (p : X ⥤ BigFppfOver B S hS)
    (q : Y ⥤ BigFppfOver B S hS)
    (hp : p.IsFiberedInGroupoids) (hq : q.IsFiberedInGroupoids)
    (F : X ⥤ Y) (hF : p.IsFibredOneMorphism q F)
    (τ : SiteKind)
    [∀ (G : Xᵒᵖ ⥤ Type u), F.op.HasPointwiseRightKanExtension G] :
    RingedToposHom
      (associatedRingedTopos B S hS p hp τ)
      (associatedRingedTopos B S hS q hq τ)

AlgebraicGeometry.FibredSite.ringedToposMorphism_inverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/StructureSheafFunctoriality.lean, line 173. The attribute's comment: “inverse image of the underlying geometric morphism”.

The morphism of ringed topoi AlgebraicGeometry.FibredSite.ringedToposMorphism sits over the morphism of topoi that F itself induces: its inverse image is restriction of sheaves along F for the two inherited topologies.

theorem ringedToposMorphism_inverseImage
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X : Type v} [Category.{w} X] {Y : Type v'} [Category.{w'} Y]
    (p : X ⥤ BigFppfOver B S hS)
    (q : Y ⥤ BigFppfOver B S hS)
    (hp : p.IsFiberedInGroupoids) (hq : q.IsFiberedInGroupoids)
    (F : X ⥤ Y) (hF : p.IsFibredOneMorphism q F)
    (τ : SiteKind)
    [∀ (G : Xᵒᵖ ⥤ Type u), F.op.HasPointwiseRightKanExtension G] :
    letI := hp.isFibered
    letI := hq.isFibered
    letI := (hF.isContinuous_and_isCocontinuous_inheritedTopology
      ((B.baseTopology τ).over (B.obj hS))).1
    (ringedToposMorphism B S hS p q hp hq F hF τ).toToposHom.inverseImage =
      F.sheafPushforwardContinuous (Type u)
        (BigFppfOver.associatedTopology B S hS p τ)
        (BigFppfOver.associatedTopology B S hS q τ)

AlgebraicGeometry.FibredSite.ringedToposMorphism_fSharpInverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/StructureSheafFunctoriality.lean, line 196. The attribute's comment: “canonical structure map”.

The inverse-image form of the structure map of AlgebraicGeometry.FibredSite.ringedToposMorphism is the canonical identification itself: the comparison of the inverse image of a sheaf of commutative rings with its restriction, followed by the equality AlgebraicGeometry.FibredSite.inverseImageStructureSheaf_eq.

theorem ringedToposMorphism_fSharpInverseImage
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X : Type v} [Category.{w} X] {Y : Type v'} [Category.{w'} Y]
    (p : X ⥤ BigFppfOver B S hS)
    (q : Y ⥤ BigFppfOver B S hS)
    (hp : p.IsFiberedInGroupoids) (hq : q.IsFiberedInGroupoids)
    (F : X ⥤ Y) (hF : p.IsFibredOneMorphism q F)
    (τ : SiteKind)
    [∀ (G : Xᵒᵖ ⥤ Type u), F.op.HasPointwiseRightKanExtension G] :
    letI := hp.isFibered
    letI := hq.isFibered
    letI := (hF.isContinuous_and_isCocontinuous_inheritedTopology
      ((B.baseTopology τ).over (B.obj hS))).1
    (ringedToposMorphism B S hS p q hp hq F hF τ).fSharpInverseImage =
      (restrictionCommRingIso
        (BigFppfOver.associatedTopology B S hS p τ)
        (BigFppfOver.associatedTopology B S hS q τ) F
        (FibredSite.structureSheaf B S hS q hq τ)).hom ≫
        eqToHom (inverseImageStructureSheaf_eq B S hS p q hp hq F hF τ)

AlgebraicGeometry.FibredSite.ringedToposMorphism_isIso_fSharpInverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/StructureSheafFunctoriality.lean, line 233. The attribute's comment: “canonical identification gives an isomorphism of structure sheaves”.

The inverse-image form of the structure map of AlgebraicGeometry.FibredSite.ringedToposMorphism is an isomorphism.

theorem ringedToposMorphism_isIso_fSharpInverseImage
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {X : Type v} [Category.{w} X] {Y : Type v'} [Category.{w'} Y]
    (p : X ⥤ BigFppfOver B S hS)
    (q : Y ⥤ BigFppfOver B S hS)
    (hp : p.IsFiberedInGroupoids) (hq : q.IsFiberedInGroupoids)
    (F : X ⥤ Y) (hF : p.IsFibredOneMorphism q F)
    (τ : SiteKind)
    [∀ (G : Xᵒᵖ ⥤ Type u), F.op.HasPointwiseRightKanExtension G] :
    IsIso (ringedToposMorphism B S hS p q hp hq F hF τ).fSharpInverseImage

AlgebraicGeometry.Stack.sheafPushforwardContinuous_structureSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/StructureSheafFunctoriality.lean, line 85. The attribute's comment: “the canonical identification of structure sheaves”.

Stacks 06TW. The inverse image of the structure sheaf of 𝒴 along a 1-morphism F is the structure sheaf of 𝒳, as an equality of sheaves of commutative rings: being a 1-morphism means p = F ⋙ q on the nose, and both structure sheaves are restrictions of one and the same structure sheaf of the base.

theorem sheafPushforwardContinuous_structureSheaf (hF : F ⋙ q = p)
    [F.IsContinuous (associatedTopology B S hS p τ) (associatedTopology B S hS q τ)] :
    (F.sheafPushforwardContinuous CommRingCat.{u} (associatedTopology B S hS p τ)
          (associatedTopology B S hS q τ)).obj (structureSheaf B S hS q hq τ hτ) =
      structureSheaf B S hS p hp τ hτ

AlgebraicGeometry.Stack.structureSheafInverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/StructureSheafFunctoriality.lean, line 141. The attribute's comment: “the structure sheaves are identified by the morphism of topoi”.

Stacks 06TW. The inverse image of the structure sheaf of 𝒴 is the structure sheaf of 𝒳, as sheaves of commutative rings on the associated site of 𝒳: the inverse image of a sheaf of commutative rings along a morphism of topoi presented by restriction is restriction, and restriction of the structure sheaf of 𝒴 along F is the structure sheaf of 𝒳.

noncomputable def structureSheafInverseImageIso :
    (inverseImageCommRingFunctor
          (associatedToposMorphism B S hS p q F hp hq τ hF)).obj (structureSheaf B S hS q hq τ hτ) ≅
      structureSheaf B S hS p hp τ hτ

AlgebraicGeometry.Stack.associatedRingedToposHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/StructureSheafFunctoriality.lean, line 156. The attribute's comment: “the morphism of ringed topoi”.

Stacks 06TW. The morphism of ringed topoi induced by a 1-morphism of categories fibred in groupoids: the morphism of topoi of Stacks 06NW together with the structure map adjoint to the identification of the structure sheaves.

noncomputable def associatedRingedToposHom :
    RingedToposHom (associatedRingedTopos B S hS p hp τ hτ)
      (associatedRingedTopos B S hS q hq τ hτ)

AlgebraicGeometry.Stack.fSharpInverseImage_associatedRingedToposHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/StructureSheafFunctoriality.lean, line 173. The attribute's comment: “the structure map is the canonical identification”.

Stacks 06TW. The structure map of the induced morphism of ringed topoi is, in inverse-image form, exactly the identification of the structure sheaves.

theorem fSharpInverseImage_associatedRingedToposHom :
    (associatedRingedToposHom B S hS p q F hp hq τ hτ hF).fSharpInverseImage =
      (structureSheafInverseImageIso B S hS p q F hp hq τ hτ hF).hom

AlgebraicGeometry.Stack.isIso_fSharpInverseImage_associatedRingedToposHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/StructureSheafFunctoriality.lean, line 183. The attribute's comment: “the structure map is an isomorphism”.

Stacks 06TW. The structure map of the induced morphism of ringed topoi is an isomorphism, so the morphism of ringed topoi is a morphism of ringed topoi with invertible structure map.

theorem isIso_fSharpInverseImage_associatedRingedToposHom :
    IsIso (associatedRingedToposHom B S hS p q F hp hq τ hτ hF).fSharpInverseImage
Tag 06TX, a remark

Tag 06TX in the Stacks Project.

AlgebraicGeometry.Stack.isFlat_associatedRingedToposHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/StructureSheafFunctorialityFlat.lean, line 113. The attribute's comment: “flatness of the morphism of ringed topoi of a 1-morphism”.

Stacks 06TX. The morphism of ringed topoi f : Sh(𝒳_τ) → Sh(𝒴_τ) induced by a 1-morphism of categories fibred in groupoids is flat: its structure map in inverse-image form is the identification f⁻¹O_𝒴 = O_𝒳 of Stacks 06TW, and an isomorphism of sheaves of commutative rings makes its target a flat module over its source.

theorem isFlat_associatedRingedToposHom :
    RingedToposHom.IsFlat
      (X := associatedRingedTopos B S hS p hp τ hτ)
      (Y := associatedRingedTopos B S hS q hq τ hτ)
      (associatedRingedToposHom B S hS p q F hp hq τ hτ hF)

AlgebraicGeometry.Stack.isFlat_associatedRingedToposHom_overMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/StructureSheafFunctorialityFlat.lean, line 172. The attribute's comment: “flatness of the morphism of big τ-sites of a morphism of schemes”.

Stacks 06TX, the second assertion. For a morphism i : X ⟶ Y of schemes over S the induced morphism of ringed big τ-sites i : (Sch/X)_τ → (Sch/Y)_τ is flat, for the same reason: the two structure sheaves are restrictions of one and the same structure sheaf of the base, so the inverse-image structure map is an isomorphism.

The source states this for a closed immersion; no hypothesis on i is used, which is the point the remark makes.

theorem isFlat_associatedRingedToposHom_overMap :
    RingedToposHom.IsFlat
      (X := associatedRingedTopos B S hS (Over.map X.hom) (.over_map X.hom) τ hτ)
      (Y := associatedRingedTopos B S hS (Over.map Y.hom) (.over_map Y.hom) τ hτ)
      (associatedRingedToposHom B S hS (Over.map X.hom) (Over.map Y.hom) (Over.map i.left)
        (.over_map X.hom) (.over_map Y.hom) τ hτ (isFibredOneMorphism_overMap X Y i))
Sources
LeanAlgebraicGeometry.Stack.structureSheaf · AlgebraicGeometry.FibredSite.inverseImageStructureSheaf_eq · AlgebraicGeometry.FibredSite.ringedToposMorphism · AlgebraicGeometry.FibredSite.ringedToposMorphism_inverseImage · AlgebraicGeometry.FibredSite.ringedToposMorphism_fSharpInverseImage · AlgebraicGeometry.FibredSite.ringedToposMorphism_isIso_fSharpInverseImage · AlgebraicGeometry.Stack.sheafPushforwardContinuous_structureSheaf · AlgebraicGeometry.Stack.structureSheafInverseImageIso

Section96.7 Sheaves of modules#

Section 96.7 of the Stacks Project, Tag 06WA. 3 tags here are carried by 7 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06WB, a definition

Tag 06WB in the Stacks Project.

AlgebraicGeometry.Stack.presheavesOfModules, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Modules.lean, line 99. The attribute's comment: “part (1), the category of presheaves of modules”.

Stacks 06WB, part (1). A presheaf of modules on a category fibred in groupoids 𝒳 over the schemes over S is a presheaf of 𝒪_𝒳-modules, and PMod(𝒪_𝒳) is the category they form, with morphisms the morphisms of presheaves of modules.

abbrev presheavesOfModules

AlgebraicGeometry.Stack.IsModule, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Modules.lean, line 105. The attribute's comment: “part (2), the fppf sheaf condition”.

Stacks 06WB, part (2). A presheaf of 𝒪_𝒳-modules is an 𝒪_𝒳-module, or a sheaf of 𝒪_𝒳-modules, when it is an fppf sheaf, that is, when its underlying presheaf of abelian groups satisfies the sheaf condition for the fppf topology on 𝒳.

abbrev IsModule : ObjectProperty (presheavesOfModules.{u, v, w, m} B S hS p hp)

AlgebraicGeometry.Stack.modules, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Modules.lean, line 112. The attribute's comment: “part (2), the category of modules”.

Stacks 06WB, part (2). The category Mod(𝒪_𝒳) of 𝒪_𝒳-modules on a category fibred in groupoids 𝒳 over the schemes over S: presheaves of 𝒪_𝒳-modules that are fppf sheaves, with morphisms the morphisms of presheaves of modules.

abbrev modules
Tag 06WD, an equation

Tag 06WD in the Stacks Project.

AlgebraicGeometry.Stack.moduleFunctoriality, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ModuleFunctoriality.lean, line 407.

The two functors on presheaves of modules induced by a morphism of categories fibred in groupoids over the big fppf site.

noncomputable def moduleFunctoriality (hf : f ⋙ pY = pX) :
    ModuleFunctoriality.{u, v, w, m, v', w'} B S hS pX pY hpX hpY f
Tag 06WE, an equation

Tag 06WE in the Stacks Project.

AlgebraicGeometry.Stack.modulePullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ModuleSheafFunctoriality.lean, line 84. The attribute's comment: “the inverse image, in an arbitrary module universe”.

The inverse image of sheaves of modules along a 1-morphism of categories fibred in groupoids, in an arbitrary module universe: objectwise restriction of modules along f, with scalars transported along AlgebraicGeometry.Stack.ringStructureSheafCore_obj_eq.

noncomputable def modulePullback :
    SheafOfModules.{m} (ringStructureSheafCore B S hS q hq τ hτ) ⥤
      SheafOfModules.{m} (ringStructureSheafCore B S hS p hp τ hτ)

AlgebraicGeometry.Stack.moduleSheafAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ModuleSheafFunctoriality.lean, line 191. The attribute's comment: “the adjunction”.

The inverse image of sheaves of modules is left adjoint to the direct image.

noncomputable def moduleSheafAdjunction :
    modulePullback.{u, v, w, max u v w m v' w', v', w'} B S hS p q hp hq f hf τ hτ ⊣
      moduleSheafPushforward.{u, v, w, m, v', w'} B S hS p q hp hq f hf τ hτ

AlgebraicGeometry.Stack.moduleSheafFunctoriality, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ModuleSheafFunctoriality.lean, line 206. The attribute's comment: “the adjoint pair on sheaves of modules”.

The adjoint pair of inverse- and direct-image functors on sheaves of modules induced by a 1-morphism of categories fibred in groupoids.

noncomputable def moduleSheafFunctoriality :
    ModuleSheafFunctoriality.{u, v, w, m, v', w'} B S hS p q hp hq f hf τ hτ
Sources
LeanAlgebraicGeometry.Stack.presheavesOfModules · AlgebraicGeometry.Stack.IsModule · AlgebraicGeometry.Stack.modules · AlgebraicGeometry.Stack.moduleFunctoriality · AlgebraicGeometry.Stack.modulePullback · AlgebraicGeometry.Stack.moduleSheafAdjunction · AlgebraicGeometry.Stack.moduleSheafFunctoriality

Section96.8 Representable categories#

Section 96.8 of the Stacks Project, Tag 076N. 2 tags here are carried by 11 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 075I, a lemma

Tag 075I in the Stacks Project.

AlgebraicGeometry.Stack.representableBy_isContinuous_and_isCocontinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/StructureSheafRepresentable.lean, line 71. The attribute's comment: “the equivalence of the underlying sites”.

Stacks 075I. The equivalence over the base representing p by X is continuous and cocontinuous for the associated topologies (Stacks 06TP) of 𝒳 and of the slice (Sch/S)/X, so it is an equivalence of the two sites. It is a 1-morphism of categories fibred in groupoids because the slice is fibred in groupoids over the base, so this is Stacks 06NW.

theorem representableBy_isContinuous_and_isCocontinuous :
    e.hom.functor.IsContinuous (associatedTopology B S hS p τ)
        (associatedTopology B S hS (Over.forget X) τ) ∧
      e.hom.functor.IsCocontinuous (associatedTopology B S hS p τ)
        (associatedTopology B S hS (Over.forget X) τ)

AlgebraicGeometry.Stack.structureSheaf_representableBy, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/StructureSheafRepresentable.lean, line 88. The attribute's comment: “the structure sheaves agree”.

Stacks 075I. The representing equivalence carries the structure sheaf of the slice (Sch/S)/X to the structure sheaf of 𝒳: restriction along it of the one is the other, as sheaves of commutative rings.

theorem structureSheaf_representableBy
    [e.hom.functor.IsContinuous (associatedTopology B S hS p τ)
      (associatedTopology B S hS (Over.forget X) τ)] :
    (e.hom.functor.sheafPushforwardContinuous CommRingCat.{u}
          (associatedTopology B S hS p τ)
          (associatedTopology B S hS (Over.forget X) τ)).obj
        (structureSheaf B S hS (Over.forget X)
          (Functor.IsFiberedInGroupoids.over_forget X) τ hτ) =
      structureSheaf B S hS p hp τ hτ

AlgebraicGeometry.Stack.structureSheafRepresentableByIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/StructureSheafRepresentable.lean, line 115. The attribute's comment: “the comparison of structure sheaves”.

Stacks 075I. The comparison isomorphism of structure sheaves under the representing equivalence. It is the canonical isomorphism attached to the equality AlgebraicGeometry.Stack.structureSheaf_representableBy, hence the identity on sections.

noncomputable def structureSheafRepresentableByIso
    [e.hom.functor.IsContinuous (associatedTopology B S hS p τ)
      (associatedTopology B S hS (Over.forget X) τ)] :
    (e.hom.functor.sheafPushforwardContinuous CommRingCat.{u}
          (associatedTopology B S hS p τ)
          (associatedTopology B S hS (Over.forget X) τ)).obj
        (structureSheaf B S hS (Over.forget X)
          (Functor.IsFiberedInGroupoids.over_forget X) τ hτ) ≅
      structureSheaf B S hS p hp τ hτ
Tag 075J, a lemma

Tag 075J in the Stacks Project.

AlgebraicGeometry.Stack.representingObjectHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/StructureSheafRepresentableMorphism.lean, line 239. The attribute's comment: “the corresponding morphism of schemes”.

Stacks 075J. The morphism of schemes X ⟶ Y over S corresponding to a 1-morphism F : 𝒳 ⥤ 𝒴 of categories representable by X and by Y: the morphism carried by the functor of slices that F becomes under the two representing equivalences.

def representingObjectHom (hF : F ⋙ q = p) : X ⟶ Y

AlgebraicGeometry.Stack.eq_map_representingObjectHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/StructureSheafRepresentableMorphism.lean, line 246. The attribute's comment: “the 1-morphism of slices is the one of the morphism of schemes”.

Stacks 075J. Read through the two representing equivalences, the 1-morphism F is postcomposition with the corresponding morphism of schemes g : X ⟶ Y, as an equality of functors (Sch/S)/X ⥤ (Sch/S)/Y.

theorem eq_map_representingObjectHom (hF : F ⋙ q = p) :
    e.inv.functor ⋙ F ⋙ d.hom.functor =
      Over.map (representingObjectHom B S hS p q F X Y e d hF)

AlgebraicGeometry.Stack.representableBySquareIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/StructureSheafRepresentableMorphism.lean, line 255. The attribute's comment: “the square of 1-morphisms 2-commutes”.

Stacks 075J. The square formed by F, the two representing equivalences and postcomposition with the corresponding morphism of schemes 2-commutes: its 2-cell is the unit of the representing equivalence of X, whiskered with F ⋙ d.

def representableBySquareIso (hF : F ⋙ q = p) :
    F ⋙ d.hom.functor ≅
      e.hom.functor ⋙ Over.map (representingObjectHom B S hS p q F X Y e d hF)

AlgebraicGeometry.Stack.whiskerRight_representableBySquareIso_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/StructureSheafRepresentableMorphism.lean, line 266. The attribute's comment: “the 2-cell of the square is over the base”.

Stacks 075J. The 2-cell filling the square is a 2-cell over (Sch/S): whiskering it with the projection of (Sch/S)/Y gives the identity 2-cell. So the square 2-commutes in the 2-category of categories fibred in groupoids over (Sch/S), which is where the comparison of Stacks 075I takes place.

theorem whiskerRight_representableBySquareIso_hom (hF : F ⋙ q = p) :
    Functor.whiskerRight (representableBySquareIso B S hS p q F X Y e d hF).hom
        (Over.forget Y) =
      eqToHom (by
        rw [Functor.assoc, d.hom.w, hF, Functor.assoc, Over.mapForget_eq, e.hom.w])

AlgebraicGeometry.Stack.representingObjectRingedToposHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/StructureSheafRepresentableMorphism.lean, line 371. The attribute's comment: “the morphism of ringed topoi of the morphism of schemes”.

Stacks 075J. The morphism of ringed topoi (Sh((Sch/X)_τ), O_X) → (Sh((Sch/Y)_τ), O_Y) of the morphism of schemes g : X ⟶ Y over S corresponding to F: the morphism of ringed topoi of Stacks 06TW of the 1-morphism CategoryTheory.Over.map g of slices.

noncomputable def representingObjectRingedToposHom (hF : F ⋙ q = p) :
    RingedToposHom (associatedRingedTopos B S hS (Over.forget X) (.over_forget X) τ hτ)
      (associatedRingedTopos B S hS (Over.forget Y) (.over_forget Y) τ hτ)

AlgebraicGeometry.Stack.conjugatedRingedToposHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/StructureSheafRepresentableMorphism.lean, line 399. The attribute's comment: “the morphism of ringed topoi of the 1-morphism, read on the representing sites”.

Stacks 075J. The morphism of ringed topoi F : (Sh(𝒳_τ), O_𝒳) → (Sh(𝒴_τ), O_𝒴) of Stacks 06TW, read through the two representing equivalences of Stacks 075I: the composite (Sh((Sch/X)_τ), O_X) → (Sh(𝒳_τ), O_𝒳) → (Sh(𝒴_τ), O_𝒴) → (Sh((Sch/Y)_τ), O_Y) of morphisms of ringed topoi, whose outer two factors are the morphisms of ringed topoi of the 1-morphisms e⁻¹ and d of the two representing equivalences.

noncomputable def conjugatedRingedToposHom (hF : F ⋙ q = p) :
    RingedToposHom (associatedRingedTopos B S hS (Over.forget X) (.over_forget X) τ hτ)
      (associatedRingedTopos B S hS (Over.forget Y) (.over_forget Y) τ hτ)

AlgebraicGeometry.Stack.fSharpInverseImage_conjugatedRingedToposHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/StructureSheafRepresentableMorphism.lean, line 488. The attribute's comment: “the two morphisms of ringed topoi agree, structure sheaves included”.

Stacks 075J. The two morphisms of ringed topoi agree. The morphism of ringed topoi F : (Sh(𝒳_τ), O_𝒳) → (Sh(𝒴_τ), O_𝒴) of Stacks 06TW, read through the two representing equivalences of Stacks 075I, and the morphism of ringed topoi g : (Sh((Sch/X)_τ), O_X) → (Sh((Sch/Y)_τ), O_Y) of the corresponding morphism of schemes have the same inverse image up to the canonical comparison AlgebraicGeometry.Stack.conjugatedRingedToposHomInverseImageIso, and under that comparison their structure maps g⁻¹O_Y ⟶ O_X coincide as morphisms of sheaves of commutative rings: the comparison of the two inverse images of the structure sheaf of (Sch/S)/Y takes the one to the other.

theorem fSharpInverseImage_conjugatedRingedToposHom (hF : F ⋙ q = p) :
    haveI : EssentiallySmall.{u} 𝒳 := essentiallySmall_of_representableBy B S hS p X e
    haveI : EssentiallySmall.{u} 𝒴 := essentiallySmall_of_representableBy B S hS q Y d
    (conjugatedRingedToposHom B S hS p q F X Y e d hp hq τ hτ hF).fSharpInverseImage =
      (pullbackCommRingSheafIsoOfNatIso (associatedTopology B S hS (Over.forget X) τ)
          (conjugatedRingedToposHomInverseImageIso B S hS p q F X Y e d hp hq τ hτ hF)
          (structureSheaf B S hS (Over.forget Y)
            (Functor.IsFiberedInGroupoids.over_forget Y) τ hτ)).hom ≫
        (representingObjectRingedToposHom B S hS p q F X Y e d τ hτ hF).fSharpInverseImage

AlgebraicGeometry.Stack.fSharp_conjugatedRingedToposHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/StructureSheafRepresentableMorphism.lean, line 513. The attribute's comment: “the square of morphisms of ringed topoi commutes”.

Stacks 075J. The square of morphisms of ringed topoi commutes, in the direct-image form in which a morphism of ringed topoi (Stacks 01D3) states its structure map: the structure map of F read through the two representing equivalences of Stacks 075I, transported along the adjoint mate of the comparison of the two inverse images, is the structure map of the morphism of ringed topoi of the corresponding morphism of schemes.

theorem fSharp_conjugatedRingedToposHom (hF : F ⋙ q = p) :
    haveI : EssentiallySmall.{u} 𝒳 := essentiallySmall_of_representableBy B S hS p X e
    haveI : EssentiallySmall.{u} 𝒴 := essentiallySmall_of_representableBy B S hS q Y d
    (associatedRingedTopos B S hS (Over.forget Y) (.over_forget Y) τ hτ).forgetRing.map
          (conjugatedRingedToposHom B S hS p q F X Y e d hp hq τ hτ hF).fSharp ≫
        (((conjugatedRingedToposHom B S hS p q F X Y e d hp hq τ hτ
              hF).toToposHom.adj.ofNatIsoLeft
            (conjugatedRingedToposHomInverseImageIso B S hS p q F X Y e d hp hq τ hτ
              hF)).rightAdjointUniq
          (representingObjectRingedToposHom B S hS p q F X Y e d τ hτ
            hF).toToposHom.adj).hom.app
          ((associatedRingedTopos B S hS (Over.forget X) (.over_forget X) τ hτ).forgetRing.obj
            (structureSheaf B S hS (Over.forget X)
              (Functor.IsFiberedInGroupoids.over_forget X) τ hτ)) =
      (associatedRingedTopos B S hS (Over.forget Y) (.over_forget Y) τ hτ).forgetRing.map
        (representingObjectRingedToposHom B S hS p q F X Y e d τ hτ hF).fSharp
Sources
LeanAlgebraicGeometry.Stack.representableBy_isContinuous_and_isCocontinuous · AlgebraicGeometry.Stack.structureSheaf_representableBy · AlgebraicGeometry.Stack.structureSheafRepresentableByIso · AlgebraicGeometry.Stack.representingObjectHom · AlgebraicGeometry.Stack.eq_map_representingObjectHom · AlgebraicGeometry.Stack.representableBySquareIso · AlgebraicGeometry.Stack.whiskerRight_representableBySquareIso_hom · AlgebraicGeometry.Stack.representingObjectRingedToposHom

Section96.9 Restriction#

Section 96.9 of the Stacks Project, Tag 075C. 8 tags here are carried by 36 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06W0, a lemma

Tag 06W0 in the Stacks Project.

AlgebraicGeometry.Stack.isEquivalence_overPost, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AssociatedSiteLocalization.lean, line 101. The attribute's comment: “equivalence of categories”.

Stacks 06W0. The canonical localization functor from the slice of a category fibred in groupoids at an object x to the schemes over the scheme x lies over is an equivalence of categories.

theorem isEquivalence_overPost {𝒳 : Type v} [Category.{w} 𝒳]
    (p : 𝒳 ⥤ BigFppfOver B S hS) (hp : p.IsFiberedInGroupoids) (x : 𝒳) :
    (Over.post (X := x) (p ⋙ Over.forget (B.obj hS))).IsEquivalence

AlgebraicGeometry.Stack.inducedTopology_overPost, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/AssociatedSiteLocalization.lean, line 110. The attribute's comment: “equivalence of site topologies”.

Stacks 06W0. The canonical localization functor identifies the localization at x of the associated topology with the localization of the base topology at the scheme x lies over, so it is an equivalence of sites and not merely of categories.

theorem inducedTopology_overPost {𝒳 : Type v} [Category.{w} 𝒳]
    (p : 𝒳 ⥤ BigFppfOver B S hS) (hp : p.IsFiberedInGroupoids)
    (τ : GrothendieckTopology B.Schemes) (x : 𝒳) :
    (Over.post (X := x) (p ⋙ Over.forget (B.obj hS))).inducedTopology
        (τ.over (p.obj x).left) =
      (associatedTopology B S hS p τ).over x

Declarations registered for the tag:

Tag 06W1, a definition

Tag 06W1 in the Stacks Project.

AlgebraicGeometry.Stack.presheafPullback, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocalizationPullback.lean, line 81. The attribute's comment: “part (1)”.

The pullback of a presheaf on a category fibred in groupoids to the big fppf site of the scheme underlying an object x: restrict to the slice at x, then transport across the localization equivalence of Stacks 06W0.

noncomputable abbrev presheafPullback
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 : Type v} [Category.{w} 𝒳]
    (p : 𝒳 ⥤ BigFppfOver B S hS) (hp : p.IsFiberedInGroupoids) (x : 𝒳)
    {A : Type t} [Category.{s} A] (F : 𝒳ᵒᵖ ⥤ A) :
    (Over (p.obj x).left)ᵒᵖ ⥤ A

AlgebraicGeometry.Stack.restrictToSmallEtale, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocalizationPullback.lean, line 93. The attribute's comment: “part (2)”.

The restriction of the pulled-back presheaf to the small étale site of the same scheme, for an étale site with the same size cutoff.

noncomputable abbrev restrictToSmallEtale
    (B : BigFppfSite.{u}) (E : BigEtaleSite.{u}) (h : E.cutoff = B.cutoff)
    (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 : Type v} [Category.{w} 𝒳]
    (p : 𝒳 ⥤ BigFppfOver B S hS) (hp : p.IsFiberedInGroupoids) (x : 𝒳)
    {A : Type t} [Category.{s} A] (F : 𝒳ᵒᵖ ⥤ A) :
    (SmallEtale E (p.obj x).left.1
      (show E.Contains (p.obj x).left.1 from by simpa [h] using (p.obj x).left.2))ᵒᵖ ⥤ A
Tag 06W2, an equation

Tag 06W2 in the Stacks Project.

AlgebraicGeometry.Stack.smallEtaleBaseMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/SmallEtaleRestriction.lean, line 125. The attribute's comment: “the morphism of schemes below an arrow”.

Stacks 06W2. The morphism of the big étale category of schemes below an arrow of a category fibred in groupoids: the fppf and étale cutoffs agree, so the scheme morphism underlying the arrow is a morphism of the étale site's bounded category.

def smallEtaleBaseMorphism {𝒳 : Type v} [Category.{w} 𝒳]
    (p : 𝒳 ⥤ BigFppfOver B S hS) {x y : 𝒳} (φ : x ⟶ y) :
    E.obj (p.obj x).left.1 (contains_base B E h S hS p x) ⟶
      E.obj (p.obj y).left.1 (contains_base B E h S hS p y)

AlgebraicGeometry.Stack.restrictionPushforwardComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/SmallEtaleRestriction.lean, line 138. The attribute's comment: “the comparison with the direct image”.

Stacks 06W2. The comparison c_φ : F|_{V_ét} ⟶ a_{small, *}(F|_{U_ét}) from the restriction of a presheaf at the target of an arrow φ : x ⟶ y to the direct image, along the underlying morphism of schemes, of its restriction at the source.

The direct image on small étale sites is precomposition with base change, so the target is spelled as such.

noncomputable def restrictionPushforwardComparison {𝒳 : Type v} [Category.{w} 𝒳]
    (p : 𝒳 ⥤ BigFppfOver B S hS) (hp : p.IsFiberedInGroupoids) {x y : 𝒳} (φ : x ⟶ y)
    {A : Type t} [Category.{s} A] (F : 𝒳ᵒᵖ ⥤ A) :
    restrictToSmallEtale B E h S hS p hp y F ⟶
      (smallEtaleBaseChange E (smallEtaleBaseMorphism B E h S hS p φ)).op ⋙
        restrictToSmallEtale B E h S hS p hp x F

AlgebraicGeometry.Stack.restrictionPushforwardComparison_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/SmallEtaleRestriction.lean, line 241. The attribute's comment: “the component formula”.

Stacks 06W2. On a small étale object W over V, the comparison with the direct image is restriction of F along the arrow of 𝒳 between the cartesian lifts of W and of its base change, characterized by lying over the projection of the base-change square.

This specifies the comparison map, rather than merely producing one.

theorem restrictionPushforwardComparison_app {𝒳 : Type v} [Category.{w} 𝒳]
    (p : 𝒳 ⥤ BigFppfOver B S hS) (hp : p.IsFiberedInGroupoids) {x y : 𝒳} (φ : x ⟶ y)
    {A : Type t} [Category.{s} A] (F : 𝒳ᵒᵖ ⥤ A)
    (W : SmallEtale E (p.obj y).left.1 (contains_base B E h S hS p y)) :
    letI : (Over.post (X := x) (p ⋙ Over.forget (B.obj hS))).IsEquivalence :=
      isEquivalence_overPost B S hS p hp x
    letI : (Over.post (X := y) (p ⋙ Over.forget (B.obj hS))).IsEquivalence :=
      isEquivalence_overPost B S hS p hp y
    let f := smallEtaleBaseMorphism B E h S hS p φ
    let V' := (smallEtaleInclusion B E h (p.obj y).left.1 (contains_base B E h S hS p y)).obj W
    let U' := (smallEtaleInclusion B E h (p.obj x).left.1
      (contains_base B E h S hS p x)).obj ((smallEtaleBaseChange E f).obj W)
    let y' := (Over.post (X := y) (p ⋙ Over.forget (B.obj hS))).inv.obj V'
    let x' := (Over.post (X := x) (p ⋙ Over.forget (B.obj hS))).inv.obj U'
    let εy := (Over.post (X := y) (p ⋙ Over.forget (B.obj hS))).asEquivalence.counit.app V'
    let εx := (Over.post (X := x) (p ⋙ Over.forget (B.obj hS))).asEquivalence.counit.app U'
    ∀ φ' : x'.left ⟶ y'.left, φ' ≫ y'.hom = x'.hom ≫ φ →
      B.inclusion.map (p.map φ').left ≫ B.inclusion.map εy.left =
        B.inclusion.map εx.left ≫ E.inclusion.map (pullback.fst W.obj.hom f) →
      (restrictionPushforwardComparison B E h S hS p hp φ F).app (Opposite.op W) =
        F.map φ'.op

AlgebraicGeometry.Stack.restrictionPushforwardComparison_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/SmallEtaleRestriction.lean, line 501. The attribute's comment: “functoriality in the presheaf”.

Stacks 06W2. The comparison with the direct image is natural in the presheaf.

theorem restrictionPushforwardComparison_naturality {𝒳 : Type v} [Category.{w} 𝒳]
    (p : 𝒳 ⥤ BigFppfOver B S hS) (hp : p.IsFiberedInGroupoids) {x y : 𝒳} (φ : x ⟶ y)
    {A : Type t} [Category.{s} A] {F G : 𝒳ᵒᵖ ⥤ A} (η : F ⟶ G)
    (W : SmallEtale E (p.obj y).left.1 (contains_base B E h S hS p y)) :
    letI : (Over.post (X := x) (p ⋙ Over.forget (B.obj hS))).IsEquivalence :=
      isEquivalence_overPost B S hS p hp x
    letI : (Over.post (X := y) (p ⋙ Over.forget (B.obj hS))).IsEquivalence :=
      isEquivalence_overPost B S hS p hp y
    let y' := (Over.post (X := y) (p ⋙ Over.forget (B.obj hS))).inv.obj
      ((smallEtaleInclusion B E h (p.obj y).left.1 (contains_base B E h S hS p y)).obj W)
    let x' := (Over.post (X := x) (p ⋙ Over.forget (B.obj hS))).inv.obj
      ((smallEtaleInclusion B E h (p.obj x).left.1 (contains_base B E h S hS p x)).obj
        ((smallEtaleBaseChange E (smallEtaleBaseMorphism B E h S hS p φ)).obj W))
    (restrictionPushforwardComparison B E h S hS p hp φ F).app (Opposite.op W) ≫
        η.app (Opposite.op x'.left) =
      η.app (Opposite.op y'.left) ≫
        (restrictionPushforwardComparison B E h S hS p hp φ G).app (Opposite.op W)
Tag 06W3, an equation

Tag 06W3 in the Stacks Project.

AlgebraicGeometry.Stack.restrictToSmallEtale_isSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/SmallEtaleRestriction.lean, line 640. The attribute's comment: “the restriction is a sheaf”.

Stacks 06W3. The restriction of an étale sheaf on a category fibred in groupoids to the small étale site of the scheme an object lies over is a sheaf, not merely a presheaf whose sheafification is of interest.

theorem restrictToSmallEtale_isSheaf {𝒳 : Type v} [Category.{w} 𝒳]
    (p : 𝒳 ⥤ BigFppfOver B S hS) (hp : p.IsFiberedInGroupoids) (x : 𝒳)
    (F : Sheaf (associatedTopology B S hS p (etaleTopology B)) (Type (max (u + 1) t))) :
    Presheaf.IsSheaf
      (SmallEtale.topology E (p.obj x).left.1 (contains_base B E h S hS p x))
      (restrictToSmallEtale B E h S hS p hp x F.obj)

AlgebraicGeometry.Stack.restrictionInverseImageComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/SmallEtaleRestriction.lean, line 725. The attribute's comment: “the comparison with the inverse image”.

Stacks 06W3. The comparison c_φ : a_{small}^{-1}(F|_{V_ét}) ⟶ F|_{U_ét} from the inverse image of the restriction at the target of an arrow φ : x ⟶ y to the restriction at its source, the mate of the direct-image comparison of Stacks 06W2 under the pullback–pushforward adjunction on small étale sheaves.

noncomputable def restrictionInverseImageComparison {𝒳 : Type v} [Category.{w} 𝒳]
    (p : 𝒳 ⥤ BigFppfOver B S hS) (hp : p.IsFiberedInGroupoids) {x y : 𝒳} (φ : x ⟶ y)
    (F : Sheaf (associatedTopology B S hS p (etaleTopology B)) (Type (max (u + 1) t))) :
    ((smallEtaleBaseChange E (smallEtaleBaseMorphism B E h S hS p φ)).sheafPullback
        (Type (max (u + 1) t))
        (SmallEtale.topology E (p.obj y).left.1 (contains_base B E h S hS p y))
        (SmallEtale.topology E (p.obj x).left.1 (contains_base B E h S hS p x))).obj
      (restrictToSmallEtaleSheaf B E h S hS p hp y F) ⟶
    restrictToSmallEtaleSheaf B E h S hS p hp x F
Tag 075D, a lemma

Tag 075D in the Stacks Project.

AlgebraicGeometry.Stack.smallEtaleStructureComparison_app_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/SmallEtaleModuleComparisonComposition.lean, line 56. The attribute's comment: “part (1), for the maps of structure sheaves below an arrow”.

The map a_{small}^♯ of structure sheaves below φ, applied after the map b_{small}^♯ below ψ, is the map below ψ ∘ φ followed by restriction along the identification of the two base changes.

theorem smallEtaleStructureComparison_app_comp
    (W : (SmallEtale E (p.obj z).left.1 (contains_base B E h S hS p z))ᵒᵖ)
    (r : (SmallEtale.structureSheaf E (p.obj z).left.1
      (contains_base B E h S hS p z)).obj.obj W) :
    (smallEtaleStructureComparison B E h S hS p hp φ τ hτ).app
        ((smallEtaleBaseChange E (smallEtaleBaseMorphism B E h S hS p ψ)).op.obj W)
        ((smallEtaleStructureComparison B E h S hS p hp ψ τ hτ).app W r) =
      (SmallEtale.structureSheaf E (p.obj x).left.1
          (contains_base B E h S hS p x)).obj.map
        ((smallEtaleBaseChangeCompIso B E h S hS p φ ψ).hom.app W.unop).op
        ((smallEtaleStructureComparison B E h S hS p hp (φ ≫ ψ) τ hτ).app W r)

AlgebraicGeometry.Stack.restrictModulePushforwardComparison_app_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/SmallEtaleModuleComparisonComposition.lean, line 89. The attribute's comment: “part (1), for the direct-image comparison of a presheaf of modules”.

The direct-image comparison of a presheaf of modules below φ, applied after the comparison below ψ, is the comparison below ψ ∘ φ followed by restriction along the identification of the two base changes.

theorem restrictModulePushforwardComparison_app_comp
    (F : PresheafOfModules.{m} (ringStructureSheafCore B S hS p hp τ hτ).obj)
    (W : (SmallEtale E (p.obj z).left.1 (contains_base B E h S hS p z))ᵒᵖ)
    (n : (restrictModuleToSmallEtale B E h S hS p hp z τ hτ F).obj W) :
    (restrictModulePushforwardComparison B E h S hS p hp φ τ hτ F).app
        ((smallEtaleBaseChange E (smallEtaleBaseMorphism B E h S hS p ψ)).op.obj W)
        ((restrictModulePushforwardComparison B E h S hS p hp ψ τ hτ F).app W n) =
      (restrictModuleToSmallEtale B E h S hS p hp x τ hτ F).presheaf.map
        ((smallEtaleBaseChangeCompIso B E h S hS p φ ψ).hom.app W.unop).op
        ((restrictModulePushforwardComparison B E h S hS p hp (φ ≫ ψ) τ hτ F).app W n)

AlgebraicGeometry.Stack.restrictModulePullbackComparison_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/SmallEtalePullbackComparisonComposition.lean, line 90. The attribute's comment: “part (1), for the pullback comparison map of a presheaf of modules”.

The comparison map c_φ of Stacks 06WC is functorial in the arrow. For arrows φ : x ⟶ y and ψ : y ⟶ z of 𝒳 lying over morphisms of schemes a : U ⟶ V and b : V ⟶ W, the pullback along a_{small}^♯ of the comparison map below ψ, followed by the comparison map below φ, is the composition law AlgebraicGeometry.Stack.smallEtalePullbackComparisonCompIso for the pullbacks followed by the comparison map below ψ ∘ φ.

public theorem restrictModulePullbackComparison_comp :
    (PresheafOfModules.pullback.{u}
          (smallEtaleStructureComparison B E h S hS p hp φ τ hτ)).map
        (restrictModulePullbackComparison B E h S hS p hp ψ τ hτ F) ≫
      restrictModulePullbackComparison B E h S hS p hp φ τ hτ F =
    (smallEtalePullbackComparisonCompIso B E h S hS p hp τ hτ φ ψ).hom.app
        (restrictModuleToSmallEtale B E h S hS p hp z τ hτ F) ≫
      restrictModulePullbackComparison B E h S hS p hp (φ ≫ ψ) τ hτ F

AlgebraicGeometry.Stack.restrictionPushforwardComparison_app_eval_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/SmallEtaleRestrictionFinalComparison.lean, line 196. The attribute's comment: “part (1), the direct-image comparisons read through the evaluation maps of the restriction of Stacks 06W1, so that no comparison of base changes is left over”.

Stacks 075D (1) through the evaluation maps. For arrows φ : x ⟶ y and ψ : y ⟶ z of 𝒳, the composite of the two comparison maps of Stacks 06W2, precomposed with the evaluation map over z, is restriction of F along ψ ∘ φ followed by the evaluation map over x.

Read this way the composition statement of Stacks 075D (1) leaves no comparison of base changes over: both the composite c_φ ∘ c_ψ and the single c_{ψ ∘ φ} become restriction along ψ ∘ φ, and AlgebraicGeometry.Stack.restrictionPushforwardComparison_app_eval_comp_eq_app_comp recovers AlgebraicGeometry.Stack.restrictionPushforwardComparison_app_comp from this form.

theorem restrictionPushforwardComparison_app_eval_comp {A : Type t} [Category.{s} A]
    (F : 𝒳ᵒᵖ ⥤ A) (φ : x ⟶ y) (ψ : y ⟶ z)
    (W : SmallEtale E (p.obj z).left.1 (contains_base B E h S hS p z)) :
    restrictToSmallEtaleEval B E h S hS p hp z F W ≫
        (restrictionPushforwardComparison B E h S hS p hp ψ F).app (op W) ≫
          (restrictionPushforwardComparison B E h S hS p hp φ F).app (op
            ((smallEtaleBaseChange E (smallEtaleBaseMorphism B E h S hS p ψ)).obj W)) =
      F.map (φ ≫ ψ).op ≫ restrictToSmallEtaleEval B E h S hS p hp x F
        ((smallEtaleBaseChange E (smallEtaleBaseMorphism B E h S hS p φ)).obj
          ((smallEtaleBaseChange E (smallEtaleBaseMorphism B E h S hS p ψ)).obj W))

AlgebraicGeometry.Stack.restrictModulePushforwardComparison_app_eval_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/SmallEtaleRestrictionFinalComparison.lean, line 294. The attribute's comment: “part (1), for the direct-image comparison of a presheaf of modules read through the evaluation maps of the restriction of Stacks 06W1”.

Stacks 075D (1) for the module comparison of Stacks 06WC, through the evaluation maps. The module form of AlgebraicGeometry.Stack.restrictionPushforwardComparison_app_eval_comp.

theorem restrictModulePushforwardComparison_app_eval_comp
    (F : PresheafOfModules.{m} (ringStructureSheafCore B S hS p hp τ hτ).obj)
    (φ : x ⟶ y) (ψ : y ⟶ z)
    (W : SmallEtale E (p.obj z).left.1 (contains_base B E h S hS p z))
    (n : F.presheaf.obj (op z)) :
    (restrictModulePushforwardComparison B E h S hS p hp φ τ hτ F).app
        (op ((smallEtaleBaseChange E (smallEtaleBaseMorphism B E h S hS p ψ)).obj W))
        ((restrictModulePushforwardComparison B E h S hS p hp ψ τ hτ F).app (op W)
          (restrictToSmallEtaleEval B E h S hS p hp z F.presheaf W n)) =
      restrictToSmallEtaleEval B E h S hS p hp x F.presheaf
        ((smallEtaleBaseChange E (smallEtaleBaseMorphism B E h S hS p φ)).obj
          ((smallEtaleBaseChange E (smallEtaleBaseMorphism B E h S hS p ψ)).obj W))
        (F.presheaf.map (φ ≫ ψ).op n)

AlgebraicGeometry.Stack.restrictToSmallEtaleInverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/SmallEtaleRestrictionComparison.lean, line 160. The attribute's comment: “part (3), the identification”.

Restriction to a small étale site commutes canonically with inverse image along a 1-morphism of categories fibred in groupoids: the restriction at y of the inverse image of F is the restriction of F at G y.

noncomputable def restrictToSmallEtaleInverseImageIso {𝒳 : Type v} [Category.{w} 𝒳]
    (p : 𝒳 ⥤ BigFppfOver B S hS) (hp : p.IsFiberedInGroupoids)
    {𝒴 : Type v'} [Category.{w'} 𝒴] (G : 𝒴 ⥤ 𝒳) (hGp : (G ⋙ p).IsFiberedInGroupoids)
    (hG : (G ⋙ p).IsFibredOneMorphism p G) (y : 𝒴)
    (F : Sheaf (associatedTopology B S hS p (etaleTopology B)) (Type t)) :
    letI : (G ⋙ p).IsFibered := hGp.isFibered
    letI : p.IsFibered := hp.isFibered
    letI := (hG.isContinuous_and_isCocontinuous_inheritedTopology
      ((etaleTopology B).over (B.obj hS))).1
    restrictToSmallEtale B E h S hS (G ⋙ p) hGp y
        ((G.sheafPushforwardContinuous (Type t)
          (associatedTopology B S hS (G ⋙ p) (etaleTopology B))
          (associatedTopology B S hS p (etaleTopology B))).obj F).obj ≅
      restrictToSmallEtale B E h S hS p hp (G.obj y) F.obj

AlgebraicGeometry.Stack.existsUnique_inverseImageComparisonLift, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/SmallEtaleRestrictionComparison.lean, line 277. The attribute's comment: “part (3), the unique comparison arrow”.

Over a small étale object there is exactly one arrow of 𝒳 from the cartesian lift at G y to the image of the cartesian lift at y compatible with the structure morphisms and lying over the canonical comparison of their bases.

theorem existsUnique_inverseImageComparisonLift {𝒳 : Type v} [Category.{w} 𝒳]
    (p : 𝒳 ⥤ BigFppfOver B S hS) (hp : p.IsFiberedInGroupoids)
    {𝒴 : Type v'} [Category.{w'} 𝒴] (G : 𝒴 ⥤ 𝒳) (hGp : (G ⋙ p).IsFiberedInGroupoids) (y : 𝒴)
    (W : SmallEtale E (p.obj (G.obj y)).left.1 (contains_base B E h S hS p (G.obj y))) :
    let P := Over.post (X := G.obj y) (p ⋙ Over.forget (B.obj hS))
    let Q := Over.post (X := y) ((G ⋙ p) ⋙ Over.forget (B.obj hS))
    letI : P.IsEquivalence := isEquivalence_overPost B S hS p hp (G.obj y)
    letI : Q.IsEquivalence := isEquivalence_overPost B S hS (G ⋙ p) hGp y
    let V := (smallEtaleInclusion B E h (p.obj (G.obj y)).left.1
      (contains_base B E h S hS p (G.obj y))).obj W
    let a := P.inv.obj V
    let b := Q.inv.obj V
    ∃! φ : a.left ⟶ G.obj b.left,
      (φ ≫ G.map b.hom = a.hom) ∧
      ((p.map φ).left ≫ (Q.objObjPreimageIso V).hom.left =
        (P.objObjPreimageIso V).hom.left)

AlgebraicGeometry.Stack.restrictToSmallEtaleInverseImageIso_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/SmallEtaleRestrictionComparison.lean, line 338. The attribute's comment: “part (3), the component formula”.

On sections over a small étale object, the identification AlgebraicGeometry.Stack.restrictToSmallEtaleInverseImageIso is restriction of F along the unique comparison arrow of AlgebraicGeometry.Stack.existsUnique_inverseImageComparisonLift.

theorem restrictToSmallEtaleInverseImageIso_app {𝒳 : Type v} [Category.{w} 𝒳]
    (p : 𝒳 ⥤ BigFppfOver B S hS) (hp : p.IsFiberedInGroupoids)
    {𝒴 : Type v'} [Category.{w'} 𝒴] (G : 𝒴 ⥤ 𝒳) (hGp : (G ⋙ p).IsFiberedInGroupoids)
    (hG : (G ⋙ p).IsFibredOneMorphism p G) (y : 𝒴)
    (F : Sheaf (associatedTopology B S hS p (etaleTopology B)) (Type t))
    (W : SmallEtale E (p.obj (G.obj y)).left.1 (contains_base B E h S hS p (G.obj y))) :
    letI : (G ⋙ p).IsFibered := hGp.isFibered
    letI : p.IsFibered := hp.isFibered
    letI := (hG.isContinuous_and_isCocontinuous_inheritedTopology
      ((etaleTopology B).over (B.obj hS))).1
    let P := Over.post (X := G.obj y) (p ⋙ Over.forget (B.obj hS))
    let Q := Over.post (X := y) ((G ⋙ p) ⋙ Over.forget (B.obj hS))
    letI : P.IsEquivalence := isEquivalence_overPost B S hS p hp (G.obj y)
    letI : Q.IsEquivalence := isEquivalence_overPost B S hS (G ⋙ p) hGp y
    let V := (smallEtaleInclusion B E h (p.obj (G.obj y)).left.1
      (contains_base B E h S hS p (G.obj y))).obj W
    let a := P.inv.obj V
    let b := Q.inv.obj V
    ∀ φ : a.left ⟶ G.obj b.left, φ ≫ G.map b.hom = a.hom →
      (p.map φ).left ≫ (Q.objObjPreimageIso V).hom.left =
        (P.objObjPreimageIso V).hom.left →
      (restrictToSmallEtaleInverseImageIso B E h S hS p hp G hGp hG y F).hom.app
          (Opposite.op W) = F.obj.map φ.op

AlgebraicGeometry.Stack.restrictToSmallEtaleSheafInverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/SmallEtaleRestrictionComparison.lean, line 409. The attribute's comment: “part (3), on sheaves”.

The identification AlgebraicGeometry.Stack.restrictToSmallEtaleInverseImageIso, as an isomorphism of sheaves.

noncomputable def restrictToSmallEtaleSheafInverseImageIso {𝒳 : Type v} [Category.{w} 𝒳]
    (p : 𝒳 ⥤ BigFppfOver B S hS) (hp : p.IsFiberedInGroupoids)
    {𝒴 : Type v'} [Category.{w'} 𝒴] (G : 𝒴 ⥤ 𝒳) (hGp : (G ⋙ p).IsFiberedInGroupoids)
    (hG : (G ⋙ p).IsFibredOneMorphism p G) (y : 𝒴)
    (F : Sheaf (associatedTopology B S hS p (etaleTopology B)) (Type (max (u + 1) t))) :
    letI : (G ⋙ p).IsFibered := hGp.isFibered
    letI : p.IsFibered := hp.isFibered
    letI := (hG.isContinuous_and_isCocontinuous_inheritedTopology
      ((etaleTopology B).over (B.obj hS))).1
    restrictToSmallEtaleSheaf B E h S hS (G ⋙ p) hGp y
        ((G.sheafPushforwardContinuous (Type (max (u + 1) t))
          (associatedTopology B S hS (G ⋙ p) (etaleTopology B))
          (associatedTopology B S hS p (etaleTopology B))).obj F) ≅
      restrictToSmallEtaleSheaf B E h S hS p hp (G.obj y) F

AlgebraicGeometry.Stack.restrictionPushforwardComparison_comp_inverseImageIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/SmallEtaleRestrictionComparison.lean, line 481. The attribute's comment: “part (4), for the direct-image comparison of a presheaf of sets”.

The comparison maps of Stacks 06W2 for ψ : y' ⟶ y in 𝒴 and for its image G ψ in 𝒳 agree under the identifications AlgebraicGeometry.Stack.restrictToSmallEtaleInverseImageIso.

theorem restrictionPushforwardComparison_comp_inverseImageIso {𝒳 : Type v} [Category.{w} 𝒳]
    (p : 𝒳 ⥤ BigFppfOver B S hS) (hp : p.IsFiberedInGroupoids)
    {𝒴 : Type v'} [Category.{w'} 𝒴] (G : 𝒴 ⥤ 𝒳) (hGp : (G ⋙ p).IsFiberedInGroupoids)
    (hG : (G ⋙ p).IsFibredOneMorphism p G) {y' y : 𝒴} (ψ : y' ⟶ y)
    (F : Sheaf (associatedTopology B S hS p (etaleTopology B)) (Type t)) :
    letI : (G ⋙ p).IsFibered := hGp.isFibered
    letI : p.IsFibered := hp.isFibered
    letI := (hG.isContinuous_and_isCocontinuous_inheritedTopology
      ((etaleTopology B).over (B.obj hS))).1
    let F' := (G.sheafPushforwardContinuous (Type t)
      (associatedTopology B S hS (G ⋙ p) (etaleTopology B))
      (associatedTopology B S hS p (etaleTopology B))).obj F
    let b := smallEtaleBaseChange E (smallEtaleBaseMorphism B E h S hS p (G.map ψ))
    (restrictToSmallEtaleInverseImageIso B E h S hS p hp G hGp hG y F).hom ≫
        restrictionPushforwardComparison B E h S hS p hp (G.map ψ) F.obj =
      restrictionPushforwardComparison B E h S hS (G ⋙ p) hGp ψ F'.obj ≫
        Functor.whiskerLeft b.op
          (restrictToSmallEtaleInverseImageIso B E h S hS p hp G hGp hG y' F).hom

AlgebraicGeometry.Stack.restrictionInverseImageComparison_comp_inverseImageIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/SmallEtaleRestrictionComparison.lean, line 759. The attribute's comment: “part (4)”.

The comparison maps of Stacks 06W3 for ψ : y' ⟶ y in 𝒴 and for its image G ψ in 𝒳 agree under the identifications AlgebraicGeometry.Stack.restrictToSmallEtaleSheafInverseImageIso.

theorem restrictionInverseImageComparison_comp_inverseImageIso {𝒳 : Type v} [Category.{w} 𝒳]
    (p : 𝒳 ⥤ BigFppfOver B S hS) (hp : p.IsFiberedInGroupoids)
    {𝒴 : Type v'} [Category.{w'} 𝒴] (G : 𝒴 ⥤ 𝒳) (hGp : (G ⋙ p).IsFiberedInGroupoids)
    (hG : (G ⋙ p).IsFibredOneMorphism p G) {y' y : 𝒴} (ψ : y' ⟶ y)
    (F : Sheaf (associatedTopology B S hS p (etaleTopology B)) (Type (max (u + 1) t))) :
    letI : (G ⋙ p).IsFibered := hGp.isFibered
    letI : p.IsFibered := hp.isFibered
    letI := (hG.isContinuous_and_isCocontinuous_inheritedTopology
      ((etaleTopology B).over (B.obj hS))).1
    let F' := (G.sheafPushforwardContinuous (Type (max (u + 1) t))
      (associatedTopology B S hS (G ⋙ p) (etaleTopology B))
      (associatedTopology B S hS p (etaleTopology B))).obj F
    let a := smallEtaleBaseChange E (smallEtaleBaseMorphism B E h S hS (G ⋙ p) ψ)
    letI : a.IsContinuous
        (SmallEtale.topology E (p.obj (G.obj y)).left.1
          (contains_base B E h S hS p (G.obj y)))
        (SmallEtale.topology E (p.obj (G.obj y')).left.1
          (contains_base B E h S hS p (G.obj y'))) :=
      smallEtaleBaseChange_isContinuous E (smallEtaleBaseMorphism B E h S hS (G ⋙ p) ψ)
    let iy := restrictToSmallEtaleSheafInverseImageIso B E h S hS p hp G hGp hG y F
    let iy' := restrictToSmallEtaleSheafInverseImageIso B E h S hS p hp G hGp hG y' F
    (a.sheafPullback (Type (max (u + 1) t))
          (SmallEtale.topology E (p.obj (G.obj y)).left.1
            (contains_base B E h S hS p (G.obj y)))
          (SmallEtale.topology E (p.obj (G.obj y')).left.1
            (contains_base B E h S hS p (G.obj y')))).map iy.hom ≫
        restrictionInverseImageComparison B E h S hS p hp (G.map ψ) F =
      restrictionInverseImageComparison B E h S hS (G ⋙ p) hGp ψ F' ≫ iy'.hom

AlgebraicGeometry.Stack.restrictionInverseImageCompIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/SmallEtaleRestrictionComposition.lean, line 166. The attribute's comment: “part (1), the identification of successive inverse images”.

The canonical identification, for arrows φ : x ⟶ y and ψ : y ⟶ z of a category fibred in groupoids, of the composite of the small étale inverse images along the underlying morphisms of schemes with the inverse image along the underlying morphism of ψ ∘ φ.

This is the identification appearing in Stacks 075D (1). It is the mate of the direct-image comparison induced by AlgebraicGeometry.smallEtaleBaseChange_factoredCompIso.

noncomputable def restrictionInverseImageCompIso {𝒳 : Type v} [Category.{w} 𝒳]
    (p : 𝒳 ⥤ BigFppfOver B S hS) {x y z : 𝒳} (φ : x ⟶ y) (ψ : y ⟶ z) :
    (smallEtaleBaseChange E (smallEtaleBaseMorphism B E h S hS p ψ)).sheafPullback
        (Type (max (u + 1) t))
        (SmallEtale.topology E (p.obj z).left.1 (contains_base B E h S hS p z))
        (SmallEtale.topology E (p.obj y).left.1 (contains_base B E h S hS p y)) ⋙
      (smallEtaleBaseChange E (smallEtaleBaseMorphism B E h S hS p φ)).sheafPullback
        (Type (max (u + 1) t))
        (SmallEtale.topology E (p.obj y).left.1 (contains_base B E h S hS p y))
        (SmallEtale.topology E (p.obj x).left.1 (contains_base B E h S hS p x)) ≅
    (smallEtaleBaseChange E (smallEtaleBaseMorphism B E h S hS p (φ ≫ ψ))).sheafPullback
      (Type (max (u + 1) t))
      (SmallEtale.topology E (p.obj z).left.1 (contains_base B E h S hS p z))
      (SmallEtale.topology E (p.obj x).left.1 (contains_base B E h S hS p x))

AlgebraicGeometry.Stack.restrictionPushforwardComparison_app_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/SmallEtaleRestrictionComposition.lean, line 290. The attribute's comment: “part (1), the direct-image form”.

Stacks 075D (1) for the direct-image comparisons of Stacks 06W2: the comparison for a composite arrow, followed by restriction along the composition comparison of base changes, is the composite of the two comparisons.

This is the form with content; the inverse-image statement of the source is its mate. It holds for a presheaf with values in an arbitrary category.

theorem restrictionPushforwardComparison_app_comp {𝒳 : Type v} [Category.{w} 𝒳]
    (p : 𝒳 ⥤ BigFppfOver B S hS) (hp : p.IsFiberedInGroupoids) {x y z : 𝒳}
    (φ : x ⟶ y) (ψ : y ⟶ z) {A : Type t} [Category.{s} A] (F : 𝒳ᵒᵖ ⥤ A)
    (W : SmallEtale E (p.obj z).left.1 (contains_base B E h S hS p z)) :
    (restrictionPushforwardComparison B E h S hS p hp ψ F).app (Opposite.op W) ≫
        (restrictionPushforwardComparison B E h S hS p hp φ F).app (Opposite.op
          ((smallEtaleBaseChange E (smallEtaleBaseMorphism B E h S hS p ψ)).obj W)) =
      (restrictionPushforwardComparison B E h S hS p hp (φ ≫ ψ) F).app (Opposite.op W) ≫
        (restrictToSmallEtale B E h S hS p hp x F).map
          ((smallEtaleBaseChange_factoredCompIso E _ _ _
            (smallEtaleBaseMorphism B E h S hS p φ) (smallEtaleBaseMorphism B E h S hS p ψ)
            (smallEtaleBaseMorphism B E h S hS p (φ ≫ ψ))
            (smallEtaleBaseMorphism_comp B E h S hS p φ ψ).symm).hom.app W).op

AlgebraicGeometry.Stack.restrictionInverseImageComparison_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/SmallEtaleRestrictionComposition.lean, line 414. The attribute's comment: “part (1)”.

Stacks 075D (1). For an étale sheaf on a category fibred in groupoids, the comparison map of Stacks 06W3 for a composite arrow is the composite of the two comparison maps, under the canonical identification of successive small étale inverse images.

theorem restrictionInverseImageComparison_comp {𝒳 : Type v} [Category.{w} 𝒳]
    (p : 𝒳 ⥤ BigFppfOver B S hS) (hp : p.IsFiberedInGroupoids) {x y z : 𝒳}
    (φ : x ⟶ y) (ψ : y ⟶ z)
    (F : Sheaf (associatedTopology B S hS p (etaleTopology B)) (Type (max (u + 1) t))) :
    ((smallEtaleBaseChange E (smallEtaleBaseMorphism B E h S hS p φ)).sheafPullback
          (Type (max (u + 1) t))
          (SmallEtale.topology E (p.obj y).left.1 (contains_base B E h S hS p y))
          (SmallEtale.topology E (p.obj x).left.1 (contains_base B E h S hS p x))).map
        (restrictionInverseImageComparison B E h S hS p hp ψ F) ≫
      restrictionInverseImageComparison B E h S hS p hp φ F =
    (restrictionInverseImageCompIso B E h S hS p φ ψ).hom.app
        (restrictToSmallEtaleSheaf B E h S hS p hp z F) ≫
      restrictionInverseImageComparison B E h S hS p hp (φ ≫ ψ) F

AlgebraicGeometry.Stack.isIso_restrictionInverseImageComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/SmallEtaleRestrictionEtaleIso.lean, line 176. The attribute's comment: “part (2)”.

Stacks 075D, part (2). If an arrow of 𝒳 lies over an étale morphism of schemes, the comparison of Stacks 06W3 between the inverse image of the restriction at its target and the restriction at its source is an isomorphism.

theorem isIso_restrictionInverseImageComparison {𝒳 : Type v} [Category.{w} 𝒳]
    (p : 𝒳 ⥤ BigFppfOver B S hS) (hp : p.IsFiberedInGroupoids) {x y : 𝒳} (φ : x ⟶ y)
    (hφ : Etale (B.inclusion.map (p.map φ).left))
    (F : Sheaf (associatedTopology B S hS p (etaleTopology B)) (Type (max (u + 1) t))) :
    IsIso (restrictionInverseImageComparison B E h S hS p hp φ F)
Tag 06W9, a lemma

Tag 06W9 in the Stacks Project.

AlgebraicGeometry.Stack.ringStructureSheafCore_overPost, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocalizationStructureSheaf.lean, line 77.

Stacks 06W9. The canonical localization equivalence of Stacks 06W0 carries the structure sheaf of the schemes over (p.obj x).left to the restriction of the structure sheaf of 𝒳 to the slice at x, including all restriction maps.

theorem ringStructureSheafCore_overPost
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 : Type v} [Category.{w} 𝒳]
    (p : 𝒳 ⥤ BigFppfOver B S hS) (hp : p.IsFiberedInGroupoids)
    (τ : GrothendieckTopology B.Schemes) (hτ : τ ≤ B.topology) (x : 𝒳) :
    (Over.forget x).op ⋙ (ringStructureSheafCore B S hS p hp τ hτ).obj =
      (Over.post (X := x) (p ⋙ Over.forget (B.obj hS))).op ⋙
        (baseRingStructureSheaf B (p.obj x).left.1 (p.obj x).left.2 τ hτ).obj

AlgebraicGeometry.Stack.sheafPushforwardContinuous_baseStructureSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocalizationStructureSheaf.lean, line 142. The attribute's comment: “equivalence of ringed sites”.

Stacks 06W9. The equivalence of Stacks 06W0 is an equivalence of ringed sites (𝒳_τ/x, 𝒪_𝒳|_x) ≌ ((Sch/U)_τ, 𝒪): the direct image along it of the structure sheaf of the big τ-site of U = p(x) is the structure sheaf of 𝒳 restricted to the slice at x.

The two sites are identified by AlgebraicGeometry.Stack.localizationEquivalence and AlgebraicGeometry.Stack.isDenseSubsite_localizationEquivalence, and the structure sheaves by this equality, which is an equality and not merely an isomorphism.

theorem sheafPushforwardContinuous_baseStructureSheaf
    (τ : GrothendieckTopology B.Schemes) (hτ : τ ≤ B.topology) (x : 𝒳) :
    ((localizationEquivalence B S hS p hp x).functor.sheafPushforwardContinuous
        CommRingCat.{u} ((associatedTopology B S hS p τ).over x)
        (τ.over (B.obj (p.obj x).left.2))).obj
        (baseStructureSheaf B (p.obj x).left.1 (p.obj x).left.2 τ hτ) =
      (structureSheaf B S hS p hp τ hτ).over x

AlgebraicGeometry.Stack.sheafPushforwardContinuous_baseRingStructureSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/LocalizationStructureSheaf.lean, line 156. The attribute's comment: “equivalence of ringed sites, underlying sheaves of rings”.

Stacks 06W9, the same equivalence of ringed sites read on the underlying sheaves of (not necessarily commutative) rings, which is the form the categories of sheaves of modules are indexed by: the transport of the base sheaf of rings along the localization equivalence is the restriction of the sheaf of rings of 𝒳 to the slice at x.

theorem sheafPushforwardContinuous_baseRingStructureSheaf
    (τ : GrothendieckTopology B.Schemes) (hτ : τ ≤ B.topology) (x : 𝒳) :
    ((localizationEquivalence B S hS p hp x).functor.sheafPushforwardContinuous
        RingCat.{u} ((associatedTopology B S hS p τ).over x)
        (τ.over (B.obj (p.obj x).left.2))).obj
        (baseRingStructureSheaf B (p.obj x).left.1 (p.obj x).left.2 τ hτ) =
      (ringStructureSheafCore B S hS p hp τ hτ).over x
Tag 06WC, an equation

Tag 06WC in the Stacks Project.

AlgebraicGeometry.Stack.restrictModulePushforwardComparison_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FlatBaseChangeNaturality.lean, line 129. The attribute's comment: “functoriality of the direct-image comparison in the module”.

Stacks 06WC. The direct-image comparison of a presheaf of modules below an arrow of 𝒳 is natural in the module, at an arbitrary universe for the sections of the module.

On underlying abelian presheaves this is the naturality of Stacks 06W2, which holds for presheaves with values in any category, and putting the module structure on the comparison does not change it on sections. No universe inequality is needed: the direct image of presheaves of modules is restriction of scalars followed by reindexing, and exists at every module universe.

theorem restrictModulePushforwardComparison_naturality
    {F F' : PresheafOfModules.{m} (ringStructureSheafCore B S hS p hp τ hτ).obj} (α : F ⟶ F') :
    (restrictModuleToSmallEtaleFunctor.{u, v, w, m} B E h S hS p hp τ hτ y).map α ≫
        restrictModulePushforwardComparison B E h S hS p hp φ τ hτ F' =
      restrictModulePushforwardComparison B E h S hS p hp φ τ hτ F ≫
        (PresheafOfModules.pushforward.{m}
          (F := smallEtaleBaseChange E (smallEtaleBaseMorphism B E h S hS p φ))
          (smallEtaleStructureComparison B E h S hS p hp φ τ hτ)).map
          ((restrictModuleToSmallEtaleFunctor.{u, v, w, m} B E h S hS p hp τ hτ x).map α)

AlgebraicGeometry.Stack.restrictModulePullbackComparison_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FlatBaseChangeNaturality.lean, line 157. The attribute's comment: “functoriality of the comparison map in the module”.

Stacks 06WC. The comparison map c_φ is natural in the module.

The square for c_φ is the square for the direct-image comparison carried across the pullback–direct image adjunction along a_{small}^♯, using that c_φ is by definition the mate of that comparison: naturality of the adjunction isomorphism on the left turns the left-hand composite into a mate, naturality on the right does the same for the right-hand composite, and the two mates agree by AlgebraicGeometry.Stack.restrictModulePushforwardComparison_naturality.

theorem restrictModulePullbackComparison_naturality
    {F F' : PresheafOfModules.{u} (ringStructureSheafCore B S hS p hp τ hτ).obj} (α : F ⟶ F') :
    (PresheafOfModules.pullback.{u}
          (F := smallEtaleBaseChange E (smallEtaleBaseMorphism B E h S hS p φ))
          (smallEtaleStructureComparison B E h S hS p hp φ τ hτ)).map
        ((restrictModuleToSmallEtaleFunctor.{u, v, w, u} B E h S hS p hp τ hτ y).map α) ≫
          restrictModulePullbackComparison B E h S hS p hp φ τ hτ F' =
      restrictModulePullbackComparison B E h S hS p hp φ τ hτ F ≫
        (restrictModuleToSmallEtaleFunctor.{u, v, w, u} B E h S hS p hp τ hτ x).map α

AlgebraicGeometry.Stack.restrictModulePullbackComparisonNatTrans, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FlatBaseChangeNaturality.lean, line 181. The attribute's comment: “the comparison map as a natural transformation”.

Stacks 06WC. The comparison map c_φ below an arrow φ : x ⟶ y of 𝒳, as a natural transformation from the restriction at y followed by a_{small}^* to the restriction at x.

noncomputable def restrictModulePullbackComparisonNatTrans :
    restrictModuleToSmallEtaleFunctor.{u, v, w, u} B E h S hS p hp τ hτ y ⋙
        PresheafOfModules.pullback.{u}
          (F := smallEtaleBaseChange E (smallEtaleBaseMorphism B E h S hS p φ))
          (smallEtaleStructureComparison B E h S hS p hp φ τ hτ) ⟶
      restrictModuleToSmallEtaleFunctor.{u, v, w, u} B E h S hS p hp τ hτ x

AlgebraicGeometry.Stack.smallEtaleStructureComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/SmallEtaleModuleComparison.lean, line 90. The attribute's comment: “the map of structure sheaves below an arrow”.

The map a_{small}^♯ : 𝒪_{V_ét} ⟶ a_{small, *}𝒪_{U_ét} of structure sheaves below an arrow φ : x ⟶ y of 𝒳: the comparison of Stacks 06W2 for the structure sheaf of 𝒳, conjugated by the identifications of Stacks 06W9 of its restrictions with the structure sheaves of the small étale sites.

noncomputable def smallEtaleStructureComparison {𝒳 : Type v} [Category.{w} 𝒳]
    (p : 𝒳 ⥤ BigFppfOver B S hS) (hp : p.IsFiberedInGroupoids) {x y : 𝒳} (φ : x ⟶ y)
    (τ : GrothendieckTopology B.Schemes) (hτ : τ ≤ B.topology) :
    (SmallEtale.structureSheaf E (p.obj y).left.1 (contains_base B E h S hS p y)).obj ⟶
      (smallEtaleBaseChange E (smallEtaleBaseMorphism B E h S hS p φ)).op ⋙
        (SmallEtale.structureSheaf E (p.obj x).left.1 (contains_base B E h S hS p x)).obj

AlgebraicGeometry.Stack.restrictModulePushforwardComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/SmallEtaleModuleComparison.lean, line 108. The attribute's comment: “compatibility of the comparison map with the map of structure sheaves”.

Stacks 06WC. The comparison of Stacks 06W2 for a presheaf of modules on 𝒳 is a morphism of presheaves of modules over the map a_{small}^♯ of structure sheaves: the restriction at y maps to the direct image of the restriction at x.

This is the compatibility of the comparison map with a_{small}^♯ asserted by the source.

noncomputable def restrictModulePushforwardComparison {𝒳 : Type v} [Category.{w} 𝒳]
    (p : 𝒳 ⥤ BigFppfOver B S hS) (hp : p.IsFiberedInGroupoids) {x y : 𝒳} (φ : x ⟶ y)
    (τ : GrothendieckTopology B.Schemes) (hτ : τ ≤ B.topology)
    (F : PresheafOfModules.{m} (ringStructureSheafCore B S hS p hp τ hτ).obj) :
    restrictModuleToSmallEtale B E h S hS p hp y τ hτ F ⟶
      (PresheafOfModules.pushforward.{m}
          (F := smallEtaleBaseChange E (smallEtaleBaseMorphism B E h S hS p φ))
          (smallEtaleStructureComparison B E h S hS p hp φ τ hτ)).obj
        (restrictModuleToSmallEtale B E h S hS p hp x τ hτ F)

AlgebraicGeometry.Stack.restrictModulePullbackComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/SmallEtaleModuleComparison.lean, line 198.

Stacks 06WC. The comparison map c_φ : a_{small}^*(F|_{V_ét}) ⟶ F|_{U_ét} of 𝒪_{U_ét}-modules below an arrow φ : x ⟶ y of 𝒳 lying over a morphism of schemes a : U ⟶ V: the mate, under the pullback–direct image adjunction along a_{small}^♯, of the comparison of Stacks 06W2 for the presheaf of modules F.

noncomputable def restrictModulePullbackComparison
    (F : PresheafOfModules.{u} (ringStructureSheafCore B S hS p hp τ hτ).obj) :
    (PresheafOfModules.pullback.{u}
        (F := smallEtaleBaseChange E (smallEtaleBaseMorphism B E h S hS p φ))
        (smallEtaleStructureComparison B E h S hS p hp φ τ hτ)).obj
        (restrictModuleToSmallEtale B E h S hS p hp y τ hτ F) ⟶
      restrictModuleToSmallEtale B E h S hS p hp x τ hτ F

AlgebraicGeometry.Stack.restrictModulePullbackComparison_adjunct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/SmallEtaleModuleComparison.lean, line 212. The attribute's comment: “the adjoint characterization”.

The comparison map of Stacks 06WC is characterized by its mate being the comparison of Stacks 06W2 for the presheaf of modules.

theorem restrictModulePullbackComparison_adjunct
    (F : PresheafOfModules.{u} (ringStructureSheafCore B S hS p hp τ hτ).obj) :
    (PresheafOfModules.pullbackPushforwardAdjunction.{u}
        (smallEtaleStructureComparison B E h S hS p hp φ τ hτ)).homEquiv _ _
        (restrictModulePullbackComparison B E h S hS p hp φ τ hτ F) =
      restrictModulePushforwardComparison B E h S hS p hp φ τ hτ F
Tag 06W4, a lemma

Tag 06W4 in the Stacks Project.

AlgebraicGeometry.Stack.hasConservativeFamily_siteKind, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/EnoughPoints.lean, line 243.

Stacks 06W4. Let p : 𝒳 ⥤ (Sch/S)_fppf be a category fibred in groupoids and let τ ∈ {Zar, étale, smooth, syntomic, fppf}. Then the site 𝒳_τ has enough points: it has a conservative family of points.

The site 𝒳_τ is AlgebraicGeometry.BigFppfOver.associatedTopology, the topology 𝒳 inherits along p from the localization at S of the big τ topology (Stacks 06TP). The proof is the one of the source: hasConservativeFamily_associatedTopology reduces to the localizations of the big site, which have enough points by Stacks 06VX.

theorem hasConservativeFamily_siteKind (hp : p.IsFiberedInGroupoids) (τ : SiteKind) :
    (BigFppfOver.associatedTopology B S hS p τ).HasConservativeFamily.{u + 1}
Sources
LeanAlgebraicGeometry.Stack.isEquivalence_overPost · AlgebraicGeometry.Stack.inducedTopology_overPost · CategoryTheory.Over.post · AlgebraicGeometry.Stack.presheafPullback · AlgebraicGeometry.Stack.restrictToSmallEtale · AlgebraicGeometry.Stack.smallEtaleBaseMorphism · AlgebraicGeometry.Stack.restrictionPushforwardComparison · AlgebraicGeometry.Stack.restrictionPushforwardComparison_app

Section96.10 Restriction to algebraic spaces#

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

Tag 073M, a lemma

Tag 073M in the Stacks Project.

AlgebraicGeometry.Space.projectionRingedToposHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RestrictionProjection.lean, line 275. The attribute's comment: “the morphism of ringed topoi pi_F”.

Stacks 073M. The morphism of ringed topoi π_F : (Sh(𝒳_étale), 𝒪_𝒳) ⟶ (Sh(F_étale), 𝒪_F): its direct image is restriction along the functor F_étale ⥤ 𝒳, its inverse image is the left adjoint g_! of that restriction, which is left exact, and its structure map is the identification of the restricted structure sheaf of 𝒳 with the structure sheaf of F.

noncomputable def projectionRingedToposHom (hp : p.IsFiberedInGroupoids)
    (hF : IsAlgebraicSpace B S hS F)
    (e : StacksRepresentableCFG.EquivalenceOver p
      (presheafOfCategories (F ⋙ typeToCat)).p) :
    RingedToposHom (FibredSite.associatedRingedTopos B S hS p hp .etale)
      (smallEtaleRingedTopos B S hS ⟨F, hF⟩)

AlgebraicGeometry.Space.projectionRingedToposHom_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RestrictionProjection.lean, line 314. The attribute's comment: “the direct image of pi_F is restriction along the functor”.

Stacks 073M, equation 075K. The direct image of π_F is restriction along the functor F_étale ⥤ 𝒳, that is, π_{F,*}ℱ(U) = ℱ(u(U)).

This is the right-hand identification ℱ|_{F_étale} = π_{F, *}ℱ of equation 075K: the right-hand side here is the term that AlgebraicGeometry.Space.restrictionSheafFunctor names ℱ|_{F_étale}. The left-hand identification ℱ|_{F_étale} = i_F^{-1}ℱ is AlgebraicGeometry.Space.restrictionToposHom_inverseImage; together they give the chain.

theorem projectionRingedToposHom_pushforward (hp : p.IsFiberedInGroupoids)
    (hF : IsAlgebraicSpace B S hS F)
    (e : StacksRepresentableCFG.EquivalenceOver p
      (presheafOfCategories (F ⋙ typeToCat)).p) :
    letI := restrictionFunctor_isContinuous B S hS F p hp e
    (projectionRingedToposHom B S hS F p hp hF e).toToposHom.pushforward =
      (restrictionFunctor B S hS F p e).sheafPushforwardContinuous (Type u)
        (SmallEtale.topology B S hS F)
        (BigFppfOver.associatedTopology B S hS p .etale)

AlgebraicGeometry.Space.restrictionFunctor_isContinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RestrictionToAlgebraicSpace.lean, line 213. The attribute's comment: “continuity of the functor from the small étale site of the space”.

Stacks 073M. The functor F_étale ⥤ 𝒳 is continuous for the étale topology on 𝒳: it preserves fibre products and carries a covering family of étale charts to a covering family of the inherited étale topology, the images of its members being strongly cartesian.

theorem restrictionFunctor_isContinuous (hp : p.IsFiberedInGroupoids)
    (e : StacksRepresentableCFG.EquivalenceOver p
      (presheafOfCategories (F ⋙ typeToCat)).p) :
    (restrictionFunctor B S hS F p e).IsContinuous
      (SmallEtale.topology B S hS F)
      (BigFppfOver.associatedTopology B S hS p .etale)

AlgebraicGeometry.Space.restrictionFunctor_isCocontinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RestrictionToAlgebraicSpace.lean, line 333. The attribute's comment: “cocontinuity of the functor from the small étale site of the space”.

Stacks 073M. The functor F_étale ⥤ 𝒳 is cocontinuous for the étale topology on 𝒳: a covering sieve of the image of a chart pulls back to a covering sieve of that chart, because its image under the structure functor already does and the members of a covering sieve of the inherited topology are strongly cartesian.

theorem restrictionFunctor_isCocontinuous (hp : p.IsFiberedInGroupoids)
    (e : StacksRepresentableCFG.EquivalenceOver p
      (presheafOfCategories (F ⋙ typeToCat)).p) :
    (restrictionFunctor B S hS F p e).IsCocontinuous
      (SmallEtale.topology B S hS F)
      (BigFppfOver.associatedTopology B S hS p .etale)

AlgebraicGeometry.Space.restrictionToposHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RestrictionToAlgebraicSpace.lean, line 474. The attribute's comment: “the morphism of topoi i_F”.

Stacks 073M. The morphism of topoi i_F : Sh(F_étale) ⟶ Sh(𝒳_étale) induced by the continuous and cocontinuous functor F_étale ⥤ 𝒳: its inverse image is restriction along that functor and its direct image is the right Kan extension along it.

noncomputable def restrictionToposHom (hp : p.IsFiberedInGroupoids)
    (e : StacksRepresentableCFG.EquivalenceOver p
      (presheafOfCategories (F ⋙ typeToCat)).p) :
    MorphismOfTopoi (Sheaf (SmallEtale.topology B S hS F) (Type u))
      (Sheaf (BigFppfOver.associatedTopology B S hS p .etale) (Type u))

AlgebraicGeometry.Space.restrictionToposHom_inverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RestrictionToAlgebraicSpace.lean, line 496. The attribute's comment: “the inverse image of i_F is restriction along the functor”.

Stacks 073M, equation 075K. The inverse image of i_F is restriction along the functor F_étale ⥤ 𝒳. This is the source's π_{F,*} = i_F^{-1}: both send a sheaf ℱ to U ↦ ℱ(u(U)).

It is also the left-hand identification ℱ|_{F_étale} = i_F^{-1}ℱ of equation 075K, the right-hand side of this statement being the term that AlgebraicGeometry.Space.restrictionSheafFunctor names ℱ|_{F_étale}. The right-hand identification ℱ|_{F_étale} = π_{F, *}ℱ is AlgebraicGeometry.Space.projectionRingedToposHom_pushforward.

theorem restrictionToposHom_inverseImage (hp : p.IsFiberedInGroupoids)
    (e : StacksRepresentableCFG.EquivalenceOver p
      (presheafOfCategories (F ⋙ typeToCat)).p) :
    letI := restrictionFunctor_isContinuous B S hS F p hp e
    (restrictionToposHom B S hS F p hp e).inverseImage =
      (restrictionFunctor B S hS F p e).sheafPushforwardContinuous (Type u)
        (SmallEtale.topology B S hS F)
        (BigFppfOver.associatedTopology B S hS p .etale)

AlgebraicGeometry.Space.inverseImage_structureSheaf_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RestrictionToAlgebraicSpace.lean, line 535. The attribute's comment: “the restricted structure sheaf of the category is that of the space”.

Stacks 073M. Restriction along the functor F_étale ⥤ 𝒳 carries the structure sheaf of 𝒳 to the structure sheaf of the small étale site of F, on the nose: both send a chart to the ring of global functions on its underlying scheme.

theorem inverseImage_structureSheaf_eq (hp : p.IsFiberedInGroupoids)
    (e : StacksRepresentableCFG.EquivalenceOver p
      (presheafOfCategories (F ⋙ typeToCat)).p)
    (hF : IsAlgebraicSpace B S hS F) :
    letI := restrictionFunctor_isContinuous B S hS F p hp e
    ((restrictionFunctor B S hS F p e).sheafPushforwardContinuous CommRingCat.{u}
      (SmallEtale.topology B S hS F)
      (BigFppfOver.associatedTopology B S hS p .etale)).obj
        (FibredSite.structureSheaf B S hS p hp .etale) = structureSheaf B S hS F hF

AlgebraicGeometry.Space.restrictionRingedToposHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RestrictionToAlgebraicSpace.lean, line 556. The attribute's comment: “the morphism of ringed topoi i_F”.

Stacks 073M. The morphism of ringed topoi i_F : (Sh(F_étale), 𝒪_F) ⟶ (Sh(𝒳_étale), 𝒪_𝒳): the morphism of topoi i_F together with the identification of the restricted structure sheaf of 𝒳 with the structure sheaf of F.

noncomputable def restrictionRingedToposHom (hp : p.IsFiberedInGroupoids)
    (e : StacksRepresentableCFG.EquivalenceOver p
      (presheafOfCategories (F ⋙ typeToCat)).p)
    (hF : IsAlgebraicSpace B S hS F) :
    RingedToposHom (smallEtaleRingedTopos B S hS ⟨F, hF⟩)
      (FibredSite.associatedRingedTopos B S hS p hp .etale)

AlgebraicGeometry.Space.lowerShriek, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RestrictionToAlgebraicSpace.lean, line 773. The attribute's comment: “the inverse image i_F! of the morphism of sites”.

Stacks 073M. The inverse image π_F^{-1} = i_{F,!} of the source: lower shriek along the functor F_étale ⥤ 𝒳, the sheafification of the left Kan extension of a sheaf of sets on the small étale site of F. It is the left adjoint of restriction i_F^{-1}.

noncomputable def lowerShriek (hp : p.IsFiberedInGroupoids)
    (e : StacksRepresentableCFG.EquivalenceOver p
      (presheafOfCategories (F ⋙ typeToCat)).p) :
    Sheaf (SmallEtale.topology B S hS F) (Type u) ⥤
      Sheaf (BigFppfOver.associatedTopology B S hS p .etale) (Type u)

AlgebraicGeometry.Space.lowerShriekAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RestrictionToAlgebraicSpace.lean, line 792. The attribute's comment: “the direct image of the morphism of sites is the inverse image of i_F”.

Stacks 073M. π_{F,*} = i_F^{-1} is right adjoint to π_F^{-1} = i_{F,!}.

This is the source's "Moreover π_{F,*} = i_F^{-1}": the direct image of π_F is restriction along the functor F_étale ⥤ 𝒳, which is exactly the inverse image of i_F recorded by AlgebraicGeometry.Space.restrictionToposHom_inverseImage.

noncomputable def lowerShriekAdjunction (hp : p.IsFiberedInGroupoids)
    (e : StacksRepresentableCFG.EquivalenceOver p
      (presheafOfCategories (F ⋙ typeToCat)).p) :
    letI := restrictionFunctor_isContinuous B S hS F p hp e
    lowerShriek B S hS F p hp e ⊣
      (restrictionFunctor B S hS F p e).sheafPushforwardContinuous (Type u)
        (SmallEtale.topology B S hS F)
        (BigFppfOver.associatedTopology B S hS p .etale)

AlgebraicGeometry.Space.lowerShriek_preservesFiniteLimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RestrictionToAlgebraicSpace.lean, line 814. The attribute's comment: “left exactness of i_F! on sheaves of sets”.

Stacks 073M. i_{F,!} is left exact on sheaves of sets.

This is the claim the source proves in order to define π_F: the small étale site of F has binary products and fibre products, which the functor F_étale ⥤ 𝒳 preserves, so the left Kan extension is a pointwise filtered colimit and commutes with fibre products; and the images of the étale charts cover the final object, which gives i_{F,!}* = *.

theorem lowerShriek_preservesFiniteLimits (hF : IsAlgebraicSpace B S hS F)
    (hp : p.IsFiberedInGroupoids)
    (e : StacksRepresentableCFG.EquivalenceOver p
      (presheafOfCategories (F ⋙ typeToCat)).p) :
    PreservesFiniteLimits (lowerShriek B S hS F p hp e)

AlgebraicGeometry.Space.lowerShriek_preservesFiniteColimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RestrictionToAlgebraicSpace.lean, line 832. The attribute's comment: “right exactness of i_F! on sheaves of sets”.

Stacks 073M. i_{F,!} is right exact on sheaves of sets, being a left adjoint.

theorem lowerShriek_preservesFiniteColimits (hp : p.IsFiberedInGroupoids)
    (e : StacksRepresentableCFG.EquivalenceOver p
      (presheafOfCategories (F ⋙ typeToCat)).p) :
    PreservesFiniteColimits (lowerShriek B S hS F p hp e)

AlgebraicGeometry.Space.restrictionFunctor_isMorphismOfSites, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RestrictionToAlgebraicSpace.lean, line 844. The attribute's comment: “the functor from the small etale site defines a morphism of sites”.

Stacks 073M. The functor F_étale ⥤ 𝒳 defines a morphism of sites π_F : 𝒳_étale ⟶ F_étale: restriction along it has a left exact left adjoint, namely i_{F,!}.

theorem restrictionFunctor_isMorphismOfSites (hF : IsAlgebraicSpace B S hS F)
    (hp : p.IsFiberedInGroupoids)
    (e : StacksRepresentableCFG.EquivalenceOver p
      (presheafOfCategories (F ⋙ typeToCat)).p) :
    IsMorphismOfSites.{u} (restrictionFunctor B S hS F p e)
      (SmallEtale.topology B S hS F)
      (BigFppfOver.associatedTopology B S hS p .etale)

AlgebraicGeometry.Space.lowerShriekAdjunction_unit_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RestrictionToAlgebraicSpace.lean, line 863. The attribute's comment: “the unit of i_F! ⊣ i_F^{-1} is an isomorphism, so π_F ∘ i_F = id”.

Stacks 073M. π_F ∘ i_F = id.

The inverse image of the composite is i_F^{-1} ∘ π_F^{-1} = i_F^{-1} ∘ i_{F,!}, so the composite is the identity exactly when the unit ℱ ⟶ i_F^{-1} i_{F,!} ℱ of i_{F,!} ⊣ i_F^{-1} is an isomorphism. That holds because the functor F_étale ⥤ 𝒳 is continuous, cocontinuous and fully faithful, which presents the small étale topos of F as a subtopos of that of 𝒳.

theorem lowerShriekAdjunction_unit_isIso (hp : p.IsFiberedInGroupoids)
    (e : StacksRepresentableCFG.EquivalenceOver p
      (presheafOfCategories (F ⋙ typeToCat)).p) :
    letI := restrictionFunctor_isContinuous B S hS F p hp e
    IsIso (lowerShriekAdjunction B S hS F p hp e).unit
Tag 0GQA, a remark

Tag 0GQA in the Stacks Project.

AlgebraicGeometry.Space.etaleLocalizationRingedSquares, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RestrictionEtaleLocalization.lean, line 479. The attribute's comment: “both squares of the diagram formed by i_F, i_G, pi_F, pi_G, f and f_small commute as diagrams of ringed topoi, for an etale induced morphism f : F -> G”.

Stacks 0GQA. Let f : 𝒳 ⥤ 𝒴 be a morphism of categories fibred in groupoids over (Sch/S)_{fppf}, with 𝒳 and 𝒴 representable by algebraic spaces F and G through the chosen equivalences eF and eG, such that the induced morphism of algebraic spaces f : F ⟶ G (AlgebraicGeometry.Space.inducedSpacesHom) is étale, and let f_small be the corresponding morphism of small étale ringed topoi (AlgebraicGeometry.Space.smallEtaleRingedToposHom). Then the diagram 

(Sh(F_étale), 𝒪_F) --f_small--> (Sh(G_étale), 𝒪_G)
       |                              |
      i_F                            i_G
       v                              v
(Sh(𝒳_étale), 𝒪_𝒳) -----f-----> (Sh(𝒴_étale), 𝒪_𝒴)
       |                              |
      π_F                            π_G
       v                              v
(Sh(F_étale), 𝒪_F) --f_small--> (Sh(G_étale), 𝒪_G)
is a commutative diagram of ringed topoi: the first component is a 2-isomorphism (Stacks 04IC) f ∘ i_F ≅ i_G ∘ f_small of morphisms of ringed topoi, the second a 2-isomorphism π_G ∘ f ≅ f_small ∘ π_F. Here i_F, i_G are AlgebraicGeometry.Space.restrictionRingedToposHom and π_F, π_G are AlgebraicGeometry.Space.projectionRingedToposHom (Stacks 073M), and the middle arrow is AlgebraicGeometry.FibredSite.ringedToposMorphism (Stacks 06TW), whose direct image exists by AlgebraicGeometry.Space.hasPointwiseRightKanExtension_op_of_equivalenceOver.

noncomputable def etaleLocalizationRingedSquares
    (hg : IsEtale B S hS
      (inducedSpacesHom B S hS (X := ⟨F, hF⟩) (Y := ⟨G, hG⟩) p q eF eG f hf.comp_eq).hom) :
    letI : ∀ P : 𝒳ᵒᵖ ⥤ Type u, f.op.HasPointwiseRightKanExtension P :=
      hasPointwiseRightKanExtension_op_of_equivalenceOver B S hS F p G q eF eG f
    RingedToposHom.TwoIso (A := smallEtaleRingedTopos B S hS ⟨F, hF⟩)
        (B := FibredSite.associatedRingedTopos B S hS q hq .etale)
        (etaleSquareFibredLeg B S hS F p q hp hq hF eF f hf)
        (etaleSquareSpaceLeg B S hS F G p q hq hF hG eF eG f hf) ×
      RingedToposHom.TwoIso (A := FibredSite.associatedRingedTopos B S hS p hp .etale)
        (B := smallEtaleRingedTopos B S hS ⟨G, hG⟩)
        (restrictionSquareFibredLeg B S hS G p q hp hq hG eG f hf)
        (restrictionSquareSpaceLeg B S hS F G p hp hF hG eF
          (inducedSpacesHom B S hS (X := ⟨F, hF⟩) (Y := ⟨G, hG⟩) p q eF eG f hf.comp_eq))
Tag 075K, an equation

Tag 075K in the Stacks Project.

AlgebraicGeometry.Space.moduleRestriction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuasicoherentRestrictionAlgebraicSpace.lean, line 184. The attribute's comment: “the restriction of a module to the small étale site of the representing space”.

The restriction ℱ|_{X_étale} = i_X^*ℱ = π_{X,*}ℱ of an 𝒪_𝒳-module on the inherited étale site of a category fibred in groupoids representable by the algebraic space X, as an 𝒪_X-module on the small étale site of X: the pushforward along the continuous functor u_X : X_étale ⥤ 𝒳 of Stacks 073M, with coefficient homomorphism AlgebraicGeometry.Space.restrictionStructureHom.

noncomputable def moduleRestriction :
    SheafOfModules.{m} (FibredSite.ringStructureSheafCore B S hS p hp .etale) ⥤
      Modules.{u, m} B S hS X.1 X.2

AlgebraicGeometry.Space.projectionRingedToposHom_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RestrictionProjection.lean, line 314. The attribute's comment: “the identification ℱ|_{F_étale} = π_{F, *}ℱ”.

Stacks 073M, equation 075K. The direct image of π_F is restriction along the functor F_étale ⥤ 𝒳, that is, π_{F,*}ℱ(U) = ℱ(u(U)).

This is the right-hand identification ℱ|_{F_étale} = π_{F, *}ℱ of equation 075K: the right-hand side here is the term that AlgebraicGeometry.Space.restrictionSheafFunctor names ℱ|_{F_étale}. The left-hand identification ℱ|_{F_étale} = i_F^{-1}ℱ is AlgebraicGeometry.Space.restrictionToposHom_inverseImage; together they give the chain.

theorem projectionRingedToposHom_pushforward (hp : p.IsFiberedInGroupoids)
    (hF : IsAlgebraicSpace B S hS F)
    (e : StacksRepresentableCFG.EquivalenceOver p
      (presheafOfCategories (F ⋙ typeToCat)).p) :
    letI := restrictionFunctor_isContinuous B S hS F p hp e
    (projectionRingedToposHom B S hS F p hp hF e).toToposHom.pushforward =
      (restrictionFunctor B S hS F p e).sheafPushforwardContinuous (Type u)
        (SmallEtale.topology B S hS F)
        (BigFppfOver.associatedTopology B S hS p .etale)

AlgebraicGeometry.Space.restrictionToposHom_inverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RestrictionToAlgebraicSpace.lean, line 496. The attribute's comment: “the identification ℱ|_{F_étale} = i_F^{-1}ℱ”.

Stacks 073M, equation 075K. The inverse image of i_F is restriction along the functor F_étale ⥤ 𝒳. This is the source's π_{F,*} = i_F^{-1}: both send a sheaf ℱ to U ↦ ℱ(u(U)).

It is also the left-hand identification ℱ|_{F_étale} = i_F^{-1}ℱ of equation 075K, the right-hand side of this statement being the term that AlgebraicGeometry.Space.restrictionSheafFunctor names ℱ|_{F_étale}. The right-hand identification ℱ|_{F_étale} = π_{F, *}ℱ is AlgebraicGeometry.Space.projectionRingedToposHom_pushforward.

theorem restrictionToposHom_inverseImage (hp : p.IsFiberedInGroupoids)
    (e : StacksRepresentableCFG.EquivalenceOver p
      (presheafOfCategories (F ⋙ typeToCat)).p) :
    letI := restrictionFunctor_isContinuous B S hS F p hp e
    (restrictionToposHom B S hS F p hp e).inverseImage =
      (restrictionFunctor B S hS F p e).sheafPushforwardContinuous (Type u)
        (SmallEtale.topology B S hS F)
        (BigFppfOver.associatedTopology B S hS p .etale)

AlgebraicGeometry.Space.restrictionSheafFunctor, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RestrictionToAlgebraicSpace.lean, line 509.

Stacks 073M, equation 075K. The restriction ℱ|_{F_étale} = i_F^{-1}ℱ of a sheaf on the inherited étale site of 𝒳 to the small étale site of the algebraic space F.

noncomputable abbrev restrictionSheafFunctor (hp : p.IsFiberedInGroupoids)
    (e : StacksRepresentableCFG.EquivalenceOver p
      (presheafOfCategories (F ⋙ typeToCat)).p) :
    letI := restrictionFunctor_isContinuous B S hS F p hp e
    Sheaf (BigFppfOver.associatedTopology B S hS p .etale) (Type u) ⥤
      Sheaf (SmallEtale.topology B S hS F) (Type u)

AlgebraicGeometry.Space.restrictionSheafFunctor_obj_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RestrictionToAlgebraicSpace.lean, line 522. The attribute's comment: “sections of a restriction”.

Stacks 073M, equation 075K. The sections of a restriction are the sections of the original sheaf on the image of the chart: ℱ|_{F_étale}(U) = ℱ(u(U)).

theorem restrictionSheafFunctor_obj_obj (hp : p.IsFiberedInGroupoids)
    (e : StacksRepresentableCFG.EquivalenceOver p
      (presheafOfCategories (F ⋙ typeToCat)).p)
    (𝓕 : Sheaf (BigFppfOver.associatedTopology B S hS p .etale) (Type u))
    (U : SmallEtale B S hS F) :
    ((restrictionSheafFunctor B S hS F p hp e).obj 𝓕).obj.obj (Opposite.op U) =
      𝓕.obj.obj (Opposite.op ((restrictionFunctor B S hS F p e).obj U))

Declarations registered for the tag:

Tag 073N, a lemma

Tag 073N in the Stacks Project.

AlgebraicGeometry.Space.restrictionRingedSquareTwoIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RestrictionRingedSquareCommutes.lean, line 104. The attribute's comment: “the square of ringed topoi formed by pi_F, pi_G, the morphism induced by f and f_small commutes: its two composites are 2-isomorphic morphisms of ringed topoi”.

Let f : 𝒳 ⥤ 𝒴 be a morphism of categories fibred in groupoids over (Sch/S)_{fppf}, with 𝒳 and 𝒴 representable by algebraic spaces F and G through the chosen equivalences eF and eG. Write f : F ⟶ G for the induced morphism of algebraic spaces (AlgebraicGeometry.Space.inducedSpacesHom) and f_small for the corresponding morphism of small étale ringed topoi (AlgebraicGeometry.Space.smallEtaleRingedToposHom). Then the square 

(Sh(𝒳_étale), 𝒪_𝒳) ---f---> (Sh(𝒴_étale), 𝒪_𝒴)
       |                            |
      π_F                          π_G
       v                            v
(Sh(F_étale), 𝒪_F) --f_small--> (Sh(G_étale), 𝒪_G)
is a commutative diagram of ringed topoi: this is a 2-isomorphism of morphisms of ringed topoi (Stacks 04IC) between its two composites π_G ∘ f (AlgebraicGeometry.Space.restrictionSquareFibredLeg) and f_small ∘ π_F (AlgebraicGeometry.Space.restrictionSquareSpaceLeg), where π_F and π_G are the morphisms of ringed topoi of Stacks 073M and the upper arrow is the morphism of ringed topoi of Stacks 06TW.

Its underlying isomorphism π_{G,*}f_* ≅ f_{small,*}π_{F,*} is the canonical comparison map of equation 075M, which is invertible by AlgebraicGeometry.Space.isIso_restrictedDirectImageComparison, and its compatibility with the structure sheaves is AlgebraicGeometry.Space.restrictedDirectImageComparison_structureSheafCompatible. The direct image f_* exists with no size hypothesis, by AlgebraicGeometry.Space.hasPointwiseRightKanExtension_op_of_equivalenceOver.

noncomputable def restrictionRingedSquareTwoIso :
    letI : ∀ P : 𝒳ᵒᵖ ⥤ Type u, f.op.HasPointwiseRightKanExtension P :=
      hasPointwiseRightKanExtension_op_of_equivalenceOver B S hS F p G q eF eG f
    RingedToposHom.TwoIso
      (A := FibredSite.associatedRingedTopos B S hS p hp .etale)
      (B := smallEtaleRingedTopos B S hS ⟨G, hG⟩)
      (restrictionSquareFibredLeg B S hS G p q hp hq hG eG f hf)
      (restrictionSquareSpaceLeg B S hS F G p hp hF hG eF
        (inducedSpacesHom B S hS (X := ⟨F, hF⟩) (Y := ⟨G, hG⟩) p q eF eG f hf.comp_eq))
Tag 075M, an equation

Tag 075M in the Stacks Project.

AlgebraicGeometry.Space.restrictedDirectImageChartEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RestrictionDirectImage.lean, line 204. The attribute's comment: “the left-hand side, as sections over the 2-fibre product at a chart”.

Equation 075M, left-hand side. The sections of the restriction (f_*ℱ)|_{G_étale} of a direct image to the small étale site of the algebraic space G representing 𝒴, at a chart V of G, are the global sections of the pullback of ℱ to the 2-fibre product (Sch/V)_{fppf} ×_{u_G V, 𝒴} 𝒳.

This is the opening display of the source's proof of Stacks 073N, from which equation 075M is drawn: π_{G,*}f_*ℱ(V) = f_*ℱ(V/G) = Γ((Sch/V)_{fppf} ×_𝒴 𝒳, pr^{-1}ℱ). The first step is equation 075K, that restriction is evaluation at u_G V; the second is Stacks 06W6.

Only the left-hand side of 075M is covered. Identifying these sections with those of f_{small,*}(ℱ|_{F_étale}) is the content of Stacks 073N, which is not proved in this library; the implementation notes of this file say which input to the identification is still missing. Accordingly 𝒳 is an arbitrary category fibred in groupoids here, with no representability assumed of it.

noncomputable def restrictedDirectImageChartEquiv (hp : p.IsFiberedInGroupoids)
    (hq : q.IsFiberedInGroupoids)
    (eG : StacksRepresentableCFG.EquivalenceOver q (presheafOfCategories (G ⋙ typeToCat)).p)
    (f : 𝒳 ⥤ 𝒴) (hf : p.IsFibredOneMorphism q f) (c : q.ChoiceOfPullbacks)
    [∀ H : 𝒳ᵒᵖ ⥤ Type u, f.op.HasPointwiseRightKanExtension H]
    (ℱ : Sheaf (BigFppfOver.associatedTopology B S hS p .etale) (Type u))
    (V : SmallEtale B S hS G) :
    ((restrictionSheafFunctor B S hS G q hq eG).obj
        ((etaleDirectImage B S hS p q hp f hf).obj ℱ)).obj.obj (op V) ≃
      Presheaf.globalSections
        ((TwoFibreProductOver.snd (Over.forget ((SmallEtale.toOver B S hS G).obj V)) p q
          (c.sliceFunctor (chartFiberObj B S hS G q eG V)) f).op ⋙ ℱ.obj)

AlgebraicGeometry.Space.restrictedDirectImageComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RestrictionDirectImageComparison.lean, line 585. The attribute's comment: “the comparison map between the two sides, natural in the sheaf: both sides of the equation are present -- the left-hand side (f_*F)|_{G_etale} as the direct image of restrictionSquareFibredLeg and the right-hand side f_{small,*}(F|_{F_etale}) as that of restrictionSquareSpaceLeg -- together with the canonical map from the first to the second and its naturality in the sheaf. That this map is an ISOMORPHISM, which is what the displayed equality asserts, is isIso_restrictedDirectImageComparison of StacksFrontier/AlgebraicGeometry/Stacks/RestrictionDirectImageComparisonIso.lean, which reduces it by isIso_restrictedDirectImageComparison_of_bijective to a bijection on sections over one etale scheme chart of G at a time. The compatibility ha of the 1-morphism f with the morphism fSpace of algebraic spaces through the two chosen presentations is a hypothesis; it is realized for every fSpace by exists_comparisonChartFunctorIso”.

Equation 075M. The comparison of the two direct images around the square of Stacks 073N: the canonical map π_{G,*}f_*ℱ ⟶ f_{small,*}(ℱ|_{F_étale}), natural in ℱ, whose source is the left-hand side (f_*ℱ)|_{G_étale} of equation 075M and whose target is its right-hand side.

Its value on sections over a diagram of étale scheme charts is AlgebraicGeometry.Space.restrictedDirectImageComparisonSections. That it is an isomorphism, which is what the displayed equality of the source asserts, is AlgebraicGeometry.Space.isIso_restrictedDirectImageComparison of StacksFrontier/AlgebraicGeometry/Stacks/RestrictionDirectImageComparisonIso.lean.

noncomputable def restrictedDirectImageComparison :
    (restrictionSquareFibredLeg B S hS G p q hp hq hG eG f hf).toToposHom.pushforward ⟶
      (restrictionSquareSpaceLeg B S hS F G p hp hF hG eF fSpace).toToposHom.pushforward

AlgebraicGeometry.Space.exists_restrictedDirectImageComparisonTarget_equalizer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RestrictionDirectImageComparison.lean, line 615. The attribute's comment: “the right-hand side f_{small,*}(F|_{F_etale}), as an equalizer of sections of F|_{F_etale} over two etale scheme charts of F, at a chart V of G”.

The right-hand side of equation 075M at a chart, as an equalizer. The target of the comparison map is f_{small,*}(ℱ|_{F_étale}); its sections over an étale scheme chart V of G are the equalizer of the sections of ℱ|_{F_étale} over an étale scheme chart W of F covering F ×_G V and over a chart W' presenting the self-fibre product of W over F ×_G V.

This is AlgebraicGeometry.Space.exists_smallEtaleDirectImageChartEqualizerEquiv — Tag 03H7 for the direct image on the small étale sites — specialized at the chart of equation 075M. The target of the comparison is that direct image on the nose: the direct image of the geometric morphism underlying AlgebraicGeometry.Space.smallEtaleRingedToposHom is the spaces-étale direct image of Stacks 03G2 conjugated by the comparison equivalences of Stacks 03G1, which is how AlgebraicGeometry.Space.smallEtaleDirectImage is defined.

theorem exists_restrictedDirectImageComparisonTarget_equalizer
    (ℱ : Sheaf (BigFppfOver.associatedTopology B S hS p .etale) (Type u))
    (V : SmallEtale B S hS G) :
    ∃ (W W' : SmallEtale B S hS F) (a b : W' ⟶ W),
      Nonempty (((smallEtaleRingedToposHom B S hS fSpace).toToposHom.pushforward.obj
            ((restrictionSheafFunctor B S hS F p hp eF).obj ℱ)).obj.obj (op V) ≃
        {y : ((restrictionSheafFunctor B S hS F p hp eF).obj ℱ).obj.obj (op W) //
          ((restrictionSheafFunctor B S hS F p hp eF).obj ℱ).obj.map a.op y =
            ((restrictionSheafFunctor B S hS F p hp eF).obj ℱ).obj.map b.op y})

AlgebraicGeometry.Space.isIso_restrictedDirectImageComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RestrictionDirectImageComparisonIso.lean, line 399. The attribute's comment: “the displayed equality itself: the canonical comparison map between the two sides is an isomorphism”.

Equation 075M. The canonical comparison map of equation 075M, AlgebraicGeometry.Space.restrictedDirectImageComparison, is an isomorphism: the two sides of the equation, 

(f_*ℱ)|_{G_étale} = f_{small,*}(ℱ|_{F_étale}),
agree, naturally in the sheaf, through that canonical map.

Invertibility is reduced to a bijection on sections over each étale scheme chart V of G by AlgebraicGeometry.Space.isIso_restrictedDirectImageComparison_of_bijective, and there:

  • injectivity is AlgebraicGeometry.Space.injective_restrictedDirectImageComparisonHom_app. A section of f_*ℱ over u_G V is determined by its values at the pairs (Z, κ : f(Z) ⟶ u_G V) (Stacks 06W6), the chart correspondence of Stacks 03G8 determines those values at the morphisms out of the image of an étale chart of F, and the factorization lemma together with the sheaf condition on ℱ carries that to all of them.
  • surjectivity is AlgebraicGeometry.Space.surjective_restrictedDirectImageComparisonHom_app. The canonical restrictions of a section of the right-hand side to the diagrams of étale scheme charts over V form a family which the refinement of two chart diagrams shows compatible, the sheaf condition on ℱ glues that family to a value at every pair (Z, κ), and those values are the components of a global section over the 2-fibre product (Sch/V)_{fppf} ×_𝒴 𝒳 — a section of the left-hand side. It is carried to the given section because a section of the right-hand side is determined by its restriction to one diagram whose chart covers the cartesian base change F ×_G V, which is Properties of Spaces 03H7.

The choice of pullbacks that the pushforward formula of Stacks 06W6 needs is not a hypothesis: a category fibred in groupoids admits one.

theorem isIso_restrictedDirectImageComparison :
    IsIso (restrictedDirectImageComparison B S hS F G p q hp hq hF hG eF eG f hf fSpace ha)

AlgebraicGeometry.Space.exists_restrictedDirectImageComparisonSource_equalizer, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RestrictionDirectImageLeftEqualizer.lean, line 363. The attribute's comment: “the left-hand side (f_*F)|_{G_etale}, as an equalizer of sections of F over two objects of the 2-fibre product (Sch/V)_fppf x_Y X, at a chart V of G. This is the counterpart of exists_restrictedDirectImageComparisonTarget_equalizer, which is the right-hand side at the same chart; with both sides presented the comparison map is a map of equalizer diagrams. The representability of the 2-fibre product by an algebraic space over S -- the identification of (Sch/V)_fppf x_Y X with the split category fibred in groupoids of V x_G F that the source's proof of Tag 073N makes -- is supplied by exists_isAlgebraicSpace_twoFibreProductStructureFunctor from the presentations of X and Y alone”.

Equation 075M, the left-hand side at a chart, as an equalizer. The sections of (f_*ℱ)|_{G_étale} over an étale scheme chart V of G are the equalizer of the sections of ℱ over two objects of the 2-fibre product (Sch/V)_{fppf} ×_𝒴 𝒳, namely an object A coming from an étale scheme chart of an algebraic space representing that 2-fibre product and the object presenting the self-product of A.

This is the counterpart of AlgebraicGeometry.Space.exists_restrictedDirectImageComparisonTarget_equalizer, which presents the right-hand side at the same chart as an equalizer of sections of ℱ|_{F_étale} over two étale scheme charts of F. With both sides presented, the comparison map of equation 075M is a map between two equalizer diagrams, which is the shape in which the source proves it invertible.

The hypotheses are those of equation 075M itself: 𝒳 and 𝒴 are presented by the algebraic spaces F and G and f is a 1-morphism of fibred categories between them. The representability of the 2-fibre product that the equalizer presentation needs — the identification the source makes in its proof of Stacks 073N — is supplied by AlgebraicGeometry.Space.exists_isAlgebraicSpace_twoFibreProductStructureFunctor, and the equalizer itself by exists_restrictedDirectImageComparisonSource_equalizer_of_equivalenceOver.

theorem exists_restrictedDirectImageComparisonSource_equalizer
    (Fpsh : (BigFppfOver B S hS)ᵒᵖ ⥤ Type u) (hFpsh : IsAlgebraicSpace B S hS Fpsh)
    (eFpsh : StacksRepresentableCFG.EquivalenceOver p
      (presheafOfCategories (Fpsh ⋙ typeToCat)).p)
    (hG : IsAlgebraicSpace B S hS G) (hf : p.IsFibredOneMorphism q f)
    [∀ H : 𝒳ᵒᵖ ⥤ Type u, f.op.HasPointwiseRightKanExtension H]
    (ℱ : Sheaf (BigFppfOver.associatedTopology B S hS p .etale) (Type u))
    (V : SmallEtale B S hS G) :
    ∃ (A A' : TwoFibreProductOver (Over.forget ((SmallEtale.toOver B S hS G).obj V)) p q
          (c.sliceFunctor (chartFiberObj B S hS G q eG V)) f) (a b : A' ⟶ A),
      Nonempty (((restrictionSheafFunctor B S hS G q hq eG).obj
            ((etaleDirectImage B S hS p q hp f hf).obj ℱ)).obj.obj (op V) ≃
        {y : ℱ.obj.obj (op ((twoFibreProductSnd B S hS G p q eG f c V).obj A)) //
          ℱ.obj.map ((twoFibreProductSnd B S hS G p q eG f c V).map a).op y =
            ℱ.obj.map ((twoFibreProductSnd B S hS G p q eG f c V).map b).op y})
Tag 076Q, an equation

Tag 076Q in the Stacks Project.

AlgebraicGeometry.Space.comparisonAlgebraicSpaces, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RestrictionComparisonAlgebraicSpace.lean, line 425. The attribute's comment: “the comparison map of a 2-commutative triangle, on sheaves of sets”.

The comparison map

c_φ : a_small⁻¹(g⁻¹ℱ|_{V_étale}) ⟶ f⁻¹ℱ|_{U_étale}

of a 2-commutative triangle φ : a ⋙ g ≅ f of 1-morphisms of categories fibred in groupoids over (Sch/S)_{fppf} whose two source categories 𝒰, 𝒱 are representable by algebraic spaces U, V, for a sheaf ℱ on the inherited étale site of 𝒳.

Here a_small is the morphism of small étale topoi attached to the morphism aSpace : U ⟶ V of algebraic spaces corresponding to a, and c_φ is the adjoint, under a_small⁻¹ ⊣ a_{small,*}, of AlgebraicGeometry.Space.comparisonPushforwardHom.

noncomputable def comparisonAlgebraicSpaces
    (ℱ : Sheaf (BigFppfOver.associatedTopology B S hS r .etale) (Type u)) :
    (smallToposMorphismTypeU B S hS aSpace).inverseImage.obj
        (etaleRestrictedInverseImage B S hS q r hq eV g hg ℱ) ⟶
      etaleRestrictedInverseImage B S hS p r hp eU f hf ℱ
Tag 076R, an equation

Tag 076R in the Stacks Project.

AlgebraicGeometry.Space.comparisonAlgebraicSpacesModules, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/RestrictionComparisonAlgebraicSpace.lean, line 605. The attribute's comment: “the comparison map of a 2-commutative triangle, on modules”.

The comparison map

c_φ : a_small^*(g^*ℱ|_{V_étale}) ⟶ f^*ℱ|_{U_étale}

of a 2-commutative triangle φ : a ⋙ g ≅ f of 1-morphisms of categories fibred in groupoids over (Sch/S)_{fppf} whose two source categories 𝒰, 𝒱 are representable by algebraic spaces U, V, for an 𝒪_𝒳-module ℱ on the inherited étale site of 𝒳.

Here a_small^* is the inverse image of modules (AlgebraicGeometry.Space.modulePullback) for the morphism aSpace : U ⟶ V of algebraic spaces corresponding to a, and c_φ is the adjoint, under a_small^* ⊣ a_{small,*}, of AlgebraicGeometry.Space.moduleComparisonPushforwardHom.

noncomputable def comparisonAlgebraicSpacesModules
    (ℱ : inheritedEtaleModules B S hS r hr) :
    (modulePullback B S hS aSpace).obj
        (etaleRestrictedModuleInverseImage B S hS q r hq hr eV g hg ℱ) ⟶
      etaleRestrictedModuleInverseImage B S hS p r hp hr eU f hf ℱ
Sources
LeanAlgebraicGeometry.Space.projectionRingedToposHom · AlgebraicGeometry.Space.projectionRingedToposHom_pushforward · AlgebraicGeometry.Space.restrictionFunctor_isContinuous · AlgebraicGeometry.Space.restrictionFunctor_isCocontinuous · AlgebraicGeometry.Space.restrictionToposHom · AlgebraicGeometry.Space.restrictionToposHom_inverseImage · AlgebraicGeometry.Space.inverseImage_structureSheaf_eq · AlgebraicGeometry.Space.restrictionRingedToposHom

Section96.11 Quasi-coherent modules#

Section 96.11 of the Stacks Project, Tag 06WF. 4 tags here are carried by 5 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06WG, a definition

Tag 06WG in the Stacks Project.

AlgebraicGeometry.FibredSite.quasicoherentModules, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Modules.lean, line 53.

The category of quasi-coherent modules on the fppf ringed site of a category fibred in groupoids over the schemes over S.

public abbrev quasicoherentModules
Tag 06WH, a lemma

Tag 06WH in the Stacks Project.

AlgebraicGeometry.Stack.isQuasicoherentOnSite_modulePullback, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/ModulePullback.lean, line 215.

Stacks 06WH. The inverse image of sheaves of modules along a 1-morphism of categories fibred in groupoids over the big fppf category of S preserves quasi-coherence.

The inverse image is AlgebraicGeometry.Stack.modulePullback, which on underlying presheaves of modules is restriction along the 1-morphism followed by the change of scalars identifying the two structure presheaves; and the slices of a 1-morphism of categories fibred in groupoids are equivalences by Stacks 06W0.

instance isQuasicoherentOnSite_modulePullback
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 𝒴 : Type v} [Category.{w} 𝒳] [Category.{w} 𝒴]
    (p : 𝒳 ⥤ BigFppfOver B S hS) (q : 𝒴 ⥤ BigFppfOver B S hS)
    (hp : p.IsFiberedInGroupoids) (hq : q.IsFiberedInGroupoids)
    (f : 𝒳 ⥤ 𝒴) (hf : f ⋙ q = p)
    (M : SheafOfModules.{max u v w m}
      (ringStructureSheafCore B S hS q hq B.topology le_rfl))
    [M.IsQuasicoherentOnSite] :
    ((modulePullback.{u, v, w, max u v w m} B S hS p q hp hq f hf
      B.topology le_rfl).obj M).IsQuasicoherentOnSite
Tag 06WI, a lemma

Tag 06WI in the Stacks Project.

AlgebraicGeometry.FibredSite.isQuasicoherentOnSite_iff_forall_objectInverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Descent/FibredSiteLocalization.lean, line 373.

Stacks 06WI. A sheaf of modules on the associated fppf site of a category fibred in groupoids is quasi-coherent if and only if its inverse image x^*𝓕 is a quasi-coherent sheaf on the big fppf site (Sch/U)_fppf of the scheme U = p(x), for every object x of 𝒳.

Necessity is stability of quasi-coherence under restriction to a slice site, transported along the equivalence of ringed sites 𝒳_fppf/x ≌ (Sch/U)_fppf. Sufficiency is Stacks 03DN for the family of all objects of 𝒳, which covers the final object: quasi-coherence is a local and intrinsic property, so no further input is needed.

public theorem isQuasicoherentOnSite_iff_forall_objectInverseImage
    (M : SheafOfModules.{u} (ringStructureSheafCore B S hS p hp .fppf)) :
    M.IsQuasicoherentOnSite ↔
      ∀ x : 𝒳, (objectInverseImage B S hS p hp x M).IsQuasicoherentOnSite
Tag 0EM8, a lemma

Tag 0EM8 in the Stacks Project.

AlgebraicGeometry.FibredSite.tfae_isQuasicoherentClause, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/SiteEquivalence.lean, line 282. The attribute's comment: “the three-way equivalence, with the two inputs at each of the Zariski and the étale topology carried as explicit hypotheses: h₁z/h₁e, a τ-sheaf of modules that is quasi-coherent on (𝒳_τ, 𝒪_𝒳) is a sheaf for the inherited fppf topology, and h₂z/h₂e, quasi-coherence passes from the inherited fppf topology to a coarser one. At τ = .fppf both are discharged here. Neither is discharged at τ = .zariski or τ = .etale: both funnel into the essential-surjectivity half of Descent, Proposition 03DX, which this repository does not prove and carries as the hypothesis AlgebraicGeometry.BigFppfOver.QuasicoherentIsEssImageAssociatedModule, its only open reduction being AlgebraicGeometry.BigFppfOver.AssociatedModuleGlueDescentDatum; the two existing 03DX declarations state the different criterion that quasi-coherence on the small étale site of an algebraic space is equivalent to being cartesian on affine charts”.

The three-way equivalence of Stacks 0EM8, over its two inputs at the Zariski and the étale topology: for a presheaf of modules on a category fibred in groupoids over the big fppf category of schemes over S, being a quasi-coherent Zariski module, being a quasi-coherent étale module, and being a quasi-coherent module on 𝒳 in the sense of Stacks 06WG are equivalent.

public theorem tfae_isQuasicoherentClause
    (h₁z : IsSheafFppfOfQuasicoherentOnSite B S hS p hp .zariski)
    (h₁e : IsSheafFppfOfQuasicoherentOnSite B S hS p hp .etale)
    (h₂z : QuasicoherentOnSiteOfLeFppf B S hS p hp .zariski)
    (h₂e : QuasicoherentOnSiteOfLeFppf B S hS p hp .etale)
    (𝓕 : PresheafOfModules.{u} (structureRingPresheaf B S hS p hp)) :
    [IsQuasicoherentClause B S hS p hp .zariski 𝓕,
      IsQuasicoherentClause B S hS p hp .etale 𝓕,
      IsQuasicoherentClause B S hS p hp .fppf 𝓕].TFAE

AlgebraicGeometry.FibredSite.tfae_isQuasicoherentClause', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/SiteEquivalenceAffine.lean, line 280. The attribute's comment: “the three-way equivalence, for a category fibred in groupoids over the big fppf category of schemes over S and a presheaf of modules on it”.

Stacks 0EM8. For a category 𝒳 fibred in groupoids over the big fppf category of schemes over S and a presheaf of modules 𝓕 on 𝒳, the three conditions

  1. 𝓕 is an object of Mod(𝒳_Zar, 𝒪_𝒳) and is quasi-coherent on (𝒳_Zar, 𝒪_𝒳),
  2. 𝓕 is an object of Mod(𝒳_ét, 𝒪_𝒳) and is quasi-coherent on (𝒳_ét, 𝒪_𝒳),
  3. 𝓕 is a quasi-coherent module on 𝒳 in the sense of Stacks 06WG, that is on (𝒳_fppf, 𝒪_𝒳),

are equivalent.

This is AlgebraicGeometry.FibredSite.tfae_isQuasicoherentClause with its four hypotheses discharged by AlgebraicGeometry.FibredSite.isSheafFppfOfQuasicoherentOnSite_zariski, AlgebraicGeometry.FibredSite.isSheafFppfOfQuasicoherentOnSite_etale, AlgebraicGeometry.FibredSite.quasicoherentOnSiteOfLeFppf_zariski and AlgebraicGeometry.FibredSite.quasicoherentOnSiteOfLeFppf_etale.

public theorem tfae_isQuasicoherentClause'
    (𝓕 : PresheafOfModules.{u} (structureRingPresheaf B S hS p hp)) :
    [IsQuasicoherentClause B S hS p hp .zariski 𝓕,
      IsQuasicoherentClause B S hS p hp .etale 𝓕,
      IsQuasicoherentClause B S hS p hp .fppf 𝓕].TFAE
Sources
LeanAlgebraicGeometry.FibredSite.quasicoherentModules · AlgebraicGeometry.Stack.isQuasicoherentOnSite_modulePullback · AlgebraicGeometry.FibredSite.isQuasicoherentOnSite_iff_forall_objectInverseImage · AlgebraicGeometry.FibredSite.tfae_isQuasicoherentClause · AlgebraicGeometry.FibredSite.tfae_isQuasicoherentClause'

Section96.12 Locally quasi-coherent modules#

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

Tag 06WJ, a definition

Tag 06WJ in the Stacks Project.

AlgebraicGeometry.Stack.restrictModuleToSmallEtale, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/LocallyQuasicoherent.lean, line 113. The attribute's comment: “the restriction to the small étale site”.

Stacks 06WJ. The restriction x^*F|_{U_ét} at an object x of a presheaf of modules on 𝒳 to the small étale site of the scheme U below x: restrict the underlying abelian presheaf as in Stacks 06W1, then transport the scalars through AlgebraicGeometry.Stack.localStructurePresheafIso.

noncomputable def restrictModuleToSmallEtale {𝒳 : Type v} [Category.{w} 𝒳]
    (p : 𝒳 ⥤ BigFppfOver B S hS) (hp : p.IsFiberedInGroupoids) (x : 𝒳)
    (τ : GrothendieckTopology B.Schemes) (hτ : τ ≤ B.topology)
    (F : PresheafOfModules.{m} (ringStructureSheafCore B S hS p hp τ hτ).obj) :
    PresheafOfModules.{m}
      (SmallEtale.structureSheaf E (p.obj x).left.1 (contains_base B E h S hS p x)).obj

AlgebraicGeometry.Stack.IsLocallyQuasicoherent, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/LocallyQuasicoherent.lean, line 146. The attribute's comment: “local quasi-coherence”.

Stacks 06WJ. A presheaf of modules over the structure sheaf of a category fibred in groupoids is locally quasi-coherent when it is a sheaf for the étale topology and, at every object x of 𝒳, its restriction to the small étale site of the scheme below x is a quasi-coherent sheaf of modules.

The source calls the notation nonstandard; it is the condition under which the module is determined by quasi-coherent modules on the small étale sites of the objects.

noncomputable abbrev IsLocallyQuasicoherent {𝒳 : Type v} [Category.{w} 𝒳]
    (p : 𝒳 ⥤ BigFppfOver B S hS) (hp : p.IsFiberedInGroupoids)
    (F : PresheafOfModules.{m}
      (ringStructureSheafCore B S hS p hp (etaleTopology B) (etaleTopology_le_topology B)).obj) :
    Prop
Tag 06WK, a lemma

Tag 06WK in the Stacks Project.

AlgebraicGeometry.Stack.isSheaf_etale_of_isQuasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentEtaleSheafClause.lean, line 124. The attribute's comment: “the étale sheaf condition, which is the first conjunct of clause (1), in the forward direction”.

Stacks 06WK. A quasi-coherent module on a category fibred in groupoids is a sheaf for the inherited étale topology.

This is the first conjunct of clause (1) of the source, local quasi-coherence being the étale sheaf condition together with quasi-coherence of the restrictions to the small étale sites, and it is the first step of the source's proof: quasi-coherence of F in the sense of Stacks 06WG asserts in particular that F is a sheaf for the inherited fppf topology, and the inherited étale topology is coarser.

theorem isSheaf_etale_of_isQuasicoherent {𝒳 : Type v} [Category.{w} 𝒳]
    (p : 𝒳 ⥤ BigFppfOver B S hS) (hp : p.IsFiberedInGroupoids)
    (F : PresheafOfModules.{m} (ringStructureSheafCore B S hS p hp
      (etaleTopology B) (etaleTopology_le_topology B)).obj)
    (hF : ∃ h : Presheaf.IsSheaf (associatedTopology B S hS p B.topology) F.presheaf,
      SheafOfModules.IsQuasicoherentOnSite
        (⟨F, h⟩ : SheafOfModules.{m}
          (ringStructureSheafCore B S hS p hp B.topology le_rfl))) :
    Presheaf.IsSheaf (associatedTopology B S hS p (etaleTopology B)) F.presheaf

AlgebraicGeometry.Stack.isQuasicoherentFppf_iff_isLocallyQuasicoherent_and_isIso_sheafifiedRestrictComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentIffComparisonIso.lean, line 396.

Stacks 06WK. A presheaf of modules F on a category fibred in groupoids 𝒳 over (Sch/S)_{fppf} is quasi-coherent (Stacks 06WG) if and only if

  1. F is locally quasi-coherent (Stacks 06WJ), and
  2. for every arrow φ : x ⟶ y of 𝒳 the comparison map c_φ : f_{small}^*(F|_{V_ét}) ⟶ F|_{U_ét} of Stacks 06WC, read on sheaves of modules on the small étale site of the scheme U below x, is an isomorphism.
theorem isQuasicoherentFppf_iff_isLocallyQuasicoherent_and_isIso_sheafifiedRestrictComparison
    (F : PresheafOfModules.{u} (ringStructureSheafCore B S hS p hp (etaleTopology B)
      (etaleTopology_le_topology B)).obj) :
    IsQuasicoherentFppf B S hS p hp F ↔
      ∃ hlqc : IsLocallyQuasicoherent B E h S hS p hp F,
        ∀ {x y : 𝒳} (φ : x ⟶ y),
          IsIso (sheafifiedRestrictComparison B E h S hS p hp F φ (hlqc.2 x).1)
Tag 06WL, a lemma

Tag 06WL in the Stacks Project.

AlgebraicGeometry.Stack.isLocallyQuasicoherent_modulePullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/LocallyQuasicoherentPullback.lean, line 296.

The inverse image of presheaves of modules along a 1-morphism of categories fibred in groupoids over the big fppf category of S preserves local quasi-coherence.

theorem isLocallyQuasicoherent_modulePullback
    (G : PresheafOfModules.{m} (ringStructureSheafCore B S hS q hq (etaleTopology B)
      (etaleTopology_le_topology B)).obj)
    (hG : IsLocallyQuasicoherent B E h S hS q hq G) :
    IsLocallyQuasicoherent B E h S hS (f ⋙ q) hp
      ((modulePresheafPullback.{u, v, w, v', w', m} B S hS q hq f hp).obj G)
Tag 06WM, a lemma

Tag 06WM in the Stacks Project.

AlgebraicGeometry.Stack.locallyQuasicoherentModules_colimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/LocallyQuasicoherentClosure.lean, line 89. The attribute's comment: “(1): LQCoh(𝒪_𝒳) has colimits and they agree with colimits in Mod(𝒳_ét, 𝒪_𝒳)”.

Stacks 06WM (1). The category LQCoh(𝒪_𝒳) of locally quasi-coherent modules has colimits, and they agree with colimits in Mod(𝒳_ét, 𝒪_𝒳): local quasi-coherence is closed under colimits computed in Mod(𝒳_ét, 𝒪_𝒳), the full subcategory therefore has them, and its inclusion preserves them.

theorem locallyQuasicoherentModules_colimits :
    (∀ (K : Type u) [Category.{u} K],
      (isLocallyQuasicoherent.{u, v, w, u} B E h S hS p hp).IsClosedUnderColimitsOfShape K) ∧
      HasColimitsOfSize.{u, u} (locallyQuasicoherentModules.{u, v, w, u} B E h S hS p hp) ∧
      PreservesColimitsOfSize.{u, u} (isLocallyQuasicoherent.{u, v, w, u} B E h S hS p hp).ι

AlgebraicGeometry.Stack.locallyQuasicoherentModules_abelian, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/LocallyQuasicoherentClosure.lean, line 104. The attribute's comment: “(2): LQCoh(𝒪_𝒳) is abelian with kernels and cokernels computed in Mod(𝒳_ét, 𝒪_𝒳), i.e. the inclusion is exact”.

Stacks 06WM (2). The category LQCoh(𝒪_𝒳) is abelian, with kernels and cokernels computed in Mod(𝒳_ét, 𝒪_𝒳): local quasi-coherence is closed under kernels and cokernels, so the full subcategory is abelian and its inclusion into Mod(𝒳_ét, 𝒪_𝒳) is exact.

theorem locallyQuasicoherentModules_abelian :
    (isLocallyQuasicoherent.{u, v, w, u} B E h S hS p hp).IsClosedUnderKernels ∧
      (isLocallyQuasicoherent.{u, v, w, u} B E h S hS p hp).IsClosedUnderCokernels ∧
      Nonempty (Abelian (locallyQuasicoherentModules.{u, v, w, u} B E h S hS p hp)) ∧
      PreservesFiniteLimits (isLocallyQuasicoherent.{u, v, w, u} B E h S hS p hp).ι ∧
      PreservesFiniteColimits (isLocallyQuasicoherent.{u, v, w, u} B E h S hS p hp).ι

AlgebraicGeometry.Stack.isLocallyQuasicoherent_twoOutOfThree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/LocallyQuasicoherentClosure.lean, line 137. The attribute's comment: “(3): in a short exact sequence of Mod(𝒳_ét, 𝒪_𝒳), if two out of three terms are locally quasi-coherent so is the third”.

Stacks 06WM (3). In a short exact sequence 0 → 𝓕₁ → 𝓕₂ → 𝓕₃ → 0 of Mod(𝒳_ét, 𝒪_𝒳), if two of the three terms are locally quasi-coherent then so is the third. A cokernel and a kernel of a morphism of locally quasi-coherent modules are locally quasi-coherent by Stacks 06WM (2); for the middle term the restriction to the small étale site of the scheme below an object is exact, so it carries the sequence to a short exact sequence there, and an extension of quasi-coherent modules on a small étale site is quasi-coherent (Descent, Lemma 0GNB).

theorem isLocallyQuasicoherent_twoOutOfThree
    (T : ShortComplex (SheafOfModules.{u} (ringStructureSheafCore B S hS p hp (etaleTopology B)
      (etaleTopology_le_topology B))))
    (hT : T.ShortExact) :
    (IsLocallyQuasicoherent B E h S hS p hp T.X₁.val →
        IsLocallyQuasicoherent B E h S hS p hp T.X₂.val →
          IsLocallyQuasicoherent B E h S hS p hp T.X₃.val) ∧
      (IsLocallyQuasicoherent B E h S hS p hp T.X₂.val →
        IsLocallyQuasicoherent B E h S hS p hp T.X₃.val →
          IsLocallyQuasicoherent B E h S hS p hp T.X₁.val) ∧
      (IsLocallyQuasicoherent B E h S hS p hp T.X₁.val →
        IsLocallyQuasicoherent B E h S hS p hp T.X₃.val →
          IsLocallyQuasicoherent B E h S hS p hp T.X₂.val)

AlgebraicGeometry.Stack.isLocallyQuasicoherent_etaleInternalHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/LocallyQuasicoherentInternalHom.lean, line 294. The attribute's comment: “(5): for F, G in LQCoh(𝒪_𝒳) with F of finite presentation on 𝒳_ét, the internal Hom 𝓗om_{𝒪_𝒳}(F, G) of Mod(𝒳_ét, 𝒪_𝒳) is locally quasi-coherent”.

Stacks 06WM, clause (5). Let p : 𝒳 ⥤ (Sch/S)_{fppf} be a category fibred in groupoids and let F, G be locally quasi-coherent sheaves of 𝒪_𝒳-modules on 𝒳_étale, with F of finite presentation on 𝒳_étale. Then the internal Hom 𝓗om_{𝒪_𝒳}(F, G) of Mod(𝒳_étale, 𝒪_𝒳) is locally quasi-coherent.

Local quasi-coherence is étale-local on the object (AlgebraicGeometry.Stack.isQuasicoherentOnSite_restrictModuleToSmallEtale_of_etaleCover), and every covering of an object of 𝒳_étale is refined by arrows lying over a jointly surjective family of étale morphisms (AlgebraicGeometry.Stack.exists_etaleCovering_le_of_mem_associatedTopology); at the members of such a refinement of a covering on which F is finitely presented the claim is AlgebraicGeometry.Stack.isQuasicoherentOnSite_restrictSheafToSmallEtale_etaleInternalHom. The hypothesis that F is locally quasi-coherent is part of the source's statement; the argument does not use it.

theorem isLocallyQuasicoherent_etaleInternalHom
    (F G : SheafOfModules.{u}
      (ringStructureSheafCore B S hS p hp (etaleTopology B) (etaleTopology_le_topology B)))
    (_hF : IsLocallyQuasicoherent B E h S hS p hp F.val)
    (hG : IsLocallyQuasicoherent B E h S hS p hp G.val)
    (hfp : F.IsFinitePresentationOnSite) :
    IsLocallyQuasicoherent B E h S hS p hp (etaleInternalHom B S hS p hp F G).val

AlgebraicGeometry.Stack.isLocallyQuasicoherent_tensorSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/LocallyQuasicoherentTensor.lean, line 689. The attribute's comment: “(4): the tensor product in Mod(𝒳_ét, 𝒪_𝒳) of two locally quasi-coherent modules is locally quasi-coherent”.

Stacks 06WM, clause (4). The tensor product in Mod(𝒳_ét, 𝒪_𝒳) of two locally quasi-coherent sheaves of modules on a category fibred in groupoids is locally quasi-coherent.

The tensor product is the sheafification, for the associated étale topology, of the objectwise tensor product. Its restriction to the small étale site of the scheme below an object x is the tensor product there of the restrictions of the two factors, by AlgebraicGeometry.Stack.restrictModuleEtaleTensorSheafIso: restriction commutes with the objectwise tensor product because that is sectionwise, and with sheafification because the restriction functor of Stacks 06W1 is cocontinuous as well as continuous. Quasi-coherence of a tensor product on a ringed site is Stacks.Modules.isQuasicoherentOnSite_sheafificationTensorObjUlift.

theorem isLocallyQuasicoherent_tensorSheaf
    (E : BigEtaleSite.{u}) (h : E.cutoff = B.cutoff)
    (F G : SheafOfModules.{u}
      (ringStructureSheafCore B S hS p hp (etaleTopology B) (etaleTopology_le_topology B)))
    (hF : IsLocallyQuasicoherent B E h S hS p hp F.val)
    (hG : IsLocallyQuasicoherent B E h S hS p hp G.val) :
    letI := hasSheafify_etaleAssociatedTopology B S hS p hp
    letI := wEqualsLocallyBijective_etaleAssociatedTopology B S hS p hp
    IsLocallyQuasicoherent B E h S hS p hp
      (((Stacks.SheafOfModules.Tensor.sheafTensor.{_, _, _, u, u}
        (structureSheaf B S hS p hp (etaleTopology B)
          (etaleTopology_le_topology B))).obj F).obj G).val
Tag 06WN, a lemma

Tag 06WN in the Stacks Project.

Stacks.SheafOfModules.TensorProduct.isQuasicoherentOnSite_tensorSheaf, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Descent/QuasicoherentTensor.lean, line 354. The attribute's comment: “tensor_product, not 06WG's site”. References: EGA I (9.1.1), “more general”.

The tensor clause of Stacks 06WV (5) and of Stacks 06WN (2), for the quasi-coherence of Stacks 03DL (6), on a site satisfying the hypotheses of this section: the tensor product of two sheaves of modules which are quasi-coherent in the sense of SheafOfModules.IsQuasicoherentOnSite is again quasi-coherent in that sense. That is the quasi-coherence the notion QCoh(𝒪_𝒳) of Stacks 06WG is defined by, and not Mathlib's predicate.

The hypotheses of this section exclude the site of Stacks 06WG, which is why both clause strings say so. Of the five, the fibred fppf site of a category fibred in groupoids over (Sch/S)_fppf satisfies three and fails two; the two failures are AlgebraicGeometry.FibredSite.not_univLE_associatedSite, the size hypothesis, which at that site's universes reads UnivLE.{u + 1, u}, and AlgebraicGeometry.FibredSite.not_hasBinaryProducts_twoLabel, binary products, which such a category generally lacks for want of a final object. See StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Descent/FibredTensorHypotheses.lean, where the five are settled one by one. So this statement does not instantiate to the source's clause, and the source's clause is not proved anywhere on this development.

The proof is the proof of Stacks.SheafOfModules.TensorProduct.isQuasicoherent_tensorSheaf run through SheafOfModules.isQuasicoherent_iff_isQuasicoherentOnSite, the identification of the two predicates on a site whose objects and morphisms are small relative to the universe of the sections — which is the extra hypothesis UnivLE.{max u v w, w} and the only thing separating the two statements. It is not removable: on a big site, whose objects live one universe above its sections, the two predicates genuinely differ.

What is not asserted is the rest of Stacks 06WN (2), namely that the tensor products formed in Mod(𝒳_Zar, 𝒪), Mod(𝒳_étale, 𝒪) and Mod(𝒪_𝒳) agree. Those are formed in different categories, where sheafification is a different functor, so the agreement is not a consequence of this statement and the comparison is not available; hence the qualified clause string, as in AlgebraicGeometry.FibredSite.colimits_quasicoherentModules_of_descent for part (1).

public instance isQuasicoherentOnSite_tensorSheaf
    (F G : SheafOfModules.{w}
      (TensorSheafification.structureSheaf O.obj (isSheaf_structureRingPresheaf O)))
    [F.IsQuasicoherentOnSite] [G.IsQuasicoherentOnSite] :
    ((((Stacks.SheafOfModules.Tensor.sheafTensor
      ⟨O.obj, Presheaf.isSheaf_of_isSheaf_comp _ (O.obj) (forget₂ CommRingCat RingCat)
        ((isSheaf_structureRingPresheaf O))⟩).obj (F)).obj (G))).IsQuasicoherentOnSite

Stacks.SheafOfModules.TensorProduct.isQuasicoherentOnSite_tensorObj, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Descent/QuasicoherentTensor.lean, line 376. The attribute's comment: “tensor_product, not 06WG's site”.

The tensor clause of Stacks 06WV (5) and of Stacks 06WN (2), for the quasi-coherence of Stacks 03DL (6), for the tensor product of the monoidal category Mod(𝒪) itself. Together with Stacks.SheafOfModules.TensorProduct.isQuasicoherentOnSite_tensorSheaf this is the covering set of the clause at the source's predicate, the development carrying both descriptions of the tensor product.

As there, the hypotheses of this section exclude the fibred fppf site of Stacks 06WG, by AlgebraicGeometry.FibredSite.not_univLE_associatedSite and AlgebraicGeometry.FibredSite.not_hasBinaryProducts_twoLabel; hence the qualified clause strings.

public instance isQuasicoherentOnSite_tensorObj
    (F G : SheafOfModules.{w}
      (TensorSheafification.structureSheaf O.obj (isSheaf_structureRingPresheaf O)))
    [F.IsQuasicoherentOnSite] [G.IsQuasicoherentOnSite] :
    (MonoidalCategory.tensorObj F G).IsQuasicoherentOnSite

Stacks.SheafOfModules.TensorProduct.quasicoherentOnSiteTensorBifunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Descent/QuasicoherentTensor.lean, line 398. The attribute's comment: “tensor_product, not 06WG's site”.

The tensor product as a bifunctor on the quasi-coherent modules of Stacks 03DL (6): the restriction of the tensor product of Mod(𝒪) to the full subcategory cut out by that quasi-coherence. It exists exactly because that tensor product preserves that quasi-coherence, which is the tensor clause of Stacks 06WV (5).

On the fibred fppf site of Stacks 06WG this subcategory is QCoh(𝒪_𝒳) (AlgebraicGeometry.FibredSite.quasicoherentModules), but the hypotheses of this section do not hold at that site — see AlgebraicGeometry.FibredSite.not_univLE_associatedSite and AlgebraicGeometry.FibredSite.not_hasBinaryProducts_twoLabel — so this bifunctor is not the one the source asserts; hence the qualified clause strings.

public noncomputable def quasicoherentOnSiteTensorBifunctor :
    (SheafOfModules.isQuasicoherentOnSite (TensorSheafification.structureSheaf O.obj
        (isSheaf_structureRingPresheaf O))).FullSubcategory ×
      (SheafOfModules.isQuasicoherentOnSite (TensorSheafification.structureSheaf O.obj
        (isSheaf_structureRingPresheaf O))).FullSubcategory ⥤
      (SheafOfModules.isQuasicoherentOnSite (TensorSheafification.structureSheaf O.obj
        (isSheaf_structureRingPresheaf O))).FullSubcategory

AlgebraicGeometry.FibredSite.existsUnique_hom_tensorSheafMixed_quasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FibredMixedTensorProduct.lean, line 369. The attribute's comment: “tensor_products”.

Stacks 06WN(2). Restricted to a pair of quasi-coherent modules with sections in independent universes, the tensor product formed on an associated site of the fibred category is the tensor product in the ambient category of sheaves of modules on that site: every bilinear map into a sheaf of modules there has a unique linear factorization through the pure-tensor map. This is the universal property the source asserts of the common tensor product on the Zariski, étale and fppf sites; it is proved here for all five associated sites, and the factorization is tested against every sheaf of modules, not only the quasi-coherent ones.

public theorem existsUnique_hom_tensorSheafMixed_quasicoherent (τ : SiteKind)
    (F : quasicoherentModules.{u, v, u, m} B S hS p hp)
    (G : quasicoherentModules.{u, v, u, n} B S hS p hp)
    (H : SheafOfModules.{max u m n} (ringStructureSheafCore B S hS p hp τ))
    (b : Stacks.Modules.BilinearMap (structureSheaf B S hS p hp τ).obj
      F.obj.val G.obj.val H.val) :
    ∃! f : tensorSheafMixed B S hS p hp τ ((toSiteModules B S hS p hp τ).obj F)
        ((toSiteModules B S hS p hp τ).obj G) ⟶ H,
      ∀ (U : 𝒳ᵒᵖ) (x : F.obj.val.obj U) (y : G.obj.val.obj U),
        f.val.app U ((toTensorSheafMixed B S hS p hp τ
          ((toSiteModules B S hS p hp τ).obj F)
          ((toSiteModules B S hS p hp τ).obj G)).app U x y) = b.app U x y

AlgebraicGeometry.FibredSite.internalHomSheaf_val_eq_fppf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/InternalHom.lean, line 190. The attribute's comment: “internal_homs”.

The internal Hom of two quasi-coherent modules on a category fibred in groupoids has the same underlying presheaf of modules on each of the five associated sites as on the fppf one; in particular on the Zariski and étale ones.

public theorem internalHomSheaf_val_eq_fppf (hp : p.IsFiberedInGroupoids) (τ : SiteKind)
    (F G : quasicoherentModules.{u, v, w, u} B S hS p hp) :
    ((ringedSite B S hS p hp τ).internalHomSheaf
        ((toSiteModules B S hS p hp τ).obj F)
        ((toSiteModules B S hS p hp τ).obj G)).val =
      ((ringedSite B S hS p hp .fppf).internalHomSheaf F.obj G.obj).val

AlgebraicGeometry.FibredSite.internalHomSheaf_isQuasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/InternalHom.lean, line 201. The attribute's comment: “internal_homs”.

The internal Hom of a finite locally free quasi-coherent module into a quasi-coherent module on a category fibred in groupoids is quasi-coherent on the fppf associated site.

public theorem internalHomSheaf_isQuasicoherent (hp : p.IsFiberedInGroupoids)
    (F G : quasicoherentModules.{u, v, w, u} B S hS p hp)
    (hF : SheafOfModules.IsFiniteLocallyFreeOnSite F.obj) :
    ((ringedSite B S hS p hp .fppf).internalHomSheaf F.obj G.obj).IsQuasicoherentOnSite

AlgebraicGeometry.FibredSite.isQuasicoherentOnSite_tensorSheafMixed_quasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/MixedTensorQuasicoherent.lean, line 239. The attribute's comment: “tensor_products”.

The tensor product of a pair of quasi-coherent modules with sections in independent universes, formed on the fppf site of a category fibred in groupoids, is quasi-coherent. This is the object whose universal property is AlgebraicGeometry.FibredSite.existsUnique_hom_tensorSheafMixed_quasicoherent, so the tensor product of quasi-coherent modules is again a quasi-coherent module.

theorem isQuasicoherentOnSite_tensorSheafMixed_quasicoherent
    (F : quasicoherentModules.{u, v, u, m} B S hS p hp)
    (G : quasicoherentModules.{u, v, u, n} B S hS p hp) :
    (tensorSheafMixed B S hS p hp .fppf ((toSiteModules B S hS p hp .fppf).obj F)
      ((toSiteModules B S hS p hp .fppf).obj G)).IsQuasicoherentOnSite

AlgebraicGeometry.FibredSite.quasicoherentModules_colimits_siteAgreement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentSiteAgreement.lean, line 290. The attribute's comment: “(1): QCoh(O_X) has colimits and they agree with colimits in Mod(X_Zar, O_X), Mod(X_et, O_X), Mod(O_X) and LQCoh(O_X)”.

Stacks 06WN (1). For a category fibred in groupoids p : 𝒳 ⥤ (Sch/S)_fppf, the category QCoh(𝒪_𝒳) has colimits, and they agree with the colimits in Mod(𝒪_𝒳), in Mod(𝒳_τ, 𝒪_𝒳) for each of the coarser inherited topologies — in particular in Mod(𝒳_Zar, 𝒪_𝒳) and Mod(𝒳_étale, 𝒪_𝒳) — and in LQCoh(𝒪_𝒳): the inclusion into Mod(𝒪_𝒳), the reading functors into Mod(𝒳_τ, 𝒪_𝒳) and the inclusion into LQCoh(𝒪_𝒳) preserve them. Colimits are indexed by categories in the universe of the schemes.

theorem quasicoherentModules_colimits_siteAgreement (E : BigEtaleSite.{u})
    (h : E.cutoff = B.cutoff) :
    HasColimitsOfSize.{u, u} (quasicoherentModules.{u, u + 1, u, u} B S hS p hp) ∧
      PreservesColimitsOfSize.{u, u} (SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
        (ringStructureSheafCore B S hS p hp .fppf)).ι ∧
      (∀ τ : SiteKind,
        PreservesColimitsOfSize.{u, u} (toSiteModules.{u, u + 1, u, u} B S hS p hp τ)) ∧
      PreservesColimitsOfSize.{u, u} (toLocallyQuasicoherentModules B S hS p hp E h)

AlgebraicGeometry.FibredSite.internalHomSheaf_quasicoherent_siteAgreement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentSiteAgreement.lean, line 386. The attribute's comment: “(3): for F, G in QCoh(O_X) the internal homs computed in Mod(X_Zar, O_X), Mod(X_et, O_X) and Mod(O_X) agree, F being finite locally free does not depend on the topology, and for F finite locally free the common value is quasi-coherent”.

Stacks 06WN (3). Let 𝓕 and 𝓖 be quasi-coherent modules on a category fibred in groupoids over (Sch/S)_fppf. Then 𝓕 is finite locally free for the fppf topology if and only if it is for the étale, and if and only if for the Zariski topology (indeed for each of the five topologies); the internal homs ℋom(𝓕, 𝓖) computed in Mod(𝒳_Zar, 𝒪_𝒳), Mod(𝒳_étale, 𝒪_𝒳) and Mod(𝒪_𝒳) agree; and when 𝓕 is finite locally free for any one of these topologies the common value is an object of QCoh(𝒪_𝒳).

theorem internalHomSheaf_quasicoherent_siteAgreement
    (F G : quasicoherentModules.{u, u + 1, u, u} B S hS p hp) :
    (∀ τ : SiteKind, SheafOfModules.IsFiniteLocallyFreeOnSite F.obj ↔
      SheafOfModules.IsFiniteLocallyFreeOnSite ((toSiteModules B S hS p hp τ).obj F)) ∧
    (∀ τ : SiteKind,
      (ringedSite B S hS p hp τ).internalHomSheaf ((toSiteModules B S hS p hp τ).obj F)
          ((toSiteModules B S hS p hp τ).obj G) =
        (Stacks.SheafOfModules.comparisonPushforward.{u + 1, u, u, u + 1}
          (BigFppfOver.associatedTopology_le_fppf B S hS p τ)
          (ringStructureSheafCore B S hS p hp .fppf)).obj
          ((ringedSite B S hS p hp .fppf).internalHomSheaf F.obj G.obj)) ∧
    (∀ τ : SiteKind,
      SheafOfModules.IsFiniteLocallyFreeOnSite ((toSiteModules B S hS p hp τ).obj F) →
        ((ringedSite B S hS p hp .fppf).internalHomSheaf F.obj G.obj).IsQuasicoherentOnSite)

AlgebraicGeometry.FibredSite.sheafTensor_quasicoherent_siteAgreement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentSiteAgreement.lean, line 479. The attribute's comment: “(2): for F, G in QCoh(O_X) the tensor products computed in Mod(X_Zar, O_X), Mod(X_et, O_X) and Mod(O_X) agree and the common value is quasi-coherent”.

Stacks 06WN (2). For quasi-coherent modules 𝓕 and 𝓖 on a category fibred in groupoids over (Sch/S)_fppf, the tensor products 𝓕 ⊗ 𝓖 computed in Mod(𝒳_Zar, 𝒪_𝒳), Mod(𝒳_étale, 𝒪_𝒳) and Mod(𝒪_𝒳) agree — the one computed in Mod(𝒪_𝒳), read for each coarser topology, is the one computed for that topology — and the common value is an object of QCoh(𝒪_𝒳); it is moreover quasi-coherent on each of the coarser sites.

theorem sheafTensor_quasicoherent_siteAgreement
    (F G : quasicoherentModules.{u, v, w, u} B S hS p hp) :
    (∀ τ : SiteKind, Nonempty ((Stacks.SheafOfModules.comparisonPushforward.{v, w, u, u}
        (BigFppfOver.associatedTopology_le_fppf B S hS p τ)
        (ringStructureSheafCore B S hS p hp .fppf)).obj
        (((sheafTensor B S hS p hp .fppf).obj F.obj).obj G.obj) ≅
      ((sheafTensor B S hS p hp τ).obj ((toSiteModules B S hS p hp τ).obj F)).obj
        ((toSiteModules B S hS p hp τ).obj G))) ∧
    (((sheafTensor B S hS p hp .fppf).obj F.obj).obj G.obj).IsQuasicoherentOnSite ∧
    (∀ τ : SiteKind, (((sheafTensor B S hS p hp τ).obj
      ((toSiteModules B S hS p hp τ).obj F)).obj
        ((toSiteModules B S hS p hp τ).obj G)).IsQuasicoherentOnSite)
Sources
LeanAlgebraicGeometry.Stack.restrictModuleToSmallEtale · AlgebraicGeometry.Stack.IsLocallyQuasicoherent · AlgebraicGeometry.Stack.isSheaf_etale_of_isQuasicoherent · AlgebraicGeometry.Stack.isQuasicoherentFppf_iff_isLocallyQuasicoherent_and_isIso_sheafifiedRestrictComparison · AlgebraicGeometry.Stack.isLocallyQuasicoherent_modulePullback · AlgebraicGeometry.Stack.locallyQuasicoherentModules_colimits · AlgebraicGeometry.Stack.locallyQuasicoherentModules_abelian · AlgebraicGeometry.Stack.isLocallyQuasicoherent_twoOutOfThree

Section96.13 Stackification and sheaves#

Section 96.13 of the Stacks Project, Tag 06WP. 2 tags here are carried by 5 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06WQ, a lemma

Tag 06WQ in the Stacks Project.

AlgebraicGeometry.Stack.isEquivalence_inverseImage_of_isStackificationEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/Stackification.lean, line 377.

Stacks 06WQ. If a 1-morphism F : 𝒳 ⥤ 𝒴 of categories fibred in groupoids over the big fppf category of S induces an equivalence of stackifications, then the morphism of topoi Sh(𝒳_fppf) ⟶ Sh(𝒴_fppf) of Stacks 06TS is an equivalence.

The functor displayed is the inverse image of that morphism of topoi, which by Stacks 06TS is restriction along F; the morphism of topoi is an equivalence exactly when its inverse image is.

theorem isEquivalence_inverseImage_of_isStackificationEquivalence
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 : Type v₁} [Category.{u} 𝒳] {𝒴 : Type v₂} [Category.{u} 𝒴]
    (p : 𝒳 ⥤ BigFppfOver B S hS) (q : 𝒴 ⥤ BigFppfOver B S hS)
    (hp : p.IsFiberedInGroupoids) (hq : q.IsFiberedInGroupoids)
    (F : 𝒳 ⥤ 𝒴) (hF : p.IsFibredOneMorphism q F)
    (heq : letI : p.IsFibered := hp.isFibered
      letI : q.IsFibered := hq.isFibered
      hF.IsStackificationEquivalence (BigFppfOver.topology B S hS)) :
    letI : p.IsFibered := hp.isFibered
    letI : q.IsFibered := hq.isFibered
    letI := (hF.isContinuous_and_isCocontinuous_inheritedTopology
      (BigFppfOver.topology B S hS)).1
    (F.sheafPushforwardContinuous (Type (max t u v₁ v₂))
      (p.inheritedTopology (BigFppfOver.topology B S hS))
      (q.inheritedTopology (BigFppfOver.topology B S hS))).IsEquivalence
Tag 06WR, a lemma

Tag 06WR in the Stacks Project.

AlgebraicGeometry.Stack.isEquivalence_modulePullback_of_isStackificationEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/StackificationModules.lean, line 127. The attribute's comment: “modules”.

Stacks 06WR, the Mod clause. Let f : 𝒳 ⥤ 𝒴 be a 1-morphism of categories fibred in groupoids over the big fppf category of S. If f induces an equivalence of stackifications, then the inverse image of sheaves of modules of Stacks 06WE is an equivalence Mod(𝒪_𝒴) ⥤ Mod(𝒪_𝒳).

Equivalence of stackifications makes f a dense subsite inclusion for the associated fppf topologies, by the engine of Stacks 06WQ; the structure sheaf of 𝒳 is the restriction along f of that of 𝒴, so the inverse image is restriction of sections, and the Comparison Lemma for sheaves of modules applies.

theorem isEquivalence_modulePullback_of_isStackificationEquivalence
    (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
    {𝒳 : Type u} [Category.{u} 𝒳] {𝒴 : Type u} [Category.{u} 𝒴]
    (p : 𝒳 ⥤ BigFppfOver B S hS) (q : 𝒴 ⥤ BigFppfOver B S hS)
    (hp : p.IsFiberedInGroupoids) (hq : q.IsFiberedInGroupoids)
    (f : 𝒳 ⥤ 𝒴) (hF : p.IsFibredOneMorphism q f)
    (heq : letI : p.IsFibered := hp.isFibered
      letI : q.IsFibered := hq.isFibered
      hF.IsStackificationEquivalence (BigFppfOver.topology B S hS)) :
    (modulePullback.{u, u, u, u, u, u} B S hS p q hp hq f hF.comp_eq
      B.topology le_rfl).IsEquivalence

AlgebraicGeometry.Stack.isEquivalence_quasicoherentPullback_of_isStackificationEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/StackificationModules.lean, line 273. The attribute's comment: “quasi-coherent modules”.

Stacks 06WR, the QCoh clause. If f : 𝒳 ⥤ 𝒴 induces an equivalence of stackifications, then the inverse image of quasi-coherent modules is an equivalence QCoh(𝒪_𝒴) ⥤ QCoh(𝒪_𝒳).

Fullness and faithfulness come from the equivalence on all modules, since QCoh is a full subcategory; essential surjectivity needs in addition that f^* reflects quasi-coherence, which is AlgebraicGeometry.Stack.isQuasicoherentOnSite_of_modulePullback.

theorem isEquivalence_quasicoherentPullback_of_isStackificationEquivalence
    (heq : letI : p.IsFibered := hp.isFibered
      letI : q.IsFibered := hq.isFibered
      hF.IsStackificationEquivalence (BigFppfOver.topology B S hS)) :
    (quasicoherentPullback B S hS p q hp hq f hF).IsEquivalence

AlgebraicGeometry.Stack.isEquivalence_modulePullback_of_isStackificationEquivalence_anyUniverse, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/StackificationModulesAnyUniverse.lean, line 265. The attribute's comment: “the Mod clause: f^* is an equivalence Mod(𝒪_𝒴) ⥤ Mod(𝒪_𝒳), for categories fibred in groupoids in arbitrary universes and modules in any universe containing that of the rings”.

Stacks 06WR, the Mod clause. Let f : 𝒳 ⥤ 𝒴 be a 1-morphism of categories fibred in groupoids over the big fppf category of S. If f induces an equivalence of stackifications, then the inverse image of sheaves of modules of Stacks 06WE is an equivalence Mod(𝒪_𝒴) ⥤ Mod(𝒪_𝒳), for modules with sections in any universe containing u.

f is a dense subsite inclusion for the associated fppf topologies (Stacks 06WQ), restriction of abelian sheaves along it is an equivalence (isEquivalence_sheafPushforwardContinuous_of_isStackificationEquivalence), and the structure sheaf of 𝒳 is the restriction along f of that of 𝒴, so the Comparison Lemma for sheaves of modules applies.

theorem isEquivalence_modulePullback_of_isStackificationEquivalence_anyUniverse
    (heq : letI : p.IsFibered := hp.isFibered
      letI : q.IsFibered := hq.isFibered
      hF.IsStackificationEquivalence' (BigFppfOver.topology B S hS)) :
    (modulePullback.{u, v₁, w, max u m, v₂, w} B S hS p q hp hq f hF.comp_eq
      B.topology le_rfl).IsEquivalence

AlgebraicGeometry.Stack.isEquivalence_quasicoherentPullback_of_isStackificationEquivalence_anyUniverse, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Sheaves/StackificationModulesAnyUniverse.lean, line 293. The attribute's comment: “the QCoh clause: f^* is an equivalence QCoh(𝒪_𝒴) ⥤ QCoh(𝒪_𝒳), for categories fibred in groupoids in arbitrary universes and modules in any universe containing that of the rings”.

Stacks 06WR, the QCoh clause. Let f : 𝒳 ⥤ 𝒴 be a 1-morphism of categories fibred in groupoids over the big fppf category of S. If f induces an equivalence of stackifications, then the inverse image of quasi-coherent modules is an equivalence QCoh(𝒪_𝒴) ⥤ QCoh(𝒪_𝒳), for modules with sections in any universe containing u.

Fullness and faithfulness come from the Mod clause, since QCoh is a full subcategory; essential surjectivity needs in addition that f^* reflects quasi-coherence, which holds because f is cover-dense (AlgebraicGeometry.Stack.isQuasicoherentOnSite_of_modulePullback').

theorem isEquivalence_quasicoherentPullback_of_isStackificationEquivalence_anyUniverse
    (heq : letI : p.IsFibered := hp.isFibered
      letI : q.IsFibered := hq.isFibered
      hF.IsStackificationEquivalence' (BigFppfOver.topology B S hS)) :
    (quasicoherentPullback'.{u, v₁, w, max u m, v₂, w} B S hS p q hp hq f
      hF.comp_eq).IsEquivalence
Sources
LeanAlgebraicGeometry.Stack.isEquivalence_inverseImage_of_isStackificationEquivalence · AlgebraicGeometry.Stack.isEquivalence_modulePullback_of_isStackificationEquivalence · AlgebraicGeometry.Stack.isEquivalence_quasicoherentPullback_of_isStackificationEquivalence · AlgebraicGeometry.Stack.isEquivalence_modulePullback_of_isStackificationEquivalence_anyUniverse · AlgebraicGeometry.Stack.isEquivalence_quasicoherentPullback_of_isStackificationEquivalence_anyUniverse

Section96.14 Quasi-coherent sheaves and presentations#

Section 96.14 of the Stacks Project, Tag 06WS. 4 tags here are carried by 6 declarations of the repository (all in StacksFrontier) and 3 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0GQC, a lemma

Tag 0GQC in the Stacks Project.

AlgebraicGeometry.Space.isQuasicoherentOnSite_etaleRestriction, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/ChartRestrictionModuleIdentification.lean, line 672.

Let 𝒳 ⥤ (Sch/S)_{fppf} be a category fibred in groupoids representable by the algebraic space U, through a chosen equivalence over the site as in Stacks 073M. If ℱ is a locally quasi-coherent 𝒪_𝒳-module (Stacks 06WJ) then its restriction ℱ|_{U_étale} (equation 075K) is quasi-coherent.

The auxiliary big étale site is taken to be AlgebraicGeometry.associatedBigEtaleSite of the big fppf site, which the source does not name; that is the canonical choice, and it is the one AlgebraicGeometry.Space.isQuasicoherentOnSite_of_chartLocalModuleIdentification already makes.

theorem isQuasicoherentOnSite_etaleRestriction
    (ℱ : inheritedEtaleModules B S hS p hp)
    (hℱ : Stack.IsLocallyQuasicoherent B (associatedBigEtaleSite B) rfl S hS p hp ℱ.val) :
    (etaleRestrictedModuleInverseImage B S hS p p hp hp e (𝟭 𝒳)
      (Functor.IsFibredOneMorphism.id p) ℱ).IsQuasicoherentOnSite
Tag 0GQD, a lemma

Tag 0GQD in the Stacks Project.

Declarations registered for the tag:

Tag 06WT, a proposition

Tag 06WT in the Stacks Project.

AlgebraicGeometry.Stack.quotientStackModulePullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuotientStackQuasicoherentModules.lean, line 88. The attribute's comment: “the inverse image of modules along the canonical map from the object space, the first step of the forward functor”.

The functor ℱ ↦ x^*ℱ, the inverse image of sheaves of modules of Stacks 06WE along the canonical projection x : 𝒮_U ⟶ [U/R] of Stacks 044R.

def quotientStackModulePullback (G : GroupoidInAlgebraicSpaces C S hS B) :
    SheafOfModules.{u + 1}
        (ringStructureSheafCore C S hS (quotientStack G).p
          (isFiberedInGroupoids_quotientStack G) C.topology le_rfl) ⥤
      SheafOfModules.{u + 1}
        (ringStructureSheafCore C S hS (fibredCategory C S hS G.objects.obj).val.p
          (fibredCategory C S hS G.objects.obj).property C.topology le_rfl)

AlgebraicGeometry.Stack.quotientPrestackQuasicoherentPullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Groupoids/QuotientStackQuasicoherentModules.lean, line 104. The attribute's comment: “the restriction of quasi-coherent modules along the stackification map of the pointwise quotient”.

The restriction of quasi-coherent modules along the stackification map [U/_pR] ⟶ [U/R]: the inverse image of modules of Stacks 06WE, which preserves quasi-coherence by Stacks 06WH.

def quotientPrestackQuasicoherentPullback (G : GroupoidInAlgebraicSpaces C S hS B) :
    FibredSite.quasicoherentModules.{u, u + 1, u + 1, u + 1} C S hS (quotientStack G).p
        (isFiberedInGroupoids_quotientStack G) ⥤
      FibredSite.quasicoherentModules.{u, u + 1, u + 1, u + 1} C S hS (quotientPrestack G).p
        (isFiberedInGroupoids_quotientPrestack G)

AlgebraicGeometry.Stack.quotientStackQuasicoherentEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuotientStackQuasicoherentEquivalence.lean, line 53.

For a groupoid in algebraic spaces (U, R, s, t, c) over S with quotient stack 𝒳 = [U/R], the category of quasi-coherent 𝒪_𝒳-modules is equivalent to the category of quasi-coherent modules on (U, R, s, t, c), by ℱ ↦ (x^*ℱ|_{U_étale}, α).

def quotientStackQuasicoherentEquivalence :
    FibredSite.quasicoherentModules.{u, u + 1, u + 1, u} C S hS (quotientStack G).p
        (isFiberedInGroupoids_quotientStack G) ≌ Space.QuasicoherentModule C S hS G

AlgebraicGeometry.Stack.quasicoherentEquivalenceGroupoid, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/QuotientStackQuasicoherentEquivalence.lean, line 83. The attribute's comment: “the equivalence QCoh(𝒪_{[U/R]}) ≌ QCoh(U, R, s, t, c), with functor ℱ ↦ (x^*ℱ|_{U_étale}, α)”.

For a groupoid (U, R, s, t, c) in algebraic spaces, the category of quasi-coherent modules on the quotient stack [U/R] is equivalent to the category of quasi-coherent modules on (U, R, s, t, c), by the functor ℱ ↦ (x^*ℱ|_{U_étale}, α) with α the transport of the canonical 2-morphism of Stacks 044S through the comparison maps of equation 076R.

def quasicoherentEquivalenceGroupoid (G : GroupoidInAlgebraicSpaces C S hS A) :
    FibredSite.quasicoherentModules.{u, u + 1, u + 1, u} C S hS (quotientStack G).p
        (isFiberedInGroupoids_quotientStack G) ≌ Space.QuasicoherentModule C S hS G
Tag 076S, a lemma

Tag 076S in the Stacks Project.

AlgebraicGeometry.Stack.quotientStackObjectRestrictionMap_injective_and_range, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuotientStackHomRestriction.lean, line 415.

Stacks 076S. Let (U, R, s, t, c) be a groupoid in algebraic spaces over S whose source and target are flat and locally of finite presentation, let 𝒳 = [U/R] be the quotient stack and x the object of 𝒳 over U (the canonical projection of Stacks 044R). Let ℱ be a quasi-coherent 𝒪_𝒳-module and ℋ any 𝒪_𝒳-module. Then the map Hom_{𝒪_𝒳}(ℱ, ℋ) ⟶ Hom_{𝒪_U}(x^*ℱ|_{U_étale}, x^*ℋ|_{U_étale}), ψ ↦ x^*ψ|_{U_étale}, is injective, and its image consists of exactly those φ which give rise to a commutative diagram of modules on R_étale: there is a morphism χ : (x ∘ s)^*ℱ|_{R_étale} ⟶ (x ∘ s)^*ℋ|_{R_étale} with c_s(ℱ) ≫ χ = s_small^*φ ≫ c_s(ℋ) and c_t(ℱ) ≫ χ = t_small^*φ ≫ c_t(ℋ), where c_s and c_t are the comparison maps of equation 076R of the triangles through the source and through the target, the latter carried by the 2-morphism of Stacks 044S which identifies (x ∘ t)^*ℱ|_{R_étale} with (x ∘ s)^*ℱ|_{R_étale}.

theorem quotientStackObjectRestrictionMap_injective_and_range
    (_hsflat : Space.IsFlat C S hS G.source.hom) (_htflat : Space.IsFlat C S hS G.target.hom)
    (_hslfp : Space.IsLocallyOfFinitePresentation C S hS G.source.hom)
    (_htlfp : Space.IsLocallyOfFinitePresentation C S hS G.target.hom)
    (F : FibredSite.quasicoherentModules.{u, u + 1, u + 1, u} C S hS (quotientStack G).p
      (isFiberedInGroupoids_quotientStack G))
    (H : QuotientStackModules G) :
    Function.Injective (fun ψ : F.obj ⟶ H => quotientStackObjectRestrictionMap G ψ) ∧
      ∀ φ : quotientStackObjectRestriction G F.obj ⟶ quotientStackObjectRestriction G H,
        (∃ ψ : F.obj ⟶ H, quotientStackObjectRestrictionMap G ψ = φ) ↔
          ∃ χ, quotientStackSourceComparison G F.obj ≫ χ =
              (Space.modulePullback C S hS G.source).map φ ≫ quotientStackSourceComparison G H ∧
            quotientStackTargetComparison G F.obj ≫ χ =
              (Space.modulePullback C S hS G.target).map φ ≫ quotientStackTargetComparison G H
Sources
LeanAlgebraicGeometry.Space.isQuasicoherentOnSite_etaleRestriction · AlgebraicGeometry.Space.isEquivalence_quasicoherentRestriction_unconditional · AlgebraicGeometry.Space.nonempty_inv_toSiteModules_iso_projectionModulePullback_unconditional · AlgebraicGeometry.Space.nonempty_projectionPullbackModules_comp_iso · AlgebraicGeometry.Stack.quotientStackModulePullback · AlgebraicGeometry.Stack.quotientPrestackQuasicoherentPullback · AlgebraicGeometry.Stack.quotientStackQuasicoherentEquivalence · AlgebraicGeometry.Stack.quasicoherentEquivalenceGroupoid

Section96.15 Quasi-coherent sheaves on algebraic stacks#

Section 96.15 of the Stacks Project, Tag 06WU. 2 tags here are carried by 25 declarations of the repository (all in StacksFrontier) and 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06WV, a lemma

Tag 06WV in the Stacks Project.

AlgebraicGeometry.Stack.colimits_quasicoherentModules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/AlgebraicStackColimits.lean, line 71. The attribute's comment: “part (4): QCoh(𝒪_𝒳) has colimits and they agree with colimits in Mod(𝒪_𝒳)”.

For an algebraic stack 𝒳, the category QCoh(𝒪_𝒳) has colimits, and they agree with colimits in Mod(𝒪_𝒳): the inclusion QCoh(𝒪_𝒳) → Mod(𝒪_𝒳) preserves them.

theorem colimits_quasicoherentModules (𝒳 : AlgebraicStacks.{u, w} B S hS) :
    HasColimitsOfSize.{u, u}
        (FibredSite.quasicoherentModules.{u, u + 1, u, u} B S hS 𝒳.val.val.p
          𝒳.val.isFiberedInGroupoids) ∧
      PreservesColimitsOfSize.{u, u}
        (SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
          (FibredSite.ringStructureSheafCore B S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids
            .fppf)).ι

AlgebraicGeometry.Stack.quasicoherentInclusion_rightExact_not_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/AlgebraicStackInclusionNotExact.lean, line 244. The attribute's comment: “part (3): the inclusion QCoh(𝒪_𝒳) → Mod(𝒪_𝒳) is right exact, and on every big site the algebraic stack Spec(ℤ) is one for which it is not exact”.

Stacks 06WV (3). The inclusion QCoh(𝒪_𝒳) → Mod(𝒪_𝒳) is right exact for every algebraic stack 𝒳, but it is not exact in general: on every big fppf site there is an algebraic stack, namely Spec(ℤ), for which it is not exact.

theorem quasicoherentInclusion_rightExact_not_exact :
    (∀ (B : BigFppfSite.{u}) (S : Scheme.{u}) (hS : B.Contains S)
        (𝒳 : AlgebraicStacks.{u, w} B S hS),
        PreservesFiniteColimits
          (SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
            (FibredSite.ringStructureSheafCore B S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids
              .fppf)).ι) ∧
      ∀ B : BigFppfSite.{u}, ∃ 𝒳 : AlgebraicStacks.{u, w} B specInt.{u} (contains_specInt B),
        ¬ (PreservesFiniteLimits
            (SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
              (FibredSite.ringStructureSheafCore B specInt.{u} (contains_specInt B) 𝒳.val.val.p
                𝒳.val.isFiberedInGroupoids .fppf)).ι ∧
          PreservesFiniteColimits
            (SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
              (FibredSite.ringStructureSheafCore B specInt.{u} (contains_specInt B) 𝒳.val.val.p
                𝒳.val.isFiberedInGroupoids .fppf)).ι)

AlgebraicGeometry.Stack.GroupoidPresentation.quasicoherentEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/AlgebraicStackPresentation.lean, line 95. The attribute's comment: “part (1): a presentation [U/R] → 𝒳 induces a canonical equivalence QCoh(𝒪_𝒳) ≌ QCoh(U, R, s, t, c)”.

Stacks 06WV (1). A presentation [U/R] → 𝒳 of an algebraic stack — a smooth groupoid (U, R, s, t, c) in algebraic spaces over S and an equivalence [U/R] → 𝒳 (Stacks 04TI) — induces a canonical equivalence QCoh(𝒪_𝒳) ≌ QCoh(U, R, s, t, c).

It is the inverse image along the presenting equivalence, QCoh(𝒪_𝒳) ≌ QCoh(𝒪_{[U/R]}), followed by the equivalence of Stacks 06WT, AlgebraicGeometry.Stack.quasicoherentEquivalenceGroupoid.

def GroupoidPresentation.quasicoherentEquivalence {𝒳 : AlgebraicStacks.{u, w} B S hS}
    (P : GroupoidPresentation B S hS 𝒳.val.val) :
    FibredSite.quasicoherentModules.{u, u + 1, u, u} B S hS 𝒳.val.val.p
        𝒳.val.isFiberedInGroupoids ≌ Space.QuasicoherentModule B S hS P.groupoid

AlgebraicGeometry.Stack.abelianQuasicoherentModules, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/AlgebraicStackPresentation.lean, line 114. The attribute's comment: “part (2): QCoh(𝒪_𝒳) is abelian”.

Stacks 06WV (2). The quasi-coherent modules on an algebraic stack form an abelian category.

By Stacks 04T3 the stack has a presentation [U/R] → 𝒳 by a smooth groupoid; its source and target are smooth, hence flat, so QCoh(U, R, s, t, c) is abelian by Stacks 06VZ, and part (1) transports the abelian structure to QCoh(𝒪_𝒳).

instance abelianQuasicoherentModules (𝒳 : AlgebraicStacks.{u, w} B S hS) :
    Abelian (FibredSite.quasicoherentModules.{u, u + 1, u, u} B S hS 𝒳.val.val.p
      𝒳.val.isFiberedInGroupoids)

AlgebraicGeometry.FibredSite.preservesColimitsOfSize_quasicoherentInclusion', a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/BigSiteColimits/AffineSectionBaseChangeExit.lean, line 760. The attribute's comment: “inclusion_right_exact”.

Colimits of quasi-coherent modules are fppf-module colimits. The inclusion of the quasi-coherent modules into all module sheaves for the associated fppf topology preserves all small colimits; this is the comparison half of the colimit clause of Stacks 06WN(1), again with both hypotheses of AlgebraicGeometry.FibredSite.inclusion_preservesColimits_of_span discharged and only the standing essential smallness left assumed.

Right exactness of the inclusion functor, Stacks 06WV(3), is this statement: the source derives it from the agreement of colimits, Stacks 06WV(4).

theorem preservesColimitsOfSize_quasicoherentInclusion' :
    PreservesColimitsOfSize.{u, u}
      (SheafOfModules.isQuasicoherentOnSite.{v, w, u, u}
        (ringStructureSheafCore B S hS p hp .fppf)).ι

Stacks.SheafOfModules.TensorProduct.isQuasicoherent_tensorSheaf, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Descent/QuasicoherentTensor.lean, line 241. The attribute's comment: “tensor_product, for Mathlib's IsQuasicoherent, not 03DL(6)”. References: EGA I (9.1.1), “more general”; EGA IV (8.2.7), “case A = O_S”.

Stacks 06WV (5) for Mathlib's SheafOfModules.IsQuasicoherent: the tensor product of two quasi-coherent sheaves of modules on a site is quasi-coherent. Quasi-coherence is a local condition, and over a common refinement of the two coverings on which the factors are presented, the tensored presentation presents the tensor product.

The quasi-coherence here is Mathlib's — a covering of the final object carrying SheafOfModules.Presentations — and not the SheafOfModules.IsQuasicoherentOnSite of Stacks 03DL (6), which is the notion QCoh(𝒪_𝒳) of Stacks 06WG means; hence the qualified clause string. The clause for that notion is Stacks.SheafOfModules.TensorProduct.isQuasicoherentOnSite_tensorSheaf below, which is this statement plus SheafOfModules.isQuasicoherent_iff_isQuasicoherentOnSite and so carries one further size hypothesis on the site.

This is also the site-level form of Stacks 01CE (3), which is a statement about a ringed space and is tagged there, on AlgebraicGeometry.tensorSheaf_isQuasicoherent in StacksFrontier/CategoryTheory/Sites/Modules/TensorProduct/Basic.lean.

public instance isQuasicoherent_tensorSheaf
    (F G : SheafOfModules.{w}
      (TensorSheafification.structureSheaf O.obj (isSheaf_structureRingPresheaf O)))
    [F.IsQuasicoherent] [G.IsQuasicoherent] :
    ((((Stacks.SheafOfModules.Tensor.sheafTensor
      ⟨O.obj, Presheaf.isSheaf_of_isSheaf_comp _ (O.obj) (forget₂ CommRingCat RingCat)
        ((isSheaf_structureRingPresheaf O))⟩).obj (F)).obj (G))).IsQuasicoherent

Stacks.SheafOfModules.TensorProduct.isQuasicoherent_tensorObj, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Descent/QuasicoherentTensor.lean, line 267. The attribute's comment: “tensor_product, for Mathlib's IsQuasicoherent, not 03DL(6)”. References: EGA I (9.1.1), “more general”; EGA IV (8.2.7), “case A = O_S”.

Stacks 06WV (5) for Mathlib's SheafOfModules.IsQuasicoherent, for the tensor product of the monoidal category Mod(𝒪) itself: given quasi-coherent sheaves of modules F and G, the tensor product F ⊗_𝒪 G formed in Mod(𝒪) is quasi-coherent. This is the shape in which the source states the clause; Stacks.SheafOfModules.TensorProduct.isQuasicoherent_tensorSheaf is the same statement for the explicit model of that tensor product as a sheafified objectwise tensor product, and the two together are the covering set at this predicate, the development carrying both descriptions. The same pair for the quasi-coherence of Stacks 03DL (6) is Stacks.SheafOfModules.TensorProduct.isQuasicoherentOnSite_tensorObj and …isQuasicoherentOnSite_tensorSheaf.

public instance isQuasicoherent_tensorObj
    (F G : SheafOfModules.{w}
      (TensorSheafification.structureSheaf O.obj (isSheaf_structureRingPresheaf O)))
    [F.IsQuasicoherent] [G.IsQuasicoherent] :
    (MonoidalCategory.tensorObj F G).IsQuasicoherent

Stacks.SheafOfModules.TensorProduct.quasicoherentTensorBifunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Descent/QuasicoherentTensor.lean, line 286. The attribute's comment: “tensor_product, for Mathlib's IsQuasicoherent, not 03DL(6)”.

The tensor product as a bifunctor on quasi-coherent modules, QCoh(𝒪) × QCoh(𝒪) ⥤ QCoh(𝒪). It is the restriction of the tensor product of Mod(𝒪) to the full subcategory of quasi-coherent modules, and it exists exactly because that tensor product preserves quasi-coherence, which is Stacks 06WV (5): a bifunctor valued in QCoh(𝒪) cannot be written down before the clause is proved. The quasi-coherence cutting out the subcategory is Mathlib's; Stacks.SheafOfModules.TensorProduct.quasicoherentOnSiteTensorBifunctor is the same bifunctor on the subcategory cut out by the quasi-coherence of Stacks 03DL (6), which is the category QCoh(𝒪_𝒳) of Stacks 06WG.

public noncomputable def quasicoherentTensorBifunctor :
    (SheafOfModules.isQuasicoherent (TensorSheafification.structureSheaf O.obj
        (isSheaf_structureRingPresheaf O))).FullSubcategory ×
      (SheafOfModules.isQuasicoherent (TensorSheafification.structureSheaf O.obj
        (isSheaf_structureRingPresheaf O))).FullSubcategory ⥤
      (SheafOfModules.isQuasicoherent (TensorSheafification.structureSheaf O.obj
        (isSheaf_structureRingPresheaf O))).FullSubcategory

Stacks.SheafOfModules.TensorProduct.isQuasicoherentOnSite_tensorSheaf, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Descent/QuasicoherentTensor.lean, line 354. The attribute's comment: “tensor_product, not 06WG's site”. References: EGA I (9.1.1), “more general”.

The tensor clause of Stacks 06WV (5) and of Stacks 06WN (2), for the quasi-coherence of Stacks 03DL (6), on a site satisfying the hypotheses of this section: the tensor product of two sheaves of modules which are quasi-coherent in the sense of SheafOfModules.IsQuasicoherentOnSite is again quasi-coherent in that sense. That is the quasi-coherence the notion QCoh(𝒪_𝒳) of Stacks 06WG is defined by, and not Mathlib's predicate.

The hypotheses of this section exclude the site of Stacks 06WG, which is why both clause strings say so. Of the five, the fibred fppf site of a category fibred in groupoids over (Sch/S)_fppf satisfies three and fails two; the two failures are AlgebraicGeometry.FibredSite.not_univLE_associatedSite, the size hypothesis, which at that site's universes reads UnivLE.{u + 1, u}, and AlgebraicGeometry.FibredSite.not_hasBinaryProducts_twoLabel, binary products, which such a category generally lacks for want of a final object. See StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Descent/FibredTensorHypotheses.lean, where the five are settled one by one. So this statement does not instantiate to the source's clause, and the source's clause is not proved anywhere on this development.

The proof is the proof of Stacks.SheafOfModules.TensorProduct.isQuasicoherent_tensorSheaf run through SheafOfModules.isQuasicoherent_iff_isQuasicoherentOnSite, the identification of the two predicates on a site whose objects and morphisms are small relative to the universe of the sections — which is the extra hypothesis UnivLE.{max u v w, w} and the only thing separating the two statements. It is not removable: on a big site, whose objects live one universe above its sections, the two predicates genuinely differ.

What is not asserted is the rest of Stacks 06WN (2), namely that the tensor products formed in Mod(𝒳_Zar, 𝒪), Mod(𝒳_étale, 𝒪) and Mod(𝒪_𝒳) agree. Those are formed in different categories, where sheafification is a different functor, so the agreement is not a consequence of this statement and the comparison is not available; hence the qualified clause string, as in AlgebraicGeometry.FibredSite.colimits_quasicoherentModules_of_descent for part (1).

public instance isQuasicoherentOnSite_tensorSheaf
    (F G : SheafOfModules.{w}
      (TensorSheafification.structureSheaf O.obj (isSheaf_structureRingPresheaf O)))
    [F.IsQuasicoherentOnSite] [G.IsQuasicoherentOnSite] :
    ((((Stacks.SheafOfModules.Tensor.sheafTensor
      ⟨O.obj, Presheaf.isSheaf_of_isSheaf_comp _ (O.obj) (forget₂ CommRingCat RingCat)
        ((isSheaf_structureRingPresheaf O))⟩).obj (F)).obj (G))).IsQuasicoherentOnSite

Stacks.SheafOfModules.TensorProduct.isQuasicoherentOnSite_tensorObj, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Descent/QuasicoherentTensor.lean, line 376. The attribute's comment: “tensor_product, not 06WG's site”.

The tensor clause of Stacks 06WV (5) and of Stacks 06WN (2), for the quasi-coherence of Stacks 03DL (6), for the tensor product of the monoidal category Mod(𝒪) itself. Together with Stacks.SheafOfModules.TensorProduct.isQuasicoherentOnSite_tensorSheaf this is the covering set of the clause at the source's predicate, the development carrying both descriptions of the tensor product.

As there, the hypotheses of this section exclude the fibred fppf site of Stacks 06WG, by AlgebraicGeometry.FibredSite.not_univLE_associatedSite and AlgebraicGeometry.FibredSite.not_hasBinaryProducts_twoLabel; hence the qualified clause strings.

public instance isQuasicoherentOnSite_tensorObj
    (F G : SheafOfModules.{w}
      (TensorSheafification.structureSheaf O.obj (isSheaf_structureRingPresheaf O)))
    [F.IsQuasicoherentOnSite] [G.IsQuasicoherentOnSite] :
    (MonoidalCategory.tensorObj F G).IsQuasicoherentOnSite

Stacks.SheafOfModules.TensorProduct.quasicoherentOnSiteTensorBifunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Descent/QuasicoherentTensor.lean, line 398. The attribute's comment: “tensor_product, not 06WG's site”.

The tensor product as a bifunctor on the quasi-coherent modules of Stacks 03DL (6): the restriction of the tensor product of Mod(𝒪) to the full subcategory cut out by that quasi-coherence. It exists exactly because that tensor product preserves that quasi-coherence, which is the tensor clause of Stacks 06WV (5).

On the fibred fppf site of Stacks 06WG this subcategory is QCoh(𝒪_𝒳) (AlgebraicGeometry.FibredSite.quasicoherentModules), but the hypotheses of this section do not hold at that site — see AlgebraicGeometry.FibredSite.not_univLE_associatedSite and AlgebraicGeometry.FibredSite.not_hasBinaryProducts_twoLabel — so this bifunctor is not the one the source asserts; hence the qualified clause strings.

public noncomputable def quasicoherentOnSiteTensorBifunctor :
    (SheafOfModules.isQuasicoherentOnSite (TensorSheafification.structureSheaf O.obj
        (isSheaf_structureRingPresheaf O))).FullSubcategory ×
      (SheafOfModules.isQuasicoherentOnSite (TensorSheafification.structureSheaf O.obj
        (isSheaf_structureRingPresheaf O))).FullSubcategory ⥤
      (SheafOfModules.isQuasicoherentOnSite (TensorSheafification.structureSheaf O.obj
        (isSheaf_structureRingPresheaf O))).FullSubcategory

AlgebraicGeometry.FibredSite.existsUnique_hom_tensorSheafMixed_quasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/FibredMixedTensorProduct.lean, line 369. The attribute's comment: “tensor_product”.

Stacks 06WN(2). Restricted to a pair of quasi-coherent modules with sections in independent universes, the tensor product formed on an associated site of the fibred category is the tensor product in the ambient category of sheaves of modules on that site: every bilinear map into a sheaf of modules there has a unique linear factorization through the pure-tensor map. This is the universal property the source asserts of the common tensor product on the Zariski, étale and fppf sites; it is proved here for all five associated sites, and the factorization is tested against every sheaf of modules, not only the quasi-coherent ones.

public theorem existsUnique_hom_tensorSheafMixed_quasicoherent (τ : SiteKind)
    (F : quasicoherentModules.{u, v, u, m} B S hS p hp)
    (G : quasicoherentModules.{u, v, u, n} B S hS p hp)
    (H : SheafOfModules.{max u m n} (ringStructureSheafCore B S hS p hp τ))
    (b : Stacks.Modules.BilinearMap (structureSheaf B S hS p hp τ).obj
      F.obj.val G.obj.val H.val) :
    ∃! f : tensorSheafMixed B S hS p hp τ ((toSiteModules B S hS p hp τ).obj F)
        ((toSiteModules B S hS p hp τ).obj G) ⟶ H,
      ∀ (U : 𝒳ᵒᵖ) (x : F.obj.val.obj U) (y : G.obj.val.obj U),
        f.val.app U ((toTensorSheafMixed B S hS p hp τ
          ((toSiteModules B S hS p hp τ).obj F)
          ((toSiteModules B S hS p hp τ).obj G)).app U x y) = b.app U x y

AlgebraicGeometry.FibredSite.isQuasicoherentOnSite_tensorSheafMixed_quasicoherent, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/MixedTensorQuasicoherent.lean, line 239. The attribute's comment: “tensor_product”.

The tensor product of a pair of quasi-coherent modules with sections in independent universes, formed on the fppf site of a category fibred in groupoids, is quasi-coherent. This is the object whose universal property is AlgebraicGeometry.FibredSite.existsUnique_hom_tensorSheafMixed_quasicoherent, so the tensor product of quasi-coherent modules is again a quasi-coherent module.

theorem isQuasicoherentOnSite_tensorSheafMixed_quasicoherent
    (F : quasicoherentModules.{u, v, u, m} B S hS p hp)
    (G : quasicoherentModules.{u, v, u, n} B S hS p hp) :
    (tensorSheafMixed B S hS p hp .fppf ((toSiteModules B S hS p hp .fppf).obj F)
      ((toSiteModules B S hS p hp .fppf).obj G)).IsQuasicoherentOnSite

AlgebraicGeometry.FibredSite.isQuasicoherentOnSite_X₂_of_shortExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentExtensions.lean, line 68. The attribute's comment: “part (7): an extension in Mod(𝒪_𝒳) of quasi-coherent modules is quasi-coherent, for every category fibred in groupoids over (Sch/S)_fppf, in particular for every algebraic stack”.

Stacks 06WV (7). Let 𝒳 be a category fibred in groupoids over (Sch/S)_fppf, for instance an algebraic stack, and let 0 → 𝓕₁ → 𝓕₂ → 𝓕₃ → 0 be a short exact sequence in Mod(𝒪_𝒳) with 𝓕₁ and 𝓕₃ quasi-coherent. Then 𝓕₂ is quasi-coherent.

By Stacks 06WI it suffices that x^*𝓕₂ be quasi-coherent on (Sch/U)_fppf for each object x over a scheme U. The functor x^* is restriction to 𝒳_fppf/x followed by an equivalence; restriction to a localized site is exact (Stacks 03DA), so x^* carries the sequence to a short exact sequence on (Sch/U)_fppf, whose middle term is quasi-coherent by Stacks 0GNC (4), AlgebraicGeometry.BigFppfOver.isQuasicoherentOnSite_shortExact_X₂_all.

theorem isQuasicoherentOnSite_X₂_of_shortExact
    {C : ShortComplex (SheafOfModules.{u} (ringStructureSheafCore B S hS p hp .fppf))}
    (hC : C.ShortExact) (h₁ : C.X₁.IsQuasicoherentOnSite) (h₃ : C.X₃.IsQuasicoherentOnSite) :
    C.X₂.IsQuasicoherentOnSite

Declarations registered for the tag:

Tag 0781, a proposition

Tag 0781 in the Stacks Project.

AlgebraicGeometry.Stack.quasicoherentModules_isGrothendieckAbelian_enoughInjectives_hasLimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/AlgebraicStackCoherator.lean, line 137. The attribute's comment: “part (1): QCoh(𝒪_𝒳) is a Grothendieck abelian category; consequently it has enough injectives and all limits”.

Stacks 0781, part (1). Let 𝒳 be an algebraic stack over S. The category QCoh(𝒪_𝒳) of quasi-coherent modules on 𝒳 is a Grothendieck abelian category; consequently it has enough injectives and all limits.

Through a presentation [U/R] → 𝒳 whose space of objects is a scheme, QCoh(𝒪_𝒳) is equivalent to QCoh(U, R, s, t, c) (Stacks 06WV (1)), which is Grothendieck abelian: colimits exist, filtered colimits are exact because they and kernels are computed on 𝒪_U-modules, and there is a separator by the argument of Groupoids in Spaces, Lemma 0780 (AlgebraicGeometry.Space.QuasicoherentModule.isGrothendieckAbelian_of_objects_eq). The assertions on injectives and limits hold in every Grothendieck abelian category (Stacks 079H, 07D8).

theorem quasicoherentModules_isGrothendieckAbelian_enoughInjectives_hasLimits :
    IsGrothendieckAbelian.{u} (FibredSite.quasicoherentModules.{u, u + 1, u, u} B S hS
        𝒳.val.val.p 𝒳.val.isFiberedInGroupoids) ∧
      EnoughInjectives (FibredSite.quasicoherentModules.{u, u + 1, u, u} B S hS
        𝒳.val.val.p 𝒳.val.isFiberedInGroupoids) ∧
      HasLimitsOfSize.{u, u} (FibredSite.quasicoherentModules.{u, u + 1, u, u} B S hS
        𝒳.val.val.p 𝒳.val.isFiberedInGroupoids)

AlgebraicGeometry.Stack.exists_quasicoherentCoherator, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/AlgebraicStackCoherator.lean, line 194. The attribute's comment: “part (2): the inclusion QCoh(𝒪_𝒳) → Mod(𝒪_𝒳) has a right adjoint Q such that Q(F) → F is an isomorphism for every quasi-coherent F”.

Stacks 0781, part (2). Let 𝒳 be an algebraic stack over S. The inclusion QCoh(𝒪_𝒳) → Mod(𝒪_𝒳) has a right adjoint Q, the coherator, such that for every quasi-coherent 𝒪_𝒳-module 𝓕 the adjunction morphism Q(𝓕) → 𝓕 is an isomorphism.

The right adjoint exists by AlgebraicGeometry.Stack.isLeftAdjoint_quasicoherentInclusion. The inclusion is fully faithful, so the counit is an isomorphism exactly on its essential image, which contains the quasi-coherent modules.

theorem exists_quasicoherentCoherator :
    ∃ (Q : SheafOfModules.{u} (FibredSite.ringStructureSheafCore B S hS 𝒳.val.val.p
          𝒳.val.isFiberedInGroupoids .fppf) ⥤
        FibredSite.quasicoherentModules.{u, u + 1, u, u} B S hS 𝒳.val.val.p
          𝒳.val.isFiberedInGroupoids)
      (adj : (SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
        (FibredSite.ringStructureSheafCore B S hS 𝒳.val.val.p 𝒳.val.isFiberedInGroupoids
          .fppf)).ι ⊣ Q),
      ∀ M : SheafOfModules.{u} (FibredSite.ringStructureSheafCore B S hS 𝒳.val.val.p
          𝒳.val.isFiberedInGroupoids .fppf),
        M.IsQuasicoherentOnSite → IsIso (adj.counit.app M)

AlgebraicGeometry.FibredSite.isGrothendieckAbelian_quasicoherentModules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Coherator.lean, line 83. The attribute's comment: “part (1): QCoh(𝒪_𝒳) is Grothendieck abelian, over local smallness, the exactness of filtered colimits, and the separator the source gets from a groupoid presentation”.

The category QCoh(𝒪_𝒳) of quasi-coherent modules on the associated fppf site of a category fibred in groupoids is a Grothendieck abelian category, provided quasi-coherence is closed under colimits (hclosed), QCoh(𝒪_𝒳) is locally small (hls), its filtered colimits are exact (hab5) and it has a separator (hsep).

theorem isGrothendieckAbelian_quasicoherentModules
    [Abelian (quasicoherentModules.{u, u + 1, u, u} B S hS p hp)]
    (hclosed : SheafOfModules.ClosedUnderColimitsOfSize.{u, u + 1, u, u, u}
      (ringStructureSheafCore B S hS p hp .fppf))
    (hls : LocallySmall.{u} (quasicoherentModules.{u, u + 1, u, u} B S hS p hp))
    (hab5 : ∀ (K : Type u) [Category.{u} K] [IsFiltered K]
      [HasColimitsOfShape K (quasicoherentModules.{u, u + 1, u, u} B S hS p hp)],
      HasExactColimitsOfShape K (quasicoherentModules.{u, u + 1, u, u} B S hS p hp))
    (hsep : HasSeparator (quasicoherentModules.{u, u + 1, u, u} B S hS p hp)) :
    IsGrothendieckAbelian.{u} (quasicoherentModules.{u, u + 1, u, u} B S hS p hp)

AlgebraicGeometry.FibredSite.enoughInjectives_quasicoherentModules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Coherator.lean, line 102. The attribute's comment: “part (1), its consequence: QCoh(𝒪_𝒳) has enough injectives”.

Under the hypotheses of AlgebraicGeometry.FibredSite.isGrothendieckAbelian_quasicoherentModules, QCoh(𝒪_𝒳) has enough injectives.

theorem enoughInjectives_quasicoherentModules
    [Abelian (quasicoherentModules.{u, u + 1, u, u} B S hS p hp)]
    (hclosed : SheafOfModules.ClosedUnderColimitsOfSize.{u, u + 1, u, u, u}
      (ringStructureSheafCore B S hS p hp .fppf))
    (hls : LocallySmall.{u} (quasicoherentModules.{u, u + 1, u, u} B S hS p hp))
    (hab5 : ∀ (K : Type u) [Category.{u} K] [IsFiltered K]
      [HasColimitsOfShape K (quasicoherentModules.{u, u + 1, u, u} B S hS p hp)],
      HasExactColimitsOfShape K (quasicoherentModules.{u, u + 1, u, u} B S hS p hp))
    (hsep : HasSeparator (quasicoherentModules.{u, u + 1, u, u} B S hS p hp)) :
    EnoughInjectives (quasicoherentModules.{u, u + 1, u, u} B S hS p hp)

AlgebraicGeometry.FibredSite.hasLimitsOfSize_quasicoherentModules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Coherator.lean, line 119. The attribute's comment: “part (1), its consequence: QCoh(𝒪_𝒳) has all limits”.

Under the hypotheses of AlgebraicGeometry.FibredSite.isGrothendieckAbelian_quasicoherentModules, QCoh(𝒪_𝒳) has all limits.

theorem hasLimitsOfSize_quasicoherentModules
    [Abelian (quasicoherentModules.{u, u + 1, u, u} B S hS p hp)]
    (hclosed : SheafOfModules.ClosedUnderColimitsOfSize.{u, u + 1, u, u, u}
      (ringStructureSheafCore B S hS p hp .fppf))
    (hls : LocallySmall.{u} (quasicoherentModules.{u, u + 1, u, u} B S hS p hp))
    (hab5 : ∀ (K : Type u) [Category.{u} K] [IsFiltered K]
      [HasColimitsOfShape K (quasicoherentModules.{u, u + 1, u, u} B S hS p hp)],
      HasExactColimitsOfShape K (quasicoherentModules.{u, u + 1, u, u} B S hS p hp))
    (hsep : HasSeparator (quasicoherentModules.{u, u + 1, u, u} B S hS p hp)) :
    HasLimitsOfSize.{u, u} (quasicoherentModules.{u, u + 1, u, u} B S hS p hp)

AlgebraicGeometry.FibredSite.moduleCoherator, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Coherator.lean, line 165. The attribute's comment: “part (2): the coherator Q : Mod(𝒪_𝒳) ⥤ QCoh(𝒪_𝒳)”.

The coherator on Mod(𝒪_𝒳). The right adjoint of the inclusion of QCoh(𝒪_𝒳) into all modules on the associated fppf site of 𝒳: it sends a module A to the terminal quasi-coherent module equipped with a map to A.

def moduleCoherator
    (hclosed : SheafOfModules.ClosedUnderColimitsOfSize.{u, u + 1, u, u, u}
      (ringStructureSheafCore B S hS p hp .fppf))
    (hls : LocallySmall.{u} (quasicoherentModules.{u, u + 1, u, u} B S hS p hp))
    (hlsD : LocallySmall.{u} (SheafOfModules.{u} (ringStructureSheafCore B S hS p hp .fppf)))
    (hwp : WellPowered.{u} (quasicoherentModules.{u, u + 1, u, u} B S hS p hp)ᵒᵖ)
    (hsep : HasSeparator (quasicoherentModules.{u, u + 1, u, u} B S hS p hp)) :
    SheafOfModules.{u} (ringStructureSheafCore B S hS p hp .fppf) ⥤
      quasicoherentModules.{u, u + 1, u, u} B S hS p hp

AlgebraicGeometry.FibredSite.moduleCoheratorAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Coherator.lean, line 185. The attribute's comment: “part (2): the adjunction between the inclusion and the coherator”.

The coherator on Mod(𝒪_𝒳) is right adjoint to the inclusion. The adjunction is the universal property of the terminal objects the coherator is built from.

def moduleCoheratorAdjunction
    (hclosed : SheafOfModules.ClosedUnderColimitsOfSize.{u, u + 1, u, u, u}
      (ringStructureSheafCore B S hS p hp .fppf))
    (hls : LocallySmall.{u} (quasicoherentModules.{u, u + 1, u, u} B S hS p hp))
    (hlsD : LocallySmall.{u} (SheafOfModules.{u} (ringStructureSheafCore B S hS p hp .fppf)))
    (hwp : WellPowered.{u} (quasicoherentModules.{u, u + 1, u, u} B S hS p hp)ᵒᵖ)
    (hsep : HasSeparator (quasicoherentModules.{u, u + 1, u, u} B S hS p hp)) :
    (SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
        (ringStructureSheafCore B S hS p hp .fppf)).ι ⊣
      moduleCoherator B S hS p hp hclosed hls hlsD hwp hsep

AlgebraicGeometry.FibredSite.moduleCoheratorCompInclusionIsoId, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/Coherator.lean, line 206. The attribute's comment: “part (2): the coherator composed with the inclusion is the identity”.

The coherator fixes the quasi-coherent modules. The composite of the inclusion with the coherator is the identity functor of QCoh(𝒪_𝒳): Q 𝓕 ≅ 𝓕 for quasi-coherent 𝓕.

def moduleCoheratorCompInclusionIsoId
    (hclosed : SheafOfModules.ClosedUnderColimitsOfSize.{u, u + 1, u, u, u}
      (ringStructureSheafCore B S hS p hp .fppf))
    (hls : LocallySmall.{u} (quasicoherentModules.{u, u + 1, u, u} B S hS p hp))
    (hlsD : LocallySmall.{u} (SheafOfModules.{u} (ringStructureSheafCore B S hS p hp .fppf)))
    (hwp : WellPowered.{u} (quasicoherentModules.{u, u + 1, u, u} B S hS p hp)ᵒᵖ)
    (hsep : HasSeparator (quasicoherentModules.{u, u + 1, u, u} B S hS p hp)) :
    (SheafOfModules.isQuasicoherentOnSite.{u + 1, u, u, u}
          (ringStructureSheafCore B S hS p hp .fppf)).ι ⋙
        moduleCoherator B S hS p hp hclosed hls hlsD hwp hsep ≅
      𝟭 (quasicoherentModules.{u, u + 1, u, u} B S hS p hp)

AlgebraicGeometry.FibredSite.moduleCoheratorSucc, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentPushforward.lean, line 219. The attribute's comment: “part (2): the coherator Q : Mod(𝒪_𝒳) ⥤ QCoh(𝒪_𝒳), at section universe u + 1”.

Stacks 0781, part (2), at section universe u + 1: the coherator on Mod(𝒪_𝒳). The right adjoint of the inclusion of QCoh(𝒪_𝒳) into all modules on the associated fppf site: it sends a module A to the terminal quasi-coherent module equipped with a map to A.

AlgebraicGeometry.FibredSite.moduleCoherator is the same construction at section universe u; u + 1 is the universe the direct images of Stacks 06WE along a 1-morphism of algebraic stacks live in, and so the universe Stacks 077A needs the coherator in.

def moduleCoheratorSucc
    (hclosed : QuasicoherentClosedUnderColimitsSucc B S hS p hp)
    (hwp : WellPowered.{u + 1} (quasicoherentModules.{u, u + 1, u, u + 1} B S hS p hp)ᵒᵖ)
    (hsep : HasSeparator (quasicoherentModules.{u, u + 1, u, u + 1} B S hS p hp)) :
    SheafOfModules.{u + 1} (ringStructureSheafCore B S hS p hp .fppf) ⥤
      quasicoherentModules.{u, u + 1, u, u + 1} B S hS p hp

AlgebraicGeometry.FibredSite.moduleCoheratorSuccAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentPushforward.lean, line 233. The attribute's comment: “part (2): the adjunction between the inclusion and the coherator, at section universe u + 1”.

Stacks 0781, part (2): the coherator is right adjoint to the inclusion. The adjunction is the universal property of the terminal objects the coherator is built from.

def moduleCoheratorSuccAdjunction
    (hclosed : QuasicoherentClosedUnderColimitsSucc B S hS p hp)
    (hwp : WellPowered.{u + 1} (quasicoherentModules.{u, u + 1, u, u + 1} B S hS p hp)ᵒᵖ)
    (hsep : HasSeparator (quasicoherentModules.{u, u + 1, u, u + 1} B S hS p hp)) :
    quasicoherentInclusion B S hS p hp ⊣ moduleCoheratorSucc B S hS p hp hclosed hwp hsep

AlgebraicGeometry.FibredSite.moduleCoheratorSuccCompInclusionIsoId, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Stacks/Quasicoherent/QuasicoherentPushforward.lean, line 247. The attribute's comment: “part (2): the coherator composed with the inclusion is the identity, at section universe u + 1”.

Stacks 0781, part (2): the coherator fixes the quasi-coherent modules. The inclusion is fully faithful, so the unit of the adjunction is an isomorphism; this is the source's assertion that Q 𝓕 → 𝓕 is an isomorphism for quasi-coherent 𝓕.

def moduleCoheratorSuccCompInclusionIsoId
    (hclosed : QuasicoherentClosedUnderColimitsSucc B S hS p hp)
    (hwp : WellPowered.{u + 1} (quasicoherentModules.{u, u + 1, u, u + 1} B S hS p hp)ᵒᵖ)
    (hsep : HasSeparator (quasicoherentModules.{u, u + 1, u, u + 1} B S hS p hp)) :
    quasicoherentInclusion B S hS p hp ⋙ moduleCoheratorSucc B S hS p hp hclosed hwp hsep ≅
      𝟭 (quasicoherentModules.{u, u + 1, u, u + 1} B S hS p hp)
Sources
LeanAlgebraicGeometry.Stack.colimits_quasicoherentModules · AlgebraicGeometry.Stack.quasicoherentInclusion_rightExact_not_exact · AlgebraicGeometry.Stack.GroupoidPresentation.quasicoherentEquivalence · AlgebraicGeometry.Stack.abelianQuasicoherentModules · AlgebraicGeometry.FibredSite.preservesColimitsOfSize_quasicoherentInclusion' · Stacks.SheafOfModules.TensorProduct.isQuasicoherent_tensorSheaf · Stacks.SheafOfModules.TensorProduct.isQuasicoherent_tensorObj · Stacks.SheafOfModules.TensorProduct.quasicoherentTensorBifunctor

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.