6.23 Continuous maps and… to 6.33 Glueing sheaves

Section6.23 Continuous maps and sheaves of algebraic structures#

Section 6.23 of the Stacks Project, Tag 008P. 1 tag here is carried by 1 declaration of the repository (in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 008Q, a lemma

Tag 008Q in the Stacks Project.

main_theorem008Q, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Functors/FMap/AlgebraicStructure.lean, line 105.

Stacks 008Q. Given an f-map φ of underlying sheaves of sets whose components all lift along U, there exists a unique f-map of sheaves of algebraic structures with underlying f-map φ.

theorem main_theorem008Q
    {C : Type u} [Category.{w} C]
    (U : C ⥤ Type w) [U.Faithful] [U.ReflectsIsomorphisms]
    [HasLimits C] [PreservesLimits U]
    {X Y : TopCat} (f : X ⟶ Y)
    (F : TopCat.Sheaf C X) (G : TopCat.Sheaf C Y)
    (φ : underlyingSheaf U G ⟶
          (TopCat.Sheaf.pushforward (Type w) f).obj (underlyingSheaf U F))
    (hφ : ∀ (V : (Opens Y)ᵒᵖ),
            ∃ ψV : G.obj.obj V ⟶ F.obj.obj ((Opens.map f).op.obj V),
              U.map ψV = φ.hom.app V) :
    ∃! ψ : G ⟶ (TopCat.Sheaf.pushforward C f).obj F,
      underlyingSheafMap U ψ = φ

Sources

• Section 6.23, Tag 008P
• AxiomMath/Stacks at 5ed82d14

Leanmain_theorem008Q

Section6.24 Continuous maps and sheaves of modules#

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

Tag 008S, a lemma

Tag 008S in the Stacks Project.

Declarations registered for the tag:

• PresheafOfModules.pushforward₀Obj registered with add_to_stacks in StacksFrontier/Topology/Sheaves/Functors/Module/PushforwardPresheaf.lean, line 30 (StacksFrontier): “the pushforward f_*ℱ as a presheaf of f_*𝒪-modules”.
• PresheafOfModules.pushforward₀ registered with add_to_stacks in StacksFrontier/Topology/Sheaves/Functors/Module/PushforwardPresheaf.lean, line 32 (StacksFrontier): “pushforward as a functor PMod(𝒪) ⥤ PMod(f_*𝒪)”.
• PresheafOfModules.map_smul registered with add_to_stacks in StacksFrontier/Topology/Sheaves/Functors/Module/PushforwardPresheaf.lean, line 34 (StacksFrontier): “the scalar action is compatible with restriction, which is the naturality of the map f_*𝒪 × f_*ℱ ⟶ f_*ℱ”. References: SGA 3 I (6.4), “more general”.

Tag 008T, a lemma

Tag 008T in the Stacks Project.

Stacks.PresheafOfModules.Pullback.pullback_presheaf_module, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Functors/Module/PullbackPresheaf.lean, line 629. The attribute's comment: “(1), (2)”.

Stacks 008T (1), (2).

Let O be a presheaf of rings on Y and G a presheaf of O-modules. Then the pullback presheaf of abelian groups f_p G carries the structure of a presheaf of f_p O-modules: there is a presheaf of f_p O-modules M whose underlying presheaf of abelian groups is exactly f_p G.

The data of M : PresheafOfModules (f_p O) packages, for each open U ⊆ X, the scalar multiplication (f_p O)(U) × (f_p G)(U) → (f_p G)(U) together with the module axioms and the compatibility with the restriction maps. That toPresheaf.obj M is literally the pullback presheaf f_p G expresses that this module structure lives on f_p G itself.

theorem pullback_presheaf_module (O : TopCat.Presheaf RingCat.{u} Y) (G : PresheafOfModules.{u} O) :
    ∃ M : PresheafOfModules.{u} (pullbackRing f O),
      (PresheafOfModules.toPresheaf (pullbackRing f O)).obj M =
        pullbackAb f (underlyingAb O G)

Stacks.PresheafOfModules.Pullback.pullbackModuleFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Functors/Module/PullbackPresheaf.lean, line 658. The attribute's comment: “(3)”.

Stacks 008T (3): the functor lifting f_p to presheaves of modules.

The construction of the module structure is functorial in G: f_p lifts to a functor Φ : PresheafOfModules O ⥤ PresheafOfModules (f_p O) from the category of presheaves of O-modules on Y to the category of presheaves of f_p O-modules on X. That it lies over the abelian-group-level functor f_p is pullbackModuleFunctorCompToPresheaf.

On objects it sends G to the presheaf of f_p O-modules with carrier f_p G and the scalar action of pullbackModule. On a morphism φ : G ⟶ G' of O-modules with underlying Ab-presheaf morphism φ̲, it takes (TopCat.Presheaf.pullback Ab f).map φ̲ : f_p G ⟶ f_p G', which is (f_p O)(U)-linear for each U by pullbackModule_morphism_smul: it is colim of the levelwise O(V)-linear maps φ_V, and the action is built from the levelwise O(V)-actions. Functoriality is inherited from that of TopCat.Presheaf.pullback Ab f, since PresheafOfModules.homMk is built on top of it and toPresheaf is faithful.

noncomputable def pullbackModuleFunctor (O : TopCat.Presheaf RingCat.{u} Y) :
    PresheafOfModules.{u} O ⥤ PresheafOfModules.{u} (pullbackRing f O)

Stacks.PresheafOfModules.Pullback.pullbackModuleFunctorCompToPresheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Functors/Module/PullbackPresheaf.lean, line 699. The attribute's comment: “(3)”.

Stacks 008T (3): the comparison isomorphism expressing that pullbackModuleFunctor lies over f_p: Φ ⋙ toPresheaf (f_p O) ≅ toPresheaf O ⋙ (pullback Ab f).

Lying over f_p means that forgetting the module structure of Φ.obj G recovers f_p applied to the abelian-group presheaf underlying G, naturally in G. In particular, for a morphism φ : G → G' of presheaves of O-modules, Φ.map φ is a morphism of presheaves of f_p O-modules whose underlying morphism of presheaves of abelian groups is f_p φ.

It is the identity natural isomorphism: Φ.obj G is ofPresheaf (f_p (underlying G)) …, whose underlying Ab presheaf is f_p (underlying G) on the nose, and Φ.map φ is homMk (f_p φ̲) …, whose underlying Ab map is f_p φ̲ on the nose, so both composites agree definitionally (compare pushforward₀CompToPresheaf and restrictScalarsCompToPresheaf in Mathlib, both also Iso.refl _).

noncomputable def pullbackModuleFunctorCompToPresheaf (O : TopCat.Presheaf RingCat.{u} Y) :
    pullbackModuleFunctor f O ⋙ PresheafOfModules.toPresheaf (pullbackRing f O) ≅
      PresheafOfModules.toPresheaf O ⋙ TopCat.Presheaf.pullback Ab.{u} f

Tag 008U, a lemma

Tag 008U in the Stacks Project.

canonicalAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Functors/Module/PresheafAdjunction.lean, line 142. References: SGA 4 IV (13.4), “special case”.

Stacks 008U. Let f : X ⟶ Y be a continuous map of topological spaces and let O be a presheaf of rings on Y. Then the pullback f_p of presheaves of modules, from presheaves of O-modules on Y to presheaves of f_p O-modules on X, is left adjoint to the pushforward f_*; in particular the hom-sets Hom_{f_p O}(f_p G, F) and Hom_O(G, f_* F) are naturally bijective, which is the bijection the lemma states.

This is Mathlib's PresheafOfModules.pullbackPushforwardAdjunction at F := Opens.map f and at the lemma's own data R := f_p O, φ := i_O (the unit of the rings-level pullback/pushforward adjunction).

noncomputable def canonicalAdjunction :
    pullbackModules f O (f_pRings f O) (iRings f O) ⊣
      pushforwardModules f O (f_pRings f O) (iRings f O)

Tag 008V, a lemma

Tag 008V in the Stacks Project.

main_hom_equiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Functors/Module/PresheafAdjunctionOverPushforward.lean, line 97. References: SGA 4 IV (13.4), “special case”.

Stacks 008V. The natural bijection Mor_{PMod(O)}(f^*G, F) ≃ Mor_{PMod(f_*O)}(G, f_*F) witnessing that f^* is left adjoint to f_* on presheaves of modules.

noncomputable def main_hom_equiv {X Y : TopCat.{u}} (f : X ⟶ Y)
    (O : (TopologicalSpace.Opens X)ᵒᵖ ⥤ RingCat.{u})
    (F : PresheafOfModules.{u} O)
    (G : PresheafOfModules.{u} (pushforwardRings f O)) :
    ((pullbackModules008V f O).obj G ⟶ F) ≃ (G ⟶ (pushforwardModules008V f O).obj F)

Tag 008W, a lemma

Tag 008W in the Stacks Project.

Declarations registered for the tag:

• CategoryTheory.Functor.sheafPushforwardContinuous registered with add_to_stacks in StacksFrontier/Topology/Sheaves/Functors/Module/PushforwardSheaf.lean, line 26 (StacksFrontier): “the pushforward f_*𝒪 of the sheaf of rings, along the continuous functor Opens.map f”. References: SGA 4 IV (4.9.1).
• SheafOfModules.pushforward registered with add_to_stacks in StacksFrontier/Topology/Sheaves/Functors/Module/PushforwardSheaf.lean, line 28 (StacksFrontier): “pushforward of sheaves of modules: f_*ℱ is a sheaf of f_*𝒪-modules, functorially in ℱ”. References: EGA 0 (4.2.1), “more general”; EGA 0 (5.3.12); EGA II (1.1.1), “more general”; EGA II (1.1.2), “partial”; EGA IV (21.13.3); SGA 4 IV (11.2.2), “more general”; SGA 4 IV (13.2.1), “special case”; SGA 4 Vbis (1.3.6), “special case”.

Tag 008X, a lemma

Tag 008X in the Stacks Project.

InverseImageModules.exists_moduleStructure_inverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Functors/Module/InverseImage.lean, line 135.

Stacks Tag 008X.

Let f : X ⟶ Y be a continuous map, O a sheaf of rings on Y and G a sheaf of O-modules. There is a scalar multiplication turning f⁻¹G into a sheaf of f⁻¹O-modules, and it is natural in the sense that it extends the presheaf-level scalar multiplication f_p O × f_p G → f_p G of Tag 008T along the sheafification maps.

Concretely: there is a sheaf of f⁻¹O-modules M whose underlying presheaf of abelian groups is literally f⁻¹G, together with a morphism ι of presheaves of f_p O-modules from f_p G to M restricted along f_p O ⟶ f⁻¹O, whose underlying morphism of presheaves of abelian groups is the sheafification map f_p G ⟶ f⁻¹G.

theorem exists_moduleStructure_inverseImage :
    ∃ (M : SheafOfModules.{u} (inverseImageRing f O))
      (h : M.val.presheaf = (inverseImageAb f O G).obj)
      (ι : pullbackPresheafOfModules f O G ⟶
            (PresheafOfModules.restrictScalars (toInverseImageRing f O)).obj M.val),
      (PresheafOfModules.toPresheaf _).map ι ≫ eqToHom h = toInverseImageAb f O G

Tag 008Y, a lemma

Tag 008Y in the Stacks Project.

adjointPullbackPushforward, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Functors/Module/SheafAdjunction.lean, line 129.

Stacks Project tag 008Y (Adjointness of f⁻¹ and f_* for sheaves of modules).

For a continuous map f : X → Y of topological spaces and a sheaf of rings O on Y, the pullback functor on sheaves of modules f⁻¹ : SheafOfModules O ⥤ SheafOfModules (f⁻¹O) is left adjoint to the pushforward functor f_* : SheafOfModules (f⁻¹O) ⥤ SheafOfModules O, where:

• f⁻¹O = (TopCat.Sheaf.pullback RingCat f).obj O is the canonical pullback sheaf of rings;
• the sheaf-of-O-module structure on f_*F (for F a sheaf of f⁻¹O-modules) is obtained by restriction of scalars along the canonical adjunction unit O → f_*f⁻¹O for sheaves of rings (i.e. adjunctionUnit f O).

The adjunction is Mathlib's SheafOfModules.pullbackPushforwardAdjunction at that unit, recorded here with its unit and counit rather than only its existence; the hom-set formula of the tag is read off it as homEquivPullbackPushforward.

noncomputable def adjointPullbackPushforward :
    SheafOfModules.pullback.{u} (adjunctionUnit f O) ⊣
      SheafOfModules.pushforward.{u} (adjunctionUnit f O)

Tag 008Z, a lemma

Tag 008Z in the Stacks Project.

pullbackPushforwardAdjunction008Z, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Functors/Module/SheafAdjunctionOverPushforward.lean, line 118. References: EGA 0 (4.4.3).

Stacks 008Z. The adjunction exhibiting the tensor pullback 𝒪 ⊗_{f^{-1}f_*𝒪} f^{-1}(–) as a left adjoint of the pushforward f_* on sheaves of modules. It is SheafOfModules.PullbackConstruction.adjunction at canonicalRingHom, and carries the unit, the counit and the hom-set bijection of the tag, the last of which is morPullbackEquivMorPushforward.

noncomputable def pullbackPushforwardAdjunction008Z {X Y : TopCat.{u}} (f : X ⟶ Y)
    (𝒪 : Sheaf (Opens.grothendieckTopology X) RingCat.{u}) :
    tensorPullbackModule f 𝒪 ⊣ pushforwardModule f 𝒪

Sources

• Section 6.24, Tag 008R
• AxiomMath/Stacks at 5ed82d14

LeanPresheafOfModules.pushforward₀Obj · PresheafOfModules.pushforward₀ · PresheafOfModules.map_smul · Stacks.PresheafOfModules.Pullback.pullback_presheaf_module · Stacks.PresheafOfModules.Pullback.pullbackModuleFunctor · Stacks.PresheafOfModules.Pullback.pullbackModuleFunctorCompToPresheaf · canonicalAdjunction · main_hom_equiv

Section6.25 Ringed spaces#

Section 6.25 of the Stacks Project, Tag 0090. 3 tags here are carried by 1 declaration of the repository (in StacksFrontier) and 5 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0091, a definition

Tag 0091 in the Stacks Project.

Declarations registered for the tag:

• AlgebraicGeometry.RingedSpace registered with add_to_stacks in StacksFrontier/Topology/Sheaves/RingedSpace/Basic.lean, line 26 (StacksFrontier): “a ringed space: a topological space together with a sheaf of commutative rings on it”. References: EGA 0 (4.1.1), “ringed space def”; SGA 4 Vbis (1.3.1), “topological space case”; SGA 4 IV (11.1.1), “site of opens of a space”.
• AlgebraicGeometry.PresheafedSpace.Hom registered with add_to_stacks in StacksFrontier/Topology/Sheaves/RingedSpace/Basic.lean, line 31 (StacksFrontier): “a morphism of ringed spaces: a continuous map base together with an f-map c of sheaves of rings”. References: EGA 0 (3.5.1); EGA 0 (4.1.1), “morphism definition”; EGA 0 (3.5.2), “category of pairs”.

Tag 0092, an example

Tag 0092 in the Stacks Project.

fSharp, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/RingedSpace/ContinuousFunctions.lean, line 43.

The natural \(f\)-map \(f^\sharp : \mathcal{C}^0_Y \to f_*\mathcal{C}^0_X\) associated to a continuous map \(f : X \to Y\) between topological spaces, given on sections over an open \(V \subseteq Y\) by precomposition with \(f\): \(h \mapsto h \circ f|_{f^{-1}(V)}\). This is the morphism asserted to exist in the Stacks example.

noncomputable def fSharp {X Y : TopCat.{0}} (f : X ⟶ Y) :
    presheafC0 Y ⟶
      (TopCat.Presheaf.pushforward (CommAlgCat ℝ) f).obj
        (presheafC0 X)

Tag 0093, a definition

Tag 0093 in the Stacks Project.

Declarations registered for the tag:

• AlgebraicGeometry.PresheafedSpace.comp registered with add_to_stacks in StacksFrontier/Topology/Sheaves/RingedSpace/Comp.lean, line 24 (StacksFrontier): “the composition of two morphisms of ringed spaces”. References: EGA 0 (3.5.2); EGA 0 (4.1.1), “composition”.
• AlgebraicGeometry.PresheafedSpace.comp_base registered with add_to_stacks in StacksFrontier/Topology/Sheaves/RingedSpace/Comp.lean, line 28 (StacksFrontier): “its base map is the composite continuous map”. References: EGA 0 (3.5.2), “partial”; EGA 0 (4.1.1), “psi''=psi'o psi”.
• AlgebraicGeometry.PresheafedSpace.comp_c registered with add_to_stacks in StacksFrontier/Topology/Sheaves/RingedSpace/Comp.lean, line 32 (StacksFrontier): “its sharp map is g^♯ followed by the pushforward of f^♯ along g”. References: EGA 0 (4.1.1), “theta''=psi_*(th)o th'”.

Sources

• Section 6.25, Tag 0090
• AxiomMath/Stacks at 5ed82d14

LeanAlgebraicGeometry.RingedSpace · AlgebraicGeometry.PresheafedSpace.Hom · fSharp · AlgebraicGeometry.PresheafedSpace.comp · AlgebraicGeometry.PresheafedSpace.comp_base · AlgebraicGeometry.PresheafedSpace.comp_c

Section6.26 Morphisms of ringed spaces and modules#

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

Tag 0095, a definition

Tag 0095 in the Stacks Project.

RingedSpaceModuleAdjunction.modulePushforward, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Functors/Module/RingedSpace.lean, line 123. The attribute's comment: “(1)”. References: EGA 0 (4.2.1), “Ψ_ functor”; EGA 0 (12.2.1); SGA 4 Vbis (1.3.6), “ringed spaces, φ_”; SGA 3 VIIA (1.1), “more general”; SGA 4 IV (13.2.1), “special case”; SGA 4 V (5.0), “special case”.

Pushforward of sheaves of modules along a morphism of ringed spaces, f_* : Mod(𝒪_X) ⥤ Mod(𝒪_Y), given on sections by (f_* F)(V) = F(f⁻¹ V), with the 𝒪_Y-module structure restricted along f^♯.

noncomputable def modulePushforward :
    SheafOfModules.{u} (structureSheafRing X) ⥤ SheafOfModules.{u} (structureSheafRing Y)

PullbackStalkTensor.modulePullbackTensor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/RingedSpace/ModulePullbackTensor.lean, line 129. The attribute's comment: “(2)”. References: EGA 0 (4.3.1), “Ψ(G) definition”; SGA 4 IV (13.2.2), “ringed space, comm O”; SGA 4 Vbis (1.3.6), “ringed spaces, φ^”.

Stacks 0095 (2). The pullback of a sheaf of O_Y-modules G along a morphism of ringed spaces (f, f^\sharp): f^*G = O_X ⊗_{f^{-1}O_Y} f^{-1}G, a sheaf of O_X-modules. The tensor product is Stacks.Sheafify.ModuleStalkTensor.tensorSheaf, i.e. the sheafification of the sectionwise tensor product presheaf U ↦ O_X(U) ⊗_{(f^{-1}O_Y)(U)} (f^{-1}G)(U); the f^{-1}O_Y-module f^{-1}G is invMod f OY G, the inverse image of Stacks 008X; and the ring map f^{-1}O_Y → O_X is sharpTranspose f OY OX sharp, the map corresponding to f^\sharp.

noncomputable def modulePullbackTensor : SheafOfModules.{u} (ringSheaf OX)

PullbackStalkTensor.ringedSpacePullbackTensor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/RingedSpace/ModulePullbackTensor.lean, line 151. The attribute's comment: “(2)”. References: EGA 0 (4.3.1), “Ψ(G) definition”; SGA 4 IV (13.2.2), “ringed space, comm O”; SGA 4 Vbis (1.3.6), “ringed spaces, φ^”.

Stacks 0095 (2) for a morphism of ringed spaces: the pullback g^*G = O_X ⊗_{g^{-1}O_Y} g^{-1}G of a sheaf of O_Y-modules G, with the ring map g^{-1}O_Y → O_X the one corresponding to the structure morphism g^\sharp = g.hom.c.

noncomputable def ringedSpacePullbackTensor (G : SheafOfModules.{u} (ringSheaf Y.sheaf)) :
    SheafOfModules.{u} (ringSheaf X.sheaf)

Tag 0096, a lemma

Tag 0096 in the Stacks Project.

RingedSpaceModuleAdjunction.modulePushforward, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Functors/Module/RingedSpace.lean, line 123. References: EGA 0 (4.2.1), “Ψ_ functor”; EGA 0 (12.2.1); SGA 4 Vbis (1.3.6), “ringed spaces, φ_”; SGA 3 VIIA (1.1), “more general”; SGA 4 IV (13.2.1), “special case”; SGA 4 V (5.0), “special case”.

Pushforward of sheaves of modules along a morphism of ringed spaces, f_* : Mod(𝒪_X) ⥤ Mod(𝒪_Y), given on sections by (f_* F)(V) = F(f⁻¹ V), with the 𝒪_Y-module structure restricted along f^♯.

noncomputable def modulePushforward :
    SheafOfModules.{u} (structureSheafRing X) ⥤ SheafOfModules.{u} (structureSheafRing Y)

RingedSpaceModuleAdjunction.modulePullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Functors/Module/RingedSpace.lean, line 161. References: EGA 0 (4.3.1); SGA 4 IV (13.2.2), “ringed space, comm O”; SGA 4 IV (13.2), “u^ for ringed spaces”; SGA 4 Vbis (1.3.6), “ringed spaces, φ^”; SGA 4 XVII (4.1), “ringed spaces”; SGA 3 III (0.1.4), “more general”; SGA 6 IV (2.6), “special case”; SGA 6 VI (2.3.1), “more general”.

Pullback of sheaves of modules along a morphism of ringed spaces, f^* : Mod(𝒪_Y) ⥤ Mod(𝒪_X): the left adjoint of f_*.

noncomputable def modulePullback {X Y : RingedSpace.{u, u}} (f : X ⟶ Y) :
    SheafOfModules.{u} (structureSheafRing Y) ⥤ SheafOfModules.{u} (structureSheafRing X)

RingedSpaceModuleAdjunction.modulePullbackPushforwardAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Functors/Module/RingedSpace.lean, line 177. References: EGA 0 (4.4.3), “partial”; EGA III (7.7.9), “more general”; SGA 4 IV (13.4), “a), ringed spaces”; SGA 4 Vbis (1.3.6), “ringed spaces”; SGA 3 I (4.6.4), “more general”; SGA 4 IV (14.2), “special case”; SGA 6 VI (2.3.1), “more general”.

