18.21 Localization of ringed… to 18.27 Internal Hom

Section18.21 Localization of ringed topoi #

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

Tag 04IE, a lemma

Tag 04IE in the Stacks Project.

Stacks.Sheaves.LocalizedRingedTopos.sliceEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/RelocalizationSliceComparison.lean, line 159. The attribute's comment: “equivalence with the slice topos”. References: SGA 3 IV (4.5.4), “more general”; SGA 4 III (5.4), “special case”.

Stacks 04IE, the equivalence with the slice topos: sheaves on the site of elements of F are the same thing as sheaves on C over F. This is the sheaf-level restriction of the canonical equivalence of Tag 0791, taken from CategoryTheory.Presheaf.IsSheaf.exists_sheafEquivalence_costructuredArrow_yoneda.

noncomputable def sliceEquivalence (X : RingedTopos.{u}) (F : X.Topos) :
    (localizedRingedTopos X F).Topos ≌ Over F

Stacks.Sheaves.LocalizedRingedTopos.shriekAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/RelocalizationSliceComparison.lean, line 169. The attribute's comment: “part (3): lower shriek on sets”. References: SGA 4 III (5.5), “Clause 3), special case”.

Stacks 04IE, part (3): the lower shriek of the localization morphism on sheaves of sets is the forgetful functor of the slice. Concretely, Sh(C/F) ≌ Sh(C)/F followed by Over.forget F is left adjoint to the inverse image of the localization morphism, which is restriction along the projection from the site of elements.

noncomputable def shriekAdjunction (X : RingedTopos.{u}) (F : X.Topos) :
    (sliceEquivalence X F).functor ⋙ Over.forget F ⊣
      (localizationToposMorphism X F).inverseImage

Stacks.Sheaves.LocalizedRingedTopos.sliceEquivalenceFibers, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/RelocalizationSliceComparison.lean, line 180. The attribute's comment: “canonical identification with the slice topos”.

Stacks 04IE: the equivalence with the slice topos is the canonical fibre construction and not merely an abstract equivalence. On underlying presheaves, the inverse of sliceEquivalence sends an object φ : A ⟶ F of Sh(C)/F to the presheaf (U, t) ↦ {x ∈ A(U) | φ(x) = t} on the site of elements of F.

noncomputable def sliceEquivalenceFibers (X : RingedTopos.{u}) (F : X.Topos) :
    (sliceEquivalence X F).inverse ⋙ sheafToPresheaf (elementTopology X F) (Type u) ≅
      Over.post (X := F) (sheafToPresheaf X.J (Type u)) ⋙
        (overEquivPresheafCostructuredArrow F.obj).functor

AlgebraicGeometry.SmallEtale.localizedToposEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/RecoveringMorphisms/OpenLocalization.lean, line 299. The attribute's comment: “for the small étale site: the topos of the small étale site of an object U of the small étale site of S is the topos of the localization of the small étale ringed topos of S at the sheaf represented by U. This form identifies the two topoi; the identification of the two RINGED topoi, structure sheaves included, is AlgebraicGeometry.SmallEtale.localizedRingedToposHom. It is the composite of three equivalences: the equivalence of sites between the small étale site of the scheme of U and the slice of the small étale site of S at U, read on sheaves; Stacks 00Y1 for the slice site; and the equivalence of the localization at a sheaf with the slice of the topos”.

Stacks 04IE for the small étale site: the small étale topos of an object U of the small étale site of S is the localization of the small étale topos of S at the sheaf h_U^#.

The three steps of the identification are each proved elsewhere and none of them is rebuilt here. The small étale site of the scheme of U is the slice (S_étale)/U, so their topoi agree (AlgebraicGeometry.SmallEtale.localizationSheafEquivalence, which is AlgebraicGeometry.SmallEtale.localizationEquivalence read on sheaves); the topos of a slice site is the slice of the topos at the represented sheaf, which is Stacks 00Y1 (CategoryTheory.OverShriek.sheafEquivalence); and the slice of a topos at a sheaf is the localization of the ringed topos at that sheaf, which is Stacks 04IE in the generality it is formalized in (AlgebraicGeometry.RingedTopos.localizationEquivalence).

What this is not: an identification of ringed topoi. It identifies the two topoi only. Upgrading it needs the comparison of the two structure sheaves — the structure sheaf of the localization is the restriction of 𝒪_S along the projection from the site of elements of h_U^#, and the structure sheaf of the small étale site of the scheme of U is its own sheaf of global functions — and that comparison is not carried here.

noncomputable def localizedToposEquivalence :
    Sheaf (SmallEtale.topology B U.obj.left.obj U.obj.left.property) (Type u) ≌
      (RingedTopos.localizedRingedTopos
        (RingedSite.toRingedTopos (smallEtaleRingedSite B S hS))
        ((presheafToSheaf (SmallEtale.topology B S hS) (Type u)).obj (yoneda.obj U))).Topos

AlgebraicGeometry.SmallEtale.openLocalizedToposEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/RecoveringMorphisms/OpenLocalization.lean, line 333. The attribute's comment: “for an open subscheme: the topos of the small étale site of an open subscheme V of S is the topos of the localization of the small étale ringed topos of S at the sheaf represented by V regarded as étale over S. This is the composite of AlgebraicGeometry.opensToBoundedEtale with the identification of the small étale site of an object with the slice over it. The sheaf localized at is the one V represents in the small étale site; that it agrees with AlgebraicGeometry.openRepresentable' is AlgebraicGeometry.SmallEtale.openRepresentableSheafIsoYoneda, and the identification of the two RINGED topoi at that spelling is AlgebraicGeometry.SmallEtale.openLocalizedRingedToposHom”. References: SGA 4 VIII (6.2), “partial”.

Stacks 04IE for an open subscheme: the small étale topos of an open subscheme V of S is the localization of the small étale topos of S at the sheaf represented by V.

This is AlgebraicGeometry.SmallEtale.localizedToposEquivalence at the object AlgebraicGeometry.opensToBoundedEtale B S hS V of the small étale site, the open subscheme V regarded as étale over S — the composite of that functor with AlgebraicGeometry.SmallEtale.localizationEquivalence, which is the identification the Zariski gluing of Stacks 04I7 restricts along.

The sheaf it localizes at is h_V^# for V read in the small étale site. It is not stated here to agree with AlgebraicGeometry.openRepresentable', which spells the same idea as the restriction to the small étale site of the presheaf V represents in the big étale slice, with its sections raised by CategoryTheory.uliftYoneda; identifying the two is a separate comparison and is not carried.

noncomputable def openLocalizedToposEquivalence (V : S.Opens) :
    Sheaf (SmallEtale.topology B V.toScheme
        (Scheme.size_lt_of_isOpenImmersion V.ι hS)) (Type u) ≌
      (RingedTopos.localizedRingedTopos
        (RingedSite.toRingedTopos (smallEtaleRingedSite B S hS))
        ((presheafToSheaf (SmallEtale.topology B S hS) (Type u)).obj
          (yoneda.obj ((opensToBoundedEtale B S hS).obj V)))).Topos

AlgebraicGeometry.SmallEtale.openRepresentableLocalizedToposEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/RecoveringMorphisms/OpenLocalization.lean, line 389. The attribute's comment: “for an open subscheme V of S, with the sheaf localized at spelled as the sheafification of AlgebraicGeometry.openRepresentable': the topos of the small étale site of V is the topos of the localization of the small étale ringed topos of S at that sheaf. This is AlgebraicGeometry.SmallEtale.openLocalizedToposEquivalence transported along the comparison of the two spellings of the represented sheaf; the identification of the two RINGED topoi at this spelling, structure sheaves included, is AlgebraicGeometry.SmallEtale.openLocalizedRingedToposHom”.

Stacks 04IE for an open subscheme, at the AlgebraicGeometry.openRepresentable' spelling of the sheaf it localizes at.

This is AlgebraicGeometry.SmallEtale.openLocalizedToposEquivalence moved along AlgebraicGeometry.SmallEtale.openRepresentableSheafIsoYoneda by AlgebraicGeometry.RingedTopos.localizedToposEquivalenceOfIso, and it is the form in which Stacks 04IE meets Stacks 04IF: the target of AlgebraicGeometry.localizedOverOpen and the source AlgebraicGeometry.inverseImageOpenLocalizedToposEquivalence produces are both localizations at the sheafification of AlgebraicGeometry.openRepresentable'.

Still the two topoi only. The morphism of ringed topoi of Stacks 04IF therefore composes with these as a morphism of topoi and not yet as one of ringed topoi; what is missing is the comparison of the two structure sheaves, and this module's implementation notes record what that needs.