The adjunction f^* ⊣ f_* between the categories of sheaves of modules on the ringed spaces Y and X.

noncomputable def modulePullbackPushforwardAdjunction {X Y : RingedSpace.{u, u}} (f : X ⟶ Y) :
    modulePullback f ⊣ modulePushforward f

RingedSpaceModuleAdjunction.homEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Functors/Module/RingedSpace.lean, line 198. References: EGA 0 (4.4.3), “partial”; EGA III (7.7.9), “more general”; SGA 4 IV (13.4), “a), ringed spaces”; SGA 4 Vbis (1.3.6), “ringed spaces”; SGA 3 I (4.6.4), “more general”; SGA 3 VIB (11.4), “(†)”; SGA 6 VI (2.3.1), “partial”.

The bijection of hom-sets Hom_{𝒪_X}(f^* G, F) ≃ Hom_{𝒪_Y}(G, f_* F) given by the adjunction f^* ⊣ f_*, natural in both F and G.

noncomputable def homEquiv {X Y : RingedSpace.{u, u}} (f : X ⟶ Y)
    (F : SheafOfModules.{u} (structureSheafRing X))
    (G : SheafOfModules.{u} (structureSheafRing Y)) :
    ((modulePullback f).obj G ⟶ F) ≃ (G ⟶ (modulePushforward f).obj F)

Tag 0097, a lemma

Tag 0097 in the Stacks Project.

pushforwardComp, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/RingedSpace/ModuleFunctors.lean, line 170. The attribute's comment: “(1)”. References: EGA 0 (4.2.6).

For composable morphisms of ringed spaces f : X ⟶ Y and g : Y ⟶ Z, there is a canonical natural isomorphism between the pushforward of the composite and the composite of the pushforwards.

noncomputable def pushforwardComp {X Y Z : RingedSpace.{u}}
    (f : X ⟶ Y) (g : Y ⟶ Z) :
    pushforward (f ≫ g) ≅ pushforward f ⋙ pushforward g

pullbackComp, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/RingedSpace/ModuleFunctors.lean, line 181. The attribute's comment: “(2)”. References: EGA 0 (4.3.6).

For composable morphisms of ringed spaces f : X ⟶ Y and g : Y ⟶ Z, there is a canonical natural isomorphism between the pullback of the composite and the composite of the pullbacks (in the reverse order).

noncomputable def pullbackComp {X Y Z : RingedSpace.{u}}
    (f : X ⟶ Y) (g : Y ⟶ Z) :
    pullback (f ≫ g) ≅ pullback g ⋙ pullback f

Tag 0098, a lemma

Tag 0098 in the Stacks Project.

Stacks.ModuleSkyscraper.pullbackStalkIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/PullbackStalkColimit.lean, line 469. The attribute's comment: “the stalk of Mathlib's Scheme.Modules.pullback at x, naturally in the module; the companion carrier PullbackStalkTensor.stalkPullbackTensorIso instead computes the stalk of the hand-built Tag 0095 (2) model over an arbitrary morphism of ringed spaces”.

Stacks 0098 for Mathlib's pullback of sheaves of modules on schemes. The stalk at x of the pullback along f is the base change of the stalk at f x along the stalk map of f:

(f^*N)_x = 𝒪_{X,x} ⊗_{𝒪_{Y,f x}} N_{f x},

naturally in N. Both sides are left adjoints — pullback f ⋙ stalk_x by Scheme.Modules.pullbackPushforwardAdjunction composed with modulesStalkSkyAdjunction, and stalk_{f x} ⋙ extendScalars by modulesStalkSkyAdjunction composed with ModuleCat.extendRestrictScalarsAdj — and pushSkyIso identifies their right adjoints, so CategoryTheory.conjugateIsoEquiv identifies them. No description of the sections of the pullback, and no colimit interchange, is used.

On the covering set. Tag 0098 is also carried by PullbackStalkTensor.stalkPullbackTensorIso (StacksFrontier/Topology/Sheaves/RingedSpace/ModulePullbackStalk.lean), and the two declarations state different things, which is what the covering-set rule requires of a shared tag. That one works over an arbitrary morphism of ringed spaces and computes the stalk of the hand-built model O_X ⊗_{f^{-1}O_Y} f^{-1}G of Tag 0095 (2), at a single object, as a linear equivalence; it does not know that model to be a pullback functor. This one works over a morphism of schemes, is about Mathlib's Scheme.Modules.pullback itself, and is natural in N. Neither subsumes the other: the first is more general in its spaces, the second in what it identifies.

noncomputable def pullbackStalkIso :
    modulesStalkFunctor Y (f x) ⋙ ModuleCat.extendScalars (f.stalkMap x).hom ≅
      Scheme.Modules.pullback f ⋙ modulesStalkFunctor X x

PullbackStalkTensor.stalkPullbackTensorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/RingedSpace/ModulePullbackStalk.lean, line 355. References: EGA 0 (4.3.1), “stalk formula”; EGA 0 (6.7.2), “special case”; EGA I (9.1.12), “case Y = S”.

For a morphism of ringed spaces (f, f^\sharp) and a sheaf of O_Y-modules G, the stalk of the pullback f^*G = O_X ⊗_{f^{-1}O_Y} f^{-1}G at x is G_{f(x)} ⊗_{O_{Y,f(x)}} O_{X,x}, where the tensor product uses f^\sharp_x : O_{Y,f(x)} → O_{X,x}.

noncomputable def stalkPullbackTensorIso :
    letI := (sharpStalk f OY OX alpha x).toAlgebra
    letI := rightTensorModule (ToType (TopCat.Presheaf.stalk (C := CommRingCat.{u}) OY.obj (f x)))
      (ToType (TopCat.Presheaf.stalk (C := CommRingCat.{u}) OX.obj x))
      (ToType (TopCat.Presheaf.stalk (C := Ab.{u}) (srcMod OY G).presheaf (f x)))
    TensorProduct (ToType (TopCat.Presheaf.stalk (C := CommRingCat.{u}) OY.obj (f x)))
        (ToType (TopCat.Presheaf.stalk (C := Ab.{u}) (srcMod OY G).presheaf (f x)))
        (ToType (TopCat.Presheaf.stalk (C := CommRingCat.{u}) OX.obj x))
      ≃ₗ[ToType (TopCat.Presheaf.stalk (C := CommRingCat.{u}) OX.obj x)]
      ToType (TopCat.Presheaf.stalk (C := Ab.{u})
        (tensorSheaf (invRing f OY) OX alpha (invMod f OY G)).val.presheaf x)

RingedSpaceModuleAdjunction.exists_modulePullbackStalkLinearEquiv, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/RingedSpace/ModulePullbackStalkAdjunction.lean, line 1164.

The stalk of the pullback is extension of scalars along the structure map on stalks, by a linear equivalence sending the germ of the adjunction-unit image of every section to the pure tensor of 1 with its original germ.

lemma exists_modulePullbackStalkLinearEquiv {X Y : RingedSpace.{u, u}} (f : X ⟶ Y)
    (G : SheafOfModules.{u} (structureSheafRing Y)) (x : X) :
    let G' : PresheafOfModules (Y.presheaf ⋙ forget₂ CommRingCat RingCat) := G.val
    let P' : PresheafOfModules (X.presheaf ⋙ forget₂ CommRingCat RingCat) :=
      ((modulePullback f).obj G).val
    letI : Algebra (Y.presheaf.stalk (f.hom.base x)) (X.presheaf.stalk x) :=
      (f.hom.stalkMap x).hom.toAlgebra
    ∃ e : ↑(TopCat.Presheaf.stalk P'.presheaf x) ≃ₗ[X.presheaf.stalk x]
        TensorProduct (Y.presheaf.stalk (f.hom.base x)) (X.presheaf.stalk x)
          ↑(TopCat.Presheaf.stalk G'.presheaf (f.hom.base x)),
      ∀ (V : Opens Y.carrier) (hx : f.hom.base x ∈ V) (s : G.val.obj (op V)),
        e (TopCat.Presheaf.germ P'.presheaf ((opensMap f).obj V) x hx
            (((modulePullbackPushforwardAdjunction f).unit.app G).val.app (op V) s)) =
          (1 : X.presheaf.stalk x) ⊗ₜ[Y.presheaf.stalk (f.hom.base x)]
            TopCat.Presheaf.germ G'.presheaf V (f.hom.base x) hx s

Sources

• Section 6.26, Tag 0094
• AxiomMath/Stacks at 5ed82d14

LeanRingedSpaceModuleAdjunction.modulePushforward · PullbackStalkTensor.modulePullbackTensor · PullbackStalkTensor.ringedSpacePullbackTensor · RingedSpaceModuleAdjunction.modulePullback · RingedSpaceModuleAdjunction.modulePullbackPushforwardAdjunction · RingedSpaceModuleAdjunction.homEquiv · pushforwardComp · pullbackComp

Section6.27 Skyscraper sheaves and stalks#

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

Tag 009A, a definition

Tag 009A in the Stacks Project.

SkyscraperSheaves.IsSkyscraperSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Skyscraper/Basic.lean, line 72. The attribute's comment: “(5), (6), (7)”.

Stacks 009A (5), (6), (7). A sheaf F on X is a skyscraper sheaf if there are a point x of X and an object A of the target category with F ≅ i_{x,*} A.

The target category is arbitrary, so this single predicate is the tag's clause (5) for sheaves of sets, its clause (6) for sheaves of abelian groups and its clause (7) for sheaves of algebraic structures. Clause (8), for sheaves of modules on a ringed space, is not covered here.

def IsSkyscraperSheaf (F : TopCat.Sheaf C X) : Prop

Stacks.Modules.skyscraper, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Skyscraper/Modules.lean, line 411. The attribute's comment: “(4)”.

Stacks 009A (4). The skyscraper sheaf of 𝒪_X-modules at the point z with value the 𝒪_{X,z}-module V: the pushforward of V along the inclusion of z, read as a morphism of ringed spaces ({z}, 𝒪_{X,z}) ⟶ (X, 𝒪_X).

noncomputable def skyscraper :
    SheafOfModules.{u} ((sheafCompose _ (forget₂ CommRingCat RingCat.{u})).obj R)

Declarations registered for the tag:

• skyscraperSheaf registered with add_to_stacks in StacksFrontier/Topology/Sheaves/Skyscraper/Basic.lean, line 41 (StacksFrontier): “The skyscraper sheaf at a point with a given value: the sheaf whose sections over U are the given object if x ∈ U and a terminal object otherwise. Mathlib's construction is uniform in the target category, so one declaration covers the tag's set, abelian-group and algebraic-structure cases; the ringed-space case, clause (4), is not covered.”.
• skyscraperPresheaf_eq_pushforward registered with add_to_stacks in StacksFrontier/Topology/Sheaves/Skyscraper/Basic.lean, line 50 (StacksFrontier): “The skyscraper is the pushforward along the map from the one-point space sending the point to x, which is how the tag defines i_{x,*} A.”.

Tag 009B, a lemma

Tag 009B in the Stacks Project.

Declarations registered for the tag:

• skyscraperSheaf registered with add_to_stacks in StacksFrontier/Topology/Sheaves/Skyscraper/Stalk.lean, line 28 (StacksFrontier): “the skyscraper sheaf i_{x,*}A”.
• skyscraperPresheafStalkOfSpecializes registered with add_to_stacks in StacksFrontier/Topology/Sheaves/Skyscraper/Stalk.lean, line 29 (StacksFrontier): “stalk at a point of the closure of {x}, i.e. a specialization of x: it is A”. References: EGA IV (21.9.1), “stalk on closure”.
• skyscraperPresheafStalkOfNotSpecializes registered with add_to_stacks in StacksFrontier/Topology/Sheaves/Skyscraper/Stalk.lean, line 33 (StacksFrontier): “stalk at a point outside the closure of {x}: it is terminal, a singleton for sheaves of sets”. References: EGA IV (21.9.1), “stalk off closure”.

Tag 009C, a lemma

Tag 009C in the Stacks Project.

Stacks.Modules.skyscraperHomEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Skyscraper/Modules.lean, line 443. The attribute's comment: “sheaves of modules”.

Stacks 009C for sheaves of modules. Morphisms of sheaves of 𝒪_X-modules from ℱ into the skyscraper at z with value V are the same thing as 𝒪_{X,z}-linear maps ℱ_z ⟶ V; this is the adjunction between the stalk functor and the skyscraper functor.

noncomputable def skyscraperHomEquiv
    (G : SheafOfModules.{u} ((sheafCompose _ (forget₂ CommRingCat RingCat.{u})).obj R)) :
    (G ⟶ skyscraper R z V) ≃
      (↑(TopCat.Presheaf.stalk G.val.presheaf z) →ₗ[↑(TopCat.Presheaf.stalk R.obj z)] ↑V)

Declarations registered for the tag:

• stalkSkyscraperSheafAdjunction registered with add_to_stacks in StacksFrontier/Topology/Sheaves/Skyscraper/Adjunction.lean, line 28 (StacksFrontier).
• skyscraperPresheafStalkAdjunction registered with add_to_stacks in StacksFrontier/Topology/Sheaves/Skyscraper/Adjunction.lean, line 30 (StacksFrontier).

Sources

• Section 6.27, Tag 0099
• AxiomMath/Stacks at 5ed82d14

LeanSkyscraperSheaves.IsSkyscraperSheaf · Stacks.Modules.skyscraper · skyscraperSheaf · skyscraperPresheaf_eq_pushforward · skyscraperPresheafStalkOfSpecializes · skyscraperPresheafStalkOfNotSpecializes · Stacks.Modules.skyscraperHomEquiv · stalkSkyscraperSheafAdjunction

Section6.29 Limits and colimits of sheaves#

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

Tag 009F, a lemma

Tag 009F in the Stacks Project.

DirectedColimitOfSheaves.canonicalMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Limits/FilteredColimitSections.lean, line 139.

The canonical map Ψ : colimᵢ ℱᵢ(U) ⟶ (colimᵢ ℱᵢ)(U), namely the component at U of the unit ℱ' ⟶ (ℱ')^# of sheafification.

noncomputable def canonicalMap (U : Opens X) :
    (colimitPresheaf F).obj (op U) ⟶ (colimitSheaf F).obj.obj (op U)

DirectedColimitOfSheaves.injective_canonicalMap_of_hasInjectiveTransitions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Limits/FilteredColimitSections.lean, line 417.

If all the transition maps are injective, then Ψ is injective for any open U.

theorem injective_canonicalMap_of_hasInjectiveTransitions
    (hInj : HasInjectiveTransitions F) (U : Opens X) :
    Function.Injective (canonicalMap F U)

DirectedColimitOfSheaves.injective_canonicalMap_of_isCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Limits/FilteredColimitSections.lean, line 438.

If U is quasi-compact, then Ψ is injective, with no hypothesis on the transition maps.

theorem injective_canonicalMap_of_isCompact (U : Opens X)
    (hU : IsCompact (U : Set X)) :
    Function.Injective (canonicalMap F U)

DirectedColimitOfSheaves.bijective_canonicalMap_of_isCompact_of_hasInjectiveTransitions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Limits/FilteredColimitSections.lean, line 452.

If U is quasi-compact and all the transition maps are injective, then Ψ is bijective.

theorem bijective_canonicalMap_of_isCompact_of_hasInjectiveTransitions
    (hInj : HasInjectiveTransitions F) (U : Opens X)
    (hU : IsCompact (U : Set X)) :
    Function.Bijective (canonicalMap F U)

DirectedColimitOfSheaves.bijective_canonicalMap_of_hasFiniteCompactCofinalCovers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Limits/FilteredColimitSections.lean, line 466. References: SGA 4 VI (1.23), “topological space case”.

If U has a cofinal system of finite open coverings whose pairwise intersections are quasi-compact, then Ψ is bijective, with no hypothesis on the transition maps.

theorem bijective_canonicalMap_of_hasFiniteCompactCofinalCovers (U : Opens X)
    (hU : HasFiniteCompactCofinalCovers (X := X) U) :
    Function.Bijective (canonicalMap F U)

Tag 009G, an example

Tag 009G in the Stacks Project.

DirectedColimitOfSheaves.exists_system_canonicalMap_not_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Limits/ColimitSectionsCounterexample.lean, line 162.

Stacks 009G. Some hypothesis is necessary in part (4) of 009F: there are a space X and a system of sheaves of sets ℱ : ℕ ⥤ TopCat.Sheaf (Type) X indexed by the directed set ℕ for which the canonical map Ψ : colimₙ ℱₙ(X) → (colimₙ ℱₙ)(X) is not bijective.

The witness is SectionsCounterexample.sheafSystem, the pushforwards jₙ,*𝐙 of the constant sheaf along the inclusions of the cofinal subsets {m : n ≤ m} of the discrete space ℕ. All its stalks die in the colimit while its global sections do not, so Ψ is not injective; and SectionsCounterexample.not_hasFiniteCompactCofinalCovers_top checks that the hypothesis of 009F (4) really fails here.

theorem exists_system_canonicalMap_not_bijective :
    ∃ (X : TopCat) (F : ℕ ⥤ TopCat.Sheaf (Type) X),
      ¬ Function.Bijective (canonicalMap F ⊤)

Tag 0A32, a lemma

Tag 0A32 in the Stacks Project.

SpectralDiagram.canonicalMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Limits/PullbackSections.lean, line 199. The attribute's comment: “the canonical map”.

The canonical map colim_{a : j → i} (f_a⁻¹𝒢)(f_a⁻¹ U) → (p_i⁻¹𝒢)(p_i⁻¹ U), induced by pulling sections back to the limit along the projections.

def canonicalMap [UnivLE.{max v v', max v u}] :
    colimit (D.sliceFunctor U 𝒢) ⟶ (D.sliceCocone U 𝒢).pt

SpectralDiagram.bijective_canonicalMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Limits/PullbackSections.lean, line 749. The attribute's comment: “bijectivity of the canonical map”.

For i an object of the cofiltered index category, 𝒢 a sheaf of sets on X_i and U ⊆ X_i a quasi-compact open, the canonical map colim_{a : j → i} (f_a⁻¹𝒢)(f_a⁻¹ U) → (p_i⁻¹𝒢)(p_i⁻¹ U) is bijective.

theorem bijective_canonicalMap [UnivLE.{max v v', max v u}] (hU : IsCompact (U : Set (D.F.obj i))) :
    Function.Bijective (D.canonicalMap U 𝒢)

Tag 0A33, a lemma

Tag 0A33 in the Stacks Project.

SpectralSheafSystem.stageColimitMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Limits/DescendOpens.lean, line 680. The attribute's comment: “the canonical map”.

The canonical map of Stacks 0A33, colim_{a : j → i} F_j(f_a⁻¹U) → F(p_i⁻¹U).

def stageColimitMap [UnivLE.{max v v', max v u}] : colimit (S.stageFunctor U) ⟶
    (S.colimitPullback).obj.obj (op (S.diagram.comapProj i U))

SpectralSheafSystem.bijective_stageColimitMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Limits/DescendOpens.lean, line 1012.

Stacks 0A33. Let J be a cofiltered index category, j ↦ X_j a diagram of spectral spaces with spectral transition maps, F_j a sheaf of sets on X_j for each j together with a compatible system of f_a-maps, and F = colim_j p_j⁻¹F_j on the limit X = lim_j X_j. Then for every i and every quasi-compact open U ⊆ X_i the canonical map colim_{a : j → i} F_j(f_a⁻¹U) → F(p_i⁻¹U) is bijective.

theorem bijective_stageColimitMap [UnivLE.{max v v', max v u}]
    (hU : IsCompact (U : Set (S.diagram.F.obj i))) :
    Function.Bijective (S.stageColimitMap U)

Sources

• Section 6.29, Tag 009E
• AxiomMath/Stacks at 5ed82d14

LeanDirectedColimitOfSheaves.canonicalMap · DirectedColimitOfSheaves.injective_canonicalMap_of_hasInjectiveTransitions · DirectedColimitOfSheaves.injective_canonicalMap_of_isCompact · DirectedColimitOfSheaves.bijective_canonicalMap_of_isCompact_of_hasInjectiveTransitions · DirectedColimitOfSheaves.bijective_canonicalMap_of_hasFiniteCompactCofinalCovers · DirectedColimitOfSheaves.exists_system_canonicalMap_not_bijective · SpectralDiagram.canonicalMap · SpectralDiagram.bijective_canonicalMap

Section6.30 Bases and sheaves#

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

Tag 009I, a definition

Tag 009I in the Stacks Project.

PresheafOnBasis, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Basis/Presheaf.lean, line 63. The attribute's comment: “(1)”. References: EGA 0 (3.2.1), “set-valued definition”.

A presheaf of sets on a basis B for the topology on X.

structure PresheafOnBasis (B : Set (Set X))

PresheafOnBasis.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Basis/Presheaf.lean, line 78. The attribute's comment: “(2)”. References: EGA 0 (3.2.3), “morphism definition”.

A morphism of presheaves of sets on a basis B.

structure PresheafOnBasis.Hom {B : Set (Set X)} (F G : PresheafOnBasis B)

Tag 009J, a definition

Tag 009J in the Stacks Project.

SheafOnBasis, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Basis/Sheaf.lean, line 113. The attribute's comment: “(1)”. References: EGA 0 (3.2.2).

A sheaf of sets on a basis B (Stacks 009J (1)): a presheaf on B satisfying the basis-sheaf condition.

structure SheafOnBasis {B : Set (Opens X)} (hB : Opens.IsBasis B)

SheafOnBasisHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Basis/Sheaf.lean, line 134. The attribute's comment: “(2)”. References: EGA 0 (3.2.3), “special case”.

A morphism of sheaves on a basis B (Stacks 009J (2)): by definition a morphism of the underlying presheaves on B.

def SheafOnBasisHom {B : Set (Opens X)} {hB : Opens.IsBasis B}
    (F G : SheafOnBasis hB) : Type _

Tag 009K, a lemma

Tag 009K in the Stacks Project.

main_theorem009K, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Basis/CofinalCoverings.lean, line 388.

Stacks Tag 009K (lemma-cofinal-systems-coverings). A presheaf on a basis is a sheaf iff the sheaf condition holds on a cofinal system of coverings.

theorem main_theorem009K
    {B : Set (Opens X)} (hB : Opens.IsBasis B)
    (C : CofinalSystem B)
    (all : GivenIntersectionCoverings B)
    (F : BasisPresheaf B) :
    IsSheafOnBasisProp F all ↔ SheafConditionOnCofinalSystem F C all

Tag 009L, a lemma

Tag 009L in the Stacks Project.

Stacks.SheafOnBasis.sheaf_iff_cofinal_sheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Basis/CofinalSheafCondition.lean, line 227.

Stacks 009L. Let B be a family of subsets closed under intersection of pairs of its members lying in a common member, and for each U ∈ B let C U be a cofinal system of coverings of U by members of B. Then a presheaf of sets on B is a sheaf on B if and only if gluing holds for the coverings in C U with compatibility tested on the intersections Uᵢ ∩ Uⱼ.

theorem sheaf_iff_cofinal_sheaf {B : Set (Set X)} (hB_inter : ClosedUnderInter B)
    (C : ∀ U ∈ B, Set (Covering.{u, v} B U)) (hC : IsCofinalSystem B C) (F : Presheaf.{u, w} B) :
    Presheaf.IsSheaf.{u, v, w} F ↔ F.IsSheafOnCofinal hB_inter C

Tag 009M, a lemma

Tag 009M in the Stacks Project.

Stacks.Topology.BasisPresheaf.germMap_bijection, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Basis/Germs.lean, line 339.

Stacks Project 009M (bijection form). The germ map Φ_U induces a bijection between F.obj U hU and the set of (*)-families of germs over U.

theorem germMap_bijection {B : Set (Set X)} (hB : IsTopologicalBasis B)
    (F : PresheafOnBasisOpenSet B) (hF : F.IsSheaf) {U : Set X} (hU : U ∈ B) :
    Function.Bijective
      (fun s : F.obj U hU =>
        (⟨germMap F hU s, by
          rw [← germMap_range_eq_conditionStar hB F hF hU]; exact ⟨s, rfl⟩⟩ :
          {f : ∀ x : U, Stalk F x.1 // ConditionStar F f}))

Tag 009N, a lemma

Tag 009N in the Stacks Project.

Stacks.BasisExtension.sheaf_extension_exists, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Basis/SetExtension.lean, line 332.

Stacks 009N. Existence. Given a sheaf F of sets on a basis B, there exists a sheaf Fext of sets on X together with bijections Fext(U) ≃ F(U) for U ∈ B, compatible with the restriction maps.

Uniqueness of the extension is sheaf_extension_unique.

theorem sheaf_extension_exists {B : Set (Opens X)} (hB : Opens.IsBasis B)
    (F : BasisPresheaf B) (hF : F.IsSheaf) :
    ∃ (Fext : OpensPresheaf X) (_ : Fext.IsSheaf),
      Nonempty (BasisPresheaf.Iso (Fext.restrictToBasis B) F)

Stacks.BasisExtension.sheaf_extension_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Basis/SetExtension.lean, line 567.

Stacks 009N. Uniqueness. Any two sheaves on X extending the same sheaf F on the basis B are isomorphic by a unique isomorphism intertwining the comparison bijections.

Existence of an extension is sheaf_extension_exists.

theorem sheaf_extension_unique {B : Set (Opens X)} (hB : Opens.IsBasis B)
    (F : BasisPresheaf B)
    (Fext : OpensPresheaf X) (hFext : Fext.IsSheaf)
    (ι : BasisPresheaf.Iso (Fext.restrictToBasis B) F)
    (G : OpensPresheaf X) (hG : G.IsSheaf)
    (ι' : BasisPresheaf.Iso (G.restrictToBasis B) F) :
    ∃! Φ : OpensPresheaf.Iso Fext G,
      ∀ (U : B) (s : Fext.obj (U : Opens X)),
        ι'.toEquiv U (Φ.toEquiv (U : Opens X) s) = ι.toEquiv U s

Tag 009O, a lemma

Tag 009O in the Stacks Project.

Stacks.OpensBasis.restrictFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Basis/OnBasis.lean, line 257.

Stacks 009O. The restriction-to-basis functor r : Sh(X) ⥤ Sh(B), sending a sheaf on X to its restriction to the basis elements.

noncomputable def restrictFunctor (hB : Opens.IsBasis B) : TopCat.Sheaf (Type u) X ⥤ SheafOnBasis B

Stacks.OpensBasis.restrictFunctor_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Basis/OnBasis.lean, line 687.

Stacks 009O. Let X be a topological space and let B be a basis for the topology on X. The restriction-to-basis functor r : Sh(X) ⥤ Sh(B) is an equivalence of categories.

theorem restrictFunctor_isEquivalence (hB : Opens.IsBasis B) :
    (restrictFunctor (X := X) B hB).IsEquivalence

Tag 009P, a definition

Tag 009P in the Stacks Project.

SheafOnBasis.PresheafOnBasis, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Basis/ValuedInCategory.lean, line 84. The attribute's comment: “(1)”. References: EGA 0 (3.2.1), “definition”.

A presheaf with values in C on the basis B (Stacks 009P (1)): a functor on the members of B ordered by reverse inclusion.

abbrev PresheafOnBasis (B : Basis X) (C : Type u) [Category.{v} C] :
    Type max v u

SheafOnBasis.MorphismOnBasis, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Basis/ValuedInCategory.lean, line 91. The attribute's comment: “(2)”. References: EGA 0 (3.2.3), “morphism definition”; SGA 3 I (2.1.1), “morphism of Ĉ-groups”.

A morphism of presheaves with values in C on the basis B (Stacks 009P (2)): a natural transformation.

abbrev MorphismOnBasis {B : Basis X} {C : Type u} [Category.{v} C]
    (F G : PresheafOnBasis B C) : Type _

SheafOnBasis.underlyingPresheafOnBasis, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Basis/ValuedInCategory.lean, line 97. The attribute's comment: “(3)”. References: SGA 4 II (6.3.0), “object assignment of ε^”.

The underlying set-valued presheaf on the basis B of a presheaf with values in C (Stacks 009P (3)), obtained by post-composing with a forgetful functor F₀ : C ⥤ Type v.

def underlyingPresheafOnBasis {B : Basis X} {C : Type u} [Category.{v} C]
    (F₀ : C ⥤ Type v) (F : PresheafOnBasis B C) : PresheafOnBasis B (Type v)

SheafOnBasis.SheafOnBasisStruct, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Basis/ValuedInCategory.lean, line 130. The attribute's comment: “(4)”.

A sheaf with values in C on the basis B (Stacks 009P (4)): a presheaf with values in C on B together with the sheaf condition on its underlying sets.

structure SheafOnBasisStruct (B : Basis X) (C : Type u) [Category.{v} C]
    (F₀ : C ⥤ Type v)

Tag 009Q, a lemma

Tag 009Q in the Stacks Project.

Stacks.BasisExtension.extension_of_sheaf_on_basis, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Basis/Extension.lean, line 728. References: EGA 0 (3.2.5), “1st para: F ≅ F₁'”.

Extension of a sheaf on a basis (Stacks 009Q / Lemma 6.30.9).

Let (C, F) be a type of algebraic structure, B a basis for X, and F a sheaf with values in C on B. Then there is a sheaf Fᵉˣᵗ with values in C on X, unique up to unique isomorphism, whose restriction to B is isomorphic to F.

• Existence: there is a sheaf Fext on X together with an isomorphism θ : Fext|_B ≅ F.presheaf.
• Uniqueness: any sheaf G on X equipped with an isomorphism η : G|_B ≅ F.presheaf admits a unique isomorphism Φ : G ≅ Fext compatible with the identifications over B, i.e. (restrictIso Φ) ≪≫ θ = η.

theorem extension_of_sheaf_on_basis
    (A : AlgebraicStructureType.{u, w}) (hB : Opens.IsBasis B)
    (F : CSheafOnBasis A hB) :
    ∃ (Fext : CSheaf A X)
      (θ : restrictToBasis A B Fext.presheaf ≅ F.presheaf),
      ∀ (G : CSheaf A X) (η : restrictToBasis A B G.presheaf ≅ F.presheaf),
        ∃! Φ : G.presheaf ≅ Fext.presheaf,
          restrictIso A B Φ ≪≫ θ = η

Tag 009R, a lemma

Tag 009R in the Stacks Project.

restrictBasisEquivalenceStructures, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Basis/Equivalence.lean, line 64. References: SGA 4 III (4.1), “special case”; SGA 4 V (8.1.12), “special case”.

Let X be a topological space, let B : ι → Opens X be a family of opens whose inclusion into Opens X is cover-dense, and let C be a category with enough limits. Then restriction along the inclusion of B into Opens X is an equivalence from sheaves on X with values in C to sheaves with values in C on the site B with the topology induced from Opens.grothendieckTopology X.

noncomputable def restrictBasisEquivalenceStructures
    {X : TopCat.{w}} {ι : Type w} (B : ι → Opens X)
    [(inducedFunctor B).IsCoverDense (Opens.grothendieckTopology X)]
    (C : Type v) [Category.{u} C]
    [∀ Y, Limits.HasLimitsOfShape
        (CategoryTheory.StructuredArrow Y (inducedFunctor B).op) C] :
    Sheaf (Opens.grothendieckTopology X) C ≌
      Sheaf ((inducedFunctor B).inducedTopology
              (Opens.grothendieckTopology X)) C

Tag 009S, a definition

Tag 009S in the Stacks Project.

PresheafOfModulesOnBasis, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Basis/Module.lean, line 115. The attribute's comment: “(1)”. References: SGA 3 I (3.1), “special case”.

A presheaf of O-modules on a basis B (Stacks 009S).

Given a presheaf of rings O on B, a presheaf of O-modules on B is a presheaf F of abelian groups on B together with an O(U)-module structure on F(U) for each U ∈ B, compatible with restriction in the sense that res(r • m) = (res r) • (res m).

structure PresheafOfModulesOnBasis {B : Set (Set X)}
    (O : PresheafOfRingsOnBasis.{u, w₁} B)

PresheafOfModulesOnBasis.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Basis/Module.lean, line 154. The attribute's comment: “(2)”.

A morphism of presheaves of O-modules on B.

A morphism φ : F → G is a family of O(U)-module homomorphisms φ(U) : F(U) → G(U) commuting with restriction.

structure PresheafOfModulesOnBasis.Hom {B : Set (Set X)}
    {O : PresheafOfRingsOnBasis.{u, w₁} B}
    (F G : PresheafOfModulesOnBasis.{u, w₁, w₂} O)

SheafOfModulesOnBasis, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Basis/Module.lean, line 205. The attribute's comment: “(3)”. References: EGA 0 (3.2.2).

A sheaf of O-modules on a basis B (Stacks 009S, part 3).

A sheaf of O-modules on B is a presheaf of O-modules on B whose underlying presheaf of abelian groups satisfies the sheaf condition.

structure SheafOfModulesOnBasis {B : Set (Set X)}
    (O : PresheafOfRingsOnBasis.{u, w₁} B)

Tag 009T, a lemma

Tag 009T in the Stacks Project.

BasesSheaves.exists_moduleStructure_on_extension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Basis/ModuleExtension.lean, line 87. The attribute's comment: “the canonical module structure, agreeing with the given one over elements of B”. References: EGA 0 (3.2.5), “special case”.

Stacks 009T (Lemma 6.30.11), the module structure on the extension.

Let X be a topological space, B a basis for its topology, 𝒪 a sheaf of rings on X (playing the role of O^ext, the extension of a sheaf of rings O on B), and N a sheaf of 𝒪|_B-modules on B (the sheaf F).

Then there is a sheaf of 𝒪-modules M on X — its scalar action 𝒪 × M → M being the asserted map O^ext × F^ext → F^ext — together with an isomorphism basis_iso : M|_B ≅ N of sheaves of 𝒪|_B-modules, i.e. the module structure agrees with the given one over elements of B. The map is canonical: for any other sheaf of 𝒪-modules M' with an identification M'|_B ≅ N there is a unique isomorphism M ≅ M' inducing it.

That the underlying abelian sheaf of M is F^ext is restrictToSheaf_iso.

theorem exists_moduleStructure_on_extension {B : Set (Opens X)} (hB : Opens.IsBasis B)
    (𝒪 : TopCat.Sheaf RingCat X) (N : ModuleSheafOnBasis hB 𝒪) :
    ∃ (M : SheafOfModules.{u} 𝒪) (basis_iso : (restrictModuleSheaf hB 𝒪).obj M ≅ N),
      ∀ (M' : SheafOfModules.{u} 𝒪) (θ : (restrictModuleSheaf hB 𝒪).obj M' ≅ N),
        ∃! Φ : M ≅ M', (restrictModuleSheaf hB 𝒪).mapIso Φ ≪≫ θ = basis_iso

BasesSheaves.restrictToSheaf_iso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Basis/ModuleExtension.lean, line 115. The attribute's comment: “the module structure is carried by the abelian extension F^ext of F”.

Stacks 009T (Lemma 6.30.11), the module structure lives on F^ext.

An isomorphism M|_B ≅ N of sheaves of 𝒪|_B-modules induces an isomorphism of the underlying abelian sheaves on B. Hence the module structure produced by exists_moduleStructure_on_extension is carried by an abelian sheaf on X whose restriction to B is the underlying abelian sheaf of N — that is, by an extension of F off B, which by the uniqueness in Stacks 009Q is F^ext.

noncomputable def restrictToSheaf_iso {B : Set (Opens X)} (hB : Opens.IsBasis B)
    (𝒪 : TopCat.Sheaf RingCat X) (M : SheafOfModules.{u} 𝒪) (N : ModuleSheafOnBasis hB 𝒪)
    (basis_iso : (restrictModuleSheaf hB 𝒪).obj M ≅ N) :
    ((basisInclusion B).sheafPushforwardContinuous AddCommGrpCat
          (basisGrothendieckTopology hB) (Opens.grothendieckTopology X)).obj
        ((SheafOfModules.toSheaf 𝒪).obj M) ≅
      (SheafOfModules.toSheaf _).obj N

Tag 009U, a lemma

Tag 009U in the Stacks Project.

Stacks.BasisRestriction.restrictModuleSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Basis/ModuleRestriction.lean, line 124.

The restriction-to-B functor on sheaves of 𝒪-modules.

This is defined as the pushforward along the inclusion B ↪ Opens X, applied to sheaves of modules. The ring-level pushforward sends 𝒪 to its restriction 𝒪|_B, so the module-level pushforward goes from SheafOfModules 𝒪 to SheafOfModules (𝒪|_B).

noncomputable def restrictModuleSheaf {B : Set (Opens X)} (hB : Opens.IsBasis B)
    (𝒪 : TopCat.Sheaf RingCat X) :
    SheafOfModules.{max u w} 𝒪 ⥤ ModuleSheafOnBasis hB 𝒪

Stacks.BasisRestriction.isEquivalence_restrictModuleSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Basis/ModuleRestriction.lean, line 583.

Stacks 009U. The restriction-to-B functor

r : SheafOfModules 𝒪 ⥤ SheafOfModules (𝒪|_B), F ↦ F|_B,

is an equivalence of categories, where 𝒪|_B is the restriction of the sheaf of rings 𝒪 to the basis category B.

theorem isEquivalence_restrictModuleSheaf {B : Set (Opens X)} (hB : Opens.IsBasis B)
    (𝒪 : TopCat.Sheaf RingCat X) :
    (restrictModuleSheaf (X := X) hB 𝒪 : SheafOfModules.{max u w} 𝒪 ⥤ _).IsEquivalence

Tag 009V, a lemma

Tag 009V in the Stacks Project.

fMap_basis_unique_extension, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Basis/FMapUniqueness.lean, line 77. References: EGA 0 (3.2.5), “second paragraph”; EGA 0 (3.5.1), “special case”.

Stacks 009V. Let B : ι → Opens Y be a family of opens whose range is a basis of Y. Then every compatible family of basis-level morphisms φ i : G(B i) ⟶ (f_* F)(B i) extends to a unique f-map ψ : G ⟶ f_* F, i.e. a unique sheaf morphism whose component at each B i is φ i.

theorem fMap_basis_unique_extension
    {C : Type u} [Category.{v} C]
    {FC : C → C → Type _} {CC : C → Type v}
    [∀ (X Y : C), FunLike (FC X Y) (CC X) (CC Y)]
    [ConcreteCategory C FC]
    [HasLimits C] [HasColimits C]
    [PreservesLimits (forget C)] [PreservesFilteredColimits (forget C)]
    [(forget C).ReflectsIsomorphisms]
    {X Y : TopCat} (f : X ⟶ Y)
    (F : TopCat.Sheaf C X) (G : TopCat.Sheaf C Y)
    {ι : Type w} (B : ι → Opens Y) (hB : Opens.IsBasis (Set.range B))
    (φ : BasisCompatibleFamily f G F B) :
    ∃! ψ : FMapParameterizedC f G F, ∀ i : ι, ψ.hom.app (op (B i)) = φ.app (op i)

Tag 009W, a lemma

Tag 009W in the Stacks Project.

AlgebraicGeometry.RingedSpace.existsUnique_fMap_of_basis, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Basis/ModuleFMap.lean, line 507. References: EGA 0 (3.2.5), “special case”.

Unique \(f\)-map extension from basis-compatible module maps.

Let \((f, f^\sharp) : (X, \mathcal{O}_X) \to (Y, \mathcal{O}_Y)\) be a morphism of ringed spaces. Let \(\mathcal{F}\) be a sheaf of \(\mathcal{O}_X\)-modules, \(\mathcal{G}\) a sheaf of \(\mathcal{O}_Y\)-modules, and \(\mathcal{B}\) a basis for the topology on \(Y\). For every basis-indexed compatible system of \(\mathcal{O}_Y(V)\)-module homomorphisms \(\varphi_V : \mathcal{G}(V) \to \mathcal{F}(f^{-1}V)\) for \(V \in \mathcal{B}\), there exists a unique \(f\)-map \(\varphi : \mathcal{G} \to \mathcal{F}\) whose basis-restricted family equals \(\{\varphi_V\}_{V \in \mathcal{B}}\).

theorem existsUnique_fMap_of_basis {X Y : RingedSpace.{u, u}} (f : X ⟶ Y)
    (G : ModuleSheaf Y) (F : ModuleSheaf X)
    (B : Set (Opens Y.carrier))
    (hB : Opens.IsBasis B)
    (φ : FMapOnBasis f G F B) :
    ∃! (Φ : FMapModuleSheaf f G F), Φ.restrictToBasis B = φ

Tag 009X, a lemma

Tag 009X in the Stacks Project.

main_theorem009X, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Basis/FMapExtension.lean, line 378. References: EGA 0 (3.2.5), “second paragraph”; EGA 0 (3.5.1), “special case”.

Stacks tag 009X (main theorem). Given a compatible basis family, there is a unique f-map extending it.

theorem main_theorem009X (C : Type u) [Category.{v} C]
    {FC : C → C → Type*} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
    [ConcreteCategory.{w} C FC]
    [HasLimits C]
    [PreservesLimits (CategoryTheory.forget C)]
    [(CategoryTheory.forget C).ReflectsIsomorphisms]
    {X Y : TopCat.{w}} (f : X ⟶ Y)
    (F : TopCat.Sheaf C X) (G : TopCat.Sheaf C Y)
    (BX : Set (Opens X)) (BY : Set (Opens Y))
    (hBX : Opens.IsBasis BX) (hBY : Opens.IsBasis BY)
    (Φ : CompatibleBasisFamily C f F G BX BY) :
    ∃! (φ : FMapValPresheaf C f F G),
      ∀ (V : Opens Y) (hV : V ∈ BY) (U : Opens X) (hU : U ∈ BX)
        (hfU : U ≤ (Opens.comap f.hom) V),
        Φ.φ V hV U hU hfU = φ.app (op V) ≫ F.obj.map (homOfLE hfU).op

Tag 009Y, a lemma

Tag 009Y in the Stacks Project.

Stacks.RingedSpace.existsUnique_fMap_of_bases, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Basis/ModuleFMapOfBasisData.lean, line 563. References: EGA 0 (4.4.1), “basis data suffices”.

Stacks 009Y. Let f : X ⟶ Y be a morphism of ringed spaces, F a sheaf of 𝒪_X-modules, G a sheaf of 𝒪_Y-modules, and BX, BY bases of the topologies of X and Y. Then a compatible system φ of maps G(V) → F(U), indexed by the pairs of basis opens with U ≤ f⁻¹ V, extends to a unique f-map ψ : G → F, and each φ_V^U is recovered from ψ as the composite G(V) → F(f⁻¹ V) → F(U).

theorem existsUnique_fMap_of_bases
    {X Y : RingedSpace.{v, u}} (f : X ⟶ Y)
    (F : SheafOfModulesOnRingedSpace X) (G : SheafOfModulesOnRingedSpace Y)
    (BY : Set (Opens Y.carrier)) (BX : Set (Opens X.carrier))
    (hBY : Opens.IsBasis BY) (hBX : Opens.IsBasis BX)
    (φ : BasisCompat f F G BX BY) :
    ∃! ψ : FMapAddGroupHom f F G,
      ∀ {V : Opens Y.carrier} (hV : V ∈ BY)
        {U : Opens X.carrier} (hU : U ∈ BX) (hUV : U ≤ (Opens.map f.hom.base).obj V)
        (g : G.sections V),
        φ.basisApp hV hU hUV g = F.restrict hUV (ψ.app V g)

Sources

• Section 6.30, Tag 009H
• AxiomMath/Stacks at 5ed82d14

LeanPresheafOnBasis · PresheafOnBasis.Hom · SheafOnBasis · SheafOnBasisHom · main_theorem009K · Stacks.SheafOnBasis.sheaf_iff_cofinal_sheaf · Stacks.Topology.BasisPresheaf.germMap_bijection · Stacks.BasisExtension.sheaf_extension_exists

Section6.31 Open immersions and (pre)sheaves#

Section 6.31 of the Stacks Project, Tag 009Z. 13 tags here are carried by 47 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00A0, a lemma

Tag 00A0 in the Stacks Project.

OpenImmersionSheaves.presheaf_pullback_iso_restriction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/OpenImmersion/Basic.lean, line 82. The attribute's comment: “(1)”.

Stacks 00A0 (1). For a presheaf of sets G on X, the presheaf pullback j_p G (the colimit-based left adjoint of j_*) is canonically isomorphic to the naive restriction V ↦ G(j V): (j_p G) ≅ restrictPresheaf hj G. Componentwise, for every open V ⊆ U, the canonical colimit map G(j V) → (j_p G)(V) is a bijection (the colimit defining (j_p G)(V) collapses to its value at the largest neighbourhood j V = V). The isomorphism is exhibited as honest data: it is Mathlib's canonical IsOpenMap.pullbackObjIso, whose V-component is the canonical comparison pullbackObjObjOfImageOpen.

noncomputable def presheaf_pullback_iso_restriction (G : X.Presheaf (Type u)) :
    (Presheaf.pullback (Type u) j).obj G ≅ restrictPresheaf j hj G

OpenImmersionSheaves.sheaf_pullback_iso_restriction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/OpenImmersion/Basic.lean, line 107. The attribute's comment: “(2)”. References: EGA 0 (3.7.1), “special case”; SGA 4 III (2.7), “Φ^* ≅ (i^{-1})^s”; SGA 4 III (5.3), “Clause 2, special case”.

Stacks 00A0 (2). For a sheaf of sets G on X, the sheaf pullback j⁻¹ G (sheafification of j_p G) is canonically isomorphic, as a sheaf on U, to the restriction sheaf restrictSheaf hj G (no sheafification is needed, by the sheaf condition built into restrictSheaf). The isomorphism lives in the category U.Sheaf (Type u). It is exhibited as honest data: the G-component of Mathlib's canonical natural isomorphism Topology.IsOpenEmbedding.sheafPullbackIso (note (hj.sheafPullback _).obj G = restrictSheaf hj G by definition).

noncomputable def sheaf_pullback_iso_restriction (G : X.Sheaf (Type u)) :
    (Sheaf.pullback (Type u) j).obj G ≅ restrictSheaf j hj G

OpenImmersionSheaves.stalk_sheaf_pullback_iso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/OpenImmersion/Basic.lean, line 122. The attribute's comment: “(3)”.

Stacks 00A0 (3). For a sheaf of sets G on X and a point u ∈ U, the stalk of the sheaf pullback j⁻¹ G at u is canonically isomorphic to the stalk of G at j u: (j⁻¹ G)_u ≅ G_{j u}. This is the special case f = j of the canonical stalk identity (f⁻¹ G)_x ≅ G_{f x}. It is exhibited as honest data, built from the canonical comparison maps: the underlying presheaf of j⁻¹ G is canonically isomorphic to the presheaf pullback j_p (G^♭) (via clause (2) and IsOpenMap.pullbackObjIso), and Presheaf.stalkPullbackIso identifies the stalk of the presheaf pullback at u with the stalk of G at j u.

noncomputable def stalk_sheaf_pullback_iso (G : X.Sheaf (Type u)) (u : U) :
    Presheaf.stalk ((Sheaf.pullback (Type u) j).obj G).obj u
      ≅ Presheaf.stalk G.obj ((ConcreteCategory.hom j) u)

OpenImmersionSheaves.presheaf_pullback_pushforward_counit_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/OpenImmersion/Basic.lean, line 245. The attribute's comment: “(4)”. References: SGA 4 IV (9.2.4), “a), special case”.

Stacks 00A0 (4). On the category PSh(U) of presheaves of sets on U, the canonical natural transformation j_p ∘ j_* ⟶ id — namely the counit of the adjunction j_p ⊣ j_* (pullback ⊣ pushforward) — is a natural isomorphism. Equivalently, for every presheaf of sets F on U and every open V ⊆ U, the canonical map (j_p j_* F)(V) → F(V) is a bijection, naturally in F. This exhibits the canonical natural isomorphism j_p ∘ j_* ≅ id_{PSh(U)}. The open-embedding hypothesis hj is required: for an arbitrary continuous j this counit need not be an isomorphism.

Proof: A counit of an adjunction L ⊣ R is an isomorphism whenever the right adjoint R is fully faithful (Adjunction.counit_isIso_of_R_fully_faithful). Here R = j_* = Presheaf.pushforward (Type u) j, which is fully faithful for the open embedding j by presheafPushforwardFullyFaithful.

theorem presheaf_pullback_pushforward_counit_isIso
    (j : U ⟶ X) (hj : Topology.IsOpenEmbedding (ConcreteCategory.hom j)) :
    IsIso (Presheaf.pullbackPushforwardAdjunction (Type u) j).counit

OpenImmersionSheaves.sheaf_pullback_pushforward_counit_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/OpenImmersion/Basic.lean, line 268. The attribute's comment: “(5)”. References: EGA I (9.4.2), “(i)”; SGA 4 IV (9.2.4), “a), special case”.

Stacks 00A0 (5). On the category Sh(U) of sheaves of sets on U, the canonical natural transformation j⁻¹ ∘ j_* ⟶ id — namely the counit of the adjunction j⁻¹ ⊣ j_* (Sheaf.pullback ⊣ Sheaf.pushforward) — is a natural isomorphism. Equivalently, for every sheaf of sets F on U and every open V ⊆ U, the canonical map (j⁻¹ j_* F)(V) → F(V) is a bijection, naturally in F. This exhibits the canonical natural isomorphism j⁻¹ ∘ j_* ≅ id_{Sh(U)}. The open-embedding hypothesis hj is required: for an arbitrary continuous j this counit need not be an isomorphism.

Proof: As for clause (4), the counit of Sheaf.pullback ⊣ Sheaf.pushforward is an isomorphism because its right adjoint j_* = Sheaf.pushforward (Type u) j is fully faithful for the open embedding j (sheafPushforwardFullyFaithful), via Adjunction.counit_isIso_of_R_fully_faithful.

theorem sheaf_pullback_pushforward_counit_isIso
    (j : U ⟶ X) (hj : Topology.IsOpenEmbedding (ConcreteCategory.hom j)) :
    IsIso (Sheaf.pullbackPushforwardAdjunction (Type u) j).counit

Tag 00A1, a definition

Tag 00A1 in the Stacks Project.

restrictPresheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/OpenImmersion/Restriction.lean, line 66. The attribute's comment: “(1)”. References: EGA 0 (3.1.5); SGA 3 I (2.1.1), “restriction G ↦ G_S”; SGA 3 IV (4.3.17), “special case”.

Restriction of a presheaf to an open subset: precomposition with the opposite of the open-embedding functor on opens.

def restrictPresheaf
    {C : Type*} [Category C] {X : TopCat}
    (G : TopCat.Presheaf C X) (U : Opens X) :
    TopCat.Presheaf C ((Opens.toTopCat X).obj U)

local_restrictSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/OpenImmersion/Restriction.lean, line 89. The attribute's comment: “(2)”. References: EGA 0 (3.1.5); EGA 0 (3.7.1), “special case”; SGA 4 III (1.9.2); SGA 4 III (5.3), “special case”.

Restriction of a sheaf to an open subset, via the open-embedding sheaf pullback.

noncomputable def local_restrictSheaf
    {A : Type*} [Category A] {X : TopCat}
    (G : TopCat.Sheaf A X) (U : Opens X) :
    TopCat.Sheaf A ((Opens.toTopCat X).obj U)

openSubspace, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/OpenImmersion/Restriction.lean, line 110. The attribute's comment: “(3)”. References: EGA 0 (4.1.2), “special case”; SGA 2 I (1.7), “special case”; SGA 4 IV (14.1), “special case”.

Open subspace of a ringed space (X, 𝒪) associated to an open U ⊆ X.

noncomputable def openSubspace
    (X : SheafedSpace CommRingCat) (U : Opens X) :
    SheafedSpace CommRingCat

restrictPresheafOfModules, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/OpenImmersion/Restriction.lean, line 128. The attribute's comment: “(4)”. References: SGA 3 I (3.1.4), “F ↦ F_U for C = Opens(X)”; SGA 4 IV (11.2.2), “special case”; SGA 4 Vbis (1.3.7), “special case”.

Restriction of a presheaf of 𝒪-modules to an open subset, via PresheafOfModules.pushforward along the open-embedding functor.

noncomputable def restrictPresheafOfModules
    {X : TopCat} (𝒪 : (Opens X)ᵒᵖ ⥤ RingCat) (U : Opens X) :
    PresheafOfModules 𝒪 ⥤ PresheafOfModules (restrictPresheaf 𝒪 U)

Tag 00A2, a definition

Tag 00A2 in the Stacks Project.

TopCat.Presheaf.extendByInitial, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/OpenImmersion/ExtensionByInitial.lean, line 142. The attribute's comment: “(1)”.

Extension by an initial object. For j : U → X the inclusion of an open subset, C a category with initial object e, and F a presheaf on U with values in C, this is the presheaf j_{p!}F on X with j_{p!}F(V) = F(V) for V ⊆ U and j_{p!}F(V) = e otherwise, with the obvious restriction maps.

When C is a category of algebraic structures its zero object is initial, so this is the classical extension by zero of an abelian presheaf; and the initial object of Type is the empty type, so this is also the extension by the empty set of a presheaf of sets.

noncomputable def extendByInitial (F : Presheaf C (sp U)) : Presheaf C X

TopCat.Presheaf.extendByInitialFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/OpenImmersion/ExtensionByInitial.lean, line 237. The attribute's comment: “(1)”.

Extension by an initial object, as a functor. j_{p!} : PSh(U) ⥤ PSh(X).

noncomputable def extendByInitialFunctor : Presheaf C (sp U) ⥤ Presheaf C X

TopCat.Presheaf.extendByInitialSheafify, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/OpenImmersion/ExtensionByInitial.lean, line 479. The attribute's comment: “(2)”. References: SGA 4 III (1.9.2), “more general”.

Extension by an initial object for sheaves. The extension j_! F of a sheaf F on U is the sheafification of the presheaf j_{p!}F.

For a category of algebraic structures the initial object is the zero object, so this is the classical extension by zero of a sheaf; for C = Type the initial object is the empty type, so this is the extension by the empty set.

noncomputable def extendByInitialSheafify :
    Presheaf C (sp U) ⥤ TopCat.Sheaf C X

TopCat.Presheaf.extendByInitialSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/OpenImmersion/ExtensionByInitial.lean, line 486. The attribute's comment: “(2)”. References: SGA 4 III (5.3), “opens of a top. space”.

Extension by an initial object, as a functor on sheaves. j_! : Sh(U) ⥤ Sh(X) sends a sheaf F on U to the sheafification of j_{p!}F.

noncomputable def extendByInitialSheaf : TopCat.Sheaf C (sp U) ⥤ TopCat.Sheaf C X

Tag 00A3, a lemma

Tag 00A3 in the Stacks Project.

TopCat.Presheaf.extendByInitialAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/OpenImmersion/ExtensionByInitial.lean, line 374. The attribute's comment: “(1) j_{p!} is a left adjoint to the restriction functor j_p”. References: SGA 4 IV (11.3.1), “presheaf, constant ring”.

The extension-by-zero/restriction adjunction, presheaf level. For j : U → X the inclusion of an open subset, j_{p!} is a left adjoint of the restriction functor j_p.

noncomputable def extendByInitialAdjunction :
    extendByInitialFunctor (C := C) U ⊣ restrictToOpen U

TopCat.Presheaf.restrictExtendByInitialIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/OpenImmersion/ExtensionByInitial.lean, line 398. The attribute's comment: “(4) on presheaves on U we have j_p j_{p!} = id”.

j_p j_{p!} = id. The extension by an initial object of a presheaf on U restricts back to that presheaf, naturally in the presheaf.

noncomputable def restrictExtendByInitialIso :
    extendByInitialFunctor (C := C) U ⋙ restrictToOpen U ≅ 𝟭 (Presheaf C (sp U))

TopCat.Presheaf.extendByInitialSheafAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/OpenImmersion/ExtensionByInitial.lean, line 500. The attribute's comment: “(2) j_! is a left adjoint to restriction on sheaves”. References: SGA 4 III (5.3), “j_! ⊣ j^*, opens site”; SGA 4 IV (11.3.1), “sheaves on a space”; SGA 4 XVII (5.1.1), “topological spaces”.

The extension-by-zero/restriction adjunction, sheaf level. j_! is a left adjoint of the restriction functor j^{-1} : Sh(X) ⥤ Sh(U), i.e. Mor_{Sh(X)}(j_!F, G) = Mor_{Sh(U)}(F, G|_U) bifunctorially.

Here j^{-1} is TopologicalSpace.Opens.sheafRestrict U, which is G ↦ (W ↦ G(j(W))) with no sheafification.

noncomputable def extendByInitialSheafAdjunction :
    extendByInitialSheaf U ⊣ Opens.sheafRestrict (C := C) U

TopCat.Presheaf.restrictExtendByInitialSheafIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/OpenImmersion/ExtensionByInitial.lean, line 529. The attribute's comment: “(5) on sheaves on U we have j^{-1} j_! = id”.

j^{-1} j_! = id. The extension by an initial object of a sheaf on U restricts back to that sheaf, naturally in the sheaf. This is the unit of j_! ⊣ j^{-1}, inverted.

noncomputable def restrictExtendByInitialSheafIso :
    extendByInitialSheaf U ⋙ Opens.sheafRestrict (C := C) U ≅ 𝟭 _

TopCat.Presheaf.isInitialStalkExtendByInitialSheafify, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/OpenImmersion/ExtensionByInitial.lean, line 612. The attribute's comment: “(3) the stalk of j_!F at x ∉ U is initial (∅ for sheaves of sets)”.

The stalk of j_!F at a point x ∉ U is an initial object. For sheaves of sets the initial object is ∅, so this is (j_!F)_x = ∅; for abelian sheaves it is the zero object.

noncomputable def isInitialStalkExtendByInitialSheafify (F : Presheaf C (sp U)) {x : X}
    (hx : x ∉ U) :
    IsInitial (((extendByInitialSheafify U).obj F).presheaf.stalk x)

TopCat.Presheaf.stalkExtendByInitialSheafifyIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/OpenImmersion/ExtensionByInitial.lean, line 629. The attribute's comment: “(3) the stalk of j_!F at a point of U is the stalk of F”.

The stalk of j_!F at a point j(x) with x ∈ U is the stalk of F at x.

noncomputable def stalkExtendByInitialSheafifyIso (F : Presheaf C (sp U)) (x : sp U) :
    ((extendByInitialSheafify U).obj F).presheaf.stalk (U.inclusion' x) ≅ F.stalk x

TopCat.Presheaf.isEmpty_stalk_extendByInitialSheafify, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/OpenImmersion/ExtensionByInitial.lean, line 643. The attribute's comment: “(3) for sheaves of sets: (j_!F)_x = ∅ for x ∉ U”. References: SGA 4 III (1.9.2), “more general”.

For a presheaf of sets F on U, the stalk of j_!F at a point outside U is empty: (j_!F)_x = ∅.

theorem isEmpty_stalk_extendByInitialSheafify {X : TopCat.{u}} (U : Opens X)
    (F : Presheaf (Type u) (sp U)) {x : X} (hx : x ∉ U) :
    IsEmpty (stalk ((extendByInitialSheafify U).obj F).presheaf x)

Tag 00A4, a definition

Tag 00A4 in the Stacks Project.

TopCat.Presheaf.extendByInitial, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/OpenImmersion/ExtensionByInitial.lean, line 142. The attribute's comment: “(1), (3)”.

Extension by an initial object. For j : U → X the inclusion of an open subset, C a category with initial object e, and F a presheaf on U with values in C, this is the presheaf j_{p!}F on X with j_{p!}F(V) = F(V) for V ⊆ U and j_{p!}F(V) = e otherwise, with the obvious restriction maps.

When C is a category of algebraic structures its zero object is initial, so this is the classical extension by zero of an abelian presheaf; and the initial object of Type is the empty type, so this is also the extension by the empty set of a presheaf of sets.

noncomputable def extendByInitial (F : Presheaf C (sp U)) : Presheaf C X

TopCat.Presheaf.extendByInitialFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/OpenImmersion/ExtensionByInitial.lean, line 237. The attribute's comment: “(1), (3)”.

Extension by an initial object, as a functor. j_{p!} : PSh(U) ⥤ PSh(X).

noncomputable def extendByInitialFunctor : Presheaf C (sp U) ⥤ Presheaf C X

TopCat.Presheaf.extendByInitialSheafify, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/OpenImmersion/ExtensionByInitial.lean, line 479. The attribute's comment: “(2)”. References: SGA 4 III (1.9.2), “more general”.

Extension by an initial object for sheaves. The extension j_! F of a sheaf F on U is the sheafification of the presheaf j_{p!}F.

For a category of algebraic structures the initial object is the zero object, so this is the classical extension by zero of a sheaf; for C = Type the initial object is the empty type, so this is the extension by the empty set.

noncomputable def extendByInitialSheafify :
    Presheaf C (sp U) ⥤ TopCat.Sheaf C X

TopCat.Presheaf.extendByInitialSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/OpenImmersion/ExtensionByInitial.lean, line 486. The attribute's comment: “(2)”. References: SGA 4 III (5.3), “opens of a top. space”.

Extension by an initial object, as a functor on sheaves. j_! : Sh(U) ⥤ Sh(X) sends a sheaf F on U to the sheafification of j_{p!}F.

noncomputable def extendByInitialSheaf : TopCat.Sheaf C (sp U) ⥤ TopCat.Sheaf C X

Tag 00A5, a lemma

Tag 00A5 in the Stacks Project.

TopCat.Presheaf.extendByInitialAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/OpenImmersion/ExtensionByInitial.lean, line 374. The attribute's comment: “(1)”. References: SGA 4 IV (11.3.1), “presheaf, constant ring”.

The extension-by-zero/restriction adjunction, presheaf level. For j : U → X the inclusion of an open subset, j_{p!} is a left adjoint of the restriction functor j_p.

noncomputable def extendByInitialAdjunction :
    extendByInitialFunctor (C := C) U ⊣ restrictToOpen U

TopCat.Presheaf.restrictExtendByInitialIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/OpenImmersion/ExtensionByInitial.lean, line 398. The attribute's comment: “(4)”.

j_p j_{p!} = id. The extension by an initial object of a presheaf on U restricts back to that presheaf, naturally in the presheaf.

noncomputable def restrictExtendByInitialIso :
    extendByInitialFunctor (C := C) U ⋙ restrictToOpen U ≅ 𝟭 (Presheaf C (sp U))

TopCat.Presheaf.extendByInitialSheafAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/OpenImmersion/ExtensionByInitial.lean, line 500. The attribute's comment: “(2)”. References: SGA 4 III (5.3), “j_! ⊣ j^*, opens site”; SGA 4 IV (11.3.1), “sheaves on a space”; SGA 4 XVII (5.1.1), “topological spaces”.

The extension-by-zero/restriction adjunction, sheaf level. j_! is a left adjoint of the restriction functor j^{-1} : Sh(X) ⥤ Sh(U), i.e. Mor_{Sh(X)}(j_!F, G) = Mor_{Sh(U)}(F, G|_U) bifunctorially.

Here j^{-1} is TopologicalSpace.Opens.sheafRestrict U, which is G ↦ (W ↦ G(j(W))) with no sheafification.

noncomputable def extendByInitialSheafAdjunction :
    extendByInitialSheaf U ⊣ Opens.sheafRestrict (C := C) U

TopCat.Presheaf.restrictExtendByInitialSheafIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/OpenImmersion/ExtensionByInitial.lean, line 529. The attribute's comment: “(5)”.

j^{-1} j_! = id. The extension by an initial object of a sheaf on U restricts back to that sheaf, naturally in the sheaf. This is the unit of j_! ⊣ j^{-1}, inverted.

noncomputable def restrictExtendByInitialSheafIso :
    extendByInitialSheaf U ⋙ Opens.sheafRestrict (C := C) U ≅ 𝟭 _

TopCat.Presheaf.isZero_stalk_extendByInitialSheafify, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/OpenImmersion/ExtensionByInitial.lean, line 620. The attribute's comment: “(3)”. References: SGA 4 III (1.9.2), “stalk at x∉Y is zero”.

When the value category has a zero object — as the categories of abelian groups and of modules do — the stalk of j_!F at a point x ∉ U is a zero object.

theorem isZero_stalk_extendByInitialSheafify [HasZeroObject C] (F : Presheaf C (sp U)) {x : X}
    (hx : x ∉ U) :
    IsZero (((extendByInitialSheafify U).obj F).presheaf.stalk x)

TopCat.Presheaf.stalkExtendByInitialSheafifyIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/OpenImmersion/ExtensionByInitial.lean, line 629. The attribute's comment: “(3)”.

The stalk of j_!F at a point j(x) with x ∈ U is the stalk of F at x.

noncomputable def stalkExtendByInitialSheafifyIso (F : Presheaf C (sp U)) (x : sp U) :
    ((extendByInitialSheafify U).obj F).presheaf.stalk (U.inclusion' x) ≅ F.stalk x

Tag 00A6, a lemma

Tag 00A6 in the Stacks Project.

statement_1_jp_adjoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/AlgebraicStructure/SheafOfAlgStruct.lean, line 442. The attribute's comment: “(1)”. References: SGA 4 I (5.1), “special case”; SGA 4 I (5.8.3), “partial”; SGA 4 IV (9.2.4), “special case”.

Adjointness on presheaves: the extension j_{p!} : PShCategory(U, C) ⥤ PShCategory(X, C) is left adjoint to the restriction j_p : PShCategory(X, C) ⥤ PShCategory(U, C).

theorem statement_1_jp_adjoint :
    Nonempty (jpShriek00A6 S X U ⊣ jpRestrict S X U)

statement_2_jShriek_adjoint, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/AlgebraicStructure/SheafOfAlgStruct.lean, line 449. The attribute's comment: “(2)”. References: SGA 4 XVII (5.1.1), “top. spaces, alg. struct”.

Adjointness on sheaves: for a sheaf 𝓕 on U and a sheaf 𝓖 on X there is a bijection Hom(j_!𝓕, 𝓖) ≃ Hom(𝓕, j^{-1}𝓖).

theorem statement_2_jShriek_adjoint :
    ∀ (𝓕 : ShOfAlgStruct S (openTopCat X U)) (𝓖 : ShOfAlgStruct S X),
      Nonempty ((((jShriek00A6 S X U) 𝓕).1 ⟶ 𝓖.1) ≃ (𝓕.1 ⟶ ((jInverseSheaf S X U) 𝓖).1))

statement_3_stalk_in_U, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/AlgebraicStructure/SheafOfAlgStruct.lean, line 491. The attribute's comment: “(3)”. References: SGA 4 III (1.9.2), “stalk at y∈Y ≅ H_y”.

For x ∈ U, the stalk (j_!𝓕)_x is isomorphic to the stalk 𝓕_x.

theorem statement_3_stalk_in_U
    (𝓕 : ShOfAlgStruct S (openTopCat X U))
    (x : X) (hx : x ∈ U) :
    Nonempty (stalk00A6 S X (jShriek00A6 S X U 𝓕).1 x ≅
              stalk00A6 S (openTopCat X U) 𝓕.1 ⟨x, hx⟩)

statement_3_stalk_off_U, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/AlgebraicStructure/SheafOfAlgStruct.lean, line 513. The attribute's comment: “(3)”. References: SGA 4 III (1.9.2), “special case”.

For x ∉ U, the stalk (j_!𝓕)_x is isomorphic to the initial object of S.C.

theorem statement_3_stalk_off_U
    (𝓕 : ShOfAlgStruct S (openTopCat X U))
    (x : X) (hx : x ∉ U) :
    Nonempty (stalk00A6 S X (jShriek00A6 S X U 𝓕).1 x ≅ (⊥_ S.C))

statement_4_counit_presheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/AlgebraicStructure/SheafOfAlgStruct.lean, line 535. The attribute's comment: “(4)”.

The composite j_p ∘ j_{p!} is naturally isomorphic to the identity functor on PShCategory(U, C).

theorem statement_4_counit_presheaf :
    Nonempty ((jpShriek00A6 S X U ⋙ jpRestrict S X U) ≅
              (Functor.id (PShCategory S (openTopCat X U))))

statement_5_counit_sheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/AlgebraicStructure/SheafOfAlgStruct.lean, line 543. The attribute's comment: “(5)”.

For every sheaf 𝓕 on U, the underlying presheaves of j^{-1}(j_!𝓕) and of 𝓕 are isomorphic.

theorem statement_5_counit_sheaf :
    ∀ (𝓕 : ShOfAlgStruct S (openTopCat X U)),
      Nonempty ((jInverseSheaf S X U (jShriek00A6 S X U 𝓕)).1 ≅ 𝓕.1)

Tag 00A7, a lemma

Tag 00A7 in the Stacks Project.

jpShriekAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/OpenImmersion/ModuleAdjunction.lean, line 152. The attribute's comment: “(1)”. References: SGA 4 IV (11.3.1), “presheaves on a space”.

The adjunction exhibiting the extension-by-zero functor j_{p!} on presheaves of modules as a left adjoint of the restriction functor j^{-1}.

noncomputable def jpShriekAdjunction : jpShriek X U ⊣ restPMod X U

jShriekAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/OpenImmersion/ModuleAdjunction.lean, line 164. The attribute's comment: “(2)”. References: SGA 4 IV (11.3.1), “ringed space, open U”; SGA 4 XVII (5.1.1), “ringed spaces, modules”; SGA 2 I (1.7), “special case”; SGA 4 IV (14.2), “partial”.

The adjunction exhibiting the extension-by-zero functor j_! on sheaves of modules as a left adjoint of the restriction functor j^{-1}.

noncomputable def jShriekAdjunction : jShriek00A7 X U ⊣ restMod X U

Tag 00A8, a lemma

Tag 00A8 in the Stacks Project.

TopCat.Presheaf.extendByInitialSheafFullyFaithful, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/OpenImmersion/ExtensionByInitial.lean, line 536. References: SGA 4 IV (11.3.1), “special case”.

j_! : Sh(U) ⥤ Sh(X) is fully faithful.

noncomputable def extendByInitialSheafFullyFaithful :
    (extendByInitialSheaf (C := C) U).FullyFaithful

TopCat.Presheaf.isEmpty_stalk_extendByInitialSheafify, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/OpenImmersion/ExtensionByInitial.lean, line 643. References: SGA 4 III (1.9.2), “more general”.

For a presheaf of sets F on U, the stalk of j_!F at a point outside U is empty: (j_!F)_x = ∅.

theorem isEmpty_stalk_extendByInitialSheafify {X : TopCat.{u}} (U : Opens X)
    (F : Presheaf (Type u) (sp U)) {x : X} (hx : x ∉ U) :
    IsEmpty (stalk ((extendByInitialSheafify U).obj F).presheaf x)

Tag 00A9, a lemma

Tag 00A9 in the Stacks Project.

ExtensionByZero.jExt_full, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/OpenImmersion/ExtensionByZero.lean, line 92. The attribute's comment: “(1)”.

Stacks 00A9 (1). The extension by zero functor j_! is full: every morphism j_! F ⟶ j_! F' of sheaves on X comes from a morphism F ⟶ F' of sheaves on U.

theorem jExt_full : (jExt U).Full

ExtensionByZero.jExt_faithful, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/OpenImmersion/ExtensionByZero.lean, line 98. The attribute's comment: “(1)”. References: SGA 4 IV (11.3.1), “special case”.

Stacks 00A9 (1). The extension by zero functor j_! is faithful: a morphism of sheaves on U is determined by the morphism it induces on the extensions by zero.

theorem jExt_faithful : (jExt U).Faithful

ExtensionByZero.jExt_essImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/OpenImmersion/ExtensionByZero.lean, line 148. The attribute's comment: “(2)”. References: SGA 4 XVII (5.1.1), “partial”.

Stacks 00A9 (2), description of the essential image. An abelian sheaf G on X lies in the essential image of j_! if and only if the stalk G_x is the zero abelian group for every point x ∈ X not belonging to U.

For "only if", an isomorphism G ≅ j_! F induces an isomorphism of stalks, and the stalk of j_! F at a point outside U is zero. For "if", the vanishing hypothesis makes the counit j_! (j⁻¹ G) ⟶ G an isomorphism, which exhibits G in the essential image.

theorem jExt_essImage (G : TopCat.Sheaf AddCommGrpCat.{u} X) :
    (jExt U).essImage G ↔ ∀ x : X, x ∉ U → IsZero (G.presheaf.stalk x)

Tag 00AA, a lemma

Tag 00AA in the Stacks Project.

Stacks.full_and_faithful_and_essImage_jLowerShriek, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/OpenImmersion/ExtensionByInitialAlgStruct.lean, line 556.

Stacks 00AA. For S = (C, F) a type of algebraic structure whose category C has an initial object, and j : U → X the inclusion of an open subset, the extension-by-initial functor j_! : Sh(U, C) ⥤ Sh(X, C) is full and faithful, and a sheaf G ∈ Sh(X, C) lies in its essential image exactly when the stalk G_x is an initial object of C for every x ∈ X ∖ U.

theorem full_and_faithful_and_essImage_jLowerShriek (S : AlgebraicStructureType.{u, u})
    [HasColimits S.C] [HasInitial S.C] (X : TopCat.{u}) (U : Opens X)
    [HasWeakSheafify (Opens.grothendieckTopology X) S.C]
    [HasWeakSheafify (Opens.grothendieckTopology (TopCat.of (U : Type _))) S.C] :
    (jLowerShriek (C := S.C) X U).Full ∧
      (jLowerShriek (C := S.C) X U).Faithful ∧
      ∀ G : TopCat.Sheaf S.C X,
        (jLowerShriek (C := S.C) X U).essImage G ↔
          ∀ x : X, x ∉ (U : Set X) → Nonempty (IsInitial (G.presheaf.stalk x))

Tag 00AB, a lemma

Tag 00AB in the Stacks Project.

ExtensionByZeroModules.full_and_faithful_and_essImage_jShriek, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/OpenImmersion/ModuleExtensionByZero.lean, line 395. References: SGA 4 IV (11.3.1), “special case”.

Stacks 00AB. Let (X, 𝒪) be a ringed space and let j : (U, 𝒪|_U) → (X, 𝒪) be an open subspace. The extension-by-zero functor j_! : Mod(𝒪|_U) ⥤ Mod(𝒪) is fully faithful, and its essential image consists exactly of those sheaves G of 𝒪-modules with G_x = 0 for all x ∈ X ∖ U.

The stalk G_x is a module over the stalk 𝒪_x whose underlying abelian group is the stalk of the underlying abelian sheaf of G (Mathlib's PresheafOfModules.instModuleStalk), and a module is zero exactly when its underlying group is; so G_x = 0 is expressed here as vanishing of that abelian group. The sheaf of rings is allowed to be non-commutative, which is more general than the ringed spaces of the source.

theorem full_and_faithful_and_essImage_jShriek :
    (jShriek U O).Full ∧ (jShriek U O).Faithful ∧
      ∀ G : SheafOfModules.{u} O, (jShriek U O).essImage G ↔
        ∀ x : X, x ∉ U → IsZero (TopCat.Presheaf.stalk (X := X) G.val.presheaf x)

Tag 00AC, a remark

Tag 00AC in the Stacks Project.

TopCat.Presheaf.isEmpty_isTerminal_extendByInitialSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/OpenImmersion/NotLeftExact.lean, line 68. The attribute's comment: “j_! does not transform a final object of Sh(U) into a final object of Sh(X)”.

Stacks 00AC, first half. For U ≠ X the sheaf j_!F is not a final object of Sh(X, Type), whatever the sheaf F on U is. In particular j_! does not transform a final object of Sh(U) into a final object of Sh(X).

A final object of a category of sheaves of sets has a one-point set of sections over every open, because Sheaf.forget and evaluation at an open both preserve limits; but the global sections of j_!F are empty by isEmpty_sections_extendByInitialSheafify.

theorem isEmpty_isTerminal_extendByInitialSheaf (hU : U ≠ ⊤)
    (F : TopCat.Sheaf (Type u) (sp U)) :
    IsEmpty (IsTerminal ((extendByInitialSheaf U).obj F))

TopCat.Presheaf.not_preservesFiniteLimits_extendByInitialSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/OpenImmersion/NotLeftExact.lean, line 86. The attribute's comment: “j_! is not left exact as a functor between the categories of sheaves of sets”.

Stacks 00AC. For U ≠ X the functor j_! : Sh(U, Type) ⥤ Sh(X, Type) does not preserve finite limits, i.e. it is not left exact.

The final object is the limit of the empty diagram, so a functor preserving finite limits would send the final object of Sh(U, Type) to a final object of Sh(X, Type), contradicting isEmpty_isTerminal_extendByInitialSheaf.

theorem not_preservesFiniteLimits_extendByInitialSheaf (hU : U ≠ ⊤) :
    ¬ PreservesFiniteLimits
      (extendByInitialSheaf U : TopCat.Sheaf (Type u) (sp U) ⥤ TopCat.Sheaf (Type u) X)

Sources

• Section 6.31, Tag 009Z
• AxiomMath/Stacks at 5ed82d14

LeanOpenImmersionSheaves.presheaf_pullback_iso_restriction · OpenImmersionSheaves.sheaf_pullback_iso_restriction · OpenImmersionSheaves.stalk_sheaf_pullback_iso · OpenImmersionSheaves.presheaf_pullback_pushforward_counit_isIso · OpenImmersionSheaves.sheaf_pullback_pushforward_counit_isIso · restrictPresheaf · local_restrictSheaf · openSubspace

Section6.32 Closed immersions and (pre)sheaves#

Section 6.32 of the Stacks Project, Tag 00AD. 5 tags here are carried by 12 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00AE, a lemma

Tag 00AE in the Stacks Project.

ClosedImmersionSheaves.isTerminalStalkPushforwardOfNotMemRange, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/ClosedImmersion/Pushforward.lean, line 116. References: EGA 0 (4.2.5), “zero stalks outside X”.

Stacks 00AE, the stalks of i_* F away from Z. For i : Z ⟶ X a closed embedding, F a sheaf on Z and x ∈ X not in the image of i, the stalk (i_* F)_x is a terminal object of the target category: a singleton for sheaves of sets, 0 for abelian sheaves, a final object for sheaves of algebraic structures.

The complement of the (closed) image is an open neighbourhood W of x with i⁻¹(W) = ∅, so pushforwardStalkIsoOfEmptyPreimage identifies the stalk with the terminal object (i_* F)(W) = F(∅).

noncomputable def isTerminalStalkPushforwardOfNotMemRange
    (hi : IsClosedEmbedding (ConcreteCategory.hom i)) (x : X)
    (hx : x ∉ Set.range (ConcreteCategory.hom i)) :
    IsTerminal (stalk (i _* F) x)

ClosedImmersionSheaves.sheaf_pullback_pushforward_counit_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/ClosedImmersion/Pushforward.lean, line 202.

Stacks 00AE, i⁻¹ i_* = id. For an inducing i : Z ⟶ X — in particular for the inclusion of a closed subset — the counit i⁻¹ i_* ⟶ 𝟭 of the adjunction i⁻¹ ⊣ i_* between categories of sheaves is a natural isomorphism, because its right adjoint i_* is fully faithful.

theorem sheaf_pullback_pushforward_counit_isIso
    (hi : IsInducing (ConcreteCategory.hom i)) :
    IsIso (Sheaf.pullbackPushforwardAdjunction A i).counit

Declarations registered for the tag:

• TopCat.Presheaf.stalkPushforward.stalkPushforward_iso_of_isInducing registered with add_to_stacks in StacksFrontier/Topology/Sheaves/ClosedImmersion/Pushforward.lean, line 217 (StacksFrontier): “The stalk of i_* F at a point i z of the closed subset Z is F_z, via the canonical comparison map stalkPushforward. Mathlib proves this for any inducing map, and a closed embedding is inducing.”. References: EGA 0 (3.4.5), “more general”.

Tag 00AF, a lemma

Tag 00AF in the Stacks Project.

pushforward_faithful, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/ClosedImmersion/Sets.lean, line 81.

The pushforward of sheaves of sets along the inclusion of a subset is faithful.

lemma pushforward_faithful (X : TopCat.{u}) (Z : Set X) : (pushforward00AF X Z).Faithful

pushforward_full, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/ClosedImmersion/Sets.lean, line 87.

The pushforward of sheaves of sets along the inclusion of a subset is full: every morphism i_* F ⟶ i_* G is i_* of a morphism F ⟶ G.

lemma pushforward_full (X : TopCat.{u}) (Z : Set X) : (pushforward00AF X Z).Full

pushforward_stalkIsSingleton_of_notMem, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/ClosedImmersion/Sets.lean, line 94. References: EGA IV (21.9.1), “special case”.

For Z closed and x ∉ Z, the stalk (i_* F)_x is a singleton.

theorem pushforward_stalkIsSingleton_of_notMem
    (X : TopCat.{u}) {Z : Set X} (hZ : IsClosed Z)
    (F : TopCat.Sheaf (Type u) (TopCat.of Z))
    (x : X) (hx : x ∉ Z) :
    StalkIsSingleton X ((pushforward00AF X Z).obj F) x

Tag 00AG, a lemma

Tag 00AG in the Stacks Project.

closedInclusion_pushforward_faithful, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/ClosedImmersion/Abelian.lean, line 63.

Stacks 00AG, faithfulness. The pushforward of sheaves of abelian groups along a closed embedding is a faithful functor.

theorem closedInclusion_pushforward_faithful
    (Z X : TopCat.{u}) (i : Z ⟶ X) (hi : Topology.IsClosedEmbedding i.hom) :
    (closedInclusionPushforward Z X i).Faithful

closedInclusion_pushforward_full, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/ClosedImmersion/Abelian.lean, line 71.

Stacks 00AG, fullness. The pushforward of sheaves of abelian groups along a closed embedding is a full functor: every morphism i_* 𝒜 ⟶ i_* ℬ is i_* of a morphism 𝒜 ⟶ ℬ.

theorem closedInclusion_pushforward_full
    (Z X : TopCat.{u}) (i : Z ⟶ X) (hi : Topology.IsClosedEmbedding i.hom) :
    (closedInclusionPushforward Z X i).Full

closedInclusion_pushforward_essImage_stalk_isZero, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/ClosedImmersion/Abelian.lean, line 112. References: EGA 0 (3.4.6), “(F)”; EGA 0 (4.2.5), “Ψ_*M is zero outside X”; EGA IV (21.9.1), “special case”; SGA 6 IX (1.1), “Support clause”.

Stacks 00AG, essential image, forward direction. If a sheaf G of abelian groups on X lies in the essential image of the pushforward along a closed embedding i, then the stalk of G vanishes at every point outside the range of i.

theorem closedInclusion_pushforward_essImage_stalk_isZero
    (Z X : TopCat.{u}) (i : Z ⟶ X) (hi : Topology.IsClosedEmbedding i.hom)
    (G : TopCat.Sheaf AddCommGrpCat.{u} X)
    (hG : (closedInclusionPushforward Z X i).essImage G) :
    ∀ x : X, x ∉ Set.range i.hom → IsZero (Presheaf.stalk G.obj x)

Tag 00AH, a lemma

Tag 00AH in the Stacks Project.

Stacks.full_and_faithful_pushforward_subsetInclusion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/ClosedImmersion/PushforwardAlgStruct.lean, line 149.

Stacks 00AH, Part 1. The pushforward functor i_* : Sh(Z, C) ⥤ Sh(X, C) along the inclusion i : Z ↪ X is full and faithful, for any type of algebraic structure (C, F). The proof only uses that Opens.map i is surjective on opens, so Z may be an arbitrary subset; closedness is needed only for essImage_pushforward_subsetInclusion_iff.

theorem full_and_faithful_pushforward_subsetInclusion (X : TopCat.{u}) (Z : Set X)
    (S : AlgebraicStructureType.{u, u}) [HasColimits S.C] :
    (TopCat.Sheaf.pushforward S.C (subsetInclusion X Z)).Full ∧
      (TopCat.Sheaf.pushforward S.C (subsetInclusion X Z)).Faithful

Stacks.essImage_pushforward_subsetInclusion_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/ClosedImmersion/PushforwardAlgStruct.lean, line 507.

Stacks 00AH, Part 2. A sheaf G ∈ Sh(X, C) lies in the essential image of i_* : Sh(Z, C) ⥤ Sh(X, C), for i the inclusion of a closed subset Z, exactly when its stalk at every point x ∉ Z is isomorphic in C to the final object 0.

theorem essImage_pushforward_subsetInclusion_iff (X : TopCat.{u}) (Z : Set X) (hZ : IsClosed Z)
    (S : AlgebraicStructureType.{u, u}) [HasColimits S.C] (Sfinal : S.WithFinal)
    (G : TopCat.Sheaf S.C X) :
    (TopCat.Sheaf.pushforward S.C (subsetInclusion X Z)).essImage G ↔
      ∀ x : X, x ∉ Z → Nonempty (TopCat.Presheaf.stalk G.obj x ≅ Sfinal.zero)

Tag 00AI, a remark

Tag 00AI in the Stacks Project.

ClosedImmersionSheaves.not_preservesColimitsOfShape_sheafPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/ClosedImmersion/NotRightExact.lean, line 78. The attribute's comment: “i_ is not right exact as a functor between categories of sheaves of sets”. References: SGA 4 IV (3.1.2), “u_ not right exact”.

Stacks 00AI, first half. For i : Z ⟶ X a closed embedding and x ∈ X outside the image of i, the pushforward i_* : Sh(Z, Type) ⥤ Sh(X, Type) does not preserve binary coproducts, i.e. it is not right exact.

Take F to be the final sheaf * on Z. Stacks 00AE makes the stalk at x of i_*G terminal for every sheaf G on Z, in particular for G = F and for G = F ⨿ F. Taking stalks of sheaves is a left adjoint, so it preserves the coproduct; if i_* preserved it too, the terminal set (i_*(F ⨿ F))_x would be the coproduct of the terminal set (i_*F)_x with itself, which isEmpty_isTerminal_coprod_self forbids.

theorem not_preservesColimitsOfShape_sheafPushforward
    (hi : IsClosedEmbedding (ConcreteCategory.hom i)) (x : X)
    (hx : x ∉ Set.range (ConcreteCategory.hom i)) :
    ¬ PreservesColimitsOfShape (Discrete WalkingPair) (Sheaf.pushforward (Type u) i)

ClosedImmersionSheaves.not_isLeftAdjoint_sheafPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/ClosedImmersion/NotRightExact.lean, line 111. The attribute's comment: “in particular i_* cannot have a right adjoint”.

Stacks 00AI, second half. For i : Z ⟶ X a closed embedding and x ∈ X outside the image of i, the pushforward i_* : Sh(Z, Type) ⥤ Sh(X, Type) has no right adjoint: a functor with a right adjoint preserves all colimits, and i_* does not preserve binary coproducts.

theorem not_isLeftAdjoint_sheafPushforward
    (hi : IsClosedEmbedding (ConcreteCategory.hom i)) (x : X)
    (hx : x ∉ Set.range (ConcreteCategory.hom i)) :
    ¬ (Sheaf.pushforward (Type u) i).IsLeftAdjoint

Sources

• Section 6.32, Tag 00AD
• AxiomMath/Stacks at 5ed82d14

LeanClosedImmersionSheaves.isTerminalStalkPushforwardOfNotMemRange · ClosedImmersionSheaves.sheaf_pullback_pushforward_counit_isIso · TopCat.Presheaf.stalkPushforward.stalkPushforward_iso_of_isInducing · pushforward_faithful · pushforward_full · pushforward_stalkIsSingleton_of_notMem · closedInclusion_pushforward_faithful · closedInclusion_pushforward_full

Section6.33 Glueing sheaves#

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

Tag 04TN, a lemma

Tag 04TN in the Stacks Project.

TopCat.Sheaf.existsUnique_hom_of_localHom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Glueing/MapGluing.lean, line 186.

Stacks 04TN. Gluing maps of sheaves. Given an open covering U : ι → Opens X of a topological space X, sheaves of sets F and G on X, and local sheaf maps φ i on each U i agreeing on all overlaps, there is a unique morphism of sheaves ψ : F ⟶ G whose restriction to each U i is φ i.

theorem existsUnique_hom_of_localHom {ι : Type*} {X : TopCat.{u}}
    (U : ι → Opens X) (hU : ⨆ i, U i = ⊤)
    (F G : TopCat.Sheaf (Type u) X)
    (φ : (i : ι) → LocalSheafHom F G (U i))
    (hφ : ∀ i j (V : Opens X) (hVi : V ≤ U i) (hVj : V ≤ U j),
      (φ i).app V hVi = (φ j).app V hVj) :
    ∃! ψ : F ⟶ G, ∀ i (V : Opens X) (hV : V ≤ U i),
      ψ.1.app (op V) = (φ i).app V hV

Tag 00AL, a lemma

Tag 00AL in the Stacks Project.

TopCat.Sheaf.GlueData.glued, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Glueing/Sheaf.lean, line 278. References: EGA 0 (4.1.7), “partial”.

The sheaf of sets on X glued from the glueing data D.

def glued (D : GlueData X U) : X.Sheaf (Type u)

TopCat.Sheaf.GlueData.sectionsEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Glueing/Sheaf.lean, line 284.

The comparison isomorphism φ i : F|_{U i} ≅ F_i on sections over an open V ≤ U i.

def sectionsEquiv (D : GlueData X U) (i : ι) {V : Opens X} (hV : V ≤ U i) :
    D.Sections V ≃ (D.sheaf i).obj V hV

TopCat.Sheaf.GlueData.sectionsEquiv_map, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Glueing/Sheaf.lean, line 309.

The comparison isomorphism φ i commutes with the restriction maps, i.e. it is an isomorphism of sheaves on U i.

theorem sectionsEquiv_map (D : GlueData X U) (i : ι) {V W : Opens X} (hV : V ≤ U i) (hWV : W ≤ V)
    (s : D.Sections V) :
    D.sectionsEquiv i (hWV.trans hV) (D.sectionsMap hWV s)
      = (D.sheaf i).map hWV (D.sectionsEquiv i hV s)

TopCat.Sheaf.GlueData.trans_sectionsEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Glueing/Sheaf.lean, line 318.

The commuting diagram φ i j ∘ φ i = φ j over the overlaps.

theorem trans_sectionsEquiv (D : GlueData X U) (i j : ι) {V : Opens X} (hi : V ≤ U i)
    (hj : V ≤ U j) (s : D.Sections V) :
    D.trans i j hi hj (D.sectionsEquiv i hi s) = D.sectionsEquiv j hj s

Tag 00AM, a lemma

Tag 00AM in the Stacks Project.

TopCat.Sheaf.AddGlueData.gluedAddPresheaf_forget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Glueing/AlgebraicStructure.lean, line 210.

Stacks 00AM. The underlying presheaf of sets of the glued presheaf of abelian groups is the presheaf of sets glued in Stacks 00AL: the additive subgroup cut out of ∏ i, F i (W ⊓ U i) by the equalizer equations has, as its underlying set, exactly the set of compatible families.

theorem gluedAddPresheaf_forget :
    D.gluedAddPresheaf ⋙ CategoryTheory.forget AddCommGrpCat = D.toGlueData.gluedPresheaf

TopCat.Sheaf.AddGlueData.gluedAddPresheaf_isSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Glueing/AlgebraicStructure.lean, line 217. References: EGA 0 (4.1.7), “partial”.

Stacks 00AM. The presheaf of abelian groups glued from a glueing data of sheaves of abelian groups is a sheaf of abelian groups. Since its underlying presheaf of sets is the sheaf of Stacks 00AL, this is the sheaf condition of Stacks 00AL read through the forgetful functor.

theorem gluedAddPresheaf_isSheaf : D.gluedAddPresheaf.IsSheaf

TopCat.Sheaf.ModuleGlueData.gluedModulePresheaf_forget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Glueing/AlgebraicStructure.lean, line 367.

Stacks 00AM. The underlying presheaf of sets of the glued presheaf of R-modules is the presheaf of sets glued in Stacks 00AL: the submodule cut out of ∏ i, F i (W ⊓ U i) by the equalizer equations has, as its underlying set, exactly the set of compatible families.

theorem gluedModulePresheaf_forget :
    D.gluedModulePresheaf ⋙ CategoryTheory.forget (ModuleCat R) = D.toGlueData.gluedPresheaf

TopCat.Sheaf.ModuleGlueData.gluedModulePresheaf_isSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Glueing/AlgebraicStructure.lean, line 374.

Stacks 00AM. The presheaf of R-modules glued from a glueing data of sheaves of R-modules is a sheaf of R-modules. Since its underlying presheaf of sets is the sheaf of Stacks 00AL, this is the sheaf condition of Stacks 00AL read through the forgetful functor.

theorem gluedModulePresheaf_isSheaf : D.gluedModulePresheaf.IsSheaf

TopCat.Sheaf.OModuleGlueData.gluedPresheafOfModules, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Glueing/OModule.lean, line 264. The attribute's comment: “sheaves of O-modules”.

The glued presheaf of 𝒪-modules. Its underlying presheaf of abelian groups is D.toAddGlueData.gluedAddPresheaf, and its 𝒪(W)-module of sections over W is gluedModule.

noncomputable def gluedPresheafOfModules : PresheafOfModules.{u} 𝒪

TopCat.Sheaf.OModuleGlueData.isSheaf_gluedPresheafOfModules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Glueing/OModule.lean, line 275. The attribute's comment: “sheaves of O-modules”.

The presheaf of 𝒪-modules glued from a glueing datum of sheaves of 𝒪-modules is a sheaf.

theorem isSheaf_gluedPresheafOfModules :
    CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology X)
      D.gluedPresheafOfModules.presheaf

Stacks.SheafOfModules.OModuleGlueData.gluedPresheafOfModules_forget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/ModuleGlueing/Basic.lean, line 377. The attribute's comment: “sheaves of O-modules, the underlying presheaf of sets”.

The underlying presheaf of sets of the glued presheaf of O-modules is the presheaf of sets glued in Stacks 00AL.

theorem gluedPresheafOfModules_forget (D : OModuleGlueData O U) :
    D.gluedPresheafOfModules.presheaf ⋙ CategoryTheory.forget AddCommGrpCat
      = D.toGlueData.gluedPresheaf

Stacks.SheafOfModules.OModuleGlueData.gluedPresheafOfModules_isSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/ModuleGlueing/Basic.lean, line 385. The attribute's comment: “sheaves of O-modules, the sheaf condition”.

The presheaf of O-modules glued from a glueing datum of sheaves of O-modules is a sheaf. Since its underlying presheaf of sets is the sheaf of Stacks 00AL, this is the sheaf condition of Stacks 00AL read through the forgetful functor.

theorem gluedPresheafOfModules_isSheaf (D : OModuleGlueData O U) :
    Presheaf.IsSheaf (Opens.grothendieckTopology X) D.gluedPresheafOfModules.presheaf

Stacks.SheafOfModules.OModuleGlueData.glued, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/ModuleGlueing/Basic.lean, line 393. The attribute's comment: “sheaves of O-modules, the glued sheaf”.

The sheaf of O-modules on X glued from a glueing datum of sheaves of O-modules.

noncomputable def glued (D : OModuleGlueData O U) : _root_.SheafOfModules.{u} O

Stacks.SheafOfModules.OModuleGlueData.chartLinearEquiv_restrict, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/ModuleGlueing/Basic.lean, line 423. The attribute's comment: “sheaves of O-modules, the comparison isomorphisms”.

The comparison isomorphism φ i commutes with the restriction maps, i.e. it is an isomorphism of sheaves of modules on U i.

theorem chartLinearEquiv_restrict (D : OModuleGlueData O U) (i : ι) {V W : Opens X}
    (hV : V ≤ U i) (h : W ≤ V) (s : D.sectionsSubmodule V) :
    D.chartLinearEquiv i (h.trans hV) (D.sectionsMap h s)
      = (D.sheaf i).map h (D.chartLinearEquiv i hV s)

Stacks.SheafOfModules.OModuleGlueData.trans_chartLinearEquiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/ModuleGlueing/Basic.lean, line 431. The attribute's comment: “sheaves of O-modules, compatibility of the comparisons”.

The commuting triangle φ i j ∘ φ i = φ j over the overlaps.

theorem trans_chartLinearEquiv (D : OModuleGlueData O U) (i j : ι) {V : Opens X} (hi : V ≤ U i)
    (hj : V ≤ U j) (s : D.sectionsSubmodule V) :
    D.trans i j hi hj (D.chartLinearEquiv i hi s) = D.chartLinearEquiv j hj s

Stacks.SheafOfModules.ModulesGlueData.glued, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/ModuleGlueing/Basic.lean, line 554. The attribute's comment: “sheaves of O-modules on a scheme, the glued module”.

The sheaf of modules on S glued from D.

noncomputable abbrev glued (D : ModulesGlueData S f) : S.Modules

Stacks.SheafOfModules.ModulesGlueData.chartIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/ModuleGlueing/Basic.lean, line 559. The attribute's comment: “sheaves of O-modules on a scheme, the comparison isomorphisms”.

The glued module restricts along each chart to the sheaf of modules it was glued from.

noncomputable def chartIso (D : ModulesGlueData S f) (i : ι) :
    D.glued.restrict (f i) ≅ D.mod i

Stacks.SheafOfModules.ModulesGlueData.trans_chartSectionsIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Modules/ModuleGlueing/Basic.lean, line 594. The attribute's comment: “sheaves of O-modules on a scheme, the comparisons related by the transitions”.

The commuting triangle φ i j ∘ φ i = φ j on sections over an open contained in two charts. Reading a section of the glued module on the i-th chart and comparing it with the j-th chart gives the same thing as reading it on the j-th chart directly. This is Stacks.SheafOfModules.OModuleGlueData.trans_chartLinearEquiv phrased with chartSectionsIso, so that it elaborates outside this file.

theorem trans_chartSectionsIso (D : ModulesGlueData S f) (i j : ι) {V : S.Opens}
    (hi : V ≤ (f i).opensRange) (hj : V ≤ (f j).opensRange)
    (x : ToType (D.glued.val.obj (op V))) :
    D.trans i j hi hj ((D.chartSectionsIso i hi).hom x) = (D.chartSectionsIso j hj).hom x

Tag 00AN, a lemma

Tag 00AN in the Stacks Project.

TopCat.Sheaf.sheafEquivGlueData, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Sheaves/Glueing/Equivalence.lean, line 188. References: EGA 0 (3.3.1), “special case”.

Stacks 00AN. For an open covering X = ⋃ i, U i, restriction to the members of the covering is an equivalence between the category of sheaves of sets on X and the category of glueing data with respect to the covering.

noncomputable def sheafEquivGlueData (hU : ⨆ i, U i = ⊤) : X.Sheaf (Type u) ≌ GlueData X U

Sources

• Section 6.33, Tag 00AK
• AxiomMath/Stacks at 5ed82d14

LeanTopCat.Sheaf.existsUnique_hom_of_localHom · TopCat.Sheaf.GlueData.glued · TopCat.Sheaf.GlueData.sectionsEquiv · TopCat.Sheaf.GlueData.sectionsEquiv_map · TopCat.Sheaf.GlueData.trans_sectionsEquiv · TopCat.Sheaf.AddGlueData.gluedAddPresheaf_forget · TopCat.Sheaf.AddGlueData.gluedAddPresheaf_isSheaf · TopCat.Sheaf.ModuleGlueData.gluedModulePresheaf_forget

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.