noncomputable def openRepresentableLocalizedToposEquivalence (V : S.Opens) :
    Sheaf (SmallEtale.topology B V.toScheme
        (Scheme.size_lt_of_isOpenImmersion V.ι hS)) (Type u) ≌
      (RingedTopos.localizedRingedTopos
        (RingedSite.toRingedTopos (smallEtaleRingedSite B S hS))
        ((presheafToSheaf (SmallEtale.topology B S hS) (Type u)).obj
          (openRepresentable'.{u, u} B S hS V))).Topos

AlgebraicGeometry.SmallEtale.openLocalizedRingedToposHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/RecoveringMorphisms/OpenLocalization.lean, line 449. The attribute's comment: “for an open subscheme V of S, as a morphism of RINGED topoi and at the AlgebraicGeometry.openRepresentable' spelling of the sheaf: the small étale ringed topos of V IS the localization of the small étale ringed topos of S at the sheaf V represents, structure sheaves included. It is 04IE at the representable spelling (AlgebraicGeometry.SmallEtale.localizedRingedToposHom, whose identification of the topoi is a restriction along a functor of sites, which is what makes the structure sheaves comparable) followed by the transport of a localization along an isomorphism of sheaves (AlgebraicGeometry.RingedTopos.localizedRingedToposHomOfIso). This is the spelling Stacks 04IF's half of input (1) of the Zariski gluing of 04I7 localizes at, so with it that input is closed”.

Stacks 04IE for an open subscheme, as a morphism of ringed topoi, at the AlgebraicGeometry.openRepresentable' spelling. The small étale ringed topos of an open subscheme V of S is the localization of the small étale ringed topos of S at the sheaf V represents — structure sheaves included, and at the spelling of that sheaf which Stacks 04IF's half of input (1) of the Zariski gluing of Stacks 04I7 localizes at.

It is AlgebraicGeometry.SmallEtale.localizedRingedToposHom, which is Stacks 04IE at the representable spelling, followed by AlgebraicGeometry.RingedTopos.localizedRingedToposHomOfIso along AlgebraicGeometry.SmallEtale.openRepresentableSheafIso. With it, the target of AlgebraicGeometry.localizedOverOpen and the source AlgebraicGeometry.inverseImageOpenLocalizedToposEquivalence produces are both identified with small étale ringed topoi of opens, as morphisms of ringed topoi, and input (1) is closed.

Universes. AlgebraicGeometry.RingedToposHom.comp elaborates its own nine universe parameters before its arguments, and the three belonging to the source default to zero if left to be inferred; they are supplied positionally, in the order comp.{Xv, Xu, Xw, Yv, Yu, Yw, Zv, Zu, Zw} that pp.universes reports, with the two localizations' object universe written max (u + 1) u. Annotating the argument, let-binding it with its type written out, and by exact all come too late.

def openLocalizedRingedToposHom (V : S.Opens) :
    RingedToposHom (RingedSite.toRingedTopos (smallEtaleRingedSite B V.toScheme
        (Scheme.size_lt_of_isOpenImmersion V.ι hS)))
      (RingedTopos.localizedRingedTopos.{u, u + 1}
        (RingedSite.toRingedTopos (smallEtaleRingedSite B S hS))
        ((presheafToSheaf (SmallEtale.topology B S hS) (Type u)).obj
          (openRepresentable'.{u, u} B S hS V)))

AlgebraicGeometry.SmallEtale.elementSiteSheafEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/RecoveringMorphisms/SmallEtaleElementSite.lean, line 283. The attribute's comment: “for the small étale site of an object U of the small étale site of S, with the identification given as restriction along a functor of sites: the small étale topos of the scheme of U is the topos of the localization of the small étale ringed topos of S at the sheaf U represents. The functor of sites is the equivalence of the small étale site of the scheme of U with the slice at U, followed by the identification of that slice with the site of elements of the represented sheaf, which is available because the small étale topology is subcanonical; the comparison of the two topologies is AlgebraicGeometry.SmallEtale.functorPushforward_mem_elementTopology_iff”.

Stacks 04IE for the small étale site, on the topoi, by restriction along a functor of sites. The small étale topos of the scheme of U is the topos of the localization of the small étale ringed topos of S at the sheaf U represents, and the identification is restriction along AlgebraicGeometry.SmallEtale.toElementSite.

That it is a restriction, and not merely an equivalence, is the whole point: the three topos-level forms in StacksFrontier/AlgebraicGeometry/EtaleCohomology/RecoveringMorphisms/OpenLocalization.lean factor through Stacks 00Y1, whose functor is a lower shriek, and so carry no comparison of structure sheaves; this one does, and the comparison is AlgebraicGeometry.SmallEtale.sheafPushforward_localizedRingedTopos_O.

def elementSiteSheafEquivalence :
    Sheaf (SmallEtale.topology B U.obj.left.obj U.obj.left.property) (Type u) ≌
      (RingedTopos.localizedRingedTopos.{u, u + 1}
        (RingedSite.toRingedTopos (smallEtaleRingedSite B S hS))
        (representableSheaf B S hS U)).Topos

AlgebraicGeometry.SmallEtale.sheafPushforward_localizedRingedTopos_O, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/RecoveringMorphisms/SmallEtaleElementSite.lean, line 312. The attribute's comment: “the comparison of the two structure sheaves, for the small étale site: the structure sheaf of the localization of the small étale ringed topos of S at the sheaf an object U represents, restricted along the functor of sites identifying the small étale site of the scheme of U with the site of elements, IS the structure sheaf of the small étale site of the scheme of U. An equality of sheaves of commutative rings, both being the restriction of the structure sheaf of S along post-composition with the structure morphism of U”.

The structure sheaf of the localization, restricted to the small étale site of the scheme of U, is its structure sheaf. This is the cheap presheaf identity, and it is an equality: the structure sheaf of the localization is the restriction of 𝒪_S along the projection from the site of elements, restricting that along toElementSite restricts along the composite (AlgebraicGeometry.SmallEtale.toElementSite_comp_elementProjection), the composite is AlgebraicGeometry.SmallEtale.postcompose, and AlgebraicGeometry.SmallEtale.commRingStructurePresheaf is (SmallEtale.toScheme B S hS).op ⋙ Scheme.Γ, which postcompose leaves alone.

This is the comparison that the topos-level forms of Stacks 04IE do not carry, and the reason this route was taken.

theorem sheafPushforward_localizedRingedTopos_O :
    ((toElementSite B S hS U).sheafPushforwardContinuous CommRingCat.{u}
        (SmallEtale.topology B U.obj.left.obj U.obj.left.property)
        (RingedTopos.elementTopology.{u, u + 1}
          (RingedSite.toRingedTopos (smallEtaleRingedSite B S hS))
          (representableSheaf B S hS U))).obj
      (RingedTopos.localizedRingedTopos.{u, u + 1}
        (RingedSite.toRingedTopos (smallEtaleRingedSite B S hS))
        (representableSheaf B S hS U)).O =
    SmallEtale.commRingStructureSheaf B U.obj.left.obj U.obj.left.property

AlgebraicGeometry.SmallEtale.localizedRingedToposHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/RecoveringMorphisms/SmallEtaleElementSite.lean, line 419. The attribute's comment: “for the small étale site, as a morphism of RINGED topoi: the small étale ringed topos of the scheme of an object U of the small étale site of S is the localization of the small étale ringed topos of S at the sheaf U represents, structure sheaves included. The morphism of topoi is restriction along the functor of sites identifying the small étale site of the scheme of U with the site of elements of that sheaf, and the structure map is the adjunct of the comparison of the two structure sheaves, which is an isomorphism because the comparison is — the two structure sheaves being equal, both the restriction of the structure sheaf of S along post-composition with the structure morphism of U”.

Stacks 04IE for the small étale site, as a morphism of ringed topoi. The small étale ringed topos of the scheme of an object U of the small étale site of S is the localization of the small étale ringed topos of S at the sheaf U represents — structure sheaves included.

The morphism of topoi is the identification of the two topoi, an equivalence; the structure map is the adjunct of AlgebraicGeometry.SmallEtale.localizedStructureSheafIso, so it is an isomorphism, and the two ringed topoi are identified and not merely compared.

def localizedRingedToposHom :
    RingedToposHom (RingedSite.toRingedTopos
        (smallEtaleRingedSite B U.obj.left.obj U.obj.left.property))
      (RingedTopos.localizedRingedTopos.{u, u + 1}
        (RingedSite.toRingedTopos (smallEtaleRingedSite B S hS))
        (representableSheaf B S hS U))

AlgebraicGeometry.RingedTopos.extensionByZeroPresheafSectionIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/ExtensionByZeroFormula.lean, line 384. The attribute's comment: “part (4): direct-sum formula”.

Stacks 04IE, part (4): the direct-sum formula. The sections over V of the presheaf-level lower shriek of G along the localization of X at F are the direct sum, over the sections s of F over V, of the sections of G at the element (V, s).

noncomputable def extensionByZeroPresheafSectionIso
    (G : SheafOfModules.{u} (localizedRingSheaf X F)) (V : X.C) :
    ((PresheafOfModules.pullback.{u}
      (F := elementProjection X F)
      (R := (Stacks.SheafOfModules.Tensor.ringSheaf X.O).obj)
      (S := (localizedRingSheaf X F).obj)
      (elementModuleRingPresheafHom X F)).obj G.val).obj (Opposite.op V) ≅
      (∐ extensionByZeroSummands X F G V)

AlgebraicGeometry.RingedTopos.extensionByZeroPresheafSectionIso_inv_ι, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/ExtensionByZeroFormula.lean, line 398. The attribute's comment: “part (4): canonical comparison on summands”.

The direct-sum comparison is the canonical one. On the summand indexed by a section s of F over V it is the component, at the element (V, s), of the unit of the adjunction between the presheaf-level lower shriek and restriction to the site of elements.

theorem extensionByZeroPresheafSectionIso_inv_ι
    (G : SheafOfModules.{u} (localizedRingSheaf X F)) (V : X.C)
    (s : F.obj.obj (Opposite.op V)) :
    HEq (Limits.Sigma.ι (extensionByZeroSummands X F G V) s ≫
      (extensionByZeroPresheafSectionIso X F G V).inv)
      (((PresheafOfModules.pullbackPushforwardAdjunction.{u}
        (F := elementProjection X F)
        (R := (Stacks.SheafOfModules.Tensor.ringSheaf X.O).obj)
        (S := (localizedRingSheaf X F).obj)
        (elementModuleRingPresheafHom X F)).unit.app G.val).app
          (Opposite.op
            (CostructuredArrow.mk (yonedaEquiv.symm s) : elementSite X F)))

AlgebraicGeometry.RingedTopos.moduleRestriction_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/ExtensionByZeroFormula.lean, line 419. The attribute's comment: “part (2): module sections”.

Stacks 04IE, part (2): module sections. At an element (V, s) of F, the restriction of a sheaf of O-modules to the site of elements has precisely the sections of the original module over V.

theorem moduleRestriction_obj (G : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))
    (V : (elementSite X F)ᵒᵖ) :
    (((SheafOfModules.pushforward (F := elementProjection X F)
      (J := elementTopology X F) (K := X.J)
      (elementModuleRingHom X F)).obj G).val.obj V : Type u) =
      (G.val.obj (Opposite.op ((elementProjection X F).obj V.unop)) : Type u)

AlgebraicGeometry.RingedTopos.localizationModulePullbackIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/ModulePullback.lean, line 133. The attribute's comment: “part (2): inverse image on modules”.

Stacks 04IE, part (2): the inverse image on modules. Pullback of sheaves of modules along the localization morphism — the inverse image of Stacks 03D2 followed by extension of scalars along the structure map — is restriction to the site of elements of F.

noncomputable def localizationModulePullbackIso :
    (localizationMorphism X F).toRingedToposModulesHom.pullbackModules ≅
      SheafOfModules.pushforward (F := elementProjection X F)
        (J := elementTopology X F) (K := X.J) (elementModuleRingHom X F)

AlgebraicGeometry.RingedTopos.extensionByZeroModules_adjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/ModulePullback.lean, line 170. The attribute's comment: “part (2) and part (4): module adjunction”.

Stacks 04IE, parts (2) and (4): the module adjunction. On sheaves of modules the lower shriek of the localization is left adjoint to pullback along the localization morphism.

noncomputable def extensionByZeroModules_adjunction :
    SheafOfModules.pullback.{u}
      (F := elementProjection X F) (J := elementTopology X F) (K := X.J)
      (elementModuleRingHom X F) ⊣
      (localizationMorphism X F).toRingedToposModulesHom.pullbackModules

AlgebraicGeometry.RingedTopos.localizationEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/SliceEquivalence.lean, line 122. The attribute's comment: “equivalence with the slice topos”.

The canonical equivalence between the localization of X at F and the slice topos Sh(C)/F: the equivalence supplied by Stacks 0791, whose inverse is the fibre construction recorded in localizationEquivalence_fibers.

noncomputable def localizationEquivalence : (localizedRingedTopos X F).Topos ≌ Over F

AlgebraicGeometry.RingedTopos.localizationEquivalence_fibers, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/SliceEquivalence.lean, line 129. The attribute's comment: “canonical identification with the slice topos”.

The equivalence with the slice topos is the canonical fibre construction: on underlying presheaves its inverse sends an object φ : G ⟶ F of Sh(C)/F to the presheaf (U, s) ↦ {t ∈ G(U) | φ(t) = s} on the site of elements of F.

noncomputable def localizationEquivalence_fibers :
    (localizationEquivalence X F).inverse ⋙
      sheafToPresheaf (elementTopology X F) (Type v) ≅
      Over.post (X := F) (sheafToPresheaf X.J (Type v)) ⋙
        (overEquivPresheafCostructuredArrow F.obj).functor

AlgebraicGeometry.RingedTopos.localizationShriekAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/SliceEquivalence.lean, line 143. The attribute's comment: “part (3): lower shriek on sets”. References: SGA 4 III (5.5), “Clause 3”.

The lower shriek of the localization on sheaves of sets is Over.forget F: read through the equivalence with the slice topos, the left adjoint of the inverse image of the localization morphism is the forgetful functor from Sh(C)/F.

This is the adjunction of Stacks 0791 for the same equivalence as localizationEquivalence_fibers, which is what pins the comparisons built from it down.

noncomputable def localizationShriekAdjunction :
    (localizationEquivalence X F).functor ⋙ Over.forget F ⊣
      (localizationMorphism X F).toToposHom.inverseImage

AlgebraicGeometry.RingedTopos.localizationInverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/SliceEquivalence.lean, line 158. The attribute's comment: “part (1): inverse image”. References: SGA 4 IV (5.2).

The inverse image of the localization is product with F: read through the equivalence with the slice topos, the inverse image of the localization morphism is toOver F, which sends a sheaf G to the product G × F viewed as an object over F.

noncomputable def localizationInverseImageIso :
    (localizationMorphism X F).toToposHom.inverseImage ⋙
      (localizationEquivalence X F).functor ≅ toOver F

AlgebraicGeometry.RingedTopos.forget_localizationInverseImageIso_hom_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/SliceEquivalence.lean, line 174. The attribute's comment: “part (1): the comparison is the one the lower shriek prescribes”.

The comparison of the inverse image with toOver F is the one the lower shriek prescribes: the component of localizationInverseImageIso at a sheaf G, followed by the projection G × F ⟶ G, is the counit of the lower shriek adjunction at G.

This is what localizationInverseImageIso means, and it is a statement only because the equivalence and the adjunction come from one package: for an unrelated adjunction the two sides are morphisms that nothing relates. With localizationInverseImageIso_eq it pins the comparison down completely.

theorem forget_localizationInverseImageIso_hom_app (G : X.Topos) :
    (Over.forget F).map ((localizationInverseImageIso X F).hom.app G) ≫
        (forgetAdjToOver F).counit.app G =
      (localizationShriekAdjunction X F).counit.app G

AlgebraicGeometry.RingedTopos.localizationInverseImageIso_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/SliceEquivalence.lean, line 204. The attribute's comment: “part (1): the comparison is unique”.

The comparison of the inverse image with toOver F is unique: an isomorphism of j⁻¹ ⋙ E.functor with toOver F whose components are, after the projection G × F ⟶ G, the counit of the lower shriek adjunction is localizationInverseImageIso.

A morphism into toOver F over F is determined by its composite with that projection, its composite with the other one being its structure morphism — which is CategoryTheory.Iso.ext_of_left_comp_forgetAdjToOver_counit. Together with forget_localizationInverseImageIso_hom_app this is what makes the comparison of a relocalization with base change computable: it is enough to exhibit one isomorphism with the right counits.

theorem localizationInverseImageIso_eq
    (Ψ : (localizationMorphism X F).toToposHom.inverseImage ⋙
      (localizationEquivalence X F).functor ≅ toOver F)
    (h : ∀ G : X.Topos, (Over.forget F).map (Ψ.hom.app G) ≫ (forgetAdjToOver F).counit.app G =
      (localizationShriekAdjunction X F).counit.app G) :
    Ψ = localizationInverseImageIso X F

AlgebraicGeometry.RingedTopos.fibreTranspose_shriek_counit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/SliceEquivalence.lean, line 327. The attribute's comment: “part (1): the fibre transpose of the lower shriek counit”.

The fibre transpose of the lower shriek counit is the unit of the equivalence. Both morphisms E⁻¹(E(j⁻¹G)) ⟶ j⁻¹G agree on fibre sections, by CategoryTheory.Presheaf.IsSheaf.app_fibers_inv_comp_homEquiv_shriek and by CategoryTheory.Presheaf.IsSheaf.app_fibers_inv_comp_unitInv; the fibre identification is an isomorphism, so they are equal.

This is the functor-level form of Stacks 0791's bridge between the fibre description of the equivalence and the counit of j_!, and it is what lets a comparison built from fibres be compared with the counit.

theorem fibreTranspose_shriek_counit (G : X.Topos) :
    fibreTranspose X F ((localizationEquivalence X F).functor.obj
          ((X.localizationMorphism F).toToposHom.inverseImage.obj G)) G
        ((X.localizationShriekAdjunction F).counit.app G) =
      (localizationEquivalence X F).unitInv.app
        ((X.localizationMorphism F).toToposHom.inverseImage.obj G)

AlgebraicGeometry.RingedTopos.localizedRingedTopos, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/ToposLocalization.lean, line 153. The attribute's comment: “the localized ringed topos”. References: SGA 4 IV (11.2.1), “(E/X, A|X)”.

The localization of the ringed topos X at the sheaf F: the site of elements of F, with the restricted topology, and with the restriction of O along the projection as structure sheaf.

noncomputable abbrev localizedRingedTopos : RingedTopos.{v, max u v, v}

AlgebraicGeometry.RingedTopos.localizationMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/ToposLocalization.lean, line 188. The attribute's comment: “canonical morphism of ringed topoi”. References: SGA 4 IV (11.2.1), “localization morphism”.

The localization as a morphism of ringed topoi: the morphism of topoi above, with the identification of the inverse image of O with the localized structure sheaf as structure map.

noncomputable def localizationMorphism :
    RingedToposHom (localizedRingedTopos X F) X

Declarations registered for the tag:

SheafOfModules.pushforward registered with add_to_stacks in StacksFrontier/CategoryTheory/Sites/Modules/Localization/ModulePullback.lean, line 180 (StacksFrontier): “part (2): restriction of modules”. 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”.
SheafOfModules.pullback registered with add_to_stacks in StacksFrontier/CategoryTheory/Sites/Modules/Localization/ModulePullback.lean, line 189 (StacksFrontier): “part (4): lower shriek on modules”. References: EGA IV (11.9.16), “more general”; EGA IV (2.5.1), “partial”; EGA IV (4.8.2), “more general”; EGA IV (9.4.9); SGA 3 I (4.6.1), “more general”; SGA 3 III (0.1.4), “more general”; SGA 4 VI (8.7.1), “partial”; SGA 4 XVII (4.1); SGA 7 XIV (4.5), “more general”.
SheafOfModules.pullbackIso registered with add_to_stacks in StacksFrontier/CategoryTheory/Sites/Modules/Localization/ModulePullback.lean, line 190 (StacksFrontier): “part (4): sheafification”.

Tag 04J2, a definition

Tag 04J2 in the Stacks Project.

AlgebraicGeometry.RingedTopos.localizedRingedTopos, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/ToposLocalization.lean, line 153. The attribute's comment: “part (1): the localization of the ringed topos at F”. References: SGA 4 IV (11.2.1), “(E/X, A|X)”.

The localization of the ringed topos X at the sheaf F: the site of elements of F, with the restricted topology, and with the restriction of O along the projection as structure sheaf.

noncomputable abbrev localizedRingedTopos : RingedTopos.{v, max u v, v}

AlgebraicGeometry.RingedTopos.localizationMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/ToposLocalization.lean, line 188. The attribute's comment: “part (2): the localization morphism”. References: SGA 4 IV (11.2.1), “localization morphism”.

The localization as a morphism of ringed topoi: the morphism of topoi above, with the identification of the inverse image of O with the localized structure sheaf as structure map.

noncomputable def localizationMorphism :
    RingedToposHom (localizedRingedTopos X F) X

Tag 04J3, a lemma

Tag 04J3 in the Stacks Project.

AlgebraicGeometry.RingedSite.left_representableLocalizationForwardInverseImageIso_hom_app_comp_counit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/RepresentableLocalization.lean, line 285. The attribute's comment: “part (2): the comparison of inverse images, read through the lower shriek”.

Stacks 04J3's comparison of inverse images, read through the lower shriek. The comparison of the two inverse images in the direction of the slice topos, read through Over.forget and followed by the lower shriek counit of the localization at h_U^#, is Stacks 00Y1's identification of Φ_U ⋙ Over.forget with j_{U!} followed by the lower shriek counit of the localization at U.

This is the statement that connects the two lower shrieks the comparison of Stacks 04J3 sits between — that of the slice site C/U and that of the localization of the ringed topos at h_U^# — and it is what lets an equation built from one be compared with an equation built from the other after transposing across j_{U!}.

Each of the two factors of representableLocalizationForwardInverseImageIso contributes one step, and each step is already proved: Stacks 04IQ's comparison read through Over.forget and followed by the first projection is Stacks 00Y1's identification followed by the slice-site counit (CategoryTheory.OverShriek.left_overPullbackCompSheafFunctorToOverIso_hom_app_comp_fst); and Stacks 04IE's comparison carries the projection to the localization counit (RingedTopos.forget_localizationInverseImageIso_inv_app), whose right-hand side is that first projection.

The step that replaces a factor inside the composite is taken by rw rather than by an explicit congrArg: a congrArg against a hand-written fun z => z ≫ _ has to have its own spelling of the composite identified with the goal's, and that identification unfolds the body of localizationShriekAdjunction — the equation is the same, and the proof is five times the elaborator's budget. rw substitutes into the goal's own term, so no such identification arises.

theorem left_representableLocalizationForwardInverseImageIso_hom_app_comp_counit
    (A : Sheaf X.J (Type u)) :
    ((representableLocalizationForwardInverseImageIso X U).hom.app A).left ≫
        (X.ringedTopos.localizationShriekAdjunction (representableSheaf X U)).counit.app A =
      (CategoryTheory.OverShriek.sheafFunctorToOverForgetIso X.J).hom.app
          ((X.J.overPullback (Type u) U).obj A) ≫
        ((Over.forget U).sheafAdjunctionContinuous (Type u) (X.J.over U) X.J).counit.app A

AlgebraicGeometry.RingedSite.representableLocalizationInverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/RepresentableLocalization.lean, line 313. The attribute's comment: “part (2): canonical comparison of inverse images”.

The canonical comparison of the two inverse images: the inverse image of the localization at h_U^#, read through the identification of the two localized topoi, is the inverse image of the localization at U. This is the previous comparison transported across the unit of Stacks 00Y1's equivalence, so it is not an arbitrary isomorphism.

noncomputable def representableLocalizationInverseImageIso :
    (RingedTopos.localizationMorphism X.ringedTopos
          (representableSheaf X U)).toToposHom.inverseImage ⋙
        (representableLocalizationEquivalence X U).inverse ≅
      (X.localizationCommRingedToposHom U).toToposHom.inverseImage

AlgebraicGeometry.RingedSite.shriek_representableLocalizationInverseImageIso_hom_app_comp_counit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/RepresentableLocalization.lean, line 390. The attribute's comment: “part (2): the comparison of inverse images after the unit cancellation, read through the lower shriek”.

Stacks 04J3's comparison of inverse images, read through the lower shriek. Applying j_{U!} to the comparison and following it by the counit of j_{U!} ⊣ j_U^{-1} is Stacks 00Y1's identification of j_{U!}Phi_U^{-1} with Over.forget followed by the counit of the lower shriek of the localization at h_U^#.

This is the form of Stacks 04J3's comparison that an equation transposed across j_{U!} consumes: on one side of such an equation the lower shriek is the slice site's, on the other it is the localization's, and nothing but this lemma relates them. It is the comparison after the cancellation of Stacks 00Y1's unit, so it applies to representableLocalizationInverseImageIso itself rather than to the comparison in the slice direction that it is built from.

The three steps are shriek_sheafEquivalence_unitInv for the cancelled unit, the naturality of CategoryTheory.OverShriek.inverseCompShriekIso, and left_representableLocalizationForwardInverseImageIso_inv_app_comp_counit for the comparison in the slice direction.

The last of those is whiskered on by CategoryTheory.whisker_eq with the whiskering morphism left to unification: written as a congrArg against an explicit fun z => _ ≫ z, the step alone takes the whole of the elaborator's budget, because the lambda's spelling of the comparison has to be identified with the goal's and that unfolds the body of localizationShriekAdjunction.

theorem shriek_representableLocalizationInverseImageIso_hom_app_comp_counit
    (A : Sheaf X.J (Type u)) :
    ((Over.forget U).sheafPullback (Type u) (X.J.over U) X.J).map
          ((representableLocalizationInverseImageIso X U).hom.app A) ≫
        ((Over.forget U).sheafAdjunctionContinuous (Type u) (X.J.over U) X.J).counit.app A =
      (CategoryTheory.OverShriek.inverseCompShriekIso X.J).hom.app
          ((X.ringedTopos.localizationEquivalence (representableSheaf X U)).functor.obj
            ((X.ringedTopos.localizationMorphism
              (representableSheaf X U)).toToposHom.inverseImage.obj A)) ≫
        (X.ringedTopos.localizationShriekAdjunction (representableSheaf X U)).counit.app A

AlgebraicGeometry.RingedSite.representableLocalizationStructureSheafIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/RepresentableLocalization.lean, line 485. The attribute's comment: “part (1): canonical structure-sheaf comparison”.

The canonical comparison of the two structure sheaves. Read through the identification of the two localized topoi, the structure sheaf of the localization at h_U^# is the structure sheaf O|_U of the localization at U: the inverse image of the former along the identification is the inverse image of O along the composite, which the lift above identifies with the inverse image of O along the localization at U, which is O|_U.

noncomputable def representableLocalizationStructureSheafIso :
    (inverseImageCommRingFunctor (representableLocalizationToposMorphism X U)).obj
        (RingedTopos.localizedRingedTopos X.ringedTopos (representableSheaf X U)).O ≅
      (X.over U).ringedTopos.O

AlgebraicGeometry.RingedSite.representableLocalizationRingInverseImageIso_existsUnique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/RepresentableLocalization.lean, line 540. The attribute's comment: “part (2): canonical comparison on ring sheaves”.

The comparison of inverse images lifts uniquely to sheaves of commutative rings. For the composite of the localization at h_U^# with the identification of the two localized topoi, and for the localization at U, there is exactly one isomorphism of their inverse images of sheaves of commutative rings whose underlying map of sheaves of sets is the canonical comparison.

theorem representableLocalizationRingInverseImageIso_existsUnique :
    ∃! β : inverseImageCommRingFunctor.{u, u, u, u, u, u}
        ((RingedTopos.localizationMorphism X.ringedTopos (representableSheaf X U)).comp
          (representableLocalizationRingedMorphism X U)).toToposHom ≅
        inverseImageCommRingFunctor.{u, u, u, u, u, u}
          (X.localizationCommRingedToposHom U).toToposHom,
      ∀ R : Sheaf X.J CommRingCat.{u},
        (sheafCompose (X.J.over U) (forget CommRingCat.{u})).map (β.hom.app R) =
          (representableLocalizationInverseImageIso X U).hom.app
            ((sheafCompose X.J (forget CommRingCat.{u})).obj R)

AlgebraicGeometry.RingedSite.representableLocalizationMorphism_compare, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/StructureSheafComparison.lean, line 297. The attribute's comment: “part (2): compatibility of localization structure maps”.

The two localizations have the same structure map, under the canonical comparison of their inverse images of sheaves of commutative rings. This is the last compatibility of Stacks 04J3: the identification of the two localized ringed topoi is compatible with their structure maps, so it is an identification of localizations and not merely of topoi.

theorem representableLocalizationMorphism_compare :
    (representableLocalizationRingInverseImageIso X U).inv.app X.O ≫
        ((RingedTopos.localizationMorphism X.ringedTopos (representableSheaf X U)).comp
          (representableLocalizationRingedMorphism X U)).fSharpInverseImage =
      (X.localizationCommRingedToposHom U).fSharpInverseImage

Tag 04J4, a lemma

Tag 04J4 in the Stacks Project.

Stacks.Sheaves.LocalizedRingedTopos.OverSite.elementPostcomp_isCocontinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/PushforwardRightExact.lean, line 595. The attribute's comment: “cocontinuity of postcomposition”.

Stacks 04J4, cocontinuity of postcomposition.

public theorem elementPostcomp_isCocontinuous (s : G ⟶ F) :
    (elementPostcomp s).IsCocontinuous (elementTopology G) (elementTopology F)

Stacks.Sheaves.LocalizedRingedTopos.OverSite.elementPostcomp_isContinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/PushforwardRightExact.lean, line 639. The attribute's comment: “continuity of postcomposition”.

Stacks 04J4, continuity of postcomposition.

public theorem elementPostcomp_isContinuous (s : G ⟶ F) :
    (elementPostcomp s).IsContinuous (elementTopology G) (elementTopology F)

Stacks.Sheaves.LocalizedRingedTopos.elementPostcomp_isCocontinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/PushforwardRightExact.lean, line 730. The attribute's comment: “cocontinuity of postcomposition”.

Stacks 04J4, cocontinuity of postcomposition. The tag is registered on OverSite.elementPostcomp_isCocontinuous, which states the same thing over a bare site.

public theorem elementPostcomp_isCocontinuous (s : G ⟶ F) :
    (elementPostcomp s).IsCocontinuous (elementTopology X G) (elementTopology X F)

Stacks.Sheaves.LocalizedRingedTopos.elementPostcomp_isContinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/PushforwardRightExact.lean, line 747. The attribute's comment: “continuity of postcomposition”.

Stacks 04J4, continuity of postcomposition. The tag is registered on OverSite.elementPostcomp_isContinuous, which states the same thing over a bare site.

public theorem elementPostcomp_isContinuous (s : G ⟶ F) :
    (elementPostcomp s).IsContinuous (elementTopology X G) (elementTopology X F)

CategoryTheory.Functor.preservesFiniteLimits_sheafPushforwardContinuous, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/Relocalization.lean, line 90. The attribute's comment: “left exactness of relocalization”. References: SGA 4 III (1.8), “partial”; SGA 4½ Arcata (2.3.3), “more general”; SGA 7 VI (3.1(a)), “partial”.

Stacks 04J4, left exactness of relocalization: restriction of sheaves along a continuous functor of sites is left exact. For the relocalization of a topos at a morphism of sheaves G ⟶ F the continuous functor is postcomposition with that morphism on the sites of elements, and this is the left exactness that makes the relocalization a morphism of topoi.

noncomputable instance preservesFiniteLimits_sheafPushforwardContinuous [HasFiniteLimits A] :
    PreservesFiniteLimits (F.sheafPushforwardContinuous A J K)

Stacks.Sheaves.LocalizedRingedTopos.relocalizationToposMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/RelocalizationRingedTopos.lean, line 137. The attribute's comment: “the relocalization geometric morphism”.

Stacks 04J4, the geometric morphism of the relocalization. A morphism of sheaves s : G ⟶ F postcomposes sections, giving a functor between the sites of elements which is continuous and cocontinuous and whose restriction functor is left exact; those three facts are exactly the data of a morphism of topoi Sh(C/G) ⟶ Sh(C/F).

noncomputable def relocalizationToposMorphism (s : G ⟶ F) :
    MorphismOfTopoi (localizedRingedTopos X G).Topos (localizedRingedTopos X F).Topos

Stacks.Sheaves.LocalizedRingedTopos.comp_inverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/RelocalizationRingedTopos.lean, line 153. The attribute's comment: “the relocalization triangle of topoi, on inverse images”.

Stacks 04J4, the inverse-image half of the relocalization triangle: localizing at F and then relocalizing along s : G ⟶ F has the same inverse image as localizing at G directly, on the nose. Postcomposition with s leaves the underlying object of the site unchanged, so the two functors of sites to C are equal, and restriction along a composite is the composite of the restrictions.

theorem comp_inverseImage (s : G ⟶ F) :
    ((localizationToposMorphism X F).comp (relocalizationToposMorphism s)).inverseImage =
      (localizationToposMorphism X G).inverseImage

Stacks.Sheaves.LocalizedRingedTopos.relocalizationRingIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/RelocalizationRingedTopos.lean, line 197. The attribute's comment: “identification of the localized structure sheaves”.

Stacks 04J4, the identification of the localized structure sheaves: restricting the structure sheaf of the localization at F along postcomposition with s : G ⟶ F gives the structure sheaf of the localization at G. Both are the restriction of O along a projection from a site of elements and the two projections agree, so the identification is the identity isomorphism.

noncomputable def relocalizationRingIso (s : G ⟶ F) :
    (relocalizationRingInverseImage s).obj (localizedRingedTopos X F).O ≅
      (localizedRingedTopos X G).O

Stacks.Sheaves.LocalizedRingedTopos.relocalizationRingAdjunction_homEquiv_symm_fSharp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/RelocalizationRingedTopos.lean, line 214. The attribute's comment: “canonical structure-sheaf map”.

Stacks 04J4, the canonical structure-sheaf map: the structure map of the relocalization morphism, read in its inverse-image form f⁻¹O_F ⟶ O_G through the ring-level adjunction, is the canonical identification of the restriction of O_F with O_G.

theorem relocalizationRingAdjunction_homEquiv_symm_fSharp (s : G ⟶ F) :
    ((relocalizationRingAdjunction s).homEquiv _ _).symm (relocalizationFSharp s) =
      (relocalizationRingIso s).hom

Stacks.Sheaves.LocalizedRingedTopos.relocalization_inverseImage_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/RelocalizationSliceComparison.lean, line 199. The attribute's comment: “uniqueness of the comparison with base change on slice topoi”.

Stacks 04J4, the uniqueness half of the identification of the relocalization inverse image with base change. Fix an identification eF of the localization of X at F with the slice topos Sh(C)/F whose composite with Over.forget F is the lower shriek, i.e. is left adjoint to the inverse image of the localization morphism (the canonical such identification is sliceEquivalence, with shriekAdjunction). Then two isomorphisms of a functor P with eF ⋙ (base change along s) which agree after whiskering with the inverse image of the localization at F are equal.

P is arbitrary; the case of interest is P = (relocalization inverse image) ⋙ eG, for an identification eG of the localization at G with Sh(C)/G. The hypothesis on eF is used only through the faithfulness of the lower shriek.

theorem relocalization_inverseImage_unique (s : G ⟶ F)
    {eF : (localizedRingedTopos X F).Topos ≌ Over F}
    (adjF : eF.functor ⋙ Over.forget F ⊣ (localizationToposMorphism X F).inverseImage)
    {P : (localizedRingedTopos X F).Topos ⥤ Over G}
    {γ γ' : P ≅ eF.functor ⋙ Over.pullback s}
    (h : Functor.isoWhiskerLeft (localizationToposMorphism X F).inverseImage γ
      = Functor.isoWhiskerLeft (localizationToposMorphism X F).inverseImage γ') :
    γ = γ'

Stacks.Sheaves.LocalizedRingedTopos.relocalization_inverseImage_unique_of_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/RelocalizationSliceComparison.lean, line 215. The attribute's comment: “the comparison with base change is pinned down by the localization comparisons”.

Stacks 04J4, the uniqueness half in the shape of the source's ∃!: a comparison of the relocalization inverse image with base change is determined by a compatibility equation with the localization comparisons. Here Φ is the isomorphism against which the compatibility is stated and Ψ is the prescribed value; both are arbitrary, so this covers any choice of the comparison isomorphisms for the localizations at F and at G.

theorem relocalization_inverseImage_unique_of_eq (s : G ⟶ F)
    {eF : (localizedRingedTopos X F).Topos ≌ Over F}
    (adjF : eF.functor ⋙ Over.forget F ⊣ (localizationToposMorphism X F).inverseImage)
    {P : (localizedRingedTopos X F).Topos ⥤ Over G} {R : X.Topos ⥤ Over G}
    (Φ : (localizationToposMorphism X F).inverseImage ⋙ (eF.functor ⋙ Over.pullback s) ≅ R)
    (Ψ : (localizationToposMorphism X F).inverseImage ⋙ P ≅ R)
    {γ γ' : P ≅ eF.functor ⋙ Over.pullback s}
    (hγ : Functor.isoWhiskerLeft (localizationToposMorphism X F).inverseImage γ ≪≫ Φ = Ψ)
    (hγ' : Functor.isoWhiskerLeft (localizationToposMorphism X F).inverseImage γ' ≪≫ Φ = Ψ) :
    γ = γ'

AlgebraicGeometry.RingedTopos.relocalizationMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Recovery04IH/ToposRelocalization.lean, line 177. The attribute's comment: “the upper edge (j, j♯) of the relocalization triangle”.

Stacks 04J4. The relocalization morphism of ringed topoi attached to a morphism s : G ⟶ F of sheaves on a ringed topos: the morphism of topoi is restriction along postcomposition of sections, and the structure map is the canonical identification of the inverse image of the structure sheaf of the localization at F with that of the localization at G.

noncomputable def relocalizationMorphism (s : G ⟶ F) :
    RingedToposHom (localizedRingedTopos X G) (localizedRingedTopos X F)

AlgebraicGeometry.RingedTopos.relocalizationInverseImageSliceIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/RelocalizationBaseChange.lean, line 390. The attribute's comment: “the inverse image of the relocalization is base change on slice topoi”.

Stacks 04J4. The inverse image of the relocalization morphism along a morphism a : H ⟶ K of sheaves of sets, read through Stacks 04IE's identifications of the localization of X at H and at K with the slice topoi Sh(C)/H and Sh(C)/K, is base change along a.

This is relocalizationFibreIso transported across the two equivalences.

noncomputable def relocalizationInverseImageSliceIso (a : H ⟶ K) :
    (X.relocalizationMorphism a).toToposHom.inverseImage ⋙
        (localizationEquivalence X H).functor ≅
      (localizationEquivalence X K).functor ⋙ Over.pullback a

AlgebraicGeometry.RingedTopos.localizationInverseImageIso_eq_relocalization, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/RelocalizationBaseChange.lean, line 538. The attribute's comment: “the comparison with base change is the one the localization comparisons of 04IE prescribe”.

Stacks 04J4: the comparison with base change is the one the localization comparisons prescribe. Stacks 04IE identifies the inverse image of the localization at H with toOver H; that identification is localizationInverseImageIso X H, and this says it is the comparison with base change along a, whiskered with the inverse image of the localization at K, followed by Stacks 04IE at K and by the identification toOver K ⋙ Over.pullback a ≅ toOver H of Stacks 03EH.

With Stacks.Sheaves.LocalizedRingedTopos.relocalization_inverseImage_unique this is the full ∃! of the source: uniqueness holds for every choice of the two identifications, and here is the one solution for the canonical choice. The proof is localizationInverseImageIso_eq — the comparison is determined by its lower shriek counits — fed with forget_map_relocalizationInverseImageSliceIso_hom_app for the relocalization half, CategoryTheory.forget_map_toOverCompPullbackIso_hom_app for the Stacks 03EH half, and localizationInverseImageIso's own counit description at K.

theorem localizationInverseImageIso_eq_relocalization (a : H ⟶ K) :
    localizationInverseImageIso X H =
      Functor.isoWhiskerLeft (X.localizationMorphism K).toToposHom.inverseImage
          (X.relocalizationInverseImageSliceIso a) ≪≫
        Functor.isoWhiskerRight (localizationInverseImageIso X K) (Over.pullback a) ≪≫
          toOverCompPullbackIso a

AlgebraicGeometry.RingedTopos.localizationAtRelocalizationObjectInverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/RelocalizationObject.lean, line 141. The attribute's comment: “the localization at G/F has base change along s as its inverse image”. References: SGA 4 IV (5.2).

The inverse image of the localization at G/F. Read through the identification of Stacks 04IE of the localization of X at F with Sh(C)/F, and through the identification of the slice at G/F with Sh(C)/G, the inverse image of the localization morphism of (Sh(C)/F, O_F) at the object G/F is base change along s.

This is Stacks 04IR for the slice topos Sh(C)/F: the inverse image of a localization at an object is the product with that object (localizationInverseImageIso), and the product with G/F is base change along s (relocalizationStarIso).

noncomputable def localizationAtRelocalizationObjectInverseImageIso (s : G ⟶ F) :
    (localizationMorphism (X.localizedRingedTopos F)
            (X.relocalizationObject s)).toToposHom.inverseImage ⋙
        ((localizationEquivalence (X.localizedRingedTopos F)
            (X.relocalizationObject s)).functor ⋙
          (X.relocalizationSliceEquivalence s).functor) ≅
      (localizationEquivalence X F).functor ⋙ Over.pullback s

AlgebraicGeometry.RingedTopos.relocalizationObjectTriangleInverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/RelocalizationObject.lean, line 173. The attribute's comment: “the triangle whose upper edge is the localization at G/F commutes on inverse images”.

The relocalization triangle with the localization at G/F as its upper edge, on inverse images: the composite of the localization of (Sh(C)/F, O_F) at the object G/F with the localization morphism j_F, read through relocalizationObjectEquivalence, is the localization morphism j_G.

The inverse image of j_F is the product with F and that of j_G the product with G, both by Stacks 04IE; the inverse image of the localization at G/F is base change along s; and the product with F followed by base change along s is the product with G.

noncomputable def relocalizationObjectTriangleInverseImageIso (s : G ⟶ F) :
    ((X.localizationMorphism F).comp
          (localizationMorphism (X.localizedRingedTopos F)
            (X.relocalizationObject s))).toToposHom.inverseImage ⋙
        (X.relocalizationObjectEquivalence s).functor ≅
      (X.localizationMorphism G).toToposHom.inverseImage

AlgebraicGeometry.RingedTopos.relocalizationObjectTriangle_fSharpInverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/RelocalizationObject.lean, line 199. The attribute's comment: “the triangle commutes on structure maps, both of them being the identity”.

The relocalization triangle with the localization at G/F as its upper edge, on structure maps: both edges from the localization at G/F to X have the identity as their structure map on underlying sheaves of sets, so the triangle commutes as a triangle of ringed topoi and not merely of topoi.

Each of the three localization morphisms in the triangle has the identity as its structure map on underlying sheaves of sets, and the structure map of a composite is the restriction of the first factor's followed by the second factor's.

theorem relocalizationObjectTriangle_fSharpInverseImage (s : G ⟶ F) :
    ((X.localizedRingedTopos F).localizedRingedTopos
          (X.relocalizationObject s)).forgetRing.map
        ((X.localizationMorphism F).comp (localizationMorphism (X.localizedRingedTopos F)
          (X.relocalizationObject s))).fSharpInverseImage =
      𝟙 (((X.localizedRingedTopos F).localizedRingedTopos
            (X.relocalizationObject s)).forgetRing.obj
          ((X.localizedRingedTopos F).localizedRingedTopos (X.relocalizationObject s)).O) ∧
      (X.localizedRingedTopos G).forgetRing.map (X.localizationMorphism G).fSharpInverseImage =
        𝟙 ((X.localizedRingedTopos G).forgetRing.obj (X.localizedRingedTopos G).O)

AlgebraicGeometry.RingedTopos.relocalizationObjectInverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/RelocalizationObject.lean, line 237. The attribute's comment: “the localization at G/F and the relocalization have the same inverse image”.

The two relocalizations have the same inverse image. Read through relocalizationObjectEquivalence, the inverse image of the localization of (Sh(C)/F, O_F) at the object G/F is the inverse image of the relocalization morphism along s.

Both are base change along s on slice topoi — the first by localizationAtRelocalizationObjectInverseImageIso, the second by relocalizationInverseImageSliceIso — so the two agree once the equivalence at G is cancelled.

noncomputable def relocalizationObjectInverseImageIso (s : G ⟶ F) :
    (localizationMorphism (X.localizedRingedTopos F)
          (X.relocalizationObject s)).toToposHom.inverseImage ⋙
        (X.relocalizationObjectEquivalence s).functor ≅
      (X.relocalizationMorphism s).toToposHom.inverseImage

AlgebraicGeometry.RingedToposHom.toposRelocalizationTriangle, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/RelocalizedMorphismComparison.lean, line 463. The attribute's comment: “the relocalization triangle commutes as a triangle of ringed topoi”.

Stacks 04J4, commutativity of the relocalization triangle as a triangle of ringed topoi: (j_G, j_G♯) is (j_F, j_F♯) composed with the relocalization (j, j♯) along s.

The two inverse images are equal on the nose — restriction along postcomposition followed by restriction along the projection from the site of elements of F is restriction along the projection from the site of elements of G — and all three structure maps are identities on underlying sheaves of sets, so there is nothing left to check.

noncomputable def toposRelocalizationTriangle (W : RingedTopos.{u, u, u}) {H K : W.Topos}
    (a : H ⟶ K) :
    TwoIso (A := W.localizedRingedTopos H) (B := W)
      (W.localizationMorphism H)
      (comp (X := W.localizedRingedTopos H) (Y := W.localizedRingedTopos K) (Z := W)
        (W.localizationMorphism K) (W.relocalizationMorphism a))

AlgebraicGeometry.RingedToposHom.relocalizationCompTwoIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/RelocalizedNaturalitySquare.lean, line 105. The attribute's comment: “the relocalization morphisms of ringed topoi compose”.

Stacks 04J4: the relocalization morphisms of ringed topoi compose. Relocalizing along s : F ⟶ H after relocalizing along a : F' ⟶ F is relocalizing along a ≫ s.

noncomputable def relocalizationCompTwoIso (W : RingedTopos.{u, u, u}) {F' F H : W.Topos}
    (a : F' ⟶ F) (s : F ⟶ H) :
    TwoIso (A := W.localizedRingedTopos F') (B := W.localizedRingedTopos H)
      (comp (X := W.localizedRingedTopos F') (Y := W.localizedRingedTopos F)
        (Z := W.localizedRingedTopos H) (W.relocalizationMorphism s) (W.relocalizationMorphism a))
      (W.relocalizationMorphism (a ≫ s))

AlgebraicGeometry.RingedToposHom.relocalizationSquareTwoIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/RelocalizedNaturalitySquare.lean, line 139. The attribute's comment: “a commuting square of sheaves gives a commuting square of relocalization morphisms of ringed topoi”.

Stacks 04J4: a commuting square of sheaves gives a commuting square of relocalizations. For a ≫ s = s' ≫ c, relocalizing along s' and then along c agrees with relocalizing along a and then along s, as morphisms of ringed topoi.

noncomputable def relocalizationSquareTwoIso (W : RingedTopos.{u, u, u})
    {F' F H' H : W.Topos} (a : F' ⟶ F) (s : F ⟶ H) (s' : F' ⟶ H') (c : H' ⟶ H)
    (h : a ≫ s = s' ≫ c) :
    TwoIso (A := W.localizedRingedTopos F') (B := W.localizedRingedTopos H)
      (comp (X := W.localizedRingedTopos F') (Y := W.localizedRingedTopos H')
        (Z := W.localizedRingedTopos H) (W.relocalizationMorphism c)
        (W.relocalizationMorphism s'))
      (comp (X := W.localizedRingedTopos F') (Y := W.localizedRingedTopos F)
        (Z := W.localizedRingedTopos H) (W.relocalizationMorphism s)
        (W.relocalizationMorphism a))

Tag 04J5, a lemma

Tag 04J5 in the Stacks Project.

AlgebraicGeometry.RingedSite.representableRelocalizationInverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/RepresentableRelocalization.lean, line 194. The attribute's comment: “the two relocalizations have the same inverse image, via the identifications of 04J3”.

Stacks 04J5, on inverse images. Read through the identification of Stacks 04J3 of Sh(C/U) with the localization of the ringed topos at h_U^#, and through the identification of the localization at h_V^#/h_U^# with Sh(C/V), the inverse image of the localization of (Sh(C)/h_U^#, O_{h_U^#}) at the object h_V^#/h_U^# is the inverse image of the relocalization of the ringed site along f : V ⟶ U.

noncomputable def representableRelocalizationInverseImageIso {U V : X.C} (f : V ⟶ U) :
    (X.representableLocalizationEquivalence U).functor ⋙
        (RingedTopos.localizationMorphism
            (RingedTopos.localizedRingedTopos X.ringedTopos (representableSheaf X U))
            (representableRelocalizationObject X f)).toToposHom.inverseImage ⋙
          (representableRelocalizationEquivalence X f).functor ≅
      (X.relocalizationRingedToposHom f).toToposHom.inverseImage

AlgebraicGeometry.RingedSite.representableRelocalizationPushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/RepresentableRelocalization.lean, line 217. The attribute's comment: “the two relocalizations have the same direct image”.

Stacks 04J5, on direct images. Read through the same two identifications, the direct image of the localization of (Sh(C)/h_U^#, O_{h_U^#}) at h_V^#/h_U^# is the direct image of the relocalization of the ringed site along f : V ⟶ U. The two inverse images agree, so the two direct images agree by uniqueness of right adjoints.

noncomputable def representableRelocalizationPushforwardIso {U V : X.C} (f : V ⟶ U) :
    ((representableRelocalizationEquivalence X f).inverse ⋙
          (RingedTopos.localizationMorphism
            (RingedTopos.localizedRingedTopos X.ringedTopos (representableSheaf X U))
            (representableRelocalizationObject X f)).toToposHom.pushforward) ⋙
        (X.representableLocalizationEquivalence U).inverse ≅
      (X.relocalizationRingedToposHom f).toToposHom.pushforward

AlgebraicGeometry.RingedSite.representableRelocalization_fSharpSet, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/RepresentableRelocalization.lean, line 240. The attribute's comment: “the two maps j^sharp agree, both being the identity”.

Stacks 04J5, on structure maps: the two relocalizations have the same structure map j^♯, both being the identity on underlying sheaves of sets. For the localization of the ringed topos at h_V^#/h_U^# the structure sheaf is the restriction of O_{h_U^#} along the projection from the site of elements, and for the relocalization of the ringed site it is the restriction of O|_U along Over.map f; in both cases the structure map is the comparison of an inverse image with that restriction, which is the identity on sections.

theorem representableRelocalization_fSharpSet {U V : X.C} (f : V ⟶ U) :
    RingedToposHom.fSharpSet
          (RingedTopos.localizationMorphism
            (RingedTopos.localizedRingedTopos X.ringedTopos (representableSheaf X U))
            (representableRelocalizationObject X f)) =
        𝟙 ((RingedTopos.localizationMorphism
              (RingedTopos.localizedRingedTopos X.ringedTopos (representableSheaf X U))
              (representableRelocalizationObject X f)).toToposHom.inverseImage.obj
            ((RingedTopos.localizedRingedTopos X.ringedTopos
              (representableSheaf X U)).forgetRing.obj
                (RingedTopos.localizedRingedTopos X.ringedTopos (representableSheaf X U)).O)) ∧
      RingedToposHom.fSharpSet (X.relocalizationRingedToposHom f) =
        𝟙 ((X.relocalizationRingedToposHom f).toToposHom.inverseImage.obj
          ((ringedTopos (X.over U)).forgetRing.obj (X.over U).O))

AlgebraicGeometry.RingedSite.representableRelocalizationTwoIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/RepresentableRelocalizationRinged.lean, line 461. The attribute's comment: “the diagrams of 04IY and 04J4 agree via the identifications of 04J3, as a 2-isomorphism of morphisms of ringed topoi”.

The two upper edges agree, as a 2-isomorphism of morphisms of ringed topoi: the localization of (Sh(C)/h_U^#, O_{h_U^#}) at the object h_V^#/h_U^#, read through the identification of the localization at h_V^#/h_U^# with Sh(C/V), is the relocalization of the ringed site along f : V ⟶ U, read through the identification of Stacks 04J3 at U.

noncomputable def representableRelocalizationTwoIso :
    TwoIso (A := ringedTopos (X.over V)) (B := representableLocalizedRingedTopos X U)
      (AlgebraicGeometry.RingedToposHom.comp (X := ringedTopos (X.over V))
        (Y := representableRelocalizedRingedTopos X f)
        (Z := representableLocalizedRingedTopos X U)
        (RingedTopos.localizationMorphism (representableLocalizedRingedTopos X U)
          (representableRelocalizationObject X f))
        (representableRelocalizationRingedMorphism X f))
      (AlgebraicGeometry.RingedToposHom.comp (X := ringedTopos (X.over V))
        (Y := ringedTopos (X.over U)) (Z := representableLocalizedRingedTopos X U)
        (representableLocalizationRingedMorphism X U) (X.relocalizationRingedToposHom f))

AlgebraicGeometry.RingedSite.representableRelocalizationTriangleCompare, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/RepresentableRelocalizationRinged.lean, line 495. The attribute's comment: “the triangle of 04J4 at a representable is the triangle of 04IY, via the identifications of 04J3”.

The two relocalization triangles agree: the relocalization triangle of Stacks 04J4 at the morphism h_f^# : h_V^# ⟶ h_U^# of representable sheaves, read through the identifications of Stacks 04J3 at U and the identification of the localization at h_V^#/h_U^# with Sh(C/V), is the relocalization triangle of Stacks 04IY along f : V ⟶ U.

noncomputable def representableRelocalizationTriangleCompare :
    TwoIso (A := ringedTopos (X.over V)) (B := ringedTopos X)
      (AlgebraicGeometry.RingedToposHom.comp (X := ringedTopos (X.over V))
        (Y := representableLocalizedRingedTopos X U) (Z := ringedTopos X)
        (RingedTopos.localizationMorphism X.ringedTopos (representableSheaf X U))
        (AlgebraicGeometry.RingedToposHom.comp (X := ringedTopos (X.over V))
          (Y := representableRelocalizedRingedTopos X f)
          (Z := representableLocalizedRingedTopos X U)
          (RingedTopos.localizationMorphism (representableLocalizedRingedTopos X U)
            (representableRelocalizationObject X f))
          (representableRelocalizationRingedMorphism X f)))
      (X.localizationRingedToposHom V)

Sources

LeanStacks.Sheaves.LocalizedRingedTopos.sliceEquivalence · Stacks.Sheaves.LocalizedRingedTopos.shriekAdjunction · Stacks.Sheaves.LocalizedRingedTopos.sliceEquivalenceFibers · AlgebraicGeometry.SmallEtale.localizedToposEquivalence · AlgebraicGeometry.SmallEtale.openLocalizedToposEquivalence · AlgebraicGeometry.SmallEtale.openRepresentableLocalizedToposEquivalence · AlgebraicGeometry.SmallEtale.openLocalizedRingedToposHom · AlgebraicGeometry.SmallEtale.elementSiteSheafEquivalence

Section18.22 Localization of morphisms of ringed topoi #

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

Tag 04IF, a lemma

Tag 04IF in the Stacks Project.

AlgebraicGeometry.SmallEtale.localizedSmallModelMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Descent/AssociatedModule/SmallEtaleLocalizedMorphism.lean, line 89. The attribute's comment: “the localized morphism of ringed topoi of a morphism of the small étale ringed topoi of two schemes, obtained by transporting the morphism through the Type u equi-universe models of the two small étale ringed topoi, to which the statement at RingedTopos.{u, u, u} applies”.

Stacks 04IF for the small étale ringed topoi of schemes. Let ψ : (S_étale, 𝒪_S) ⟶ (T_étale, 𝒪_T) be a morphism of the small étale ringed topoi of two schemes of a big étale site and let G be a sheaf of sets on the equi-universe model of the target. This is the localized morphism of ringed topoi ψ' of Stacks 04IF, from the localization of the model of the source at the inverse image of G to the localization of the model of the target at G.

It is obtained by transport: ψ is conjugated by the comparisons of the two small étale ringed topoi with their equi-universe models — an equivalence of ringed topoi on each side, so nothing is lost — and Stacks 04IF is applied to the conjugate, whose two ringed topoi are AlgebraicGeometry.RingedTopos.{u, u, u}.

def localizedSmallModelMorphism
    (ψ : RingedToposHom (ringedTopos B S hS) (ringedTopos B T hT))
    (G : (smallModelRingedTopos B T hT).Topos) :
    RingedToposHom
      ((smallModelRingedTopos B S hS).localizedRingedTopos
        (letI : EssentiallySmall.{u} (ringedTopos B S hS).C := essentiallySmall B S hS
         letI : EssentiallySmall.{u} (ringedTopos B T hT).C := essentiallySmall B T hT
         (RingedToposHom.smallModelTransport.{u} ψ).toToposHom.inverseImage.obj G))
      ((smallModelRingedTopos B T hT).localizedRingedTopos G)

AlgebraicGeometry.localizedOverOpen, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/RecoveringMorphisms/OpenLocalization.lean, line 178. The attribute's comment: “the localization of a morphism of ringed topoi at the sheaf represented by an open subscheme V of the target, for the small étale ringed topoi of two schemes: the morphism of ringed topoi from the localization of the source at the inverse image of that sheaf to the localization of the target at it, with the structure map of 04IF. This is the instance of 04IF at RingedTopos.{u, u + 1, u}, the universes of the small étale ringed topos, which is what the Zariski gluing of 04I7 restricts along; it is not a morphism between the small étale ringed topoi of two open subschemes, that identification being 04IE for the étale site, which is not carried”.

Stacks 04IF for the small étale ringed topoi: the restriction of a morphism of ringed topoi to a pair of opens.

For schemes X and Y of a big étale site, a morphism of ringed topoi g : (Sh(X_étale), 𝒪_X) ⟶ (Sh(Y_étale), 𝒪_Y) and an open subscheme V of Y, this is the localization of g at the sheaf h_V^# represented by V: the morphism of ringed topoi
  (Sh(X_étale)/g⁻¹h_V^#, (𝒪_X)_{g⁻¹h_V^#}) ⟶ (Sh(Y_étale)/h_V^#, (𝒪_Y)_{h_V^#})
of Stacks 04IF, whose inverse image is (H ⟶ h_V^#) ↦ (g⁻¹H ⟶ g⁻¹h_V^#).

It carries no hypothesis beyond g and V: the essential smallness of the small étale site that Stacks 04IF's localization needs is the instance AlgebraicGeometry.SmallEtale.essentiallySmall. This is the first input of the Zariski gluing in the proof of Stacks 04I7; the identification of the source with the small étale ringed topos of the open subscheme of X representing g⁻¹h_V^# is Stacks 04IE for the étale site and is not carried here, so this is not yet that gluing's input in full.

def localizedOverOpen (X Y : B.Scheme)
    (g : RingedToposHom (RingedSite.toRingedTopos (smallEtaleRingedSite B X.obj X.property))
      (RingedSite.toRingedTopos (smallEtaleRingedSite B Y.obj Y.property)))
    (V : Y.obj.Opens) :
    RingedToposHom
      ((RingedSite.toRingedTopos (smallEtaleRingedSite B X.obj X.property)).localizedRingedTopos
        (g.toToposHom.inverseImage.obj
          ((presheafToSheaf (SmallEtale.topology B Y.obj Y.property) (Type u)).obj
            (openRepresentable'.{u, u} B Y.obj Y.property V))))
      ((RingedSite.toRingedTopos (smallEtaleRingedSite B Y.obj Y.property)).localizedRingedTopos
        ((presheafToSheaf (SmallEtale.topology B Y.obj Y.property) (Type u)).obj
          (openRepresentable'.{u, u} B Y.obj Y.property V)))

AlgebraicGeometry.Space.localizedSmallModelMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleLocalizedMorphism.lean, line 85. The attribute's comment: “the localized morphism of ringed topoi of a morphism of the small étale ringed topoi of two algebraic spaces, obtained by transporting the morphism through the Type u equi-universe models of the two small étale ringed topoi, to which the statement at RingedTopos.{u, u, u} applies”.

Stacks 04IF for the small étale ringed topoi of algebraic spaces. Let ψ : (X_étale, 𝒪_X) ⟶ (Y_étale, 𝒪_Y) be a morphism of the small étale ringed topoi of two algebraic spaces and let G be a sheaf of sets on the equi-universe model of the target. This is the localized morphism of ringed topoi ψ' of Stacks 04IF, from the localization of the model of the source at the inverse image of G to the localization of the model of the target at G.

It is obtained by transport: ψ is conjugated by the comparisons of the two small étale ringed topoi with their equi-universe models — an equivalence of ringed topoi on each side, so nothing is lost — and the library's Stacks 04IF is applied to the conjugate, whose two ringed topoi are AlgebraicGeometry.RingedTopos.{u, u, u}.

def localizedSmallModelMorphism
    (ψ : RingedToposHom (smallEtaleRingedTopos B S hS X) (smallEtaleRingedTopos B S hS Y))
    (G : (RingedTopos.smallModel.{u} (SmallEtale.topology B S hS Y.1)
      (structureSheaf B S hS Y.1 Y.2)).Topos) :
    RingedToposHom
      ((RingedTopos.smallModel.{u} (SmallEtale.topology B S hS X.1)
          (structureSheaf B S hS X.1 X.2)).localizedRingedTopos
        ((RingedToposHom.smallModelTransport.{u} ψ).toToposHom.inverseImage.obj G))
      ((RingedTopos.smallModel.{u} (SmallEtale.topology B S hS Y.1)
        (structureSheaf B S hS Y.1 Y.2)).localizedRingedTopos G)

Stacks.Sheaves.RingedToposModules.localizationCompPushforwardModulesIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/ModulePushforwardLocalization.lean, line 1011. The attribute's comment: “f'_ j_F^ = j_G^ f_, on sheaves of modules”.

Stacks 04IF, the clause f'_* j_F^* = j_G^* f_* on sheaves of modules. For a morphism of ringed topoi f : (Sh(C), O) ⟶ (Sh(D), O'), a sheaf of sets G on D and F = f^{-1}G, pulling a sheaf of O-modules back along the localization j_F and pushing it forward along the localized morphism f' is pushing it forward along f and pulling back along the localization j_G, naturally in the sheaf of modules.

Both pullbacks are the pullbacks of sheaves of modules of Stacks 03D6 part (2) along the localization morphisms, which Stacks 04IE part (2) (AlgebraicGeometry.RingedTopos.localizationModulePullbackIso) identifies with restriction to the site of elements; the comparison is therefore elementRestrictionCompPushforwardModulesIso conjugated by those two identifications.

noncomputable def localizationCompPushforwardModulesIso :
    RingedToposHom.pullbackModules.{uu, uu, uu, uu, uu, uu}
          (X := X.localizedRingedTopos (f.toToposHom.inverseImage.obj G)) (Y := X)
          (X.localizationMorphism
            (f.toToposHom.inverseImage.obj G)).toRingedToposModulesHom ⋙
        pushforwardModules.{uu, uu, uu, uu, uu, uu}
          (f.localized G).toRingedToposModulesHom ≅
      pushforwardModules.{uu, uu, uu, uu, uu, uu} f.toRingedToposModulesHom ⋙
        RingedToposHom.pullbackModules.{uu, uu, uu, uu, uu, uu}
          (X := Y.localizedRingedTopos G) (Y := Y)
          (Y.localizationMorphism G).toRingedToposModulesHom

AlgebraicGeometry.RingedToposHom.localizedRingedToposSquare, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/RelocalizedMorphismComparison.lean, line 504. The attribute's comment: “the square of 04IF as a 2-isomorphism of ringed topoi”.

Stacks 04IF: the square of Stacks 04IF as a 2-isomorphism of ringed topoi.

The comparison of inverse images is inverseImageCompLocalizationIso, and the compatibility of the three structure maps that it needs is localized_fSharpInverseImage_forget; the structure maps of the two localization morphisms are identities on underlying sheaves of sets, so they drop out of the two composites.

noncomputable def localizedRingedToposSquare (G : Y.Topos) :
    TwoIso (A := X.localizedRingedTopos (f.toToposHom.inverseImage.obj G)) (B := Y)
      (comp (X := X.localizedRingedTopos (f.toToposHom.inverseImage.obj G))
        (Y := Y.localizedRingedTopos G) (Z := Y)
        (Y.localizationMorphism G) (f.localized G))
      (comp (X := X.localizedRingedTopos (f.toToposHom.inverseImage.obj G)) (Y := X) (Z := Y)
        f (X.localizationMorphism (f.toToposHom.inverseImage.obj G)))

AlgebraicGeometry.RingedToposHom.localizedInverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/RingedToposMorphismLocalization.lean, line 275. The attribute's comment: “the characterization (f')^{-1}(H → G) = (f^{-1}H → F) of f'”.

Stacks 04IF, the rule characterizing f': read through the identifications of the two localizations with their slice topoi, the inverse image of f' is Over.post f⁻¹, that is
(f')⁻¹(H ⟶ G) = (f⁻¹H ⟶ f⁻¹G) .

noncomputable def localizedInverseImageIso :
    (localizedToposMorphism f G).inverseImage ⋙
        (X.localizationEquivalence (f.toToposHom.inverseImage.obj G)).functor ≅
      (Y.localizationEquivalence G).functor ⋙ Over.post f.toToposHom.inverseImage

AlgebraicGeometry.RingedToposHom.inverseImageCompLocalizationIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/RingedToposMorphismLocalization.lean, line 289. The attribute's comment: “commutativity of the square, on inverse images”.

Stacks 04IF, commutativity of the square on inverse images: f⁻¹ ⋙ j\_F⁻¹ = j\_G⁻¹ ⋙ (f')⁻¹. Concretely, the inverse image of a sheaf H on D, localized at F, is the inverse image under f' of H localized at G; this is Stacks 04H1's version of the same square, transported across the identifications of the localizations with their slice topoi.

noncomputable def inverseImageCompLocalizationIso :
    f.toToposHom.inverseImage ⋙
        (X.localizationMorphism (f.toToposHom.inverseImage.obj G)).toToposHom.inverseImage ≅
      (Y.localizationMorphism G).toToposHom.inverseImage ⋙
        (localizedToposMorphism f G).inverseImage

AlgebraicGeometry.RingedToposHom.localizationCompPushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/RingedToposMorphismLocalization.lean, line 315. The attribute's comment: “f'_ j_F^{-1} = j_G^{-1} f_, on sheaves of sets”.

Stacks 04IF: f'_* j_F⁻¹ = j_G⁻¹ f_*, on sheaves of sets.

This is Stacks 04H1's identity f'_* ∘ toOver F = toOver G ∘ f_* for the slice topoi, read through the identification of the inverse image of each localization morphism with toOver (Stacks 04IE part (1)) and through the two identifications of the localizations with their slice topoi.

noncomputable def localizationCompPushforwardIso :
    (X.localizationMorphism (f.toToposHom.inverseImage.obj G)).toToposHom.inverseImage ⋙
        (localizedToposMorphism f G).pushforward ≅
      f.toToposHom.pushforward ⋙ (Y.localizationMorphism G).toToposHom.inverseImage

AlgebraicGeometry.RingedToposHom.localized, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/RingedToposMorphismLocalization.lean, line 365. The attribute's comment: “the localized morphism of ringed topoi (f', (f')^sharp)”.

Stacks 04IF. The localized morphism of ringed topoi (f', (f')♯) : (Sh(C)/F, O_F) ⟶ (Sh(D)/G, O'_G), with F = f⁻¹G.

Its structure map is the restriction j_G⁻¹(f♯) of the structure map of f: the localized structure sheaf O'_G is the inverse image j_G⁻¹O', applying j_G⁻¹ to f♯ : O' ⟶ f_*O lands in j_G⁻¹f_*O, and that is f'_*j_F⁻¹O = f'_*O_F by localizedPushforwardCommRingIso.

noncomputable def localized :
    RingedToposHom (X.localizedRingedTopos (f.toToposHom.inverseImage.obj G))
      (Y.localizedRingedTopos G)

AlgebraicGeometry.RingedToposHom.localized_fSharpInverseImage_forget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/RingedToposMorphismLocalization.lean, line 730. The attribute's comment: “commutativity of the square as a square of ringed topoi: the comparison of inverse images is compatible with the structure maps”.

Stacks 04IF: the square of Stacks 04IF is a square of ringed topoi — the comparison of inverse images carries the structure map of f restricted to the site of elements of f⁻¹G to the structure map of the localized morphism.

This is the compatibility that commutativity of 04IF's square as a square of ringed topoi needs, in inverse-image form and on underlying sheaves of sets, and with it AlgebraicGeometry.RingedToposHom.TwoIso.ofInverseImageIso turns 04IF's comparison of inverse images into a 2-isomorphism of ringed topoi.

The proof is the adjointness the source omits. Both structure maps are adjunct to their direct-image forms (fSharpInverseImage_forget), the direct-image form of (f')♯ is j_G⁻¹(f♯) followed by the comparison of direct images (localized_fSharp_forget), and inverseImageCompLocalizationIso_hom_app_comp_counit says that 04IF's two comparisons are mates of each other; naturality of the comparison of inverse images at f♯ matches the two up.

theorem localized_fSharpInverseImage_forget :
    (f.inverseImageCompLocalizationIso G).hom.app (Y.forgetRing.obj Y.O) ≫
        (X.localizedRingedTopos (f.toToposHom.inverseImage.obj G)).forgetRing.map
          (f.localized G).fSharpInverseImage =
      (X.localizationMorphism (f.toToposHom.inverseImage.obj G)).toToposHom.inverseImage.map
        (X.forgetRing.map f.fSharpInverseImage)

Tag 04J7, a lemma

Tag 04J7 in the Stacks Project.

AlgebraicGeometry.RingedSite.Hom.localizedComparisonTwoIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/LocalizedRepresentableKey/TransposedComparison.lean, line 758. The attribute's comment: “the diagrams of 04J0 and 04IF agree via the identifications of 04J3, as a 2-isomorphism of morphisms of ringed topoi”.

Stacks 04J7. The diagrams of Stacks 04J0 and Stacks 04IF agree, via the identifications of Stacks 04J3: the square commutes: the composite j_V ∘ f'_{04J0} of the localization of the source at V with Stacks 04J0's localized morphism is 2-isomorphic to the composite f'_{04IF} ∘ compareMid of Stacks 04IF's localized morphism with Stacks 04D3's identification of the two localizations of the source.

The 2-isomorphism is Hom.localizedRepresentableCompInverseImageIso on inverse images; what makes it a 2-isomorphism of morphisms of ringed topoi is Hom.key, its compatibility with the two structure maps.

noncomputable def Hom.localizedComparisonTwoIso :
    AlgebraicGeometry.RingedToposHom.TwoIso
      (A := ringedTopos (X.over (f.u.obj V)))
      (B := RingedTopos.localizedRingedTopos Y.ringedTopos (representableSheaf Y V))
      (AlgebraicGeometry.RingedToposHom.comp.{u, u, u, u, u, u, u, u, u}
        (X := ringedTopos (X.over (f.u.obj V)))
        (Y := ringedTopos (Y.over V))
        (Z := RingedTopos.localizedRingedTopos Y.ringedTopos (representableSheaf Y V))
        (representableLocalizationRingedMorphism Y V)
        (f.localizedRingedToposHom V))
      (AlgebraicGeometry.RingedToposHom.comp.{u, u, u, u, u, u, u, u, u}
        (X := ringedTopos (X.over (f.u.obj V)))
        (Y := RingedTopos.localizedRingedTopos X.ringedTopos
          (f.inverseImageRepresentableSheaf V))
        (Z := RingedTopos.localizedRingedTopos Y.ringedTopos (representableSheaf Y V))
        (f.ringedToposHom.localized (representableSheaf Y V))
        (f.compareMid V))

AlgebraicGeometry.RingedSite.Hom.localizedRepresentableInverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/RepresentableMorphismLocalization.lean, line 299. The attribute's comment: “the two localized morphisms have the same inverse image, via the identifications of 04J3”.

Stacks 04J7, on inverse images. Read through the identifications of Stacks 04J3 of Sh(D/V) with the localization of the ringed topos at h_V^# and of Sh(C/U) with the localization at h_U^#, and through Stacks 04D3's identification of F = f^{-1}h_V^# with h_U^#, the inverse image of the morphism of ringed topoi that Stacks 04IF obtains by localizing at F and G = h_V^# is the inverse image of the morphism of ringed topoi that Stacks 04J0 obtains by localizing the morphism of ringed sites at V.

noncomputable def Hom.localizedRepresentableInverseImageIso :
    (Y.representableLocalizationEquivalence V).functor ⋙
        (RingedToposHom.localizedToposMorphism f.ringedToposHom
            (representableSheaf Y V)).inverseImage ⋙
          (f.localizedSourceEquivalence V).functor ≅
      (f.localizedRingedToposHom V).toToposHom.inverseImage ⋙
        (X.representableLocalizationEquivalence (f.u.obj V)).functor

AlgebraicGeometry.RingedSite.Hom.localizedRepresentablePushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/RepresentableMorphismLocalization.lean, line 318. The attribute's comment: “the two localized morphisms have the same direct image”.

Stacks 04J7, on direct images. Read through the same identifications, the direct image of Stacks 04IF's localized morphism is the direct image of Stacks 04J0's localized morphism. The two inverse images agree, so the two direct images agree by uniqueness of right adjoints.

noncomputable def Hom.localizedRepresentablePushforwardIso :
    ((f.localizedSourceEquivalence V).inverse ⋙
          (RingedToposHom.localizedToposMorphism f.ringedToposHom
            (representableSheaf Y V)).pushforward) ⋙
        (Y.representableLocalizationEquivalence V).inverse ≅
      (X.representableLocalizationEquivalence (f.u.obj V)).inverse ⋙
        (f.localizedRingedToposHom V).toToposHom.pushforward

AlgebraicGeometry.RingedSite.Hom.localizedRepresentable_forgetFSharp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/RepresentableMorphismLocalization.lean, line 346. The attribute's comment: “the two maps (f')^sharp agree, each being the restriction j^{-1}(f^sharp) of the structure map of f along its own localization morphism”.

Stacks 04J7, on structure maps: the two (f')^♯ are the same formula, each being the restriction j^{-1}(f^♯) of the structure map of f along its own localization morphism — along j_V for Stacks 04J0 and along j_G for Stacks 04IF — and Stacks 04J3 identifies (j_G, j_G^♯) with (j_V, j_V^♯).

For Stacks 04J0 the restriction is the whole formula, because Stacks 03CF's clause (d) is a strict equality of functors f'_*j_U^{-1} = j_V^{-1}f_*. For Stacks 04IF, where G is an arbitrary sheaf, that identity is only an isomorphism, and the formula is the restriction followed by it; the identifications of sheaves of commutative rings that Stacks 04IF's definition inserts contribute nothing, being the identity on underlying sheaves of sets.

theorem Hom.localizedRepresentable_forgetFSharp :
    AlgebraicGeometry.RingedToposHom.forgetFSharp (f.localizedRingedToposHom V) =
        (Y.overMorphismOfTopoi V).inverseImage.map
          (AlgebraicGeometry.RingedToposHom.forgetFSharp f.ringedToposHom) ∧
      AlgebraicGeometry.RingedToposHom.forgetFSharp
          (AlgebraicGeometry.RingedToposHom.localized f.ringedToposHom
            (representableSheaf Y V)) =
        (RingedTopos.localizationMorphism Y.ringedTopos
              (representableSheaf Y V)).toToposHom.inverseImage.map
            (AlgebraicGeometry.RingedToposHom.forgetFSharp f.ringedToposHom) ≫
          (RingedTopos.localizedRingedTopos Y.ringedTopos
              (representableSheaf Y V)).forgetRing.map
            (AlgebraicGeometry.RingedToposHom.localizedStructureIso f.ringedToposHom
              (representableSheaf Y V)).hom

Tag 04J8, a lemma

Tag 04J8 in the Stacks Project.

AlgebraicGeometry.RingedToposHom.relocalizedNaturalityInverseImageSquare, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/RelocalizedNaturalitySquare.lean, line 168. The attribute's comment: “the naturality square of the last assertion, on inverse images”.

Stacks 04J8, the naturality square on inverse images: (j_{F'/F})⁻¹ ∘ (f_s)⁻¹ ≅ (f_{s'})⁻¹ ∘ (j_{G'/G})⁻¹.

Along the factorization f_s = f'_G ∘ j_s this is the relocalization square relocalizationInverseImage_square for a ≫ s = s' ≫ f⁻¹b, whiskered by the inverse image of f'_G, pasted with the comparison localizedCompRelocalizationIso of the localized morphism of Stacks 04IF at G with the one at G', whiskered by the inverse image of the relocalization along s'.

noncomputable def relocalizedNaturalityInverseImageSquare
    (hs : a ≫ s = s' ≫ f.toToposHom.inverseImage.map b) :
    (comp (X := X.localizedRingedTopos F') (Y := X.localizedRingedTopos F)
        (Z := Y.localizedRingedTopos G) (f.relocalized s)
        (X.relocalizationMorphism a)).toToposHom.inverseImage ≅
      (comp (X := X.localizedRingedTopos F') (Y := Y.localizedRingedTopos G')
        (Z := Y.localizedRingedTopos G) (Y.relocalizationMorphism b)
        (f.relocalized s')).toToposHom.inverseImage

AlgebraicGeometry.RingedToposHom.relocalizedNaturalityToposSquare, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/RelocalizedNaturalitySquare.lean, line 194. The attribute's comment: “the naturality square of the last assertion, as a square of topoi”.

Stacks 04J8, the naturality square as a square of topoi: the comparison of the two direct images conjugate to relocalizedNaturalityInverseImageSquare.

noncomputable def relocalizedNaturalityToposSquare
    (hs : a ≫ s = s' ≫ f.toToposHom.inverseImage.map b) :
    (comp (X := X.localizedRingedTopos F') (Y := Y.localizedRingedTopos G')
        (Z := Y.localizedRingedTopos G) (Y.relocalizationMorphism b)
        (f.relocalized s')).toToposHom.pushforward ≅
      (comp (X := X.localizedRingedTopos F') (Y := X.localizedRingedTopos F)
        (Z := Y.localizedRingedTopos G) (f.relocalized s)
        (X.relocalizationMorphism a)).toToposHom.pushforward

AlgebraicGeometry.RingedToposHom.relocalizedNaturalitySquare, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/RelocalizedNaturalitySquare.lean, line 530. The attribute's comment: “the final assertion: for b, a, s' with the compatibility square, the induced square of ringed topoi on the slices commutes”.

Stacks 04J8, the naturality square of the last assertion as a square of ringed topoi:
  (j_{G'/G}, …) ∘ (f_{s'}, f_{s'}♯) ≅ (f_s, f_s♯) ∘ (j_{F'/F}, …) .
This is the pasting of relocalizationSquareTwoIso for a ≫ s = s' ≫ f⁻¹b with localizedCompRelocalizationRingedSquare along the factorization f_s = f'_G ∘ j_s.

noncomputable def relocalizedNaturalitySquare
    (hs : a ≫ s = s' ≫ f.toToposHom.inverseImage.map b) :
    TwoIso (A := X.localizedRingedTopos F') (B := Y.localizedRingedTopos G)
      (comp (X := X.localizedRingedTopos F') (Y := Y.localizedRingedTopos G')
        (Z := Y.localizedRingedTopos G) (Y.relocalizationMorphism b) (f.relocalized s'))
      (comp (X := X.localizedRingedTopos F') (Y := X.localizedRingedTopos F)
        (Z := Y.localizedRingedTopos G) (f.relocalized s) (X.relocalizationMorphism a))

AlgebraicGeometry.RingedToposHom.relocalized, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/RingedToposRelocalizedMorphism.lean, line 193. The attribute's comment: “the morphism (f_s, f_s^sharp), and its factorization as the morphism of 04IF after the relocalization morphism of 04J4”.

Stacks 04J8. The morphism of ringed topoi (f_s, f_s♯) : (Sh(C)/F, O_F) ⟶ (Sh(D)/G, O'_G) attached to a morphism of ringed topoi (f, f♯), a sheaf G on the target, a sheaf F on the source and a morphism s : F ⟶ f⁻¹G: the composition of the localized morphism of Stacks 04IF, from the localization at f⁻¹G, with the relocalization morphism of Stacks 04J4 along s.

The factorization that Stacks 04J8 asserts is this definition.

noncomputable def relocalized :
    RingedToposHom (X.localizedRingedTopos F) (Y.localizedRingedTopos G)

AlgebraicGeometry.RingedToposHom.relocalizedInverseImageSquare, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/RingedToposRelocalizedMorphism.lean, line 224. The attribute's comment: “commutativity of the localization square, on inverse images”.

Stacks 04J8, commutativity of the localization square on inverse images: f⁻¹ ⋙ j_F⁻¹ ≅ j_G⁻¹ ⋙ (f_s)⁻¹.

Since j_F⁻¹ is j_{f⁻¹G}⁻¹ followed by the inverse image of the relocalization along s on the nose, this is Stacks 04IF's inverse-image square whiskered by that relocalization.

noncomputable def relocalizedInverseImageSquare :
    (comp (X := X.localizedRingedTopos F) (Y := X) (Z := Y) f
        (X.localizationMorphism F)).toToposHom.inverseImage ≅
      (comp (X := X.localizedRingedTopos F) (Y := Y.localizedRingedTopos G) (Z := Y)
        (Y.localizationMorphism G) (f.relocalized s)).toToposHom.inverseImage

AlgebraicGeometry.RingedToposHom.relocalizedToposSquare, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/RingedToposRelocalizedMorphism.lean, line 252. The attribute's comment: “commutativity of the localization square, as a square of topoi”.

Stacks 04J8, commutativity of the localization square as a square of topoi: the comparison of the two direct images conjugate to relocalizedInverseImageSquare.

This is the underlying morphism-of-topoi content of the square; its compatibility with the structure sheaves is relocalizedRingedSquare.

noncomputable def relocalizedToposSquare :
    (comp (X := X.localizedRingedTopos F) (Y := Y.localizedRingedTopos G) (Z := Y)
        (Y.localizationMorphism G) (f.relocalized s)).toToposHom.pushforward ≅
      (comp (X := X.localizedRingedTopos F) (Y := X) (Z := Y) f
        (X.localizationMorphism F)).toToposHom.pushforward

AlgebraicGeometry.RingedToposHom.relocalizedRingedSquare, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/RingedToposRelocalizedMorphism.lean, line 309. The attribute's comment: “commutativity of the localization square as a square of ringed topoi”.

Stacks 04J8, commutativity of the localization square as a square of ringed topoi.

The structure-map compatibility of Stacks 04IF's own square is AlgebraicGeometry.RingedToposHom.localized_fSharpInverseImage_forget: the inverse-image form of (f')♯ for the morphism f' of Stacks 04IF, read through 04IF's inverse-image square, is the restriction of the inverse-image form of f♯ to the site of elements of f⁻¹G. It is the one thing beyond the inverse-image and pushforward squares of Stacks 04IF that commutativity of 04J8's square as a square of ringed topoi needs; see the implementation notes of this file.

Given it, the square for f_s follows with no further geometry: the structure map of the relocalization along s and that of the two localization morphisms are identities on underlying sheaves of sets, and j_F⁻¹ is j_{f⁻¹G}⁻¹ followed by the inverse image of the relocalization on the nose.

noncomputable def relocalizedRingedSquare :
    TwoIso (A := X.localizedRingedTopos F) (B := Y)
      (comp (X := X.localizedRingedTopos F) (Y := Y.localizedRingedTopos G) (Z := Y)
          (Y.localizationMorphism G) (f.relocalized s))
      (comp (X := X.localizedRingedTopos F) (Y := X) (Z := Y) f
        (X.localizationMorphism F))

Tag 04J9, a lemma

Tag 04J9 in the Stacks Project.

AlgebraicGeometry.RingedSite.Hom.relocalized_fSharpInverseImage_forget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/RelocalizedMorphismComparison.lean, line 872. The attribute's comment: “the relocalized morphism of 04J1 and the relocalized morphism of 04J8 have the same structure map: each is the structure map of its own f' restricted along its own relocalization, the relocalization contributing the identity, so that the assertion reduces to the one of 04J7”.

Stacks 04J9, on structure maps: the two relocalized morphisms have the same structure map, each being the structure map of its own localized morphism f' restricted along its own relocalization.

Read in inverse-image form and on underlying sheaves of sets, the structure map of f_c is j_c^{-1} applied to the structure map of the morphism of Stacks 04J0, and the structure map of f_s is j_s^{-1} applied to the structure map of the morphism of Stacks 04IF; the structure maps of the two relocalizations themselves are identities and drop out. Stacks 04J7 (AlgebraicGeometry.RingedSite.Hom.localizedRepresentable_forgetFSharp) says that the two structure maps so restricted are the same formula, namely the structure map of f restricted along the localization morphism.

theorem Hom.relocalized_fSharpInverseImage_forget :
    (ringedTopos (X.over U)).forgetRing.map (f.relocalized c).fSharpInverseImage =
      (X.relocalizationRingedToposHom c).toToposHom.inverseImage.map
        ((ringedTopos (X.over (f.u.obj V))).forgetRing.map
          (f.localizedRingedToposHom V).fSharpInverseImage) ∧
    (RingedTopos.localizedRingedTopos X.ringedTopos (representableSheaf X U)).forgetRing.map
        (f.ringedToposHom.relocalized (f.relocalizationSheafMap c)).fSharpInverseImage =
      (X.ringedTopos.relocalizationMorphismOfTopoi (f.relocalizationSheafMap c)).inverseImage.map
        ((RingedTopos.localizedRingedTopos X.ringedTopos
            (f.ringedToposHom.toToposHom.inverseImage.obj
              (representableSheaf Y V))).forgetRing.map
          (f.ringedToposHom.localized (representableSheaf Y V)).fSharpInverseImage)

AlgebraicGeometry.RingedSite.Hom.relocalizedCompInverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/RelocalizedMorphismInverseImage.lean, line 137. The attribute's comment: “on inverse images: the relocalized morphism of 04J1 and the relocalized morphism of 04J8 have the same inverse image, through the identifications of 04J3 at U and at V, the comparison being pasted from 04J5 and 04J7 on inverse images. The upgrade of this comparison to a 2-isomorphism of ringed topoi, and the agreement of the two localization squares under it, are not established here”.

The relocalized morphism of Stacks 04J1 followed by the identification of Stacks 04J3 at V, and the relocalized morphism of Stacks 04J8 preceded by the identification of Stacks 04J3 at U, have the same inverse image.

noncomputable def Hom.relocalizedCompInverseImageIso :
    (AlgebraicGeometry.RingedToposHom.comp (X := ringedTopos (X.over U))
        (Y := ringedTopos (Y.over V))
        (Z := RingedTopos.localizedRingedTopos Y.ringedTopos (representableSheaf Y V))
        (representableLocalizationRingedMorphism Y V)
        (f.relocalized c)).toToposHom.inverseImage ≅
      (AlgebraicGeometry.RingedToposHom.comp (X := ringedTopos (X.over U))
        (Y := RingedTopos.localizedRingedTopos X.ringedTopos (representableSheaf X U))
        (Z := RingedTopos.localizedRingedTopos Y.ringedTopos (representableSheaf Y V))
        (f.ringedToposHom.relocalized (f.relocalizationSheafMap c))
        (representableLocalizationRingedMorphism X U)).toToposHom.inverseImage

AlgebraicGeometry.RingedSite.Hom.relocalizedComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/RelocalizedTriangleComparison.lean, line 555. The attribute's comment: “the commutative diagrams of 04J1 and of 04J8 agree via the identifications of 04J3”.

Stacks 04J9. The commutative diagram of Stacks 04J1 and the commutative diagram of Stacks 04J8 agree via the identifications of Stacks 04J3: there is a 2-isomorphism β : ι_V ∘ f_c ≅ f_s ∘ ι_U of morphisms of ringed topoi under which the localization square of Stacks 04J1 is the localization square of Stacks 04J8.

theorem Hom.relocalizedComparison : f.RelocalizedComparisonStatement c

AlgebraicGeometry.RingedSite.representableRelocalizationSheafMapCompInverseImageIso_hom_app_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/Localization/RepresentableRelocalizationCoherence.lean, line 397. The attribute's comment: “the comparison of 04J5 on inverse images is the one determined by 04J3 at U and at V”.

Stacks 04J5's comparison of inverse images is the one Stacks 04J3 prescribes. The component of the comparison of the relocalization of the ringed topos along h_f^# with the relocalization of the ringed site along f, taken at an object j_{h_U^#}^{-1}A and followed by Stacks 04J3's comparison at U restricted along Over.map f, is Stacks 04J3's comparison at V.

The two strictness facts the statement uses hold on the nose: the inverse image of the relocalization of the ringed topos composed with that of the localization at h_U^# is the inverse image of the localization at h_V^#, because AlgebraicGeometry.RingedToposHom.toposRelocalizationTriangle is built from Iso.refl on inverse images, and Over.forget V = Over.map f ⋙ Over.forget U.

Both sides are morphisms into j_V^{-1}A, so the equation is equivalent to its transpose across j_{V!} ⊣ j_V^{-1}, which is shriek_representableRelocalizationSheafMapCompInverseImageIso_hom_app_comp.

theorem representableRelocalizationSheafMapCompInverseImageIso_hom_app_comp
    (A : Sheaf X.J (Type u)) :
    (representableRelocalizationSheafMapCompInverseImageIso X f).hom.app
          ((RingedTopos.localizationMorphism X.ringedTopos
            (representableSheaf X U)).toToposHom.inverseImage.obj A) ≫
        (X.relocalizationRingedToposHom f).toToposHom.inverseImage.map
          ((X.representableLocalizationInverseImageIso U).hom.app A) =
      (X.representableLocalizationInverseImageIso V).hom.app A

Sources

LeanAlgebraicGeometry.SmallEtale.localizedSmallModelMorphism · AlgebraicGeometry.localizedOverOpen · AlgebraicGeometry.Space.localizedSmallModelMorphism · Stacks.Sheaves.RingedToposModules.localizationCompPushforwardModulesIso · AlgebraicGeometry.RingedToposHom.localizedRingedToposSquare · AlgebraicGeometry.RingedToposHom.localizedInverseImageIso · AlgebraicGeometry.RingedToposHom.inverseImageCompLocalizationIso · AlgebraicGeometry.RingedToposHom.localizationCompPushforwardIso

Section18.23 Local types of modules #

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

Tag 03DL, a definition

Tag 03DL in the Stacks Project.

SheafOfModules.IsLocallyFreeOnSite, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ModuleTypesOnSite.lean, line 124. The attribute's comment: “locally_free”. References: EGA 0 (5.4.1), “more general”.

A sheaf of modules on a site is locally free when every object has a covering family on whose members the restricted module is free, that is, is a coproduct of copies of the restricted structure sheaf. This is Stacks 03DL(1).

abbrev IsLocallyFreeOnSite (F : SheafOfModules.{w} R) : Prop

SheafOfModules.IsFiniteLocallyFreeOnSite, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ModuleTypesOnSite.lean, line 170. The attribute's comment: “finite_locally_free”. References: EGA 0 (5.4.1), “more general”.

A sheaf of modules on a site is finite locally free when every object has a covering family on whose members the restricted module is finite free. This is Stacks 03DL(2); rank zero is included.

abbrev IsFiniteLocallyFreeOnSite (F : SheafOfModules.{m} R) : Prop

SheafOfModules.IsLocallyGeneratedBySectionsOnSite, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ModuleTypesOnSite.lean, line 201. The attribute's comment: “locally_generated”.

A sheaf of modules on a site is locally generated by sections when every object has a covering on whose members the restricted module admits generating global sections. The covering of an object U is recorded as a family of objects of the slice site over U which covers its terminal object. This is Stacks 03DL(3).

abbrev IsLocallyGeneratedBySectionsOnSite (F : SheafOfModules.{w} R) : Prop

SheafOfModules.IsLocallyGeneratedByOnSite, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ModuleTypesOnSite.lean, line 211. The attribute's comment: “locally_generated_r”.

A sheaf of modules on a site is locally generated by r sections when every object has a covering sieve such that, for every arrow in that sieve, the restriction of the module to its source is generated by a family of global sections indexed by a type equivalent to Fin r. This is Stacks 03DL(4).

abbrev IsLocallyGeneratedByOnSite (F : SheafOfModules.{w} R) (r : ℕ) : Prop

SheafOfModules.IsFinitePresentationOnSite, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ModuleTypesOnSite.lean, line 271. The attribute's comment: “finite_presentation on an arbitrary site”.

A sheaf of modules on a site is of finite presentation when every object of the site has a covering on whose members the restricted module admits a finite global presentation.

This is the finite refinement of SheafOfModules.IsQuasicoherentOnSite; like it, it requires no sheafification instance, so it also applies to the fibred categories of Stacks 06WG.

class IsFinitePresentationOnSite (F : SheafOfModules.{m} R) : Prop

SheafOfModules.IsCoherentOnSite, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ModuleTypesOnSite.lean, line 426. The attribute's comment: “coherent”. References: EGA 0 (5.3.7).

A sheaf of modules on a site is coherent when it is of finite type and, for every object U and every finite family of sections over U, the sheaf of relations among that family is of finite type on the slice site over U. This is Stacks 03DL(8).

class IsCoherentOnSite (F : SheafOfModules.{m} R) : Prop

SheafOfModules.IsQuasicoherentOnSite, a class in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/QuasicoherentOnSite.lean, line 99. The attribute's comment: “quasi_coherent”.

A sheaf of modules on a site is quasi-coherent when every object of the site has a covering on whose members the restricted module admits a global presentation, as in Stacks 03DL(6). This predicate requires no sheafification instances.

class IsQuasicoherentOnSite (M : SheafOfModules.{m} R) : Prop

Declarations registered for the tag:

SheafOfModules.IsFiniteType registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Topologies/ModuleTypesOnSite.lean, line 539 (StacksFrontier): “finite_type”. References: EGA 0 (5.2.1); SGA 6 I (1.3).
SheafOfModules.IsFinitePresentation registered with add_to_stacks in StacksFrontier/AlgebraicGeometry/Topologies/ModuleTypesOnSite.lean, line 546 (StacksFrontier): “finite_presentation”. References: EGA 0 (5.2.5); SGA 4 VI (5.6), “special case”; SGA 6 II (2.4.3).

Tag 03DM, a lemma

Tag 03DM in the Stacks Project.

AlgebraicGeometry.RingedToposHom.isLocallyFreeOnSite_iff_pullbackModules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LocalTypesUnderEquivalence.lean, line 108. The attribute's comment: “locally free”.

Stacks 03DM for the clause 03DL (1): local freeness is intrinsic. A sheaf of modules on the target of an equivalence of ringed topoi is locally free if and only if its pullback is.

The forward implication is Stacks 03DO. The reverse one applies Stacks 03DO to the inverse equivalence and carries the conclusion back along AlgebraicGeometry.RingedToposHom.pullbackModulesInverseObjIso.

theorem isLocallyFreeOnSite_iff_pullbackModules :
    F.IsLocallyFreeOnSite ↔ (f.toModulesHom.pullbackModules.obj F).IsLocallyFreeOnSite

AlgebraicGeometry.RingedToposHom.isFiniteLocallyFreeOnSite_iff_pullbackModules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LocalTypesUnderEquivalence.lean, line 119. The attribute's comment: “finite locally free”.

Stacks 03DM for the clause 03DL (2): finite local freeness is intrinsic. A sheaf of modules on the target of an equivalence of ringed topoi is finite locally free if and only if its pullback is; the rank on each member of the covering is unchanged in both directions.

theorem isFiniteLocallyFreeOnSite_iff_pullbackModules :
    F.IsFiniteLocallyFreeOnSite ↔
      (f.toModulesHom.pullbackModules.obj F).IsFiniteLocallyFreeOnSite

AlgebraicGeometry.RingedToposHom.isLocallyGeneratedBySectionsOnSite_iff_pullbackModules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LocalTypesUnderEquivalence.lean, line 132. The attribute's comment: “locally generated by sections”.

Stacks 03DM for the clause 03DL (3): local generation by sections is intrinsic. A sheaf of modules on the target of an equivalence of ringed topoi is locally generated by sections if and only if its pullback is; the index type of the generating family is unchanged in both directions.

theorem isLocallyGeneratedBySectionsOnSite_iff_pullbackModules :
    F.IsLocallyGeneratedBySectionsOnSite ↔
      (f.toModulesHom.pullbackModules.obj F).IsLocallyGeneratedBySectionsOnSite

AlgebraicGeometry.RingedToposHom.isQuasicoherentOnSite_iff_pullbackModules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LocalTypesUnderEquivalence.lean, line 145. The attribute's comment: “quasi-coherent”.

Stacks 03DM for the clause 03DL (6): quasi-coherence is intrinsic. A sheaf of modules on the target of an equivalence of ringed topoi is quasi-coherent if and only if its pullback is.

theorem isQuasicoherentOnSite_iff_pullbackModules :
    F.IsQuasicoherentOnSite ↔ (f.toModulesHom.pullbackModules.obj F).IsQuasicoherentOnSite

AlgebraicGeometry.RingedToposHom.isCoherentOnSite_iff_pullbackModules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LocalTypesUnderEquivalence.lean, line 160. The attribute's comment: “coherent”.

Stacks 03DM for the clause 03DL (8): coherence is intrinsic. A sheaf of modules on the target of an equivalence of ringed topoi is coherent if and only if its pullback is.

The forward implication is AlgebraicGeometry.RingedToposHom.isCoherentOnSite_pullbackModules, which is not an instance of Stacks 03DO — that tag omits coherence, and could not state it. The reverse one applies the forward implication to the inverse equivalence and carries the conclusion back along AlgebraicGeometry.RingedToposHom.pullbackModulesInverseObjIso.

theorem isCoherentOnSite_iff_pullbackModules :
    F.IsCoherentOnSite ↔ (f.toModulesHom.pullbackModules.obj F).IsCoherentOnSite

AlgebraicGeometry.RingedToposHom.isFinitePresentation_iff_pullbackModules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ModuleTypesUnderEquivalence.lean, line 194. The attribute's comment: “finite_presentation”.

Stacks 03DM for the clause 03DL (7): finite presentation is intrinsic. A sheaf of modules on the target of an equivalence of ringed topoi is of finite presentation if and only if its pullback is.

The forward implication is Stacks 03DO. The reverse one applies Stacks 03DO to the inverse equivalence and carries the conclusion back along AlgebraicGeometry.RingedToposHom.pullbackModulesInverseObjIso.

For Descent, Lemma 05VG this is an engine lemma awaiting instantiation and carries no @[stacks 05VG] attribute: 05VG asserts the clause at a comparison functor of Descent, Proposition 03DX, and no such functor is known to satisfy [f.toToposHom.pushforward.IsEquivalence] [IsIso f.fSharp]. Instantiating it for 05VG would need a named morphism of ringed topoi presenting the small Zariski comparison together with proofs that its pushforward is an equivalence and its structure map an isomorphism. See the section at the end of StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LocalTypesUnderComparison.lean, where an add_to_stacks 05VG against this declaration was retracted.

theorem isFinitePresentation_iff_pullbackModules (f : RingedToposHom X Y)
    [f.toToposHom.pushforward.IsEquivalence] [IsIso f.fSharp]
    (F : SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)) :
    F.IsFinitePresentation ↔ ((f.toModulesHom.pullbackModules).obj F).IsFinitePresentation

AlgebraicGeometry.RingedToposHom.isFiniteType_iff_pullbackModules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ModuleTypesUnderEquivalence.lean, line 221. The attribute's comment: “finite_type”.

Stacks 03DM for the clause 03DL (5): being of finite type is intrinsic. A sheaf of modules on the target of an equivalence of ringed topoi is of finite type if and only if its pullback is.

For Descent, Lemma 05VG this is an engine lemma awaiting instantiation and carries no @[stacks 05VG] attribute, for the reason given on AlgebraicGeometry.RingedToposHom.isFinitePresentation_iff_pullbackModules above: 05VG asserts the clause at a comparison functor of Descent, Proposition 03DX, and no such functor is known to satisfy this declaration's two instance hypotheses. Instantiating it would need a named morphism of ringed topoi presenting the small Zariski comparison together with proofs of those two facts about it.

theorem isFiniteType_iff_pullbackModules (f : RingedToposHom X Y)
    [f.toToposHom.pushforward.IsEquivalence] [IsIso f.fSharp]
    (F : SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)) :
    F.IsFiniteType ↔ ((f.toModulesHom.pullbackModules).obj F).IsFiniteType

AlgebraicGeometry.RingedToposHom.isLocallyGeneratedByOnSite_iff_pullbackModules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ModuleTypesUnderEquivalence.lean, line 248. The attribute's comment: “locally_generated_r”.

Stacks 03DM for the clause 03DL (4): local generation by r sections is intrinsic. A sheaf of modules on the target of an equivalence of ringed topoi is locally generated by r sections if and only if its pullback is.

For Descent, Lemma 05VG this is an engine lemma awaiting instantiation and carries no @[stacks 05VG] attribute, for the reason given on AlgebraicGeometry.RingedToposHom.isFinitePresentation_iff_pullbackModules above: 05VG asserts the clause at a comparison functor of Descent, Proposition 03DX, and no such functor is known to satisfy this declaration's two instance hypotheses. Instantiating it would need a named morphism of ringed topoi presenting the small Zariski comparison together with proofs of those two facts about it.

theorem isLocallyGeneratedByOnSite_iff_pullbackModules (f : RingedToposHom X Y)
    [f.toToposHom.pushforward.IsEquivalence] [IsIso f.fSharp]
    (F : SheafOfModules.{w} ((Stacks.SheafOfModules.Tensor.ringSheaf (J := Y.J)) Y.O)) (r : ℕ) :
    F.IsLocallyGeneratedByOnSite r ↔
      ((f.toModulesHom.pullbackModules).obj F).IsLocallyGeneratedByOnSite r

AlgebraicGeometry.Space.isFiniteLocallyFreeOnSite_chartSchemeModule_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/ChartComparisonAssembly.lean, line 127. The attribute's comment: “finite locally free, at the chart-scheme identification”.

Finite local freeness transports across the chart-scheme identification. A module on the slice at an étale chart is finite locally free on the site if and only if the module it becomes on the small étale site of the scheme underlying that chart is.

This is Stacks.SheafOfModules.isFiniteLocallyFreeOnSite_reindex_iff, the clause 03DL (2) of Modules on Sites, Lemma 03DM, applied to AlgebraicGeometry.Space.chartSchemeIdentification; it is the companion of AlgebraicGeometry.Space.isFinitePresentation_chartSchemeModule_iff.

theorem isFiniteLocallyFreeOnSite_chartSchemeModule_iff (U : AlgebraicSpaces B S hS)
    (W : (smallEtaleRingedSite B S hS U.1 U.2).C)
    (M : SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf
      ((smallEtaleRingedSite B S hS U.1 U.2).over W).O)) :
    SheafOfModules.IsFiniteLocallyFreeOnSite (chartSchemeSiteModule B S hS U W M) ↔
      SheafOfModules.IsFiniteLocallyFreeOnSite M

AlgebraicGeometry.Space.isFiniteLocallyFreeOnSite_chartSmallEtaleRestriction_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteLocallyFreeChartScheme.lean, line 69. The attribute's comment: “finite locally free, at the localization of 04M0 at a chart”.

Finite local freeness is invariant under the comparison of Stacks 04M0. The restriction of an 𝒪_X-module to an étale scheme chart, read on the small étale site of the chart, is finite locally free exactly when the restriction to the slice of the small étale site of X is.

theorem isFiniteLocallyFreeOnSite_chartSmallEtaleRestriction_iff (X : AlgebraicSpaces B S hS)
    (M : SheafOfModules.{u} (structureRingSheaf B S hS X)) (U : SmallEtale B S hS X.1) :
    SheafOfModules.IsFiniteLocallyFreeOnSite (chartSmallEtaleRestriction B S hS X M U) ↔
      SheafOfModules.IsFiniteLocallyFreeOnSite (M.over U)

AlgebraicGeometry.Space.isFiniteLocallyFreeOnSite_representedSmallEtaleModule_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteLocallyFreeChartScheme.lean, line 85. The attribute's comment: “finite locally free, at the comparison of a representable space with its scheme”.

Finite local freeness is invariant under the comparison equivalence of Stacks 03DX (2) at a representable algebraic space.

theorem isFiniteLocallyFreeOnSite_representedSmallEtaleModule_iff (U : BigFppfOver B S hS)
    (M : SheafOfModules.{u} (representedSchemeStructureSheaf B S hS U)) :
    SheafOfModules.IsFiniteLocallyFreeOnSite (representedSmallEtaleModule B S hS U M) ↔
      SheafOfModules.IsFiniteLocallyFreeOnSite M

AlgebraicGeometry.Space.isFiniteFree_representedSmallEtaleModule_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteLocallyFreeChartScheme.lean, line 97. The attribute's comment: “finite free, at the comparison of a representable space with its scheme”.

Finite freeness is invariant under the comparison equivalence of Stacks 03DX (2) at a representable algebraic space. This is AlgebraicGeometry.Space.isFiniteLocallyFreeOnSite_representedSmallEtaleModule_iff for outright finite freeness in place of finite local freeness; it is the same reindexing.

theorem isFiniteFree_representedSmallEtaleModule_iff (U : BigFppfOver B S hS)
    (M : SheafOfModules.{u} (representedSchemeStructureSheaf B S hS U)) :
    SheafOfModules.IsFiniteFree (representedStructureRingSheaf B S hS U)
        (representedSmallEtaleModule B S hS U M) ↔
      SheafOfModules.IsFiniteFree (representedSchemeStructureSheaf B S hS U) M

AlgebraicGeometry.Space.isFiniteLocallyFreeOfRank_chartSmallEtaleRestriction_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteLocallyFreeRankChartScheme.lean, line 45. The attribute's comment: “the rank clause of 0409, at the localization of 04M0 at a chart”.

The rank clause of Stacks 0409 is invariant under the comparison of Stacks 04M0. The restriction of an 𝒪_X-module to an étale scheme chart, read on the small étale site of the chart, has rank r exactly when the restriction to the slice of the small étale site of X has.

theorem isFiniteLocallyFreeOfRank_chartSmallEtaleRestriction_iff (X : AlgebraicSpaces B S hS)
    (M : SheafOfModules.{u} (structureRingSheaf B S hS X)) (U : SmallEtale B S hS X.1) (r : ℕ) :
    RingedSite.IsFiniteLocallyFreeOfRank
        (smallEtaleRingedSite B S hS (chartSpace B S hS X U).1 (chartSpace B S hS X U).2)
        (chartSmallEtaleRestriction B S hS X M U) r ↔
      RingedSite.IsFiniteLocallyFreeOfRank ((smallEtaleRingedSite B S hS X.1 X.2).over U)
        (M.over U) r

AlgebraicGeometry.Space.isFiniteLocallyFreeOfRank_representedSmallEtaleModule_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteLocallyFreeRankChartScheme.lean, line 72. The attribute's comment: “the rank clause of 0409, at the represented-space comparison of 03DX (2)”.

The rank clause of Stacks 0409 is invariant under the comparison equivalence of Stacks 03DX (2) at a representable algebraic space.

theorem isFiniteLocallyFreeOfRank_representedSmallEtaleModule_iff (U : BigFppfOver B S hS)
    (M : SheafOfModules.{u} (representedSchemeStructureSheaf B S hS U)) (r : ℕ) :
    RingedSite.IsFiniteLocallyFreeOfRank
        (smallEtaleRingedSite B S hS (yoneda.obj U)
          (AlgebraicGeometry.isAlgebraicSpace_yoneda B S hS U))
        (representedSmallEtaleModule B S hS U M) r ↔
      RingedSite.IsFiniteLocallyFreeOfRank
        (_root_.AlgebraicGeometry.smallEtaleRingedSite (associatedBigEtaleSite B)
          ((BigFppfOver.toScheme B S hS).obj U) U.left.property) M r

AlgebraicGeometry.Space.isFiniteLocallyFreeOnSite_chartModuleReindex_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SliceAssociatedModuleFiniteLocallyFree.lean, line 95. The attribute's comment: “finite locally free, at the localization of 04M0 at a chart, for a general module of the slice”.

Finite local freeness of a module on the slice at a chart is invariant under the localization of Stacks 04M0. This is the general-module form of AlgebraicGeometry.Space.isFiniteLocallyFreeOnSite_chartSmallEtaleRestriction_iff, which states the same for a module arising as the restriction of an 𝒪_X-module.

theorem isFiniteLocallyFreeOnSite_chartModuleReindex_iff
    (N : SheafOfModules.{u} ((structureRingSheaf B S hS X).over W)) :
    SheafOfModules.IsFiniteLocallyFreeOnSite
        ((chartModuleReindexEquivalence B S hS X W).functor.obj N) ↔
      SheafOfModules.IsFiniteLocallyFreeOnSite N

Tag 03DN, a lemma

Tag 03DN in the Stacks Project.

Stacks.SheafOfModules.isCoherentOnSite_iff_exists_cover_isCoherentOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LocalOnCover/Coherence.lean, line 543. The attribute's comment: “coherent”.

Stacks 03DN, coherence. A sheaf of modules on a ringed site is coherent if and only if its restriction to each member of some covering family of the final object is coherent on the corresponding localized ringed site.

theorem isCoherentOnSite_iff_exists_cover_isCoherentOnSite :
    SheafOfModules.IsCoherentOnSite F ↔
      ∃ (I : Type (max u v)) (U : I → X.C), X.J.CoversTop U ∧
        ∀ i : I, SheafOfModules.IsCoherentOnSite
          (R := (Stacks.SheafOfModules.Tensor.ringSheaf (X.over (U i)).O)) (F.over (U i))

Stacks.SheafOfModules.isFiniteLocallyFreeOnSite_iff_exists_cover_isFiniteLocallyFreeOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LocalOnCover/FiniteLocallyFree.lean, line 126. The attribute's comment: “finite_locally_free”.

Stacks 03DN, finite local freeness. A sheaf of modules on a ringed site is finite locally free if and only if its restriction to each member of some covering family of the final object is finite locally free on the corresponding localized ringed site.

theorem isFiniteLocallyFreeOnSite_iff_exists_cover_isFiniteLocallyFreeOnSite :
    SheafOfModules.IsFiniteLocallyFreeOnSite F ↔
      ∃ (I : Type (max u v)) (U : I → X.C), X.J.CoversTop U ∧
        ∀ i : I, SheafOfModules.IsFiniteLocallyFreeOnSite
          (R := (Stacks.SheafOfModules.Tensor.ringSheaf (X.over (U i)).O)) (F.over (U i))

Stacks.SheafOfModules.isFiniteLocallyFreeOnSite_iff_exists_cover_isFiniteFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LocalOnCover/FiniteLocallyFree.lean, line 177. The attribute's comment: “finite_locally_free”.

Stacks 03DN, finite local freeness. A sheaf of modules on a ringed site is finite locally free if and only if its restriction to each member of some covering family of the final object is finite free.

theorem isFiniteLocallyFreeOnSite_iff_exists_cover_isFiniteFree :
    SheafOfModules.IsFiniteLocallyFreeOnSite F ↔
      ∃ (I : Type (max u v)) (U : I → X.C), X.J.CoversTop U ∧
        ∀ i : I, ∃ n : ℕ,
          ∃ (ι : ∀ _ : Fin n,
            SheafOfModules.unit ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over (U i)) ⟶
              F.over (U i)),
            Nonempty (IsColimit (Cofan.mk (F.over (U i)) ι))

Stacks.SheafOfModules.isFinitePresentation_iff_exists_cover_isFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LocalOnCover/FinitePresentation.lean, line 156. The attribute's comment: “finite_presentation”.

Stacks 03DN, finite presentation. A sheaf of modules is of finite presentation if and only if its restrictions to the members of some covering family of the final object are of finite presentation.

theorem isFinitePresentation_iff_exists_cover_isFinitePresentation
    [∀ (U : C), ∀ (V : Over U),
      HasWeakSheafify ((J.over U).over V) AddCommGrpCat.{w}]
    [∀ (U : C), ∀ (V : Over U),
      ((J.over U).over V).WEqualsLocallyBijective AddCommGrpCat.{w}] :
    M.IsFinitePresentation ↔
      ∃ (I : Type u) (U : I → C), J.CoversTop U ∧
        ∀ i : I, (M.over (U i)).IsFinitePresentation

Stacks.SheafOfModules.isFinitePresentation_iff_exists_cover_finite_presentations, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LocalOnCover/FinitePresentation.lean, line 202. The attribute's comment: “finite_presentation”.

Stacks 03DN, finite presentation. A sheaf of modules is of finite presentation if and only if its restrictions to the members of some covering family of the final object have finite global presentations.

theorem isFinitePresentation_iff_exists_cover_finite_presentations :
    M.IsFinitePresentation ↔
      ∃ (I : Type u) (U : I → C), J.CoversTop U ∧
        ∀ i : I, ∃ (p : (M.over (U i)).Presentation), p.IsFinite

Stacks.SheafOfModules.isFiniteType_iff_exists_cover_isFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LocalOnCover/FiniteType.lean, line 148. The attribute's comment: “finite_type”.

Stacks 03DN, finite type. A sheaf of modules is of finite type if and only if it is so after restriction to each member of some covering family of the final object.

theorem isFiniteType_iff_exists_cover_isFiniteType
    [∀ (U : C), ∀ (V : Over U),
      HasWeakSheafify ((J.over U).over V) AddCommGrpCat.{w}]
    [∀ (U : C), ∀ (V : Over U),
      ((J.over U).over V).WEqualsLocallyBijective AddCommGrpCat.{w}] :
    M.IsFiniteType ↔
      ∃ (I : Type u) (U : I → C), J.CoversTop U ∧
        ∀ i : I, (M.over (U i)).IsFiniteType

Stacks.SheafOfModules.isFiniteType_iff_exists_cover_finite_generators, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LocalOnCover/FiniteType.lean, line 175. The attribute's comment: “finite_type”.

Stacks 03DN, finite type. A sheaf of modules is of finite type if and only if it is generated by finitely many global sections after restriction to each member of some covering family of the final object.

theorem isFiniteType_iff_exists_cover_finite_generators :
    M.IsFiniteType ↔
      ∃ (I : Type u) (U : I → C), J.CoversTop U ∧
        ∀ i : I, ∃ (σ : (M.over (U i)).GeneratingSections), σ.IsFiniteType

Stacks.SheafOfModules.isLocallyGeneratedBySectionsOnSite_iff_exists_cover_locallyGenerated, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LocalOnCover/LocalGeneration.lean, line 250. The attribute's comment: “locally_generated”.

Stacks 03DN, local generation by sections. A sheaf of modules on a ringed site is locally generated by sections if and only if its restriction to each member of some covering family of the final object is locally generated by sections on the corresponding localized ringed site.

theorem isLocallyGeneratedBySectionsOnSite_iff_exists_cover_locallyGenerated
    [∀ (U : X.C) (V : Over U), HasWeakSheafify ((X.J.over U).over V) AddCommGrpCat.{w}]
    [∀ (U : X.C) (V : Over U), ((X.J.over U).over V).WEqualsLocallyBijective AddCommGrpCat.{w}] :
    SheafOfModules.IsLocallyGeneratedBySectionsOnSite F ↔
      ∃ (I : Type u) (U : I → X.C), X.J.CoversTop U ∧
        ∀ i : I, SheafOfModules.IsLocallyGeneratedBySectionsOnSite
          (R := (Stacks.SheafOfModules.Tensor.ringSheaf X.O).over (U i)) (F.over (U i))

Stacks.SheafOfModules.isLocallyGeneratedBySectionsOnSite_iff_exists_cover_generatingSections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LocalOnCover/LocalGeneration.lean, line 283. The attribute's comment: “locally_generated”.

Stacks 03DN, local generation by sections. A sheaf of modules on a ringed site is locally generated by sections if and only if its restriction to each member of some covering family of the final object is generated by global sections.

theorem isLocallyGeneratedBySectionsOnSite_iff_exists_cover_generatingSections :
    SheafOfModules.IsLocallyGeneratedBySectionsOnSite F ↔
      ∃ (I : Type u) (U : I → X.C), X.J.CoversTop U ∧
        ∀ i : I, Nonempty ((F.over (U i)).GeneratingSections)

Stacks.SheafOfModules.isLocallyGeneratedByOnSite_iff_exists_cover_isLocallyGeneratedBy, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LocalOnCover/LocalGeneration.lean, line 300. The attribute's comment: “locally_generated_r”.

Stacks 03DN, local generation by r sections. A sheaf of modules on a ringed site is locally generated by r sections if and only if its restriction to each member of some covering family of the final object is, on the corresponding localized ringed site.

theorem isLocallyGeneratedByOnSite_iff_exists_cover_isLocallyGeneratedBy
    [∀ (U : X.C) (V : Over U), HasWeakSheafify ((X.J.over U).over V) AddCommGrpCat.{w}]
    [∀ (U : X.C) (V : Over U), ((X.J.over U).over V).WEqualsLocallyBijective AddCommGrpCat.{w}] :
    SheafOfModules.IsLocallyGeneratedByOnSite F r ↔
      ∃ (I : Type u) (U : I → X.C), X.J.CoversTop U ∧
        ∀ i : I, SheafOfModules.IsLocallyGeneratedByOnSite
          (R := (Stacks.SheafOfModules.Tensor.ringSheaf X.O).over (U i)) (F.over (U i)) r

Stacks.SheafOfModules.isLocallyGeneratedByOnSite_iff_exists_cover_generators, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LocalOnCover/LocalGeneration.lean, line 352. The attribute's comment: “locally_generated_r”.

Stacks 03DN, local generation by r sections. A sheaf of modules on a ringed site is locally generated by r sections if and only if its restriction to each member of some covering family of the final object is generated by r global sections.

theorem isLocallyGeneratedByOnSite_iff_exists_cover_generators :
    SheafOfModules.IsLocallyGeneratedByOnSite F r ↔
      ∃ (I : Type u) (U : I → X.C), X.J.CoversTop U ∧
        ∀ i : I, ∃ σ : (F.over (U i)).GeneratingSections, Nonempty (σ.I ≃ Fin r)

Stacks.SheafOfModules.isLocallyFreeOnSite_iff_exists_cover_isLocallyFreeOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LocalOnCover/LocallyFree.lean, line 171. The attribute's comment: “locally_free”.

Stacks 03DN, local freeness. A sheaf of modules on a ringed site is locally free if and only if its restriction to each member of some covering family of the final object is locally free on the corresponding localized ringed site.

theorem isLocallyFreeOnSite_iff_exists_cover_isLocallyFreeOnSite :
    SheafOfModules.IsLocallyFreeOnSite F ↔
      ∃ (I : Type (max u v)) (U : I → X.C), X.J.CoversTop U ∧
        ∀ i : I, SheafOfModules.IsLocallyFreeOnSite
          (R := Stacks.SheafOfModules.Tensor.ringSheaf (X.over (U i)).O) (F.over (U i))

Stacks.SheafOfModules.isLocallyFreeOnSite_iff_exists_cover_isFree, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LocalOnCover/LocallyFree.lean, line 208. The attribute's comment: “locally_free”.

Stacks 03DN, local freeness. A sheaf of modules on a ringed site is locally free if and only if its restriction to each member of some covering family of the final object is free.

theorem isLocallyFreeOnSite_iff_exists_cover_isFree :
    SheafOfModules.IsLocallyFreeOnSite F ↔
      ∃ (I : Type (max u v)) (U : I → X.C), X.J.CoversTop U ∧
        ∀ i : I, SheafOfModules.IsFree (F.over (U i))

Stacks.SheafOfModules.isQuasicoherentOnSite_iff_exists_cover_isQuasicoherentOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LocalOnCover/Quasicoherence.lean, line 461. The attribute's comment: “quasi_coherent”.

Stacks 03DN, quasi-coherence. A sheaf of modules is quasi-coherent if and only if its restriction to each member of some covering family of the final object is quasi-coherent.

theorem isQuasicoherentOnSite_iff_exists_cover_isQuasicoherentOnSite :
    M.IsQuasicoherentOnSite ↔
      ∃ (I : Type u) (U : I → C), J.CoversTop U ∧
        ∀ i : I, (M.over (U i)).IsQuasicoherentOnSite

Stacks.SheafOfModules.isQuasicoherentOnSite_iff_exists_cover_hasGlobalPresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LocalOnCover/Quasicoherence.lean, line 471. The attribute's comment: “quasi_coherent”.

Stacks 03DN, quasi-coherence. A sheaf of modules is quasi-coherent if and only if its restriction to each member of some covering family of the final object has a global presentation.

theorem isQuasicoherentOnSite_iff_exists_cover_hasGlobalPresentation :
    M.IsQuasicoherentOnSite ↔
      ∃ (I : Type u) (U : I → C), J.CoversTop U ∧
        ∀ i : I, (M.over (U i)).HasGlobalPresentation

Stacks.SheafOfModules.isQuasicoherentOnSite_iff_coversTop_hasGlobalPresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/QuasicoherentLocality.lean, line 118. The attribute's comment: “quasi_coherent”.

Stacks 03DN, quasi-coherence. A sheaf of modules is quasi-coherent if and only if it has a global presentation on each member of some family of objects covering the final object.

This is Stacks.SheafOfModules.isQuasicoherentOnSite_iff_exists_cover_hasGlobalPresentation with the universe of the module sections independent of the universe of the coefficient rings.

theorem isQuasicoherentOnSite_iff_coversTop_hasGlobalPresentation (M : SheafOfModules.{m} R) :
    M.IsQuasicoherentOnSite ↔
      ∃ (I : Type u) (W : I → C), J.CoversTop W ∧
        ∀ i : I, (M.over (W i)).HasGlobalPresentation

Tag 03DO, a lemma

Tag 03DO in the Stacks Project.

Stacks.Sheaves.LocalizedPullback.isQuasicoherentOnSite_pullbackTopos_of_quasicoherentData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LocalizedPullbackQuasicoherent.lean, line 472. The attribute's comment: “quasi_coherent, for a morphism of ringed sites presented by a left exact continuous functor — the case 03DO's own proof reduces its quasi-coherent clause to through Section 03DG. The clause for an arbitrary morphism of ringed topoi is AlgebraicGeometry.RingedToposHom.isQuasicoherentOnSite_pullbackModules, which transports this one along the two equivalences of ringed topoi 03CR produces”.

The quasi-coherent clause of Stacks 03DO for a morphism of ringed sites presented by a left exact continuous functor. The pullback of a sheaf of O'-modules admitting quasi-coherent data is quasi-coherent on the site.

The data is transported by Stacks.Sheaves.LocalizedPullback.localizedPullbackMapData and the transported presentations assemble into quasi-coherence on the site by Stacks.SheafOfModules.isQuasicoherentOnSite_of_mapData.

This is the case to which Stacks 03DO's own proof reduces its quasi-coherent clause through Section 03DG; the general statement, for an arbitrary morphism of ringed topoi, is AlgebraicGeometry.RingedToposHom.isQuasicoherentOnSite_pullbackModules, which transports this one along the two equivalences of ringed topoi that Stacks 03CR produces.

theorem isQuasicoherentOnSite_pullbackTopos_of_quasicoherentData
    (q : M.QuasicoherentData.{ww}) :
    (f.toRingedToposSiteHom.pullbackTopos.obj M).IsQuasicoherentOnSite

Stacks.Sheaves.LocalizedPullback.isQuasicoherentOnSite_pullbackTopos, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LocalizedPullbackQuasicoherent.lean, line 527. The attribute's comment: “quasi_coherent, for a morphism of ringed sites presented by a left exact continuous functor — the case 03DO's own proof reduces its quasi-coherent clause to through Section 03DG. The clause for an arbitrary morphism of ringed topoi is AlgebraicGeometry.RingedToposHom.isQuasicoherentOnSite_pullbackModules, which transports this one along the two equivalences of ringed topoi 03CR produces”.

The quasi-coherent clause of Stacks 03DO for a morphism of ringed sites, with the hypothesis in the form the clause states it. If a sheaf of O'-modules is quasi-coherent on the site, so is its pullback along a morphism of ringed sites presented by a left exact continuous functor.

Quasi-coherence may be tested on a single family covering the final object, by Stacks 03DN in the form Stacks.SheafOfModules.isQuasicoherentOnSite_iff_exists_cover_hasGlobalPresentation. Such a family {W_i} for M is carried to the family {u(W_i)} by Stacks.Sheaves.LocalizedPullback.coversTop_mapObj, and the global presentation of M|_{W_i} to one of (f^*M)|_{u(W_i)} by Stacks.Sheaves.LocalizedPullback.hasGlobalPresentation_over_pullbackTopos. No smallness hypothesis on the slices of the target site is needed, for the reason recorded there.

This is the case to which Stacks 03DO's own proof reduces its quasi-coherent clause through Section 03DG; the general statement, for an arbitrary morphism of ringed topoi, is AlgebraicGeometry.RingedToposHom.isQuasicoherentOnSite_pullbackModules, which transports this one along the two equivalences of ringed topoi that Stacks 03CR produces.

theorem isQuasicoherentOnSite_pullbackTopos (hM : M.IsQuasicoherentOnSite) :
    (f.toRingedToposSiteHom.pullbackTopos.obj M).IsQuasicoherentOnSite

Stacks.Sheaves.LocalizedPullback.isFiniteLocallyFreeOnSite_pullbackTopos, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LocalizedPullbackQuasicoherent.lean, line 590. The attribute's comment: “the finite locally free property, clause 03DL (2), for a morphism of ringed sites presented by a left exact continuous functor — the case 03DO's own proof reduces that clause to through Section 03DG. The clause for an arbitrary morphism of ringed topoi is AlgebraicGeometry.RingedToposHom.isFiniteLocallyFreeOnSite_pullbackModules, which transports this one along the two equivalences of ringed topoi 03CR produces”. References: EGA II (6.4.8), “more general”.

The finite locally free clause of Stacks 03DO for a morphism of ringed sites presented by a left exact continuous functor. If a sheaf of O'-modules is finite locally free on the site, so is its pullback along a morphism of ringed sites whose underlying functor is left exact. This is the clause of Stacks 03DO for Stacks 03DL (2).

Finite local freeness may be tested on a single family covering the final object, by Stacks 03DN in the form Stacks.SheafOfModules.isFiniteLocallyFreeOnSite_iff_exists_cover_isFiniteFree. Such a family {W_i} for M is carried to the family {u(W_i)} by Stacks.Sheaves.LocalizedPullback.coversTop_mapObj, and the finite freeness of M|_{W_i} is carried to that of (f^*M)|_{u(W_i)} by Stacks.Sheaves.LocalizedPullback.isFiniteFree_over_pullbackTopos.

This is the case to which Stacks 03DO's own proof reduces the clause through Section 03DG; the general statement, for an arbitrary morphism of ringed topoi, is AlgebraicGeometry.RingedToposHom.isFiniteLocallyFreeOnSite_pullbackModules, which transports this one along the two equivalences of ringed topoi that Stacks 03CR produces.

theorem isFiniteLocallyFreeOnSite_pullbackTopos
    (hM : SheafOfModules.IsFiniteLocallyFreeOnSite M) :
    SheafOfModules.IsFiniteLocallyFreeOnSite
      (f.toRingedToposSiteHom.pullbackTopos.obj M)

Stacks.Sheaves.LocalizedPullback.isLocallyFreeOnSite_pullbackTopos, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LocalizedPullbackQuasicoherent.lean, line 650. The attribute's comment: “the locally free property, clause 03DL (1), for a morphism of ringed sites presented by a left exact continuous functor — the case 03DO's own proof reduces that clause to through Section 03DG. The clause for an arbitrary morphism of ringed topoi is AlgebraicGeometry.RingedToposHom.isLocallyFreeOnSite_pullbackModules, which transports this one along the two equivalences of ringed topoi 03CR produces”.

The locally free clause of Stacks 03DO for a morphism of ringed sites presented by a left exact continuous functor. If a sheaf of O'-modules is locally free on the site, so is its pullback along a morphism of ringed sites whose underlying functor is left exact. This is the clause of Stacks 03DO for Stacks 03DL (1).

Local freeness may be tested on a single family covering the final object, by Stacks 03DN in the form Stacks.SheafOfModules.isLocallyFreeOnSite_iff_exists_cover_isFree. Such a family {W_i} for M is carried to the family {u(W_i)} by Stacks.Sheaves.LocalizedPullback.coversTop_mapObj, and the freeness of M|_{W_i} is carried to that of (f^*M)|_{u(W_i)} by Stacks.Sheaves.LocalizedPullback.isFree_over_pullbackTopos.

This is the case to which Stacks 03DO's own proof reduces the clause through Section 03DG; the general statement, for an arbitrary morphism of ringed topoi, is AlgebraicGeometry.RingedToposHom.isLocallyFreeOnSite_pullbackModules, which transports this one along the two equivalences of ringed topoi that Stacks 03CR produces.

theorem isLocallyFreeOnSite_pullbackTopos (hM : SheafOfModules.IsLocallyFreeOnSite M) :
    SheafOfModules.IsLocallyFreeOnSite
      (f.toRingedToposSiteHom.pullbackTopos.obj M)

Stacks.Sheaves.LocalizedPullback.isLocallyGeneratedBySectionsOnSite_pullbackTopos, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LocalizedPullbackQuasicoherent.lean, line 713. The attribute's comment: “the locally generated property, clause 03DL (3), for a morphism of ringed sites presented by a left exact continuous functor — the case 03DO's own proof reduces that clause to through Section 03DG. The clause for an arbitrary morphism of ringed topoi is AlgebraicGeometry.RingedToposHom.isLocallyGeneratedBySectionsOnSite_pullbackModules, which transports this one along the two equivalences of ringed topoi 03CR produces”.

The locally generated clause of Stacks 03DO for a morphism of ringed sites presented by a left exact continuous functor. If a sheaf of O'-modules is locally generated by sections, so is its pullback along a morphism of ringed sites whose underlying functor is left exact. This is the clause of Stacks 03DO for Stacks 03DL (3).

Local generation by sections may be tested on a single family covering the final object, by Stacks 03DN in the form Stacks.SheafOfModules.isLocallyGeneratedBySectionsOnSite_iff_exists_cover_generatingSections. Such a family {W_i} for M is carried to the family {u(W_i)} by Stacks.Sheaves.LocalizedPullback.coversTop_mapObj, and the generating sections of M|_{W_i} to those of (f^*M)|_{u(W_i)} by Stacks.Sheaves.LocalizedPullback.generatingSectionsPullbackTopos.

This is the case to which Stacks 03DO's own proof reduces the clause through Section 03DG; the general statement, for an arbitrary morphism of ringed topoi, is AlgebraicGeometry.RingedToposHom.isLocallyGeneratedBySectionsOnSite_pullbackModules, which transports this one along the two equivalences of ringed topoi that Stacks 03CR produces. The clause for local generation by a fixed number r of sections, Stacks 03DL (4), is proved for an arbitrary morphism of ringed topoi in Stacks.Sheaves.LocalGeneration.pullbackModules_isLocallyGeneratedByOnSite.

theorem isLocallyGeneratedBySectionsOnSite_pullbackTopos
    (hM : SheafOfModules.IsLocallyGeneratedBySectionsOnSite M) :
    SheafOfModules.IsLocallyGeneratedBySectionsOnSite
      (f.toRingedToposSiteHom.pullbackTopos.obj M)

AlgebraicGeometry.RingedToposHom.isLocallyFreeOnSite_pullbackModules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LocalTypesToposPullback.lean, line 392. The attribute's comment: “part (1), locally free: for an arbitrary morphism of ringed topoi”.

Stacks 03DO for the clause 03DL (1). If a sheaf of O_D-modules is locally free, then so is its pullback along an arbitrary morphism of ringed topoi (f, f♯) : (Sh(C), O_C) ⟶ (Sh(D), O_D).

Stacks 03CR factors (f, f♯) through two equivalences attached to dense subsite inclusions and a morphism presented by a left exact morphism of sites, and the clause travels around that square by AlgebraicGeometry.RingedToposHom.isLocallyFreeOnSite_pullbackModules_of_twoSided.

theorem isLocallyFreeOnSite_pullbackModules (hF : F.IsLocallyFreeOnSite) :
    (f.toModulesHom.pullbackModules.obj F).IsLocallyFreeOnSite

AlgebraicGeometry.RingedToposHom.isFiniteLocallyFreeOnSite_pullbackModules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LocalTypesToposPullback.lean, line 405. The attribute's comment: “part (2), finite locally free: for an arbitrary morphism of ringed topoi”.

Stacks 03DO for the clause 03DL (2). If a sheaf of O_D-modules is finite locally free, then so is its pullback along an arbitrary morphism of ringed topoi; the rank on each member of the covering is unchanged.

theorem isFiniteLocallyFreeOnSite_pullbackModules (hF : F.IsFiniteLocallyFreeOnSite) :
    (f.toModulesHom.pullbackModules.obj F).IsFiniteLocallyFreeOnSite

AlgebraicGeometry.RingedToposHom.isLocallyGeneratedBySectionsOnSite_pullbackModules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LocalTypesToposPullback.lean, line 419. The attribute's comment: “part (3), locally generated by sections: for an arbitrary morphism of ringed topoi”.

Stacks 03DO for the clause 03DL (3). If a sheaf of O_D-modules is locally generated by sections, then so is its pullback along an arbitrary morphism of ringed topoi; the index type of the generating family is unchanged.

theorem isLocallyGeneratedBySectionsOnSite_pullbackModules
    (hF : F.IsLocallyGeneratedBySectionsOnSite) :
    (f.toModulesHom.pullbackModules.obj F).IsLocallyGeneratedBySectionsOnSite

AlgebraicGeometry.RingedToposHom.isQuasicoherentOnSite_pullbackModules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/LocalTypesToposPullback.lean, line 432. The attribute's comment: “part (6), quasi-coherent: for an arbitrary morphism of ringed topoi”.

Stacks 03DO for the clause 03DL (6). If a sheaf of O_D-modules is quasi-coherent, then so is its pullback along an arbitrary morphism of ringed topoi.

theorem isQuasicoherentOnSite_pullbackModules (hF : F.IsQuasicoherentOnSite) :
    (f.toModulesHom.pullbackModules.obj F).IsQuasicoherentOnSite

Stacks.Sheaves.FinitePresentation.isFiniteLocallyFreeOnSite_pullbackModules, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ToposPullbackFiniteLocallyFree.lean, line 198. The attribute's comment: “finite_locally_free”. References: EGA 0 (5.4.5), “locally free clause”; EGA II (6.4.8), “more general”; EGA III (7.7.9), “partial”.

Stacks 03DO for the clause 03DL(2): pullback preserves finite local freeness. The pullback f^*F = O_C ⊗_{f⁻¹O_D} f⁻¹F of Stacks 03D6(2) of a finite locally free sheaf of O_D-modules along a morphism of ringed topoi (f, f♯) : (Sh(C), O_C) ⟶ (Sh(D), O_D) is finite locally free.

The two halves are Stacks.Sheaves.PresentationTransport.exists_cover_isFiniteFree_inverseImage, which produces a covering of each object of the source site on whose members f⁻¹F is finite free, and Stacks.Sheaves.FinitePresentation.isFiniteFree_extendScalarsOver, which carries that across extension of scalars along f⁻¹O_D ⟶ O_C.

theorem isFiniteLocallyFreeOnSite_pullbackModules {X : RingedTopos.{v, u, w}}
    {Y : RingedTopos.{v', u', w}}
    [X.J.HasSheafCompose (forget₂ CommRingCat.{w} RingCat.{w})]
    [Y.J.HasSheafCompose (forget₂ CommRingCat.{w} RingCat.{w})]
    [X.J.HasSheafCompose (forget RingCat.{w})]
    [Y.J.HasSheafCompose (forget RingCat.{w})]
    [X.J.HasSheafCompose (forget AddCommGrpCat.{w})]
    [Y.J.HasSheafCompose (forget AddCommGrpCat.{w})]
    [HasWeakSheafify X.J AddCommGrpCat.{w}] [HasWeakSheafify Y.J AddCommGrpCat.{w}]
    [X.J.WEqualsLocallyBijective AddCommGrpCat.{w}]
    [Y.J.WEqualsLocallyBijective AddCommGrpCat.{w}]
    [∀ Z : X.C, HasWeakSheafify (X.J.over Z) AddCommGrpCat.{w}]
    [∀ Z : Y.C, HasWeakSheafify (Y.J.over Z) AddCommGrpCat.{w}]
    [∀ Z : X.C, (X.J.over Z).WEqualsLocallyBijective AddCommGrpCat.{w}]
    [∀ Z : Y.C, (Y.J.over Z).WEqualsLocallyBijective AddCommGrpCat.{w}]
    (f : RingedToposModules.RingedToposHom X Y)
    (F : SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O))
    (hF : _root_.SheafOfModules.IsFiniteLocallyFreeOnSite F) :
    _root_.SheafOfModules.IsFiniteLocallyFreeOnSite (f.pullbackModules.obj F)

Stacks.Sheaves.FiniteType.pullbackModules_isFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ToposPullbackFiniteType.lean, line 249. The attribute's comment: “part (5), finite type: for an arbitrary morphism of ringed topoi”.

Stacks 03DO for the clause 03DL(5): pullback preserves finite type. The pullback f^*F = O_C ⊗_{f⁻¹O_D} f⁻¹F of Stacks 03D6(2) of a sheaf of O_D-modules of finite type along a morphism of ringed topoi (f, f♯) : (Sh(C), O_C) ⟶ (Sh(D), O_D) is of finite type.

The two factors are exists_cover_finite_generators_inverseImage, which produces a covering of each object of the source site carrying finitely many generating sections of f⁻¹F, and Stacks.Sheaves.LocalGeneration.extendScalars_exists_finite_generators, which carries those sections across extension of scalars along f⁻¹O_D ⟶ O_C; the result is assembled by Stacks.SheafOfModules.isFiniteType_of_locally_finite_generators.

theorem pullbackModules_isFiniteType
    {X : AlgebraicGeometry.RingedTopos.{v, u, w}}
    {Y : AlgebraicGeometry.RingedTopos.{v', u', w}}
    [X.J.HasSheafCompose (forget₂ CommRingCat.{w} RingCat.{w})]
    [Y.J.HasSheafCompose (forget₂ CommRingCat.{w} RingCat.{w})]
    [X.J.HasSheafCompose (forget RingCat.{w})]
    [Y.J.HasSheafCompose (forget RingCat.{w})]
    [X.J.HasSheafCompose (forget AddCommGrpCat.{w})]
    [Y.J.HasSheafCompose (forget AddCommGrpCat.{w})]
    [HasWeakSheafify X.J AddCommGrpCat.{w}]
    [X.J.WEqualsLocallyBijective AddCommGrpCat.{w}]
    [∀ U : X.C, HasWeakSheafify (X.J.over U) AddCommGrpCat.{w}]
    [∀ U : Y.C, HasWeakSheafify (Y.J.over U) AddCommGrpCat.{w}]
    [∀ U : X.C, (X.J.over U).WEqualsLocallyBijective AddCommGrpCat.{w}]
    [∀ U : Y.C, (Y.J.over U).WEqualsLocallyBijective AddCommGrpCat.{w}]
    (f : Stacks.Sheaves.RingedToposModules.RingedToposHom X Y)
    (F : SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O))
    (hF : F.IsFiniteType) :
    ((f.pullbackModules).obj F).IsFiniteType

Stacks.Sheaves.LocalGeneration.pullbackModules_isLocallyGeneratedByOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ToposPullbackLocalGeneration.lean, line 1260. The attribute's comment: “part (4), locally generated by r sections: for an arbitrary morphism of ringed topoi”.

The pullback of a sheaf of modules that is locally generated by r sections along a morphism of ringed topoi is again locally generated by r sections.

theorem pullbackModules_isLocallyGeneratedByOnSite
    {X : AlgebraicGeometry.RingedTopos.{v, u, w}}
    {Y : AlgebraicGeometry.RingedTopos.{v', u', w}}
    [X.J.HasSheafCompose (forget₂ CommRingCat.{w} RingCat.{w})]
    [Y.J.HasSheafCompose (forget₂ CommRingCat.{w} RingCat.{w})]
    [X.J.HasSheafCompose (forget RingCat.{w})]
    [Y.J.HasSheafCompose (forget RingCat.{w})]
    [X.J.HasSheafCompose (forget AddCommGrpCat.{w})]
    [Y.J.HasSheafCompose (forget AddCommGrpCat.{w})]
    [HasWeakSheafify X.J AddCommGrpCat.{w}]
    [X.J.WEqualsLocallyBijective AddCommGrpCat.{w}]
    [∀ U : X.C, HasWeakSheafify (X.J.over U) AddCommGrpCat.{w}]
    [∀ U : Y.C, HasWeakSheafify (Y.J.over U) AddCommGrpCat.{w}]
    [∀ U : X.C, (X.J.over U).WEqualsLocallyBijective AddCommGrpCat.{w}]
    [∀ U : Y.C, (Y.J.over U).WEqualsLocallyBijective AddCommGrpCat.{w}]
    (f : RingedToposModules.RingedToposHom X Y)
    (F : SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)) (r : ℕ)
    (hF : F.IsLocallyGeneratedByOnSite r) :
    ((RingedToposModules.RingedToposHom.pullbackModules f).obj F).IsLocallyGeneratedByOnSite r

Stacks.Sheaves.FinitePresentation.isFinitePresentation_pullbackModules, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/ToposPullbackPresentationAssembly.lean, line 205. The attribute's comment: “part (7), finite presentation: for an arbitrary morphism of ringed topoi”. References: EGA 0 (5.2.5), “more general”.

Stacks 03DO for the clause 03DL (7): pullback preserves finite presentation. The pullback f^*F = O_C ⊗_{f⁻¹O_D} f⁻¹F of Stacks 03D6 (2) of a sheaf of O_D-modules of finite presentation along a morphism of ringed topoi (f, f♯) : (Sh(C), O_C) ⟶ (Sh(D), O_D) is of finite presentation.

The two halves are Stacks.Sheaves.PresentationTransport.exists_cover_isFinite_presentation_inverseImage, which produces a covering of each object of the source site carrying a finite presentation of f⁻¹F, and Stacks.Sheaves.FinitePresentation.isFinitePresentation_pullbackModules_of_inverseImage_local, which transports those presentations across extension of scalars along f⁻¹O_D ⟶ O_C and assembles them.

instance isFinitePresentation_pullbackModules {X : RingedTopos.{v, u, w}}
    {Y : RingedTopos.{v', u', w}}
    [X.J.HasSheafCompose (forget₂ CommRingCat.{w} RingCat.{w})]
    [Y.J.HasSheafCompose (forget₂ CommRingCat.{w} RingCat.{w})]
    [X.J.HasSheafCompose (forget RingCat.{w})]
    [Y.J.HasSheafCompose (forget RingCat.{w})]
    [X.J.HasSheafCompose (forget AddCommGrpCat.{w})]
    [Y.J.HasSheafCompose (forget AddCommGrpCat.{w})]
    [HasWeakSheafify X.J AddCommGrpCat.{w}] [HasWeakSheafify Y.J AddCommGrpCat.{w}]
    [X.J.WEqualsLocallyBijective AddCommGrpCat.{w}]
    [Y.J.WEqualsLocallyBijective AddCommGrpCat.{w}]
    [∀ U : X.C, HasWeakSheafify (X.J.over U) AddCommGrpCat.{w}]
    [∀ U : Y.C, HasWeakSheafify (Y.J.over U) AddCommGrpCat.{w}]
    [∀ U : X.C, (X.J.over U).WEqualsLocallyBijective AddCommGrpCat.{w}]
    [∀ U : Y.C, (Y.J.over U).WEqualsLocallyBijective AddCommGrpCat.{w}]
    (f : RingedToposHom X Y) (F : SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf Y.O))
    [F.IsFinitePresentation] : ((f.pullbackModules).obj F).IsFinitePresentation

AlgebraicGeometry.Space.isFiniteLocallyFreeOnSite_modulePullback_of_isEtale, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteLocallyFreeModulePullback.lean, line 74. The attribute's comment: “the finite locally free property, clause 03DL (2), along an étale morphism of algebraic spaces”.

The inverse image of a finite locally free 𝒪_Y-module along an étale morphism f : X ⟶ Y of algebraic spaces is finite locally free.

theorem isFiniteLocallyFreeOnSite_modulePullback_of_isEtale
    {X Y : AlgebraicSpaces B S hS} (f : X ⟶ Y) (hf : IsEtale B S hS f.hom)
    (M : Modules.{u, u} B S hS Y.1 Y.2)
    (hM : SheafOfModules.IsFiniteLocallyFreeOnSite M) :
    SheafOfModules.IsFiniteLocallyFreeOnSite ((modulePullback B S hS f).obj M)

AlgebraicGeometry.Space.isFiniteLocallyFreeOnSite_modulePullback_representedSpaceMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteLocallyFreeModulePullback.lean, line 167. The attribute's comment: “the finite locally free property, clause 03DL (2), along a morphism of representable algebraic spaces”.

The inverse image of a quasi-coherent finite locally free module along the morphism of representable algebraic spaces attached to a morphism g of the big fppf category is finite locally free.

theorem isFiniteLocallyFreeOnSite_modulePullback_representedSpaceMap
    {T' T : BigFppfOver B S hS} (g : T' ⟶ T)
    (N : SheafOfModules.{u} (representedStructureRingSheaf B S hS T))
    (hN : N.IsQuasicoherentOnSite)
    (h : SheafOfModules.IsFiniteLocallyFreeOnSite N) :
    SheafOfModules.IsFiniteLocallyFreeOnSite
      ((modulePullback B S hS (representedSpaceMap B S hS g)).obj N)

AlgebraicGeometry.Space.isFiniteLocallyFreeOnSite_modulePullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/FiniteLocallyFreeModulePullback.lean, line 210. The attribute's comment: “the finite locally free property, clause 03DL (2), for the morphism of small étale ringed topoi of an arbitrary morphism of algebraic spaces, stated for a quasi-coherent module: the source assumes no such hypothesis, and it is carried here because the reduction to the representable case runs through the comparison of Stacks 03DX (2), which needs it”.

The inverse image a^*N of Stacks 03LU of a quasi-coherent finite locally free 𝒪_Y-module along a morphism a : X ⟶ Y of algebraic spaces over S is finite locally free.

theorem isFiniteLocallyFreeOnSite_modulePullback {X Y : AlgebraicSpaces B S hS} (a : X ⟶ Y)
    (N : Modules.{u, u} B S hS Y.1 Y.2) (hN : N.IsQuasicoherentOnSite)
    (h : SheafOfModules.IsFiniteLocallyFreeOnSite N) :
    SheafOfModules.IsFiniteLocallyFreeOnSite ((modulePullback B S hS a).obj N)

AlgebraicGeometry.Space.isFiniteLocallyFreeOnSite_modulePullback_of_isFiniteLocallyFreeOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/Thickenings/LiftingSheafQuasicoherentSmooth.lean, line 86. The attribute's comment: “the finite locally free property, clause 03DL (2), for the morphism of small étale ringed topoi of an arbitrary morphism of algebraic spaces, stated for a quasi-coherent module: the source assumes no such hypothesis, and it is carried here because the reduction to the representable case runs through the comparison of Stacks 03DX (2), which needs it”.

Stacks 03DO for the clause 03DL(2) at a morphism of algebraic spaces. The inverse image of Stacks 03LU of a finite locally free 𝒪_X-module on the small étale site is again finite locally free on the small étale site.

This is Stacks.Sheaves.FinitePresentation.isFiniteLocallyFreeOnSite_pullbackModules at the morphism of small étale ringed topoi of Stacks 03G8, exactly as AlgebraicGeometry.Space.isFinitePresentationOnSite_modulePullback is its companion for the clause 03DL(7). Stacks 03DO for the clause 03DL(2) is also registered against the ringed-topoi statement, of which this is the specialization; the registration below is the one previously carried by a version of this statement which additionally assumed the module quasi-coherent, so its clause text still speaks of that hypothesis. No hypothesis of the kind is needed here, because nothing in the proof passes through the comparison of Stacks 03DX (2).

theorem isFiniteLocallyFreeOnSite_modulePullback_of_isFiniteLocallyFreeOnSite
    {X' X : AlgebraicSpaces B S hS} (g : X' ⟶ X)
    (F : Modules.{u, u} B S hS X.1 X.2)
    (hF : SheafOfModules.IsFiniteLocallyFreeOnSite F) :
    SheafOfModules.IsFiniteLocallyFreeOnSite ((modulePullback B S hS g).obj F)

Sources

LeanSheafOfModules.IsLocallyFreeOnSite · SheafOfModules.IsFiniteLocallyFreeOnSite · SheafOfModules.IsLocallyGeneratedBySectionsOnSite · SheafOfModules.IsLocallyGeneratedByOnSite · SheafOfModules.IsFinitePresentationOnSite · SheafOfModules.IsCoherentOnSite · SheafOfModules.IsQuasicoherentOnSite · SheafOfModules.IsFiniteType

Section18.24 Basic results on local types of modules #

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

Tag 0H98, a lemma

Tag 0H98 in the Stacks Project.

Stacks.SheafOfModules.LocalCokernel.isFinitePresentation_cokernel, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/CokernelFinitePresentation.lean, line 716.

Stacks Project, Tag 0H98. The cokernel of a morphism from a finite-type sheaf of modules to a finitely presented sheaf of modules on a ringed site is finitely presented.

theorem isFinitePresentation_cokernel
    (X : AlgebraicGeometry.RingedSite.{u, v, w})
    [HasWeakSheafify X.J AddCommGrpCat.{w}]
    [X.J.WEqualsLocallyBijective AddCommGrpCat.{w}]
    [∀ U : X.C, HasWeakSheafify (X.J.over U) AddCommGrpCat.{w}]
    [∀ U : X.C, (X.J.over U).WEqualsLocallyBijective AddCommGrpCat.{w}]
    {F G : SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)} (φ : G ⟶ F)
    [F.IsFinitePresentation] [G.IsFiniteType] :
    (cokernel φ).IsFinitePresentation

Tag 082T, a lemma

Tag 082T in the Stacks Project.

Stacks.SheafOfModules.SliceFinite.isFiniteType_kernel_of_epi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/SliceRestrictionFiniteKernel.lean, line 226.

On a site with no products and no pullbacks assumed, the kernel of a surjection from a sheaf of modules of finite type onto a sheaf of modules of finite presentation is of finite type. This also gives Stacks Project, Tag 01BP part (2).

theorem isFiniteType_kernel_of_epi {F G : SheafOfModules.{u} R}
    [F.IsFinitePresentation] [G.IsFiniteType] (theta : G ⟶ F) [Epi theta] :
    (kernel theta).IsFiniteType

Tag 0GZN, a lemma

Tag 0GZN in the Stacks Project.

ChaoticQCoh.quasiCoherent_iff_canonicalMap_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Presheaf/QuasicoherentChaotic.lean, line 913.

Stacks Tag 0GZN, Lemma 18.24.3: A sheaf of O-modules F on the chaotic site C is quasi-coherent if and only if for every morphism f : U ⟶ V of C the canonical map c_f : F(V) ⊗_{O(V)} O(U) ⟶ F(U) is an isomorphism.

theorem quasiCoherent_iff_canonicalMap_isIso :
    QuasiCoherent O F ↔ ∀ ⦃U V : C⦄ (f : U ⟶ V), IsIso (canonicalMap O F f)

Stacks.SheafOfModules.isQuasicoherent_iff_canonicalMap_isIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/QuasicoherentChaoticSite.lean, line 682.

A module sheaf on a chaotic site is quasi-coherent precisely when its canonical base-change maps are isomorphisms.

public theorem isQuasicoherent_iff_canonicalMap_isIso
    (hX : X.J = ⊥) :
    F.IsQuasicoherentOnSite ↔
      ∀ ⦃U V : X.C⦄ (f : U ⟶ V), IsIso (canonicalMap X F f)

Tag 0GZP, a lemma

Tag 0GZP in the Stacks Project.

Stacks.Sheaves.ChaoticFlatQuasicoherent.isQuasicoherentOnSite_isWeakSerreClass, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Topologies/ChaoticFlatQuasicoherent.lean, line 475.

Quasi-coherent modules on a chaotic site with flat restrictions form a weak Serre subcategory of all sheaves of modules.

public instance isQuasicoherentOnSite_isWeakSerreClass
    (X : RingedSite.{u, v, r}) [Fact (X.J = ⊥)]
    [Fact (∀ {U V : X.Cᵒᵖ} (a : V ⟶ U),
      RingHom.Flat (X.O.obj.map a).hom)] :
    ObjectProperty.IsWeakSerreClass
      (SheafOfModules.isQuasicoherentOnSite (Stacks.SheafOfModules.Tensor.ringSheaf X.O) :
        ObjectProperty (SheafOfModules.{m} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))

Sources

LeanStacks.SheafOfModules.LocalCokernel.isFinitePresentation_cokernel · Stacks.SheafOfModules.SliceFinite.isFiniteType_kernel_of_epi · ChaoticQCoh.quasiCoherent_iff_canonicalMap_isIso · Stacks.SheafOfModules.isQuasicoherent_iff_canonicalMap_isIso · Stacks.Sheaves.ChaoticFlatQuasicoherent.isQuasicoherentOnSite_isWeakSerreClass

Section18.25 Closed immersions of ringed topoi #

Section 18.25 of the Stacks Project, Tag 08M2. 1 tag here is carried by 4 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 08M3, a lemma

Tag 08M3 in the Stacks Project.

AlgebraicGeometry.ClosedRingedImmersion.pushforwardModules_exact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/PushforwardEssentialImageDirect/Exactness.lean, line 263. The attribute's comment: “exactness”. References: SGA 4 IV (13.6), “special case”.

Stacks Project, Tag 08M3. The direct image of sheaves of modules along a closed immersion of ringed topoi with locally surjective structure map is exact.

Left exactness: the underlying sheaf of sets of the direct image is the direct image of the underlying sheaf of sets, the latter preserves finite limits because it is a right adjoint, and the underlying-sheaf functor on sheaves of modules preserves and reflects them. Right exactness: the direct image is fully faithful with essential image the modules annihilated by the kernel ideal, hence a left adjoint, hence preserves all colimits.

theorem ClosedRingedImmersion.pushforwardModules_exact
    (S : ClosedRingedImmersion.{v, u, v', u', w}) :
    exactFunctor (_root_.SheafOfModules.{w} S.sourceRingSheaf)
      (_root_.SheafOfModules.{w} S.targetRingSheaf) S.hom.pushforwardModules

Stacks.Sheaves.PushforwardEssentialImage.essImage_pushforwardModules_iff_of_isClosedImmersion, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/PushforwardEssentialSurjectivity.lean, line 408. The attribute's comment: “essential_image”.

Stacks 08M3, the essential-image statement. Let i : (Sh(C), O) → (Sh(D), O') be a morphism of ringed topoi whose underlying morphism of topoi is a closed immersion and whose structure map i^# : O' ⟶ i_*O is locally surjective, and let I ⊆ O' be the sectionwise kernel of i^#. Then a sheaf of O'-modules is in the essential image of the direct image i_* : Mod(O) ⥤ Mod(O') exactly when I annihilates it.

The forward implication needs neither hypothesis on i (smul_eq_zero_of_essImage_pushforwardModules); the reverse one spends local surjectivity in Stacks.SheafOfModules.ChangeOfRings.essImage_restrictScalars_of_smul_eq_zero and the closed-immersion hypothesis in essSurj_pushforwardModuleFunctor.

theorem essImage_pushforwardModules_iff_of_isClosedImmersion
    (hfc : MorphismOfTopoi.IsClosedImmersion f) {O' : Sheaf K RingCat.{w}}
    (fSharp : O' ⟶ pushforwardRingSheaf f O) [Sheaf.IsLocallySurjective fSharp]
    (G : SheafOfModules.{w} O') :
    (pushforwardModules f O fSharp).essImage G ↔
      ∀ (X : Dᵒᵖ) (a : O'.obj.obj X), a ∈ RingHom.ker (fSharp.hom.app X).hom →
        ∀ m : G.val.obj X, a • m = 0

AlgebraicGeometry.ClosedRingedImmersion.pushforwardModules_fullyFaithful, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/PushforwardFullyFaithful/Basic.lean, line 152. The attribute's comment: “full_faithfulness”.

Stacks 08M3. The direct image of sheaves of modules along a closed immersion of ringed topoi with locally surjective structure map is fully faithful.

The direct image is the Stacks 03D1 direct image followed by restriction of scalars along the structure map. The first factor is fully faithful because the direct image of sheaves of sets is, the underlying morphism of topoi being an embedding; the second is fully faithful by Stacks 0930, the structure map being locally surjective.

theorem pushforwardModules_fullyFaithful :
    Nonempty S.hom.pushforwardModules.FullyFaithful

Stacks.ToposBridge.essImage_schemeModulesPushforward_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/ClosedImmersion/TopoiBridge/EssentialImage.lean, line 106. The attribute's comment: “essential_image, for a closed immersion of schemes”.

The essential-image half of Stacks 08M3 for a closed immersion of schemes. A sheaf of 𝒪_X-modules lies in the essential image of pushforward along a closed immersion i : Z ⟶ X exactly when the sectionwise kernel of the structure map of i annihilates it.

This is Stacks.ToposBridge.essImage_pushforwardModules_iff_of_iso at the morphism of topoi presented by i, whose closed-immersion and local-surjectivity hypotheses hold for a closed immersion of schemes, transported along Stacks.ToposBridge.schemePushforwardModulesIso.

theorem essImage_schemeModulesPushforward_iff {Z X : Scheme.{u}} (i : Z ⟶ X)
    [AlgebraicGeometry.IsClosedImmersion i] (G : X.Modules) :
    (Scheme.Modules.pushforward i).essImage G ↔
      ∀ (U : (Opens X.carrier)ᵒᵖ) (a : X.ringCatSheaf.obj.obj U),
        a ∈ RingHom.ker ((toposStructureRingMap i.toLRSHom.toShHom).hom.app U).hom →
          ∀ m : G.val.obj U, a • m = 0

Sources

LeanAlgebraicGeometry.ClosedRingedImmersion.pushforwardModules_exact · Stacks.Sheaves.PushforwardEssentialImage.essImage_pushforwardModules_iff_of_isClosedImmersion · AlgebraicGeometry.ClosedRingedImmersion.pushforwardModules_fullyFaithful · Stacks.ToposBridge.essImage_schemeModulesPushforward_iff

Section18.26 Tensor product #

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

Tag 0GMW, a lemma

Tag 0GMW in the Stacks Project.

PresheafOfModules.sheafificationTensorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/SheafificationTensor.lean, line 994.

Sheafification commutes with the tensor product of presheaves of modules: there is an isomorphism F⁺ ⊗_{O⁺} G⁺ ≅ (F ⊗_{p,O} G)⁺, natural in both presheaves of modules, where the left-hand tensor product is the sheafification of the objectwise tensor product of the two sheaves of sections.

noncomputable def sheafificationTensorIso :
    Functor.prod (moduleSheafification.{v, u, w, z} J a)
          (moduleSheafification.{v, u, w, z₁} J a) ⋙
        (Functor.uncurry.obj (Stacks.SheafOfModules.Tensor.sheafTensor.{u, v, w, z, z₁} Osharp)) ≅
      Functor.uncurry.obj (tensorBifunctor.{v, u, w, z, z₁} O) ⋙
        moduleSheafification.{v, u, w, max z z₁} J a

PresheafOfModules.sheafificationTensorIso_hom_unit_tmul, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/SheafificationTensor.lean, line 1019.

The isomorphism sheafificationTensorIso sends the image, under the unit exhibiting the tensor product sheaf as a sheafification, of a pure tensor of two sheafification-unit images to the sheafification-unit image of the original pure tensor.

lemma sheafificationTensorIso_hom_unit_tmul (U : Cᵒᵖ) (x : F.obj U) (y : G.obj U) :
    Hom.app ((sheafificationTensorIso.{v, u, w, z, z₁} J a).hom.app (F, G)).val U
        (Hom.app ((PresheafOfModules.sheafificationAdjunction
            (R := Stacks.SheafOfModules.Tensor.ringSheaf Osharp)
            (𝟙 (Stacks.SheafOfModules.Tensor.ringSheaf Osharp).obj)).unit.app
            (tensorObj (((moduleSheafification.{v, u, w, z} J a).obj F)).val
              (((moduleSheafification.{v, u, w, z₁} J a).obj G)).val)) U
          (Hom.app (moduleSheafificationUnit.{v, u, w, z} J a F) U x ⊗ₜ
            Hom.app (moduleSheafificationUnit.{v, u, w, z₁} J a G) U y)) =
      Hom.app (moduleSheafificationUnit.{v, u, w, max z z₁} J a (tensorObj F G)) U (x ⊗ₜ y)

Declarations registered for the tag:

PresheafOfModules.sheafificationTensorIso, declared in the repository, registered with add_to_stacks in StacksFrontier/CategoryTheory/Sites/Modules/Tensor.lean, line 304 (StacksFrontier).
PresheafOfModules.sheafificationTensorIso_hom_unit_tmul, declared in the repository, registered with add_to_stacks in StacksFrontier/CategoryTheory/Sites/Modules/Tensor.lean, line 305 (StacksFrontier).

Tag 03EL, a lemma

Tag 03EL in the Stacks Project.

Stacks.SheafOfModules.pullbackTensorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/PullbackTensor.lean, line 1006. References: SGA 4 IV (13.4), “special case”.

Stacks 03EL. For a morphism of ringed topoi (f, f♯) : (Sh(C), O_C) ⟶ (Sh(D), O_D), the pullback of a tensor product of sheaves of O_D-modules is the tensor product of their pullbacks,

f^*(F ⊗_{O_D} G) ≅ f^*F ⊗_{O_C} f^*G,

naturally in F and in G. The comparison is the one determined by the chain of bijections Stacks.SheafOfModules.pullbackTensorHomEquiv, whose naturality in the sheaf of values turns it into a morphism of sheaves of modules and whose naturality in F and G makes that morphism a natural transformation.

def pullbackTensorIso :
    (Functor.uncurry.obj (Stacks.SheafOfModules.Tensor.sheafTensor.{u', v', w', w', w'} Y.O)) ⋙
        f.pullbackModules ≅
      Functor.prod (f.pullbackModules) (f.pullbackModules) ⋙
        (Functor.uncurry.obj (Stacks.SheafOfModules.Tensor.sheafTensor.{u, v, w, w, w} X.O))

Stacks.Sheaves.RingedPoint.RingedPointSituation.stalkTensorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/RingedPointStalkTensor.lean, line 90. The attribute's comment: “the stalk at a point of a ringed topos commutes with the tensor product”.

The stalk commutes with the tensor product of sheaves of modules. At a point p of a ringed topos (Sh(C), O) the module-valued stalk carries a tensor product of sheaves of O-modules to the tensor product of the stalks over O_p,

(F ⊗_O G)_p ≅ F_p ⊗_{O_p} G_p,

naturally in F and in G. This is Tag 03EL — the compatibility of pullback with the tensor product along a morphism of ringed topoi — read along the morphism out of the ringed point of Section 18.37, whose pullback on modules is the stalk (RingedPointSituation.pullbackStalkIso).

def stalkTensorIso :
    (Functor.uncurry.obj (Stacks.SheafOfModules.Tensor.sheafTensor X.O)) ⋙ s.stalkModules ≅
      Functor.prod s.stalkModules s.stalkModules ⋙
        (Functor.uncurry.obj (Stacks.SheafOfModules.Tensor.sheafTensor s.point.O))

Stacks.SheafOfModules.RingedToposPullback.pullbackCoherence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/RingedToposPullbackCoherence.lean, line 79. The attribute's comment: “the comparison of the pullback with the tensor product is a monoidal structure: the three coherences”.

The coherence of Tag 03EL, proved. The comparison f^*(F ⊗_{O_D} G) ≅ f^*F ⊗_{O_C} f^*G is compatible with the associator and with both unitors, the unit object being matched by ν : f^*O_D ≅ O_C. The three fields are Stacks.SheafOfModules.RingedToposPullback.associativity, leftUnitality and rightUnitality; there is no hypothesis, and the four universes of the two ringed topoi stay independent.

theorem pullbackCoherence : PullbackCoherence f

CategoryTheory.SimplicialSiteSituation.componentRestrictionTensorTotalIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Simplicial/ComponentRingedTopos/ComponentTensorComplex.lean, line 97. The attribute's comment: “on total complexes, for restriction to a simplicial component”.

Stacks 03EL on total complexes, at the component inclusion. Restriction to the degree-n component commutes with the total tensor complex: g_n^*Tot(K ⊗_O L) ≅ Tot(g_n^*K ⊗_{O_n} g_n^*L), the comparison on the summand of bidegree (p, q) being g_n^*(K^p ⊗_O L^q) ≅ g_n^*K^p ⊗_{O_n} g_n^*L^q.

def componentRestrictionTensorTotalIso
    (K L : CochainComplex (S.totalRingedTopos O).Modules ℤ) :
    (S.componentModulesRestrictionComplex O n).obj
        (HomologicalComplex.mapBifunctor K L
          (Stacks.SheafOfModules.Tensor.sheafTensor (S.totalRingedTopos O).O)
          (ComplexShape.up ℤ)) ≅
      HomologicalComplex.mapBifunctor ((S.componentModulesRestrictionComplex O n).obj K)
        ((S.componentModulesRestrictionComplex O n).obj L)
        (Stacks.SheafOfModules.Tensor.sheafTensor (S.componentRingedTopos O n).O)
        (ComplexShape.up ℤ)

AlgebraicGeometry.Space.modulePullbackTensorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/Spaces/SmallEtaleModulePullbackTensor.lean, line 66. The attribute's comment: “for the small étale ringed topoi of a morphism of algebraic spaces”.

Stacks 03EL for a morphism of algebraic spaces. The inverse image of a tensor product of 𝒪_Y-modules along f : X ⟶ Y is the tensor product of the inverse images, f^*(G ⊗_{𝒪_Y} G') ≅ f^*G ⊗_{𝒪_X} f^*G'.

AlgebraicGeometry.Space.modulePullback is the inverse image of modules of the morphism of small étale ringed topoi of Stacks 03G8, so this is Stacks.SheafOfModules.pullbackTensorIso at that morphism, with the tensor product sheaf matched with the monoidal product by AlgebraicGeometry.Space.modulesTensorObjIso on each side.

noncomputable def modulePullbackTensorIso (f : X ⟶ Y)
    (G G' : Modules.{u, u} B S hS Y.1 Y.2) :
    (modulePullback B S hS f).obj (G ⊗ G') ≅
      (modulePullback B S hS f).obj G ⊗ (modulePullback B S hS f).obj G'

Tag 03L6, a lemma

Tag 03L6 in the Stacks Project.

Stacks.SheafOfModules.TensorLocalProperties.tensorSheaf_isCoherentOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/TensorCoherentOnSite.lean, line 70. The attribute's comment: “coherent”. References: EGA I (9.1.1), “coherent tensor”; EGA 0 (5.3.5), “tensor product”.

Stacks Project, Tag 03L6, coherent case. The tensor product of two coherent sheaves of modules on a ringed site is coherent.

Following the source: a coherent sheaf of modules is of finite presentation, so the mixed finite-presentation/coherence clause applies. The argument is run at the universe lift of the ringed site, where the presentation machinery of Stacks 01BW(1) is available, and transported back along Stacks.SheafOfModules.CoherentLift.isCoherentOnSite_liftModule_iff and Stacks.SheafOfModules.CoherentLift.tensorLiftIso.

theorem tensorSheaf_isCoherentOnSite (X : AlgebraicGeometry.RingedSite.{u, v, w})
    [X.J.HasSheafCompose (forget₂ CommRingCat.{w} RingCat.{w})]
    [HasWeakSheafify X.J AddCommGrpCat.{w}]
    [X.J.WEqualsLocallyBijective AddCommGrpCat.{w}]
    (F G : _root_.SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))
    [hF : _root_.SheafOfModules.IsCoherentOnSite F]
    [hG : _root_.SheafOfModules.IsCoherentOnSite G] :
    _root_.SheafOfModules.IsCoherentOnSite
      (((Stacks.SheafOfModules.Tensor.sheafTensor X.O).obj F).obj G)

Stacks.SheafOfModules.TensorLocalProperties.tensorSheaf_isFiniteType, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/TensorFiniteness.lean, line 304. The attribute's comment: “finite_type”.

Stacks Project, Tag 03L6, finite type case. The tensor product of two sheaves of modules of finite type on a ringed site is of finite type.

theorem tensorSheaf_isFiniteType (X : AlgebraicGeometry.RingedSite.{u, v, w})
    [X.J.HasSheafCompose (forget₂ CommRingCat.{w} RingCat.{w})]
    [HasWeakSheafify X.J AddCommGrpCat.{w}]
    [X.J.WEqualsLocallyBijective AddCommGrpCat.{w}]
    [∀ U : X.C, HasWeakSheafify (X.J.over U) AddCommGrpCat.{w}]
    [∀ U : X.C, (X.J.over U).WEqualsLocallyBijective AddCommGrpCat.{w}]
    (F G : _root_.SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))
    [_root_.SheafOfModules.IsFiniteType F] [_root_.SheafOfModules.IsFiniteType G] :
    _root_.SheafOfModules.IsFiniteType
      (((Stacks.SheafOfModules.Tensor.sheafTensor X.O).obj F).obj G)

Stacks.SheafOfModules.TensorLocalProperties.tensorSheaf_isLocallyGeneratedBySectionsOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/TensorFiniteness.lean, line 342. The attribute's comment: “locally_generated”.

Stacks Project, Tag 03L6, locally generated case. The tensor product of two sheaves of modules locally generated by sections on a ringed site is locally generated by sections.

theorem tensorSheaf_isLocallyGeneratedBySectionsOnSite
    (X : AlgebraicGeometry.RingedSite.{u, v, w})
    [X.J.HasSheafCompose (forget₂ CommRingCat.{w} RingCat.{w})]
    [HasWeakSheafify X.J AddCommGrpCat.{w}]
    [X.J.WEqualsLocallyBijective AddCommGrpCat.{w}]
    [∀ U : X.C, HasWeakSheafify (X.J.over U) AddCommGrpCat.{w}]
    [∀ U : X.C, (X.J.over U).WEqualsLocallyBijective AddCommGrpCat.{w}]
    (F G : _root_.SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))
    (hF : _root_.SheafOfModules.IsLocallyGeneratedBySectionsOnSite F)
    (hG : _root_.SheafOfModules.IsLocallyGeneratedBySectionsOnSite G) :
    _root_.SheafOfModules.IsLocallyGeneratedBySectionsOnSite
      (((Stacks.SheafOfModules.Tensor.sheafTensor X.O).obj F).obj G)

Stacks.SheafOfModules.TensorLocalProperties.tensorSheaf_isFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/TensorFinitePresentation.lean, line 142. The attribute's comment: “finite_presentation”.

Stacks Project, Tag 03L6, finite presentation case. The tensor product of two sheaves of modules of finite presentation on a ringed site is of finite presentation.

Following the source: F has a finite presentation over each member of a covering family and so does G; the objects admitting an arrow into a member of each family again cover, and over such an object the two restricted presentations are still finite and their tensor presentation presents the restriction of F ⊗ G.

theorem tensorSheaf_isFinitePresentation
    (F G : SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))
    [SheafOfModules.IsFinitePresentation F] [SheafOfModules.IsFinitePresentation G] :
    SheafOfModules.IsFinitePresentation
      (((Stacks.SheafOfModules.Tensor.sheafTensor X.O).obj F).obj G)

Stacks.SheafOfModules.TensorLocalProperties.tensorSheaf_isCoherent_of_isFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/TensorFinitePresentationCoherence.lean, line 188. The attribute's comment: “fp_tensor_coherent”.

Stacks Project, Tag 03L6, finite presentation against coherence. The tensor product of a sheaf of modules of finite presentation with a coherent sheaf of modules on a ringed site is coherent.

Following the source: F admits a finite presentation over each member of a covering family, the restriction of G to such a member is still coherent, and the tensor product formed on the slice site is the restriction of the global one by Stacks.SheafOfModules.TensorLocalProperties.tensorOverIso; so isCoherentOnSite_tensorSheaf_of_presentation applies on each member, and coherence is local on the site.

theorem tensorSheaf_isCoherent_of_isFinitePresentation
    (X : AlgebraicGeometry.RingedSite.{u, v, w})
    [X.J.HasSheafCompose (forget₂ CommRingCat.{w} RingCat.{w})]
    [HasWeakSheafify X.J AddCommGrpCat.{w}]
    [X.J.WEqualsLocallyBijective AddCommGrpCat.{w}]
    [∀ U : X.C, HasWeakSheafify (X.J.over U) AddCommGrpCat.{w}]
    [∀ U : X.C, (X.J.over U).WEqualsLocallyBijective AddCommGrpCat.{w}]
    (F G : _root_.SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))
    [_root_.SheafOfModules.IsFinitePresentation F]
    [hG : _root_.SheafOfModules.IsCoherentOnSite G] :
    _root_.SheafOfModules.IsCoherentOnSite
      (((Stacks.SheafOfModules.Tensor.sheafTensor X.O).obj F).obj G)

Stacks.SheafOfModules.TensorLocalProperties.tensorSheaf_isLocallyFreeOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/TensorLocallyFree.lean, line 562. The attribute's comment: “locally_free”.

Stacks Project, Tag 03L6, part (1). The tensor product of two locally free sheaves of modules on a ringed site is locally free.

theorem tensorSheaf_isLocallyFreeOnSite (X : AlgebraicGeometry.RingedSite.{u, v, w})
    [X.J.HasSheafCompose (forget₂ CommRingCat.{w} RingCat.{w})]
    [HasWeakSheafify X.J AddCommGrpCat.{w}]
    [X.J.WEqualsLocallyBijective AddCommGrpCat.{w}]
    (F G : SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))
    (hF : SheafOfModules.IsLocallyFreeOnSite F)
    (hG : SheafOfModules.IsLocallyFreeOnSite G) :
    SheafOfModules.IsLocallyFreeOnSite
      (((Functor.uncurry.obj (Stacks.SheafOfModules.Tensor.sheafTensor X.O))).obj
        (F, G))

Stacks.SheafOfModules.TensorLocalProperties.tensorSheaf_isFiniteLocallyFreeOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/TensorLocallyFree.lean, line 580. The attribute's comment: “finite_locally_free”.

Stacks Project, Tag 03L6, part (2). The tensor product of two finite locally free sheaves of modules on a ringed site is finite locally free.

theorem tensorSheaf_isFiniteLocallyFreeOnSite (X : AlgebraicGeometry.RingedSite.{u, v, w})
    [X.J.HasSheafCompose (forget₂ CommRingCat.{w} RingCat.{w})]
    [HasWeakSheafify X.J AddCommGrpCat.{w}]
    [X.J.WEqualsLocallyBijective AddCommGrpCat.{w}]
    (F G : SheafOfModules.{w} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))
    (hF : SheafOfModules.IsFiniteLocallyFreeOnSite F)
    (hG : SheafOfModules.IsFiniteLocallyFreeOnSite G) :
    SheafOfModules.IsFiniteLocallyFreeOnSite
      (((Functor.uncurry.obj (Stacks.SheafOfModules.Tensor.sheafTensor X.O))).obj
        (F, G))

Stacks.SheafOfModules.TensorLocalProperties.tensorSheaf_isQuasicoherentOnSite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/TensorQuasicoherentOnSite.lean, line 108. The attribute's comment: “quasi_coherent”. References: EGA I (9.1.1), “more general”.

Stacks Project, Tag 03L6, quasi-coherent case. The tensor product of two quasi-coherent sheaves of modules on a ringed site is quasi-coherent.

theorem tensorSheaf_isQuasicoherentOnSite (R : Sheaf J CommRingCat.{w})
    (F G : SheafOfModules.{w} (CategoryTheory.Sheaf.toRingCat J R))
    [SheafOfModules.IsQuasicoherentOnSite F] [SheafOfModules.IsQuasicoherentOnSite G] :
    SheafOfModules.IsQuasicoherentOnSite
      (((Stacks.SheafOfModules.Tensor.sheafTensor.{u, v, w, w, w} R).obj F).obj G)

Sources

LeanPresheafOfModules.sheafificationTensorIso · PresheafOfModules.sheafificationTensorIso_hom_unit_tmul · Stacks.SheafOfModules.pullbackTensorIso · Stacks.Sheaves.RingedPoint.RingedPointSituation.stalkTensorIso · Stacks.SheafOfModules.RingedToposPullback.pullbackCoherence · CategoryTheory.SimplicialSiteSituation.componentRestrictionTensorTotalIso · AlgebraicGeometry.Space.modulePullbackTensorIso · Stacks.SheafOfModules.TensorLocalProperties.tensorSheaf_isCoherentOnSite

Section18.27 Internal Hom #

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

Tag 03EM, a lemma

Tag 03EM in the Stacks Project.

internalHom_isSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Presheaf/InternalHom.lean, line 625. References: EGA 0 (4.1.5), “partial”; SGA 4 IV (12.4), “sheaf property”; SGA 3 IV (4.5.13), “special case”; SGA 4 IV (12.1), “partial”; SGA 4 IV (12.2), “Hom_A(M”; SGA 4 IV (12.5), “more general”.

Let O be a presheaf of commutative rings on a site C, let F be a presheaf of O-modules and let G be a sheaf of O-modules. Then the internal hom presheaf 𝓗om_O(F, G) = internalHom O F G is a sheaf of O-modules, i.e. its underlying abelian presheaf is a sheaf.

theorem internalHom_isSheaf
    (hG : Presheaf.IsSheaf J G.presheaf) :
    Presheaf.IsSheaf J (internalHom O F G).presheaf

Tag 0E8H, a lemma

Tag 0E8H in the Stacks Project.

Stacks.SheafOfModules.InternalHom.internalHomOverIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/InternalHomRestriction.lean, line 170.

Stacks 0E8H. Internal Hom commutes with restriction to the localized site over U.

noncomputable def internalHomOverIso
    (X : RingedSite.{u, v, w}) (U : X.C)
    (F G : _root_.SheafOfModules.{m} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) :
    (restrFun X.O.obj U).obj (internalHom X.O.obj F.val G.val) ≅
      internalHom (X.O.over U).obj
        ((restrFun X.O.obj U).obj F.val)
        ((restrFun X.O.obj U).obj G.val)

Stacks.SheafOfModules.InternalHom.internalHomOverIso_hom_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/InternalHomRestriction.lean, line 203. The attribute's comment: “canonical component on sections”.

At V ⟶ U, the isomorphism of Stacks 0E8H restricts a local morphism along the iterated-slice functor (C/U)/V ⥤ C/V.

theorem internalHomOverIso_hom_app
    (X : RingedSite.{u, v, w}) (U : X.C)
    (F G : _root_.SheafOfModules.{m} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))
    (V : (Over U)ᵒᵖ)
    (α : ((restrFun X.O.obj U).obj (internalHom X.O.obj F.val G.val)).obj V)
    (W : (Over V.unop)ᵒᵖ)
    (x : ((restrFun (X.O.over U).obj V.unop).obj
      ((restrFun X.O.obj U).obj F.val)).obj W) :
    ((((internalHomOverIso X U F G).hom.app V).hom α).app W).hom x =
      (α.app ((Over.iteratedSliceForward V.unop).op.obj W)).hom x

Tag 0GMX, a remark

Tag 0GMX in the Stacks Project.

Stacks.SheafOfModules.InternalHom.pullbackInternalHomMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/InternalHomAndFlatness/InternalHomPullback.lean, line 214. The attribute's comment: “the canonical map”.

Stacks 0GMX. The canonical map f^* Hom_{O_D}(F, G) ⟶ Hom_{O_C}(f^*F, f^*G) attached to a morphism of ringed sites: the transpose, under the correspondence of Stacks 03EO, of the pullback of the evaluation morphism.

noncomputable def pullbackInternalHomMap :
    (ringedSitePullback f).obj ((internalHomSecondFunctor Y.J Y.O F).obj G) ⟶
      (internalHomSecondFunctor X.J X.O ((ringedSitePullback f).obj F)).obj
        ((ringedSitePullback f).obj G)

Stacks.SheafOfModules.InternalHom.adjointPullbackInternalHomMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/InternalHomAndFlatness/InternalHomPullback.lean, line 226. The attribute's comment: “the adjoint map”.

Stacks 0GMX. The map Hom_{O_D}(F, G) ⟶ f_* Hom_{O_C}(f^*F, f^*G) displayed in the source: the adjoint of pullbackInternalHomMap under the adjunction f^* ⊣ f_* of Stacks 03D7.

noncomputable def adjointPullbackInternalHomMap :
    (internalHomSecondFunctor Y.J Y.O F).obj G ⟶
      (ringedSitePushforward f).obj
        ((internalHomSecondFunctor X.J X.O ((ringedSitePullback f).obj F)).obj
          ((ringedSitePullback f).obj G))

Stacks.SheafOfModules.InternalHom.tensorEvaluation_pullbackInternalHomMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/InternalHomAndFlatness/InternalHomPullback.lean, line 238. The attribute's comment: “compatibility of the canonical map with evaluation”.

Stacks 0GMX. The canonical map is compatible with evaluation: tensoring it with f^*F and then evaluating Hom_{O_C}(f^*F, f^*G) gives the pulled-back evaluation of Hom_{O_D}(F, G).

theorem tensorEvaluation_pullbackInternalHomMap :
    tensorEvaluation X.O ((ringedSitePullback f).obj F) ((ringedSitePullback f).obj G)
        (pullbackInternalHomMap f F G) =
      pullbackEvaluation f F G

Stacks.SheafOfModules.InternalHom.toposPullbackInternalHomMap_compOf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/InternalHomAndFlatness/PullbackInternalHomCompData.lean, line 171. The attribute's comment: “compatibility of the canonical map with composition, for a composite given as data”.

The canonical map is compatible with composition, with the composite supplied as data. Let φ : X ⟶ Y and ψ : Y ⟶ Z be morphisms of ringed topoi between the topoi of three ringed sites, let χ : X ⟶ Z play the role of their composite and let τ be a comparison of the geometric direct images carrying the composite structure map to the structure map of χ. Then the canonical map

χ^* Hom_{O_Z}(F, G) ⟶ Hom_{O_X}(χ^*F, χ^*G)

is the canonical map of ψ pulled back along φ, followed by the canonical map of φ, read through the comparison of pullbacks attached to (χ, τ) at Hom_{O_Z}(F, G), at the source of the internal Hom sheaf — through internalHomPre, the comparison in the first variable — and at its target.

theorem toposPullbackInternalHomMap_compOf
    (F G : SheafOfModules.{u} (Tensor.ringSheaf Z.O)) :
    toposPullbackInternalHomMap χ F G =
      toposPullbackCompComparisonOf φ ψ χ τ hτ ((internalHomSecondFunctor Z.J Z.O F).obj G) ≫
        (toposPullback φ).map (toposPullbackInternalHomMap ψ F G) ≫
          toposPullbackInternalHomMap φ ((toposPullback ψ).obj F) ((toposPullback ψ).obj G) ≫
            (internalHomPre X.O (toposPullbackCompComparisonOf φ ψ χ τ hτ F)).app
                ((toposPullback φ).obj ((toposPullback ψ).obj G)) ≫
              (internalHomSecondFunctor X.J X.O ((toposPullback χ).obj F)).map
                (toposPullbackCompComparisonInvOf φ ψ χ τ hτ G)

Stacks.SheafOfModules.InternalHom.toposPullbackInternalHomMap_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/InternalHomAndFlatness/PullbackInternalHomCompMap.lean, line 413. The attribute's comment: “compatibility of the canonical map with composition”.

The canonical map of Stacks 0GMX is compatible with composition. For morphisms of ringed topoi φ : X ⟶ Y and ψ : Y ⟶ Z between the topoi of three ringed sites and sheaves of O_Z-modules F, G, the canonical map

(ψ ∘ φ)^* Hom_{O_Z}(F, G) ⟶ Hom_{O_X}((ψ ∘ φ)^*F, (ψ ∘ φ)^*G)

of the composite is the canonical map of ψ pulled back along φ, followed by the canonical map of φ, read through the comparison of pullbacks along a composite at Hom_{O_Z}(F, G), at the source of the internal Hom sheaf — through internalHomPre, the comparison in the first variable — and at its target.

This is the law the localization square of Stacks 04J0 reduces to, and it is proved by the route the source's Remark 18.27.3 indicates: tensorEvaluation_injective turns it into an identity between two morphisms out of (ψ ∘ φ)^*Hom_{O_Z}(F, G) ⊗_{O_X} (ψ ∘ φ)^*F, where tensorEvaluation_comp and tensorEvaluation_comp_internalHomPre_comp_map read the composite route off and toposPullbackEvaluationExchange assembles the four inputs — the exchange of tensorings sheafTensor_exchange_three, the pulled-back tensor--evaluation composite toposPullback_tensorEvaluation, the naturality toposPullbackCompComparisonInv_naturality_pullbackTensorIso transported along the two readings of the inner pulled-back evaluation, and the composition law of Stacks 03EL pullbackTensorIso_inv_app_toposCompHom with the comparison of pullbacks cancelled off it by cancelWhisker.

theorem toposPullbackInternalHomMap_comp
    (F G : SheafOfModules.{u} (Tensor.ringSheaf Z.O)) :
    toposPullbackInternalHomMap (toposCompHom φ ψ) F G =
      toposPullbackCompComparison φ ψ ((internalHomSecondFunctor Z.J Z.O F).obj G) ≫
        (toposPullback φ).map (toposPullbackInternalHomMap ψ F G) ≫
          toposPullbackInternalHomMap φ ((toposPullback ψ).obj F) ((toposPullback ψ).obj G) ≫
            (internalHomPre X.O (toposPullbackCompComparison φ ψ F)).app
                ((toposPullback φ).obj ((toposPullback ψ).obj G)) ≫
              (internalHomSecondFunctor X.J X.O ((toposPullback (toposCompHom φ ψ)).obj F)).map
                (toposPullbackCompComparisonInv φ ψ G)

Stacks.SheafOfModules.InternalHom.toposPullbackInternalHomMap_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/InternalHomAndFlatness/PullbackInternalHomFlat.lean, line 999. The attribute's comment: “functoriality of the canonical map in the first variable”.

The canonical map of Stacks 0GMX is functorial in its first variable. For a morphism c : F' ⟶ F of sheaves of O_Y-modules the square built from the canonical maps at F and at F' and from the comparison internalHomPre in the first variable on the two sites commutes.

This is the "functoriality of Remark 18.27.3" that the proof of Stacks 0GN2 cites. By tensorEvaluation_injective it is an identity between two morphisms out of a tensor product, and there it is the naturality of the comparison of Stacks 03EL in its second variable: both sides become the pulled-back evaluation of Hom_{O_Y}(F, G) precomposed with c.

theorem toposPullbackInternalHomMap_naturality
    {F F' : SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf (J := Y.J)) Y.O)}
    (c : F' ⟶ F) :
    toposPullbackInternalHomMap φ F G ≫
        (internalHomPre X.O ((toposPullback φ).map c)).app ((toposPullback φ).obj G) =
      (toposPullback φ).map ((internalHomPre Y.O c).app G) ≫
        toposPullbackInternalHomMap φ F' G

Stacks.SheafOfModules.InternalHom.pullbackInternalHomNatural, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/InternalHomAndFlatness/PullbackInternalHomFlat.lean, line 1117. The attribute's comment: “first-variable functoriality, for a morphism of ringed sites”. References: EGA 0 (4.4.6), “Functoriality of γ♯”.

The canonical maps of Stacks 0GMX are functorial in the first variable. For a morphism c : F' ⟶ F of sheaves of O_D-modules the square built from the canonical maps at F and at F' and from the comparison internalHomPre on the two sites commutes.

This is the "functoriality of Remark 18.27.3" that the proof of Stacks 0GN2 cites. It is toposPullbackInternalHomMap_naturality at the morphism of ringed topoi of f, the two readings of the canonical map agreeing by toposPullbackInternalHomMap_ringedToposHom.

theorem pullbackInternalHomNatural
    {F F' : SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf (J := Y.J)) Y.O)}
    (c : F' ⟶ F) :
    pullbackInternalHomMap f F G ≫
        (internalHomPre X.O ((ringedSitePullback f).map c)).app
          ((ringedSitePullback f).obj G) =
      (ringedSitePullback f).map ((internalHomPre Y.O c).app G) ≫
        pullbackInternalHomMap f F' G

Tag 03EN, a lemma

Tag 03EN in the Stacks Project.

Stacks.PresheafOfModules.InternalHom.internalHomFunctor_preservesColimitsOfShape, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Presheaf/InternalHomVariance.lean, line 326. The attribute's comment: “presheaf_first_variable”.

For a fixed target G, internal Hom in the first variable sends arbitrary colimits of presheaves of O-modules to limits.

noncomputable instance internalHomFunctor_preservesColimitsOfShape
    (G : _root_.PresheafOfModules.{max u v} (Oforget O)) (I : Type w) [Category.{w} I] :
    PreservesColimitsOfShape I (internalHomFunctor O G)

Stacks.PresheafOfModules.InternalHom.internalHomSecondFunctor_preservesLimits, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Presheaf/InternalHomVariance.lean, line 566. The attribute's comment: “presheaf_second_variable”.

Internal Hom with fixed first variable commutes with arbitrary limits.

noncomputable instance internalHomSecondFunctor_preservesLimits :
    PreservesLimits (internalHomSecondFunctor.{v, u, w, m} O F)

Stacks.SheafOfModules.InternalHom.internalHomSecondFunctor_preservesLimits, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/InternalHomVariance.lean, line 89. The attribute's comment: “sheaf_second_variable”. References: SGA 4 IV (12.2), “partial”.

Stacks 03EN, sheaf case, second variable. Internal Hom from a fixed sheaf of modules commutes with arbitrary limits.

noncomputable instance internalHomSecondFunctor_preservesLimits
    (F : _root_.SheafOfModules.{max u v w m} (Tensor.ringSheaf O)) :
    PreservesLimits (internalHomSecondFunctor.{v, u, w, m} J O F)

Stacks.SheafOfModules.InternalHom.sheafInternalHomFunctor_preservesColimitsOfShape, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/InternalHomSiteVariance/FirstVariable.lean, line 192. The attribute's comment: “sheaf_first_variable”. References: SGA 4 IV (12.2), “partial, special case”.

Stacks 03EN, sheaf case, first variable. For a fixed target G, the internal Hom of sheaves of modules takes colimits in the first variable to limits.

public noncomputable instance sheafInternalHomFunctor_preservesColimitsOfShape
    (G : _root_.SheafOfModules.{max u v} (Tensor.ringSheaf O))
    (I : Type*) [Category I] :
    PreservesColimitsOfShape I (sheafInternalHomFunctor J O G)

Stacks.SheafOfModules.InternalHom.preservesFiniteColimits_internalHomFirstMate, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/InternalHomAndFlatness/PullbackInternalHomFlat.lean, line 865. The attribute's comment: “sheaf case, first variable, for the mate of the tensor comparison”. References: EGA 0 (6.7.6), “Left exactness of Hom(-”; SGA 4 IV (12.2), “partial, special case”.

Stacks 03EN in the first variable, for the mate. Internal Hom into a fixed sheaf of modules, contravariant in its source, carries finite colimits of sheaves of modules to finite limits of internal Hom sheaves.

This is the continuity that the proof of Stacks 0GN2 uses to pass from the structure sheaf to a finitely presented source, and it holds with no hypothesis: internalHomFirstMate is a left adjoint, by internalHomFirstMateAdjunction.

theorem preservesFiniteColimits_internalHomFirstMate :
    Limits.PreservesFiniteColimits (internalHomFirstMate O G)

Tag 0GMY, a lemma

Tag 0GMY in the Stacks Project.

Stacks.SheafOfModules.InternalHom.ringedSite_sheafInternalHomObjMapLeft_mono_of_epi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/InternalHomSiteVariance/FirstVariableLeftExact.lean, line 133. The attribute's comment: “exact_first_argument”. References: EGA 0 (4.1.5), “Injectivity of Hom(F”.

Stacks 0GMY, part (1). Precomposition along an epimorphism is a monomorphism of internal Hom sheaves, which is the initial zero of the target sequence.

theorem ringedSite_sheafInternalHomObjMapLeft_mono_of_epi
    {F₁ F G : _root_.SheafOfModules.{max u v} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)}
    (g : F₁ ⟶ F) [Epi g] :
    Mono (sheafInternalHomObjMapLeft X.J X.O (G := G) g)

Stacks.SheafOfModules.InternalHom.ringedSite_sheafInternalHomObjMapLeft_exact_of_exact_epi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/InternalHomSiteVariance/FirstVariableLeftExact.lean, line 149. The attribute's comment: “exact_first_argument”.

Stacks 0GMY, part (1). A right-exact sequence of sheaves of modules becomes exact at the middle term after applying internal Hom in the first argument.

theorem ringedSite_sheafInternalHomObjMapLeft_exact_of_exact_epi
    (S : ShortComplex (_root_.SheafOfModules.{max u v}
      (Stacks.SheafOfModules.Tensor.ringSheaf X.O)))
    (G : _root_.SheafOfModules.{max u v} (Stacks.SheafOfModules.Tensor.ringSheaf X.O))
    (hS : S.Exact) [Epi S.g] :
    ∃ h : sheafInternalHomObjMapLeft X.J X.O (G := G) S.g ≫
        sheafInternalHomObjMapLeft X.J X.O (G := G) S.f = 0,
      (ShortComplex.mk (sheafInternalHomObjMapLeft X.J X.O (G := G) S.g)
        (sheafInternalHomObjMapLeft X.J X.O (G := G) S.f) h).Exact

Declarations registered for the tag:

internalHomSecondFunctor_map_mono registered with add_to_stacks in StacksFrontier/CategoryTheory/Sites/Modules/InternalHomAndFlatness/InternalHomSecondVariable.lean, line 41 (StacksFrontier): “exact_second_argument”.
internalHomSecondFunctor_exact registered with add_to_stacks in StacksFrontier/CategoryTheory/Sites/Modules/InternalHomAndFlatness/InternalHomSecondVariable.lean, line 42 (StacksFrontier): “exact_second_argument”.

Tag 03EO, a lemma

Tag 03EO in the Stacks Project.

Stacks.PresheafOfModules.InternalHom.presheafInternalHomTensorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Presheaf/InternalHomTensorCurrying.lean, line 557. The attribute's comment: “presheaf_internal_hom_tensor_iso”.

Stacks 03EO. The canonical currying isomorphism from internal Hom out of a tensor product to iterated internal Hom.

noncomputable def presheafInternalHomTensorIso :
    internalHom O (F ⊗ G) H ≅ internalHom O F (internalHom O G H)

Stacks.PresheafOfModules.InternalHom.presheafInternalHomTensorIso_hom_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Presheaf/InternalHomTensorCurrying.lean, line 570. The attribute's comment: “presheaf_internal_hom_tensor_iso”.

On sections, the currying isomorphism is tensor currying: after restricting x, it evaluates the original morphism on x ⊗ y. This pins the isomorphism down, rather than merely asserting that some isomorphism exists.

theorem presheafInternalHomTensorIso_hom_app (a : (restrFun O U).obj (F ⊗ G) ⟶ (restrFun O U).obj H)
    {S : C} (p : S ⟶ U) (x : F.obj (op S)) {T : C} (q : T ⟶ S) (y : G.obj (op T)) :
    sectionOfRestr O H S q
        (((((((presheafInternalHomTensorIso O F G H).hom.app (op U)).hom a).app
            (op (Over.mk p))).hom (restrSection O F U p x)).app
              (op (Over.mk q))).hom (restrSection O G S q y)) =
      restrTensorHom O F G H U a (q ≫ p) (F.restrictₛₗ q.op x ⊗ₜ y)

Stacks.PresheafOfModules.InternalHom.presheafInternalHomTensorIso_natural_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Presheaf/InternalHomTensorCurrying.lean, line 636. The attribute's comment: “presheaf_internal_hom_tensor_iso”.

Stacks 03EO. The currying isomorphism is natural contravariantly in its first tensor factor.

theorem presheafInternalHomTensorIso_natural_left
    {F' : _root_.PresheafOfModules.{max u v w} (Oforget O)} (f : F' ⟶ F) :
    (presheafInternalHomTensorIso O F G H).hom ≫
        internalHomMapLeft O f =
      internalHomMapLeft O (f ⊗ₘ 𝟙 G) ≫
        (presheafInternalHomTensorIso O F' G H).hom

Stacks.PresheafOfModules.InternalHom.presheafInternalHomTensorIso_natural_middle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Presheaf/InternalHomTensorCurrying.lean, line 665. The attribute's comment: “presheaf_internal_hom_tensor_iso”.

Stacks 03EO. The currying isomorphism is natural contravariantly in its second tensor factor.

theorem presheafInternalHomTensorIso_natural_middle
    {G' : _root_.PresheafOfModules.{max u v w} (Oforget O)} (g : G' ⟶ G) :
    (presheafInternalHomTensorIso O F G H).hom ≫
        internalHomMapRight O F
          (internalHomMapLeft O g) =
      internalHomMapLeft O (𝟙 F ⊗ₘ g) ≫
        (presheafInternalHomTensorIso O F G' H).hom

Stacks.PresheafOfModules.InternalHom.presheafInternalHomTensorIso_natural_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Presheaf/InternalHomTensorCurrying.lean, line 677. The attribute's comment: “presheaf_internal_hom_tensor_iso”.

Stacks 03EO. The currying isomorphism is natural covariantly in its target.

theorem presheafInternalHomTensorIso_natural_right
    {H' : _root_.PresheafOfModules.{max u v w} (Oforget O)} (hh : H ⟶ H') :
    internalHomMapRight O (F ⊗ G) hh ≫
        (presheafInternalHomTensorIso O F G H').hom =
      (presheafInternalHomTensorIso O F G H).hom ≫
        internalHomMapRight O F
          (internalHomMapRight O G hh)

Stacks.PresheafOfModules.InternalHom.presheafTensorHomAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Presheaf/TensorHomAdjunction.lean, line 293. The attribute's comment: “presheaf_tensor_hom_adjunction”.

Stacks 03EO. Tensoring on the right by G is left adjoint to the internal-Hom functor with source G. Packaging the canonical correspondence as an adjunction records its naturality in both remaining variables.

noncomputable def presheafTensorHomAdjunction :
    (tensoringRight (_root_.PresheafOfModules.{max u v w} (Oforget O))).obj G ⊣
      internalHomSecondFunctor.{v, u, max u v w, u} O G

Stacks.PresheafOfModules.InternalHom.presheafTensorHomEquiv_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Presheaf/TensorHomAdjunction.lean, line 339. The attribute's comment: “presheaf_tensor_hom_adjunction”.

Stacks 03EO. The hom-equivalence of presheafTensorHomAdjunction is the canonical currying map: on sections it sends b to the map taking x and y to b (x ⊗ y).

theorem presheafTensorHomEquiv_apply (b : F ⊗ G ⟶ H) (U : C) (x : F.obj (op U))
    {T : C} (q : T ⟶ U) (y : G.obj (op T)) :
    sectionOfRestr O H U q
        (((((presheafTensorHomEquiv O F G H b).app (op U)).hom x).app
          (op (Over.mk q))).hom (restrSection O G U q y)) =
      globalTensorHom O F G H b T (F.restrictₛₗ q.op x ⊗ₜ y)

Stacks.PresheafOfModules.InternalHom.FreeUniverse.presheafTensorHomAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Presheaf/TensorHomAdjunctionFreeUniverse.lean, line 509. The attribute's comment: “presheaf_tensor_hom_adjunction, with the universe of the sections of the structure presheaf independent of the universes of the site”.

Stacks 03EO. Tensoring on the right by G is left adjoint to the internal-Hom functor with source G. Packaging the canonical correspondence as an adjunction records its naturality in both remaining variables.

noncomputable def presheafTensorHomAdjunction :
    (_root_.PresheafOfModules.tensorBifunctor O).flip.obj G ⊣
      internalHomSecondFunctor.{v, u, w, w} O G

Stacks.PresheafOfModules.InternalHom.FreeUniverse.presheafTensorHomEquiv_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Presheaf/TensorHomAdjunctionFreeUniverse.lean, line 557. The attribute's comment: “presheaf_tensor_hom_adjunction, with the universe of the sections of the structure presheaf independent of the universes of the site”.

Stacks 03EO. The hom-equivalence of presheafTensorHomAdjunction is the canonical currying map: on sections it sends b to the map taking x and y to b (x ⊗ y).

theorem presheafTensorHomEquiv_apply (b : F.tensorObj G ⟶ H) (U : C) (x : F.obj (op U))
    {T : C} (q : T ⟶ U) (y : G.obj (op T)) :
    sectionOfRestr O H U q
        (((((presheafTensorHomEquiv O F G H b).app (op U)).hom x).app
          (op (Over.mk q))).hom (restrSection O G U q y)) =
      globalTensorHom O F G H b T (F.restrictₛₗ q.op x ⊗ₜ y)

Stacks.SheafOfModules.InternalHom.sheafCurryIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/InternalHomTensorCurrying.lean, line 242. The attribute's comment: “sheaf_internal_hom_tensor_iso”.

Stacks 03EO, sheaf case. The canonical currying isomorphism for the sheafified tensor product and the internal Hom sheaf.

noncomputable def sheafCurryIso :
    siteSheafInternalHom J O (((Stacks.SheafOfModules.Tensor.sheafTensor O).obj F).obj G) H ≅
      siteSheafInternalHom J O F (siteSheafInternalHom J O G H)

Stacks.SheafOfModules.InternalHom.sheafCurryIso_hom_app_tmul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/InternalHomTensorCurrying.lean, line 287. The attribute's comment: “sheaf_internal_hom_tensor_iso”.

Stacks 03EO, sheaf case. The canonical isomorphism is tensor currying on every local pure tensor.

theorem sheafCurryIso_hom_app_tmul (U : C)
    (s : (siteSheafInternalHom J O
      (((Stacks.SheafOfModules.Tensor.sheafTensor O).obj F).obj G) H).val.obj (op U))
    (f : F.val.obj (op U)) (g : G.val.obj (op U)) :
    ((((((sheafCurryIso O F G H).hom.val.app (op U)).hom s).app
        (op (Over.mk (𝟙 U)))).hom f).app (op (Over.mk (𝟙 U)))).hom g =
      (s.app (op (Over.mk (𝟙 U)))).hom
        (toSheafTensorSection O F G U (f ⊗ₜ[O.obj.obj (op U)] g))

Stacks.SheafOfModules.InternalHom.sheafCurryIso_natural_left, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/InternalHomTensorCurrying.lean, line 305. The attribute's comment: “sheaf_internal_hom_tensor_iso”.

Stacks 03EO, sheaf case. Currying is contravariantly natural in the first tensor factor.

theorem sheafCurryIso_natural_left
    {F F' :
      _root_.SheafOfModules.{max u v} ((Stacks.SheafOfModules.Tensor.ringSheaf (J := J)) O)}
    (f : F' ⟶ F) :
    (sheafCurryIso O F G H).hom ≫ sheafInternalHomMapLeft J O f =
      sheafInternalHomMapLeft J O (sheafTensorMap O f (𝟙 G)) ≫
        (sheafCurryIso O F' G H).hom

Stacks.SheafOfModules.InternalHom.sheafCurryIso_natural_middle, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/InternalHomTensorCurrying.lean, line 322. The attribute's comment: “sheaf_internal_hom_tensor_iso”.

Stacks 03EO, sheaf case. Currying is contravariantly natural in the second tensor factor.

theorem sheafCurryIso_natural_middle
    {G G' :
      _root_.SheafOfModules.{max u v} ((Stacks.SheafOfModules.Tensor.ringSheaf (J := J)) O)}
    (g : G' ⟶ G) :
    (sheafCurryIso O F G H).hom ≫
        sheafInternalHomMapRight O (sheafInternalHomMapLeft J O g) =
      sheafInternalHomMapLeft J O (sheafTensorMap O (𝟙 F) g) ≫
        (sheafCurryIso O F G' H).hom

Stacks.SheafOfModules.InternalHom.sheafCurryIso_natural_right, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/InternalHomTensorCurrying.lean, line 340. The attribute's comment: “sheaf_internal_hom_tensor_iso”.

Stacks 03EO, sheaf case. Currying is covariantly natural in the target.

theorem sheafCurryIso_natural_right
    {H H' :
      _root_.SheafOfModules.{max u v} ((Stacks.SheafOfModules.Tensor.ringSheaf (J := J)) O)}
    (h : H ⟶ H') :
    sheafInternalHomMapRight O h ≫ (sheafCurryIso O F G H').hom =
      (sheafCurryIso O F G H).hom ≫
        sheafInternalHomMapRight O (sheafInternalHomMapRight O h)

Stacks.SheafOfModules.InternalHom.FreeUniverse.sheafTensorRightHomAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/TensorHomAdjunctionFreeUniverse.lean, line 95. The attribute's comment: “sheaf_tensor_hom_adjunction, with the universe of the sections of the structure sheaf independent of the universes of the site”.

Stacks 03EO, sheaf case, at a free ring universe. Tensoring on the right by G is left adjoint to the internal-Hom functor with source G, for a sheaf of rings whose sections lie in a universe independent of those of the site.

The presheaf clause Stacks.PresheafOfModules.InternalHom.FreeUniverse.presheafTensorHomAdjunction is composed with the sheafification adjunction and the result restricted along the fully faithful forgetful functor; this is legitimate because the right adjoint of the composite already takes values in sheaves, the internal Hom of Stacks 03EM being a sheaf as soon as its target is.

def sheafTensorRightHomAdjunction :
    (Stacks.SheafOfModules.Tensor.sheafTensor.{u, v, w, max u v w, max u v w} R).flip.obj G ⊣
      internalHomSecondFunctor.{v, u, w, w} J R G

Stacks.SheafOfModules.InternalHom.FreeUniverse.sheafTensorHomEquiv_apply, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/TensorHomAdjunctionFreeUniverse.lean, line 129. The attribute's comment: “sheaf_tensor_hom_adjunction, with the universe of the sections of the structure sheaf independent of the universes of the site”.

Stacks 03EO, sheaf case, at a free ring universe, on sections. The correspondence is the canonical currying map: a morphism b out of the sheafified tensor product is sent to the map taking a section x of F over U and a section y of G over T ⟶ U to the value of b on the image of the pure tensor x|_T ⊗ y.

theorem sheafTensorHomEquiv_apply
    (b : ((Stacks.SheafOfModules.Tensor.sheafTensor.{u, v, w, max u v w, max u v w} R).obj
      F).obj G ⟶ H) (U : C)
    (x : F.val.obj (Opposite.op U)) {T : C} (q : T ⟶ U)
    (y : G.val.obj (Opposite.op T)) :
    FreeUniverse.sectionOfRestr R.obj H.val U q
        (((((sheafTensorHomEquiv R F G H b).val.app (Opposite.op U)).hom x).app
          (Opposite.op (Over.mk q))).hom (FreeUniverse.restrSection R.obj G.val U q y)) =
      FreeUniverse.globalTensorHom R.obj F.val G.val H.val
        ((sheafifyForgetAdjunction R).homEquiv (F.val.tensorObj G.val) H b) T
        (F.val.restrictₛₗ q.op x ⊗ₜ y)

Tag 03EP, a lemma

Tag 03EP in the Stacks Project.

AlgebraicGeometry.SheafOfModules.PresheafOfModules.tensorLeft_preservesColimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/TensorColimits.lean, line 150. The attribute's comment: “part (1)”.

Tensoring presheaves of modules on the left by a fixed presheaf of modules preserves all colimits indexed in the module universe: at each object it is a left adjoint.

theorem tensorLeft_preservesColimits {O : Cᵒᵖ ⥤ CommRingCat.{w}}
    (F : _root_.PresheafOfModules.{z} (ringPresheaf O)) :
    PreservesColimitsOfSize.{a, z} (tensorLeft F)

AlgebraicGeometry.SheafOfModules.sheafTensorLeft_preservesColimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/TensorColimits.lean, line 265. The attribute's comment: “part (2)”. References: SGA 5 V (1.2.1), “inductive limits”.

Stacks Project, Tag 05NB. Tensoring with a fixed sheaf of modules commutes with all small colimits, independently of the ring universe.

theorem sheafTensorLeft_preservesColimits (R : Sheaf J CommRingCat.{w})
    (F : _root_.SheafOfModules.{z} (Stacks.SheafOfModules.Tensor.ringSheaf R)) :
    PreservesColimitsOfSize.{a, z} (sheafTensorLeft J R F)

Tag 0932, a lemma

Tag 0932 in the Stacks Project.

Stacks.PresheafOfModules.CoextendScalars.restrictScalars_coextendScalars_adjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Presheaf/RestrictScalarsCoextension.lean, line 1060. The attribute's comment: “the presheaf case: Hom_O(G, F) = Hom_O'(G, SheafHom_O(O', F)) for C a category and O ⟶ O' a map of presheaves of rings”.

The adjunction φ*_res ⊣ φ_*^coext: restriction of scalars along φ is left adjoint to the coextension-of-scalars functor φ_*^coext = coextendScalars φ, with Hom-bijection homEquiv (forward α ↦ (g ↦ a' ↦ α(a' • g)), inverse β ↦ (g ↦ β(g)(1))). This is the presheaf-of-modules analogue of ModuleCat.restrictCoextendScalarsAdj.

noncomputable def restrictScalars_coextendScalars_adjunction (φ : O ⟶ O') :
    PresheafOfModules.restrictScalars.{u} φ ⊣ coextendScalars φ

Stacks.SheafOfModules.CoextendScalars.sheafRestrictCoextendAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/RestrictCoextendScalarsAdjunction.lean, line 51. The attribute's comment: “the sheaf case: Hom_O(G, F) = Hom_O'(G, SheafHom_O(O', F)) for C a site and O ⟶ O' a map of sheaves of rings”.

Stacks Tag 0932 / Lemma 18.27.8, sheaf case. For a morphism φ : O ⟶ O' of sheaves of rings on a site, restriction of scalars along φ is left adjoint to coextension of scalars F ↦ SheafHom_O(O', F), i.e. Hom_O(G_O, F) = Hom_{O'}(G, SheafHom_O(O', F)) naturally in the sheaf of O'-modules G and the sheaf of O-modules F. This is restrictScalars_coextendScalars_adjunction.

noncomputable def sheafRestrictCoextendAdjunction (φ : O ⟶ O') :
    SheafOfModules.restrictScalars.{u} φ ⊣ sheafCoextendScalars φ

Tag 0E8I, a lemma

Tag 0E8I in the Stacks Project.

Stacks.Sites.ExtensionByZero.OfEssentiallySmall.restrictionTensorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/ExtensionByZeroTensorEssentiallySmall.lean, line 211. The attribute's comment: “for a site essentially u-small, objects in Type c, morphisms and modules in u”.

Stacks 0E8I over a site with large objects. For a sheaf of modules F on X, the extension by zero of G ⊗ F|_U is the extension by zero of G, tensored with F, naturally in G.

The attribute records the shape at which this holds: the objects of C form a type in an arbitrary universe c, but the morphisms, the structure sheaf and the modules all lie in one universe u, and C is required to be essentially u-small. The tag is carried in full by Stacks.SheafOfModules.ExtensionByZero.extensionByZeroTensorIso, where objects, morphisms, ring and modules lie in a single universe — the faithful reading of the tag's ringed site, which this statement specializes to at c := u; that registration stands and this one does not replace it.

noncomputable def restrictionTensorIso
    (F : SheafOfModules.{u} (ringSheaf X.O)) :
    extendByZero X U ⋙ (Stacks.SheafOfModules.Tensor.sheafTensor X.O).flip.obj F ≅
      sliceSheafTensorRight X U (F.over U) ⋙ extendByZero X U

Stacks.Sites.ExtensionByZero.FreeModuleUniverse.restrictionTensorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/ExtensionByZeroTensorFreeModuleUniverse.lean, line 183. The attribute's comment: “objects in Type u, morphisms in v, ring sections in w, modules in a free a with UnivLE v a, and no smallness assumption on the site”.

Stacks 0E8I at a free module universe. For a sheaf of modules F on X, the extension by zero of G ⊗ F|_U is the extension by zero of G, tensored with F, naturally in G.

The attribute records the shape at which this holds: the objects of C in Type u, its morphisms in v, the structure sheaf in w and the modules in a free a with UnivLE.{v, a}, and no smallness assumption on C. The tag is carried in full by Stacks.SheafOfModules.ExtensionByZero.extensionByZeroTensorIso, where objects, morphisms, ring and modules lie in a single universe; that registration stands and this one does not replace it, nor does it replace Stacks.Sites.ExtensionByZero.OfEssentiallySmall.restrictionTensorIso.

noncomputable def restrictionTensorIso
    (F : SheafOfModules.{a} (ringSheaf X.O)) :
    extendByZero.{a} X U ⋙ (Stacks.SheafOfModules.Tensor.sheafTensor X.O).flip.obj F ≅
      sliceSheafTensorRight.{a} X U (F.over U) ⋙ extendByZero.{a} X U

Stacks.SheafOfModules.ExtensionByZero.extensionByZeroTensorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/InternalHomAndFlatness/ExtensionByZeroTensor.lean, line 321.

Stacks 0E8I. Extension by zero commutes with tensoring by a module on the original site, naturally in the module on the slice site.

noncomputable def extensionByZeroTensorIso (F : _root_.SheafOfModules.{u} (Stacks.SheafOfModules.Tensor.ringSheaf X.O)) :
    letI := Stacks.Sites.ExtensionByZero.sheafRestrictionIsRightAdjoint X.J (Stacks.SheafOfModules.Tensor.ringSheaf X.O) U
    let E := _root_.SheafOfModules.pullback.{u}
      (F := Over.forget U) (𝟙 ((Stacks.SheafOfModules.Tensor.ringSheaf X.O).over U))
    E ⋙ ((sheafTensor.{u, u, u, u, u} X.O).obj F) ≅
      ((sheafTensor.{u, u, u, u, u} (X.O.over U)).obj (F.over U)) ⋙ E

Stacks.SheafOfModules.ExtensionByZero.extensionTensorBifunctorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/InternalHomAndFlatness/ExtensionByZeroTensor.lean, line 469. The attribute's comment: “bifunctorial form”.

Stacks 0E8I, bifunctorial form. Extension by zero commutes with tensoring by a module on the original site, naturally in the module on the slice site and in the module on the original site.

noncomputable def extensionTensorBifunctorIso :
    extensionTensorBifunctor X U ≅ tensorExtensionBifunctor X U

Tag 0EYY, a remark

Tag 0EYY in the Stacks Project.

Stacks.Sites.Localization.jShriekUnitIsoFreeAbelianSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/AbelianShriekIntegerBridge.lean, line 202. The attribute's comment: “j_! ℤ = Z_F^#, in the ambient category carrying the tensor product”.

Stacks Project, Tag 0EYY, part (a), in the ambient category of sheaves of ULift ℤ-modules. The extension by zero of the tensor unit along the localization morphism j : Sh(C)/F ⟶ Sh(C) is the free abelian sheaf Z_F^# on F, read through the equivalence between sheaves of ULift ℤ-modules and sheaves of abelian groups.

This transports the AddCommGrpCat-valued statement localizationShriek_constantInteger_iso_freeAbSheaf across the bridge, using that the bridge commutes with extension by zero and carries the tensor unit to the constant sheaf on ULift ℤ.

def jShriekUnitIsoFreeAbelianSheaf :
    let := Sheaf.monoidalCategory (localizationTopology J F)
      (ModuleCat.{u} (ULift.{u} ℤ))
    (abelianLocalizationShriek J F).obj (𝟙_ _) ≅
      (sheafIntegerModuleEquivalence J).inverse.obj
        ((Presheaf.freeAbelianSheaf J).obj ((sheafToPresheaf J (Type u)).obj F))

Stacks.Sites.Localization.jShriekPullbackIsoShriekUnitTensor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/AbelianShriekIntegerBridge.lean, line 233. The attribute's comment: “j_!(j⁻¹ H) = j_! ℤ ⊗ H, with no hypothesis beyond the data of the source”.

Stacks Project, Tag 0EYY, part (b), with no hypothesis beyond the data of the source. For the localization morphism j : Sh(C)/F ⟶ Sh(C) and an abelian sheaf H on C,

j_!(j⁻¹ H) ≅ j_! ℤ ⊗_ℤ H.

This is jShriekPullbackIsoTensor, which is proved for a site of arbitrary size and therefore states sheafification of ModuleCat-valued presheaves on C and on C/F, the monoidality of the two sheafification localizers and the left Kan extensions along C/F ⥤ C as hypotheses. On a site all five are available: the monoidality of the two localizers from CategoryTheory.GrothendieckTopology.W.monoidal, the left Kan extensions from Mathlib's pointwise construction CategoryTheory.Functor.pointwiseLeftKanExtension, and the two sheafifications through preservesColimitsOfShape_cover_op_forget_moduleCat above. So part (b) carries no hypothesis the source does not make.

def jShriekPullbackIsoShriekUnitTensor
    (H : Sheaf J (ModuleCat.{u} (ULift.{u} ℤ))) :
    let := Sheaf.monoidalCategory J (ModuleCat.{u} (ULift.{u} ℤ))
    let := Sheaf.monoidalCategory (localizationTopology J F)
      (ModuleCat.{u} (ULift.{u} ℤ))
    (abelianLocalizationShriek J F).obj
        ((abelianLocalizationInverseImage J F).obj H) ≅
      (abelianLocalizationShriek J F).obj (𝟙_ _) ⊗ H

Stacks.Sites.Localization.jShriekPullbackIsoFreeAbelianSheafTensor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/AbelianShriekIntegerBridge.lean, line 254. The attribute's comment: “j_!(j⁻¹ H) = Z_F^# ⊗ H, the two parts joined”.

Stacks Project, Tag 0EYY, the conclusion. For the localization morphism j : Sh(C)/F ⟶ Sh(C) and an abelian sheaf H on C,

j_!(j⁻¹ H) ≅ Z_F^# ⊗_ℤ H,

the free abelian sheaf on F tensored with H. This combines part (b), jShriekPullbackIsoTensor, with the identification of j_! ℤ with Z_F^# of part (a).

def jShriekPullbackIsoFreeAbelianSheafTensor
    (H : Sheaf J (ModuleCat.{u} (ULift.{u} ℤ))) :
    let := Sheaf.monoidalCategory J (ModuleCat.{u} (ULift.{u} ℤ))
    (abelianLocalizationShriek J F).obj
        ((abelianLocalizationInverseImage J F).obj H) ≅
      (sheafIntegerModuleEquivalence J).inverse.obj
        ((Presheaf.freeAbelianSheaf J).obj ((sheafToPresheaf J (Type u)).obj F)) ⊗ H

Stacks.Sites.Localization.localizationShriek_constantInteger_iso_freeAbSheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/InternalHomAndFlatness/LocalizationShriekInteger.lean, line 357. The attribute's comment: “j_shriek_int”.

For the localization morphism j : Sh(C)/F ⟶ Sh(C), presented by the site of elements C/F, the abelian sheaf j_! ℤ is the free abelian sheaf Z_F^# on F.

noncomputable def localizationShriek_constantInteger_iso_freeAbSheaf (F : Sheaf J (Type u)) :
    (Stacks.Sites.abelianShriek (localizationProjection J F)
          (localizationTopology J F) J).obj
        ((constantSheaf (localizationTopology J F) AddCommGrpCat.{u}).obj
          (AddCommGrpCat.of (ULift.{u} ℤ))) ≅
      (Presheaf.freeAbelianSheaf J).obj ((sheafToPresheaf J (Type u)).obj F)

Declarations registered for the tag:

jShriekPullbackIsoTensor registered with add_to_stacks in StacksFrontier/CategoryTheory/Sites/Modules/InternalHomAndFlatness/LocalizationShriekInteger.lean, line 366 (StacksFrontier): “j_!(j⁻¹ H) = j_! ℤ ⊗ H, for a site of arbitrary size: sheafification, the monoidality of the two sheafification localizers and the left Kan extensions along C/F ⥤ C are instance hypotheses here, and every one of them holds at the hypotheses of the source -- see jShriekPullbackIsoShriekUnitTensor”.

Tag 0GMZ, a lemma

Tag 0GMZ in the Stacks Project.

Stacks.SheafOfModules.InternalHom.internalHomSecondFunctor_preservesFilteredColimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/InternalHomAndFlatness/InternalHomFilteredColimits.lean, line 545.

On a ringed site, internal Hom out of a module of finite presentation commutes with filtered colimits: the canonical map colim_λ Hom_O(F, G_λ) ⟶ Hom_O(F, colim_λ G_λ) is an isomorphism for every filtered diagram λ ↦ G_λ.

theorem internalHomSecondFunctor_preservesFilteredColimits
    (F : SheafOfModules.{u} ((Stacks.SheafOfModules.Tensor.ringSheaf (J := X.J)) X.O))
    [F.IsFinitePresentation]
    (K : Type u) [Category.{u} K] [IsFiltered K] :
    PreservesColimitsOfShape K (internalHomSecondFunctor.{u, u, u, u} X.J X.O F)

Tag 0GN0, a lemma

Tag 0GN0 in the Stacks Project.

Stacks.SheafOfModules.InternalHom.coyoneda_preservesColimitsOfShape_of_isFinitePresentation, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Modules/InternalHomAndFlatness/InternalHomFilteredColimitsSections.lean, line 232. References: SGA 4 VI (5.8), “special case”.

Stacks 0GN0. On a ringed site satisfying the hypothesis of Stacks 0GMR part (4), Hom out of a module F of finite presentation commutes with filtered colimits:

colim_λ Hom_O(F, G_λ) = Hom_O(F, colim_λ G_λ).

The site hypothesis is the one the source attaches to the statement; it is needed already for F = O, where the assertion is that global sections commute with the colimit. Stacks 0GMS records sufficient conditions for it, one of which is applied in coyoneda_preservesColimitsOfShape_of_coveringSet below.

theorem coyoneda_preservesColimitsOfShape_of_isFinitePresentation
    (F : _root_.SheafOfModules.{u} (Tensor.ringSheaf X.O)) [F.IsFinitePresentation]
    (K : Type u) [Category.{u} K] [IsFiltered K]
    (hX : ∃ S : Set (Sheaf X.J (Type u)),
      (∀ H : Sheaf X.J (Type u), Sheaf.IsLocallySurjective (terminal.from H) →
          ∃ L ∈ S, Nonempty (L ⟶ H) ∧ Sheaf.IsLocallySurjective (terminal.from L)) ∧
        ∀ L ∈ S, Sheaf.IsQuasiCompact (L ⨯ L)) :
    PreservesColimitsOfShape K (coyoneda.obj (Opposite.op F))

Sources

LeaninternalHom_isSheaf · Stacks.SheafOfModules.InternalHom.internalHomOverIso · Stacks.SheafOfModules.InternalHom.internalHomOverIso_hom_app · Stacks.SheafOfModules.InternalHom.pullbackInternalHomMap · Stacks.SheafOfModules.InternalHom.adjointPullbackInternalHomMap · Stacks.SheafOfModules.InternalHom.tensorEvaluation_pullbackInternalHomMap · Stacks.SheafOfModules.InternalHom.toposPullbackInternalHomMap_compOf · Stacks.SheafOfModules.InternalHom.toposPullbackInternalHomMap_comp

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

18.21 Localization of ringed… to 18.27 Internal Hom

Section18.21 Localization of ringed topoi#

Tag 04IE, a lemma

Tag 04J2, a definition

Tag 04J3, a lemma

Tag 04J4, a lemma

Tag 04J5, a lemma

Sources

Section18.22 Localization of morphisms of ringed topoi#

Tag 04IF, a lemma

Tag 04J7, a lemma

Tag 04J8, a lemma

Tag 04J9, a lemma

Sources

Section18.23 Local types of modules#

Tag 03DL, a definition

Tag 03DM, a lemma

Tag 03DN, a lemma

Tag 03DO, a lemma

Sources

Section18.24 Basic results on local types of modules#

Tag 0H98, a lemma

Tag 082T, a lemma

Tag 0GZN, a lemma

Tag 0GZP, a lemma

Sources

Section18.25 Closed immersions of ringed topoi#

Tag 08M3, a lemma

Sources

Section18.26 Tensor product#

Tag 0GMW, a lemma

Tag 03EL, a lemma

Tag 03L6, a lemma

Sources

Section18.27 Internal Hom#

Tag 03EM, a lemma

Tag 0E8H, a lemma

Tag 0GMX, a remark

Tag 03EN, a lemma

Tag 0GMY, a lemma

Tag 03EO, a lemma

Tag 03EP, a lemma

Tag 0932, a lemma

Tag 0E8I, a lemma

Tag 0EYY, a remark

Tag 0GMZ, a lemma

Tag 0GN0, a lemma

Sources

Section18.21 Localization of ringed topoi #

Section18.22 Localization of morphisms of ringed topoi #

Section18.23 Local types of modules #

Section18.24 Basic results on local types of modules #

Section18.25 Closed immersions of ringed topoi #

Section18.26 Tensor product #

Section18.27 Internal Hom #