7.24 Existence of lower shriek to 7.43 Subtopoi

Section7.24 Existence of lower shriek#

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

Tag 09YX, a lemma

Tag 09YX in the Stacks Project.

CategoryTheory.Sheaf.isRightAdjoint_of_isCorepresentable_sections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/ExistenceOfLowerShriek.lean, line 319. The attribute's comment: “Existence of lower shriek: the inverse image of a morphism of topoi has a left adjoint as soon as it is corepresentable on sections over a family of objects covering everything.”.

Stacks 09YX. Let C, D be sites and let finv : Sh(C) ⥤ Sh(D) be a functor between their topoi of sheaves of sets — for instance the inverse image f⁻¹ of a morphism of topoi f : Sh(D) → Sh(C). Let E be a subset of the objects of D such that

1. for every V ∈ E there is a sheaf G on C with finv F (V) = Mor_{Sh(C)}(G, F) functorially in F, i.e. the functor F ↦ finv F (V) is corepresentable, and
2. every object of D has a covering by objects of E, i.e. the inclusion of the full subcategory on E is cover dense.

Then finv has a left adjoint f_!.

public theorem isRightAdjoint_of_isCorepresentable_sections {C : Type u} [Category.{v} C]
    {D : Type u} [Category.{v} D] {J : GrothendieckTopology C} {K : GrothendieckTopology D}
    (finv : Sheaf J (Type max u v) ⥤ Sheaf K (Type max u v)) (E : ObjectProperty D)
    [E.ι.IsCoverDense K]
    (hE : ∀ V : D, E V → (finv ⋙ (sheafSections K (Type max u v)).obj (op V)).IsCorepresentable) :
    finv.IsRightAdjoint

Sources

• Section 7.24, Tag 09YW
• AxiomMath/Stacks at 5ed82d14

LeanCategoryTheory.Sheaf.isRightAdjoint_of_isCorepresentable_sections

Section7.25 Localization#

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

Tag 03CD, a lemma

Tag 03CD in the Stacks Project.

CategoryTheory.OverShriek.overShriek_sheafify_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/LowerShriekCoproducts.lean, line 245.

Stacks 03CD, packaged as the existence of the isomorphism j_{U!}(G^#) ≅ (∐_{φ : V ⟶ U} G(V →φ U))^#.

theorem overShriek_sheafify_iso :
    Nonempty
      (((Over.forget U).sheafPullback (Type v) (J.over U) J).obj
          ((presheafToSheaf (J.over U) (Type v)).obj G) ≅
        (presheafToSheaf J (Type v)).obj (presheaf G))

Tag 03HU, a lemma

Tag 03HU in the Stacks Project.

CategoryTheory.overShriekSheafifyYonedaIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/LowerShriekRepresentable.lean, line 50.

Stacks 03HU. For an object X/U of the localized site C/U, the lower shriek j_{U!} = (Over.forget U).sheafPullback of the sheaf h_{X/U}^# associated to the presheaf on C/U represented by X/U is the sheaf h_X^# associated to the presheaf on C represented by the underlying object X = j_U(X/U).

noncomputable def overShriekSheafifyYonedaIso (X : Over U) :
    ((Over.forget U).sheafPullback (Type v) (J.over U) J).obj
        ((presheafToSheaf (J.over U) (Type v)).obj (yoneda.obj X)) ≅
      (presheafToSheaf J (Type v)).obj (yoneda.obj X.left)

Tag 00Y1, a lemma

Tag 00Y1 in the Stacks Project.

CategoryTheory.OverShriek.isEquivalence_sheafFunctorToOver, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/SheavesOverRepresentable.lean, line 515. The attribute's comment: “the functor j_{U!} : Sh(C/U) ⥤ Sh(C)/h_U^# is an equivalence”.

Stacks 00Y1. The functor Φ_sh : Sh(C/U) ⥤ Sh(C)/h_U^# induced by j_{U!} is full, faithful and essentially surjective, i.e. an equivalence.

instance isEquivalence_sheafFunctorToOver : (sheafFunctorToOver (U := U) J).IsEquivalence

CategoryTheory.OverShriek.sheafEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/SheavesOverRepresentable.lean, line 522. The attribute's comment: “the resulting equivalence of categories Sh(C/U) ≌ Sh(C)/h_U^#”.

Stacks 00Y1, as an equivalence of categories Sh(C/U) ≌ Sh(C)/h_U^#. Its functor is sheafFunctorToOver, the sheaf level j_{U!} viewed as a functor into the slice (sheafEquivalence_functor), and its inverse is isomorphic to the fibre functor (F, φ) ↦ F_φ.

def sheafEquivalence :
    Sheaf (J.over U) (Type v) ≌ Over ((presheafToSheaf J (Type v)).obj (yoneda.obj U))

CategoryTheory.OverShriek.sheafFunctorToOverForgetIsoOfAdjunction, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/SheavesOverRepresentable.lean, line 561. The attribute's comment: “j_{U!} is Sh(C/U) ≌ Sh(C)/h_U^# followed by Over.forget, for any left adjoint”.

Stacks 00Y1, in the form the source restates it in: j_{U!} is the equivalence Φ : Sh(C/U) ≌ Sh(C)/h_U^# followed by Over.forget : Sh(C)/h_U^# ⥤ Sh(C).

Here j_{U!} is an arbitrary left adjoint L of the restriction functor j_U^{-1}, so this is a statement about j_{U!} rather than about one model of it: sheafFunctorToOverForgetIso identifies Φ ⋙ Over.forget with the left adjoint obtained from Over.forget U, and two left adjoints of one functor are canonically isomorphic.

The adjunction adj is also what makes that left adjoint exist (J.overPullback being the pushforward along Over.forget U), so no adjointness hypothesis beyond adj is assumed.

def sheafFunctorToOverForgetIsoOfAdjunction
    {L : Sheaf (J.over U) (Type v) ⥤ Sheaf J (Type v)} (adj : L ⊣ J.overPullback (Type v) U) :
    sheafFunctorToOver (U := U) J ⋙ Over.forget _ ≅ L

Tag 04BB, a lemma

Tag 04BB in the Stacks Project.

CategoryTheory.OverShriek.preservesLimitsOfShape_of_isConnected, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/Localization.lean, line 162. The attribute's comment: “j_{U!} commutes with fibre products and equalizers, and more generally with connected limits; in particular it preserves subsheaf inclusions.”. References: SGA 4 III (5.1), “fibre products clause”; SGA 4 III (1.9.2), “more general”.

Stacks 04BB. Let C be a site and let U be an object of C. Let L be a left adjoint of the restriction functor j_U^{-1} = J.overPullback : Sh(C) ⥤ Sh(C/U), i.e. let L be j_{U!}. Then L commutes with limits of every connected shape K; in particular it commutes with fibre products (K = WalkingCospan) and equalizers (K = WalkingParallelPair), and hence carries subsheaf inclusions to subsheaf inclusions.

public theorem preservesLimitsOfShape_of_isConnected {C : Type u} [Category.{v} C]
    (J : GrothendieckTopology C) (U : C) [HasWeakSheafify J (Type v)]
    [HasWeakSheafify (J.over U) (Type v)] [J.WEqualsLocallyBijective (Type v)]
    {L : Sheaf (J.over U) (Type v) ⥤ Sheaf J (Type v)} (adj : L ⊣ J.overPullback (Type v) U)
    {K : Type w} [Category.{w'} K] [IsConnected K] :
    Limits.PreservesLimitsOfShape K L

Tag 0E8E, a lemma

Tag 0E8E in the Stacks Project.

CategoryTheory.OverShriek.reflectsMonomorphisms_and_reflectsEpimorphisms, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/Localization.lean, line 264. The attribute's comment: “j_{U!} reflects injections and surjections of sheaves of sets.”.

Stacks 0E8E. Let C be a site and let U be an object of C. Let L be a left adjoint of the restriction functor j_U^{-1} = J.overPullback : Sh(C) ⥤ Sh(C/U), i.e. let L be j_{U!}. Then L reflects monomorphisms and epimorphisms, that is (Stacks 00WN), if j_{U!}φ is an injection of sheaves of sets then so is φ, and if j_{U!}φ is a surjection of sheaves of sets then so is φ.

public theorem reflectsMonomorphisms_and_reflectsEpimorphisms {C : Type u} [Category.{v} C]
    (J : GrothendieckTopology C) (U : C) [HasWeakSheafify J (Type v)]
    [HasWeakSheafify (J.over U) (Type v)] [J.WEqualsLocallyBijective (Type v)]
    {L : Sheaf (J.over U) (Type v) ⥤ Sheaf J (Type v)} (adj : L ⊣ J.overPullback (Type v) U) :
    L.ReflectsMonomorphisms ∧ L.ReflectsEpimorphisms

Tag 03EE, a lemma

Tag 03EE in the Stacks Project.

CategoryTheory.OverShriek.overShriek_overPullback_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/LowerShriekProduct.lean, line 113.

Stacks 03EE, packaged as the existence of the isomorphism j_{U!}j_U^{-1}F ≅ F × h_U^#.

theorem overShriek_overPullback_iso (F : Sheaf J (Type v)) :
    Nonempty
      (((Over.forget U).sheafPullback (Type v) (J.over U) J).obj
          ((J.overPullback (Type v) U).obj F) ≅
        F ⨯ (presheafToSheaf J (Type v)).obj (yoneda.obj U))

Tag 03EH, a lemma

Tag 03EH in the Stacks Project.

comp_forget_eq_forget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/RelocalizationTriangle.lean, line 68. The attribute's comment: “triangle”. References: SGA 4 I (5.10), “commutative triangle”; SGA 3 I (1.6).

Commutativity of the relocalization triangle: j_U ∘ j = j_V, i.e. Over.map f ⋙ Over.forget U = Over.forget V.

theorem comp_forget_eq_forget :
    Over.map f ⋙ Over.forget U = Over.forget V

map_eq_forget_iteratedSlice, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/RelocalizationTriangle.lean, line 89. The attribute's comment: “j = j_{V/U}”. References: SGA 3 I (1.6), “partial”.

Under the identification (C/U)/(V/U) ≅ C/V given by Over.iteratedSliceEquiv (Over.mk f), the relocalization functor j = Over.map f agrees with the localization functor j_{V/U} = Over.forget (Over.mk f).

theorem map_eq_forget_iteratedSlice :
    (Over.iteratedSliceEquiv (Over.mk f)).functor ⋙ Over.map f =
      Over.forget (Over.mk f)

inverseImage_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/RelocalizationTriangle.lean, line 113. The attribute's comment: “j_V^{-1} = j^{-1} ∘ j_U^{-1}”.

(Inverse image, strict equality.) j_V^{-1} = j^{-1} ∘ j_U^{-1} as functors Sheaf J A ⟶ Sheaf (J.over V) A.

This is the strict equality of sheafPushforwardContinuous functors, valid because the underlying functors satisfy Over.map f ⋙ Over.forget U = Over.forget V strictly.

theorem inverseImage_eq :
    (Over.forget V).sheafPushforwardContinuous A (J.over V) J =
      (Over.forget U).sheafPushforwardContinuous A (J.over U) J ⋙
        (Over.map f).sheafPushforwardContinuous A (J.over V) (J.over U)

leftAdjointIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/RelocalizationTriangle.lean, line 133. The attribute's comment: “j_{V!} = j_{U!} ∘ j_!”.

(Lower-shriek, natural isomorphism.) j_{V!} ≅ j_{U!} ∘ j_! as functors Sheaf (J.over V) A ⟶ Sheaf J A.

Constructed from inverseImage_eq via uniqueness of left adjoints: each of sheafPullback is a chosen left adjoint to the corresponding sheafPushforwardContinuous, and the composition j_! ∘ j_U_! is left adjoint to j_U^{-1} ∘ j^{-1} = j_V^{-1} by inverseImage_eq.

noncomputable def leftAdjointIso :
    (Over.forget V).sheafPullback A (J.over V) J ≅
      (Over.map f).sheafPullback A (J.over V) (J.over U) ⋙
        (Over.forget U).sheafPullback A (J.over U) J

leftAdjointIso_hom_app_comp_map_comp_counit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/RelocalizationTriangle.lean, line 169. The attribute's comment: “j_{V!} = j_{U!} ∘ j_! carries one transpose to the other”.

Stacks 03EH carries one transpose to the other. A morphism u : T ⟶ j_V^{-1}Z transposes across j_{V!} ⊣ j_V^{-1} on the one hand and across (j_! ∘ j_{U!}) ⊣ j_V^{-1} on the other, and the two transposes differ by leftAdjointIso.

This is what leftAdjointIso means: it is a Adjunction.leftAdjointUniq, so on its own it is only an isomorphism of two chosen left adjoints, and the statement that identifies it is the agreement of the transposes it induces. It is also the only form in which the triangle can be used inside an equation of morphisms out of a lower shriek, where one side is written with j_{V!} and the other with j_{U!} ∘ j_!.

Adjunction.leftAdjointUniq_hom_app_counit is the case u = 𝟙; the general case is that one followed by the naturality of leftAdjointIso.

theorem leftAdjointIso_hom_app_comp_map_comp_counit {T : Sheaf (J.over V) A} {Z : Sheaf J A}
    (u : T ⟶ ((Over.forget V).sheafPushforwardContinuous A (J.over V) J).obj Z) :
    ((Over.forget V).sheafPullback A (J.over V) J).map u ≫
        ((Over.forget V).sheafAdjunctionContinuous A (J.over V) J).counit.app Z =
      (leftAdjointIso J f A).hom.app T ≫
        ((Over.map f).sheafPullback A (J.over V) (J.over U) ⋙
            (Over.forget U).sheafPullback A (J.over U) J).map u ≫
          (((Over.map f).sheafAdjunctionContinuous A (J.over V) (J.over U)).comp
            ((Over.forget U).sheafAdjunctionContinuous A (J.over U) J)).counit.app Z

Tag 04IL, a lemma

Tag 04IL in the Stacks Project.

CategoryTheory.OverShriek.shriekCompSheafFunctorToOverIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/Relocalize.lean, line 355. The attribute's comment: “(2): under the identification of 00Y1, j_! is postcomposition with h_f^#”.

Stacks 04IL (2). Under the identification of Stacks 00Y1, used in the forward direction Φ_U = sheafFunctorToOver J : Sh(C/U) ⥤ Sh(C)/h_U^#, the relocalization lower shriek j_! becomes postcomposition with h_f^# : h_V^# ⟶ h_U^#:

  j_!(H --φ--> h_V^#) = (H --φ ≫ h_f^#--> h_U^#) .

This is Stacks' proof of (2): the identification sends G to j_{V!}G ⟶ j_{V!}(*) = h_V^#, so j_!G is sent to j_{U!}j_!G ⟶ j_{U!}(*) = h_U^#, and j_{U!}j_! = j_{V!} — carried out here at the presheaf level, where the two structural maps to h_U are literally the same (relocalizePresheafFunctorToOverIso), and then transported through sheafification.

def shriekCompSheafFunctorToOverIso :
    (Over.map f).sheafPullback (Type v) (J.over V) (J.over U) ⋙ sheafFunctorToOver (U := U) J ≅
      sheafFunctorToOver (U := V) J ⋙
        Over.map ((presheafToSheaf J (Type v)).map (yoneda.map f))

CategoryTheory.OverShriek.inverseImageCompSheafFunctorToOverIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/Relocalize.lean, line 400. The attribute's comment: “(1): under the identification of 00Y1, j^{-1} is base change along h_f^#”.

Stacks 04IL (1). Under the identification of Stacks 00Y1, used in the forward direction Φ_U = sheafFunctorToOver J, the relocalization inverse image j^{-1} becomes base change along h_f^# : h_V^# ⟶ h_U^#:

  j^{-1}(H --φ--> h_U^#) = (H ×_{φ, h_U^#, h_f^#} h_V^# ⟶ h_V^#) .

This is the proof Stacks suggests: "the reader can now prove (1) by using that j^{-1} is the right adjoint to j_! and using that the rule in (1) is the right adjoint to the rule in (2)". Concretely, Over.map h_f^# ⋙ Φ_U^{-1} — which is j_! transported, by (2) — is left adjoint both to j^{-1} ⋙ Φ_V and to Φ_U ⋙ Over.pullback h_f^#, so the two agree by uniqueness of right adjoints.

def inverseImageCompSheafFunctorToOverIso :
    (Over.map f).sheafPushforwardContinuous (Type v) (J.over V) (J.over U) ⋙
        sheafFunctorToOver (U := V) J ≅
      sheafFunctorToOver (U := U) J ⋙
        Over.pullback ((presheafToSheaf J (Type v)).map (yoneda.map f))

CategoryTheory.OverShriek.homEquiv_symm_inverseImageCompSheafFunctorToOverIso_inv_app, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/Relocalize.lean, line 427. The attribute's comment: “(1): the comparison of inverse images is the one its counit prescribes”.

Stacks 04IL (1) is the comparison its counit prescribes. Transposing the inverse of the comparison across the adjunction Φ_V^{-1} ⋙ j_! ⊣ j^{-1} ⋙ Φ_V — the one whose left adjoint Stacks 04IL (2) identifies with Over.map h_f^# ⋙ Φ_U^{-1} — returns, up to that identification, the counit of base change along h_f^# read through Stacks 00Y1 at U.

Both sides are morphisms out of Φ_V^{-1}(Φ_U(j^{-1}... ) ×_{h_U^#} h_V^#), and the comparison is an Adjunction.rightAdjointUniq, so this is Adjunction.homEquiv_symm_rightAdjointUniq_hom_app for the two adjunctions it is built from, read in the inverse direction by Adjunction.rightAdjointUniq_inv_app and corrected by Adjunction.ofNatIsoLeft for the identification of the two left adjoints.

This is the form in which the comparison enters an equation that has been transposed across a lower shriek: on one side of such an equation the base change of Stacks 03EH appears, on the other the relocalization counit, and nothing but this lemma relates them.

theorem homEquiv_symm_inverseImageCompSheafFunctorToOverIso_inv_app
    (Z : Sheaf (J.over U) (Type v)) :
    (((sheafEquivalence (U := V) J).symm.toAdjunction.comp
          ((Over.map f).sheafAdjunctionContinuous (Type v) (J.over V) (J.over U))).homEquiv
        ((sheafFunctorToOver (U := U) J ⋙
          Over.pullback ((presheafToSheaf J (Type v)).map (yoneda.map f))).obj Z) Z).symm
        ((inverseImageCompSheafFunctorToOverIso f J).inv.app Z) =
      (inverseCompShriekRelocalizeIso f J).hom.app
          ((sheafFunctorToOver (U := U) J ⋙
            Over.pullback ((presheafToSheaf J (Type v)).map (yoneda.map f))).obj Z) ≫
        ((Over.mapPullbackAdj ((presheafToSheaf J (Type v)).map (yoneda.map f))).comp
          (sheafEquivalence (U := U) J).symm.toAdjunction).counit.app Z

CategoryTheory.OverShriek.left_inverseImageCompSheafFunctorToOverIso_inv_app_comp_counit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/RelocalizeCounit.lean, line 848. The attribute's comment: “(1) carries the counit of j_{V!} to the counit of j_{U!}”.

Stacks 04IL (1) carries the counit of j_{V!} ⊣ j_V^{-1} to that of j_{U!} ⊣ j_U^{-1}. The inverse of Stacks 04IL (1) at a restricted sheaf j_U^{-1}A, read through Over.forget h_V^# and followed by Stacks 00Y1's identification at V and the counit ε^V, is the first projection of the base change along h_f^# followed by Stacks 00Y1's identification at U and the counit ε^U.

The two counits belong to two different localizations of the site, and Stacks 04IL (1) is what relates them.

theorem left_inverseImageCompSheafFunctorToOverIso_inv_app_comp_counit
    (A : Sheaf J (Type v)) :
    ((inverseImageCompSheafFunctorToOverIso f J).inv.app
            ((J.overPullback (Type v) U).obj A)).left ≫
        (sheafFunctorToOverForgetIso (U := V) J).hom.app ((J.overPullback (Type v) V).obj A) ≫
          ((Over.forget V).sheafAdjunctionContinuous (Type v) (J.over V) J).counit.app A =
      pullback.fst
            ((sheafFunctorToOver (U := U) J).obj ((J.overPullback (Type v) U).obj A)).hom
            ((presheafToSheaf J (Type v)).map (yoneda.map f)) ≫
          (sheafFunctorToOverForgetIso (U := U) J).hom.app ((J.overPullback (Type v) U).obj A) ≫
            ((Over.forget U).sheafAdjunctionContinuous (Type v) (J.over U) J).counit.app A

Sources

• Section 7.25, Tag 00XZ
• AxiomMath/Stacks at 5ed82d14

LeanCategoryTheory.OverShriek.overShriek_sheafify_iso · CategoryTheory.overShriekSheafifyYonedaIso · CategoryTheory.OverShriek.isEquivalence_sheafFunctorToOver · CategoryTheory.OverShriek.sheafEquivalence · CategoryTheory.OverShriek.sheafFunctorToOverForgetIsoOfAdjunction · CategoryTheory.OverShriek.preservesLimitsOfShape_of_isConnected · CategoryTheory.OverShriek.reflectsMonomorphisms_and_reflectsEpimorphisms · CategoryTheory.OverShriek.overShriek_overPullback_iso

Section7.26 Glueing sheaves#

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

Tag 04TQ, a lemma

Tag 04TQ in the Stacks Project.

Stacks.SheafMapGluing.maps_of_sheaves_glue, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Glueing/MapsOfSheavesGlue.lean, line 513.

Stacks 04TQ — Maps of sheaves glue (existence and uniqueness).

Let (C, J) be a site with fiber products, A the target category of sheaf values, F, G : Sheaf J A, and let { f i : U i → U } be a covering of U in J. Then any family of maps of restricted sheaves φ i : F|_{C/U i} ⟶ G|_{C/U i} that is compatible on the overlaps C/(U i ×_U U j) glues to a unique map φ : F|_{C/U} ⟶ G|_{C/U} whose restriction to each C/U i is φ i.

theorem maps_of_sheaves_glue
    (hcov : Sieve.generate (Presieve.ofArrows Ui f) ∈ J U)
    (φ : ∀ i, RestrictedHom J F G (Ui i))
    (hφ : CompatibleOnOverlaps J F G U Ui f φ) :
    ∃! ψ : RestrictedHom J F G U, ∀ i, restrictHomAlong J (f i) F G ψ = φ i

Tag 0BWQ, a lemma

Tag 0BWQ in the Stacks Project.

CategoryTheory.Sheaf.tensorHomEquivIhom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/CartesianClosed.lean, line 76.

Stacks 0BWQ. For sheaves F, G, H on a site C there is a canonical bijection Mor(F × G, H) ≃ Mor(F, SheafHom(G, H)), where SheafHom(G, H) is the internal hom of the cartesian closed category of sheaves.

The bijection is the hom-equivalence of the adjunction - ⊗ G ⊣ ihom G, so it is natural in all three entries, which is Stacks' functoriality clause. See the module docstring for the caveat that the internal hom here is Mathlib's abstract one rather than Mathlib's sheafHom.

noncomputable def tensorHomEquivIhom {A : Type*} [Category.{max u v} A]
    [CartesianMonoidalCategory A] [MonoidalClosed (Cᵒᵖ ⥤ A)] [HasSheafify J A]
    (F G H : Sheaf J A) :
    (F ⊗ G ⟶ H) ≃ (F ⟶ (ihom G).obj H)

Tag 0D7X, a lemma

Tag 0D7X in the Stacks Project.

CategoryTheory.OverShriek.sheafHomYonedaSheafifyNatIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Glueing/HomSheafLocalization.lean, line 66.

Stacks 0D7X. For an object U of a small site (C, J), the internal hom sheaf SheafHom(h_U^\#, -) out of the sheafification of the representable presheaf h_U is the composite j_{U*} \circ j_U^{-1}: that is, SheafHom(h_U^\#, \mathcal{F}) = j_{U*}(\mathcal{F}|_{\mathcal{C}/U}), naturally in the sheaf \mathcal{F}.

Both functors are right adjoint to \mathcal{G} \mapsto h_U^\# \times \mathcal{G}, the first by Stacks 0BWQ and the second by the localization adjunctions together with Stacks 03EE, so they agree by uniqueness of right adjoints. This is the source's argument, whose last step is the Yoneda lemma.

noncomputable def sheafHomYonedaSheafifyNatIso :
    SheafHomAdj.sheafHomFunctor ((presheafToSheaf J (Type u)).obj (yoneda.obj U)) ≅
      localizationPullback U J ⋙ localizationPushforward U J

Tag 04TR, a lemma

Tag 04TR in the Stacks Project.

CategoryTheory.GrothendieckTopology.essSurj_toDescentData_pseudofunctorOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Glueing/GlueingSheaves.lean, line 839.

Glueing sheaves. Let (C, J) be a site, let {f i : X i ⟶ S} be a covering of an object S of C, and let A be a category with limits of the relevant size. Then every glueing datum for A-valued sheaves with respect to {f i : X i ⟶ S} — a sheaf F i on each slice site C/X i together with isomorphisms between the restrictions of F i and of F j over the overlaps, satisfying the cocycle condition over the triple overlaps — is isomorphic to the canonical glueing datum of a sheaf F on the slice site C/S, i.e. there exists such an F together with isomorphisms F|_{C/X i} ≅ F i compatible with the given ones over the overlaps.

public theorem essSurj_toDescentData_pseudofunctorOver {C : Type u} [Category.{v} C]
    (J : GrothendieckTopology C) (A : Type u') [Category.{v'} A]
    [HasLimitsOfSize.{max t u v, max t u v} A] {ι : Type t} {S : C} {X : ι → C} (f : ∀ i, X i ⟶ S)
    (hf : Sieve.ofArrows X f ∈ J S) : ((J.pseudofunctorOver A).toDescentData f).EssSurj

Tag 04TS, a lemma

Tag 04TS in the Stacks Project.

CategoryTheory.GrothendieckTopology.isEquivalence_toDescentData_pseudofunctorOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Glueing/GlueingSheaves.lean, line 1041.

Sheaves on a slice site are glueing data. Let (C, J) be a site, let {f i : X i ⟶ S} be a covering of an object S of C, and let A be a category with limits of the relevant size. Then the category of A-valued sheaves on the slice site C/S is equivalent to the category of glueing data for A-valued sheaves with respect to {f i : X i ⟶ S} — a sheaf F i on each slice site C/X i together with isomorphisms between the restrictions of F i and of F j over the overlaps, satisfying the cocycle condition over the triple overlaps — via the functor sending a sheaf F on C/S to its canonical glueing datum (F|_{C/X i}).

public theorem isEquivalence_toDescentData_pseudofunctorOver {C : Type u} [Category.{v} C]
    (J : GrothendieckTopology C) (A : Type u') [Category.{v'} A]
    [HasLimitsOfSize.{max u v, max u v} A] {ι : Type t} {S : C} {X : ι → C} (f : ∀ i, X i ⟶ S)
    (hf : Sieve.ofArrows X f ∈ J S) : ((J.pseudofunctorOver A).toDescentData f).IsEquivalence

Tag 0GWK, a lemma

Tag 0GWK in the Stacks Project.

CategoryTheory.SiteGlueing.canonicalEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Glueing/AbsoluteGlueingAnySite.lean, line 620.

Stacks 0GWK. For a site C, with no smallness hypothesis and with sheaves of sets valued in an arbitrary universe, the category of sheaves on C is equivalent to the category of absolute glueing data, via the functor sending a sheaf to its canonical absolute glueing data.

noncomputable def canonicalEquivalence : Sheaf J (Type w) ≌ GlueingData.{w} J

Sources

• Section 7.26, Tag 04TP
• AxiomMath/Stacks at 5ed82d14

LeanStacks.SheafMapGluing.maps_of_sheaves_glue · CategoryTheory.Sheaf.tensorHomEquivIhom · CategoryTheory.OverShriek.sheafHomYonedaSheafifyNatIso · CategoryTheory.GrothendieckTopology.essSurj_toDescentData_pseudofunctorOver · CategoryTheory.GrothendieckTopology.isEquivalence_toDescentData_pseudofunctorOver · CategoryTheory.SiteGlueing.canonicalEquivalence

Section7.27 More localization#

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

Tag 03HT, a lemma

Tag 03HT in the Stacks Project.

CategoryTheory.OverShriek.isIso_ofRestricted_unit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/MoreLocalization.lean, line 205. The attribute's comment: “j_{U!}G(V) = ∐_{φ : V ⟶ U} G(V →φ U) for a subcanonical topology.”.

Let C be a site, let U be an object of C whose representable presheaf h_U is a sheaf (for instance because the topology is subcanonical), and let G be a sheaf of sets on C/U. Let L be a left adjoint of the restriction functor j_U^{-1} = J.overPullback : Sh(C) ⥤ Sh(C/U), i.e. let L be j_{U!}. Then the canonical map from the coproduct presheaf V ↦ ∐_{φ : V ⟶ U} G(V →φ U) to the presheaf underlying j_{U!}G, which over V sends a pair (φ, s) to the section s of j_{U!}G, is an isomorphism: j_{U!}G(V) = ∐_{φ ∈ Hom_C(V, U)} G(V →φ U).

public theorem isIso_ofRestricted_unit {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
    (U : C) (hU : Presieve.IsSheaf J (yoneda.obj U))
    {L : Sheaf (J.over U) (Type v) ⥤ Sheaf J (Type v)} (adj : L ⊣ J.overPullback (Type v) U)
    (G : Sheaf (J.over U) (Type v)) :
    IsIso (ofRestricted G.obj (F := (L.obj G).obj) (adj.unit.app G).hom)

Tag 03CE, a lemma

Tag 03CE in the Stacks Project.

StacksLocalizationProducts.bijective_left_comp_prodSnd, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/PushforwardAdjunction.lean, line 122. References: SGA 3 I (1.6), “i_S ⊣ p_S hom bijection”.

Stacks 03CE(1). The right adjoint of the localization functor j_U = Over.forget U : C/U ⥤ C is v : X ↦ X × U / U: for Y/U in C/U and X in C the map sending a morphism Y ⟶ X × U / U over U to its underlying morphism followed by the projection to X is a bijection Mor_{C/U}(Y/U, X × U/U) ≃ Mor_C(Y, X).

This is the counit description Over.forgetAdjStar_counit_app of Mathlib's adjunction Over.forgetAdjStar U : Over.forget U ⊣ Over.star U.

theorem bijective_left_comp_prodSnd (Y : Over U) (X : C) :
    Function.Bijective fun g : Y ⟶ (Over.star U).obj X => g.left ≫ prod.snd

StacksLocalizationProducts.isMorphismOfSites_star, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/PushforwardAdjunction.lean, line 138.

Stacks 03CE(2), first half. The functor v = Over.star U : C ⥤ C/U defines a morphism of sites C/U → C: it is continuous, and the induced pullback on sheaves of sets is exact.

Exactness holds because v is a right adjoint, hence representably flat, so this is the criterion CategoryTheory.Functor.isMorphismOfSites_of_representablyFlat (Stacks 00X5).

theorem isMorphismOfSites_star : (Over.star U).IsMorphismOfSites J (J.over U)

StacksLocalizationProducts.sheafPushforwardOverForgetIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/PushforwardAdjunction.lean, line 145.

Stacks 03CE(2), second half. The pushforward j_{U*} of the morphism of topoi attached to the continuous and cocontinuous functor j_U agrees with the pushforward v^s of the morphism of sites given by v = Over.star U; that is, the two morphisms of topoi coincide.

noncomputable def sheafPushforwardOverForgetIso :
    (Over.forget U).sheafPushforwardCocontinuous (Type u) (J.over U) J ≅
      (Over.star U).sheafPushforwardContinuous (Type u) J (J.over U)

StacksLocalizationProducts.sheafPullbackStarIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/PushforwardAdjunction.lean, line 153.

Stacks 03CE(2), second half. Dually, the pullback v_s = f⁻¹ of the morphism of sites given by v = Over.star U is the restriction functor j_U⁻¹ along j_U = Over.forget U.

noncomputable def sheafPullbackStarIso :
    (Over.star U).sheafPullback (Type u) J (J.over U) ≅
      (Over.forget U).sheafPushforwardContinuous (Type u) (J.over U) J

StacksLocalizationProducts.sheafPushforwardObjEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/PushforwardAdjunction.lean, line 161.

Stacks 03CE(3). For a sheaf F on C/U the sections of j_{U*}F over an object X of C are the sections of F over X × U / U.

noncomputable def sheafPushforwardObjEquiv (F : Sheaf (J.over U) (Type u)) (X : C) :
    (((Over.forget U).sheafPushforwardCocontinuous (Type u) (J.over U) J).obj F).obj.obj (op X) ≃
      F.obj.obj (op ((Over.star U).obj X))

Tag 09W9, a lemma

Tag 09W9 in the Stacks Project.

StacksRelocalization.isMorphismOfSites_overPullback, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/OverPullbackMorphism.lean, line 43. References: SGA 4 IV (5.5), “loc(f) (5.5.2)”.

The functor v = Over.pullback f : C/V ⥤ C/U, given on objects by X/V ↦ X ×_V U / U, defines a morphism of sites C/U → C/V: it is continuous, and the induced pullback on sheaves of sets is exact.

theorem isMorphismOfSites_overPullback :
    (Over.pullback f).IsMorphismOfSites (J.over V) (J.over U)

StacksRelocalization.sheafPushforwardOverMapIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/OverPullbackMorphism.lean, line 51.

The pushforward j_* of the morphism of topoi attached to the continuous and cocontinuous functor j = Over.map f agrees with the pushforward v^s of the morphism of sites given by v = Over.pullback f; that is, the two morphisms of topoi coincide.

noncomputable def sheafPushforwardOverMapIso :
    (Over.map f).sheafPushforwardCocontinuous (Type u) (J.over U) (J.over V) ≅
      (Over.pullback f).sheafPushforwardContinuous (Type u) (J.over V) (J.over U)

StacksRelocalization.sheafPullbackOverPullbackIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/OverPullbackMorphism.lean, line 59. References: SGA 4 IV (5.5), “f^* = restriction”.

The pullback v_s = f⁻¹ of the morphism of sites given by v = Over.pullback f is the restriction functor j⁻¹ along j = Over.map f.

noncomputable def sheafPullbackOverPullbackIso :
    (Over.pullback f).sheafPullback (Type u) (J.over V) (J.over U) ≅
      (Over.map f).sheafPushforwardContinuous (Type u) (J.over U) (J.over V)

StacksRelocalization.sheafPushforwardObjEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/OverPullbackMorphism.lean, line 67. References: SGA 4 IV (5.5), “f_* formula (5.5.3)”.

For a sheaf F on C/U the sections of j_*F over an object X/V of C/V are the sections of F over X ×_V U / U.

noncomputable def sheafPushforwardObjEquiv (F : Sheaf (J.over U) (Type u)) (X : Over V) :
    (((Over.map f).sheafPushforwardCocontinuous (Type u) (J.over U) (J.over V)).obj F).obj.obj
        (op X) ≃
      F.obj.obj (op ((Over.pullback f).obj X))

Tag 00Y2, a lemma

Tag 00Y2 in the Stacks Project.

CategoryTheory.GrothendieckTopology.isIso_unit_and_sheafAdjunctionCocontinuous_counit_of_isSubterminal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/MoreLocalization.lean, line 91. The attribute's comment: “if every object of C has at most one morphism to U, the canonical maps F ⟶ j_U^{-1}j_{U!}F and j_U^{-1}j_{U*}F ⟶ F are isomorphisms, for coefficients in an arbitrary category A”. References: SGA 4 VIII (5.7), “open immersion case”; SGA 4 I (5.6), “special case”.

Let C be a site, and let U be an object of C such that every object of C has at most one morphism to U, i.e. U is subterminal. Let L be a left adjoint of j_U^{-1} = J.overPullback A U : Sh(C) ⥤ Sh(C/U), i.e. let L be j_{U!}, and let j_{U*} = {}_pj_U be the pushforward along the cocontinuous localization functor. Then the canonical maps F ⟶ j_U^{-1}j_{U!}F and j_U^{-1}j_{U*}F ⟶ F are isomorphisms for every sheaf F on C/U: they are the unit of j_{U!} ⊣ j_U^{-1} and the counit of j_U^{-1} ⊣ j_{U*}. Equivalently, j_{U!} and j_{U*} are fully faithful.

public theorem isIso_unit_and_sheafAdjunctionCocontinuous_counit_of_isSubterminal {C : Type u}
    [Category.{v} C] (J : GrothendieckTopology C) (U : C) (hU : IsSubterminal U) (A : Type w)
    [Category.{w'} A] [∀ (F : (Over U)ᵒᵖ ⥤ A), (Over.forget U).op.HasPointwiseRightKanExtension F]
    {L : Sheaf (J.over U) A ⥤ Sheaf J A} (adj : L ⊣ J.overPullback A U) :
    IsIso adj.unit ∧
      IsIso ((Over.forget U).sheafAdjunctionCocontinuous A (J.over U) J).counit

Tag 0EYV, a lemma

Tag 0EYV in the Stacks Project.

CategoryTheory.GrothendieckTopology.overMapPullbackSquare, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/MoreLocalization.lean, line 332. The attribute's comment: “The relocalization morphisms of a commutative square form a commutative square of topoi: the two composites j_{V'/V}^{-1} ⋙ j_{U'/V'}^{-1} and j_{U/V}^{-1} ⋙ j_{U'/U}^{-1} of inverse images are canonically isomorphic.”.

The square of topoi attached to a commutative square

  U' --a--> U
  |b        |c
  V' --d--> V

of C by the relocalization morphisms commutes, in the form of the commutation isomorphism j_{V'/V}^{-1} ⋙ j_{U'/V'}^{-1} ≅ j_{U/V}^{-1} ⋙ j_{U'/U}^{-1} between the two composite inverse images.

public def overMapPullbackSquare (sq : CommSq a b c d) :
    J.overMapPullback A d ⋙ J.overMapPullback A b ≅
      J.overMapPullback A c ⋙ J.overMapPullback A a

CategoryTheory.GrothendieckTopology.isIso_overMapPushforwardBaseChange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/MoreLocalization.lean, line 432. The attribute's comment: “For a cartesian square, the base change transformation j_{V'/V}^{-1} ∘ j_{U/V,*} ⟶ j_{U'/V',*} ∘ j_{U'/U}^{-1} of the relocalization morphisms is an isomorphism.”.

If the square

  U' --a--> U
  |b        |c
  V' --d--> V

of C is cartesian, then the relocalization morphisms satisfy base change, j_{V'/V}^{-1} ∘ j_{U/V, *} = j_{U'/V', *} ∘ j_{U'/U}^{-1}: the base change transformation overMapPushforwardBaseChange is an isomorphism.

public theorem isIso_overMapPushforwardBaseChange (hsq : IsPullback a b c d)
    [∀ (F : (Over U)ᵒᵖ ⥤ A), (Over.map c).op.HasPointwiseRightKanExtension F]
    [∀ (F : (Over U')ᵒᵖ ⥤ A), (Over.map b).op.HasPointwiseRightKanExtension F] :
    IsIso (J.overMapPushforwardBaseChange A hsq.toCommSq).natTrans

Sources

• Section 7.27, Tag 04IM
• AxiomMath/Stacks at 5ed82d14

LeanCategoryTheory.OverShriek.isIso_ofRestricted_unit · StacksLocalizationProducts.bijective_left_comp_prodSnd · StacksLocalizationProducts.isMorphismOfSites_star · StacksLocalizationProducts.sheafPushforwardOverForgetIso · StacksLocalizationProducts.sheafPullbackStarIso · StacksLocalizationProducts.sheafPushforwardObjEquiv · StacksRelocalization.isMorphismOfSites_overPullback · StacksRelocalization.sheafPushforwardOverMapIso

Section7.28 Localization and morphisms#

Section 7.28 of the Stacks Project, Tag 04I8. 7 tags here are carried by 23 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03CF, a lemma

Tag 03CF in the Stacks Project.

CategoryTheory.Functor.isContinuous_overPost_of_preservesPullbacks, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SlicePost/Continuous.lean, line 82. The attribute's comment: “Continuity of the functor u' : D/V ⥤ C/U, V'/V ↦ u(V')/U, which the proof of 03CF asserts without argument and which is the input to every other clause. Proved here for u continuous with fibre products which u preserves, i.e. for Stacks' notion of continuity on sites with fibre products; see Functor.isContinuous_overPost_of_flat for the flat version and the module docstring for why bare Functor.IsContinuous is not known to suffice.”.

Let u : C ⥤ D be a continuous functor of sites, let C have pullbacks and let u preserve them. Then Over.post u : Over V ⥤ Over (u.obj V) is continuous for the localized topologies J.over V and K.over (u.obj V).

theorem isContinuous_overPost_of_preservesPullbacks [HasPullbacks C] (u : C ⥤ D)
    [PreservesLimitsOfShape WalkingCospan u] [u.IsContinuous J K] (V : C) :
    (Over.post (X := V) u).IsContinuous (J.over V) (K.over (u.obj V))

CategoryTheory.Functor.isContinuous_overPost_of_isContinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SlicePost/MorphismOfSitesGeneral.lean, line 144. The attribute's comment: “Clause (a), continuity half: u' = Over.post u is continuous whenever u is, with no finite-limit or flatness hypothesis. This supersedes the flatness-based Functor.isContinuous_overPost_of_flat.”.

Stacks 03CF, continuity of u', in the generality of 03CF. If u : C ⥤ D is continuous then so is the localized functor Over.post u : Over V ⥤ Over (u.obj V).

By Stacks 00Y1 every sheaf on D/U is the fibre sheaf of a K-sheaf over h_U^# (OverShriek.sheafUnit), and the restriction of such a fibre sheaf along Over.post u is the fibre presheaf cut out on C/V by the restrictions along u, which is a sheaf by OverShriek.isSheaf_fiber_overPost.

theorem Functor.isContinuous_overPost_of_isContinuous {C : Type u} [SmallCategory C] {D : Type u}
    [SmallCategory D] (J : GrothendieckTopology C) (K : GrothendieckTopology D) (u : C ⥤ D)
    [u.IsContinuous J K] (V : C) :
    (Over.post (X := V) u).IsContinuous (J.over V) (K.over (u.obj V))

CategoryTheory.Functor.isMorphismOfSites_overPost_of_isMorphismOfSites, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SlicePost/MorphismOfSitesGeneral.lean, line 285. The attribute's comment: “Clause (a): the localized functor u' = Over.post u defines a morphism of sites D/u(V) → C/V, assuming only that u does. This is the clause Stacks derives from clause (c) via 00Y1, and which Functor.isMorphismOfSites_overPost covers only under 03EF's finite-limit and left-exactness hypotheses.”.

Stacks 03CF, clause (a), in the generality of 03CF. If u : C ⥤ D defines a morphism of sites f : D → C and V : C, then the localized functor u' = Over.post u : Over V ⥤ Over (u V) defines a morphism of sites f' : D/u(V) → C/V.

Continuity is Functor.isContinuous_overPost_of_isContinuous. Exactness of u'_s is checked on the terminal object and on fibre products: the former by Functor.preservesTerminal_sheafPullback_of_isTerminal, since Over.post u carries 𝟙_V to 𝟙_{u V}; the latter by sheafPullbackOverPostIso, u'_s ⋙ j_{U!} ≅ j_{V!} ⋙ u_s, together with the fact that j_{V!} preserves and j_{U!} reflects connected limits (Stacks 00Y1) and that u_s is left exact by hypothesis.

theorem Functor.isMorphismOfSites_overPost_of_isMorphismOfSites {C : Type u} [SmallCategory C]
    {D : Type u} [SmallCategory D] (J : GrothendieckTopology C) (K : GrothendieckTopology D)
    (u : C ⥤ D) (V : C) (h : u.IsMorphismOfSites J K) :
    (Over.post (X := V) u).IsMorphismOfSites (J.over V) (K.over (u.obj V))

CategoryTheory.sheafPushforwardContinuous_overPost_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SlicePost/Pushforward.lean, line 107. The attribute's comment: “Clause (d): the identity f'_* j_U^{-1} = j_V^{-1} f_*, for sheaves valued in any category; also the last sentence of 03EF. Clause (a) is in Sites/SlicePost/MorphismOfSitesGeneral.lean and clauses (b) and (c) are in Sites/SliceTopos/InverseImage.lean, all three in 03CF's own generality.”.

Stacks 03CF, last assertion: f'_* j_U^{-1} = j_V^{-1} f_*, as a strict equality of functors Sheaf K A ⥤ Sheaf (J.over V) A for an arbitrary target category A.

In Lean's left-to-right composition order the left-hand side below is f'_* ∘ j_U^{-1} and the right-hand side is j_V^{-1} ∘ f_*. Both are precomposition with the opposite of a functor Over V ⥤ D, and the two functors agree on the nose by Over.post_forget_eq_forget_comp; this is Stacks' remark that the identity "holds even for presheaves".

Clause (a) of Stacks 03CF, that f' is a morphism of sites, is Functor.isMorphismOfSites_overPost_of_isMorphismOfSites in StacksFrontier/CategoryTheory/Sites/SlicePost/MorphismOfSitesGeneral.lean, in the generality of 03CF. Clauses (b) and (c) are proved in StacksFrontier/CategoryTheory/Sites/SliceTopos/InverseImage.lean, also in 03CF's own generality.

theorem sheafPushforwardContinuous_overPost_eq :
    (Over.forget (u.obj V)).sheafPushforwardContinuous A (K.over (u.obj V)) K ⋙
        (Over.post (X := V) u).sheafPushforwardContinuous A (J.over V) (K.over (u.obj V)) =
      u.sheafPushforwardContinuous A J K ⋙
        (Over.forget V).sheafPushforwardContinuous A (J.over V) J

CategoryTheory.sheafPullbackOverPostIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SlicePost/Pushforward.lean, line 131. The attribute's comment: “The isomorphism j_{U!}(f')^{-1} ≅ f^{-1}j_{V!} of the proof of 03CF, deduced from clause (d) by uniqueness of left adjoints. As in the clause note on sheafPushforwardContinuous_overPost_eq, clauses (b) and (c) of 03CF are not covered; they are in Sites/SliceTopos/InverseImage.lean.”.

The lower-shriek form of Stacks 03CF's computation: (f')^{-1} j_{U!} ≅ j_{V!} f^{-1}.

This is the isomorphism j_{U!}(f')^{-1}H ≅ f^{-1}j_{V!}H displayed in the proof of Stacks 03CF, obtained here not from Stacks 00WY but by taking left adjoints in sheafPushforwardContinuous_overPost_eq: (f')^{-1} ⋙ j_{U!} is left adjoint to j_U^{-1} ⋙ f'_* and j_{V!} ⋙ f^{-1} is left adjoint to f_* ⋙ j_V^{-1}, and those two right adjoints are equal. Uniqueness of left adjoints does the rest.

noncomputable def sheafPullbackOverPostIso :
    (Over.post (X := V) u).sheafPullback A (J.over V) (K.over (u.obj V)) ⋙
        (Over.forget (u.obj V)).sheafPullback A (K.over (u.obj V)) K ≅
      (Over.forget V).sheafPullback A (J.over V) J ⋙ u.sheafPullback A J K

CategoryTheory.SliceTopos.sheafFunctorToOverCompOverPostIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SliceTopos/InverseImage.lean, line 223. The attribute's comment: “Clause (c): under 00Y1's identifications (f')⁻¹ sends (H ⟶ h_V^#) to (f⁻¹H ⟶ h_U^#). Proved in 03CF's own generality, from u.IsMorphismOfSites alone, and with the identification f⁻¹h_V^# ≅ h_U^# given by yonedaIso, which is NOT proved equal to 04D3's sheafPullbackSheafifyYonedaIso.”.

Stacks 03CF, clause (c). Under the identifications Sh(C/V) = Sh(C)/h_V^# and Sh(D/U) = Sh(D)/h_U^# of Stacks 00Y1, the inverse image (f')⁻¹ is "apply f⁻¹ to the sheaf and to its structure map":

  (f')⁻¹ (H ⟶ h_V^#) = (f⁻¹H ⟶ f⁻¹h_V^# ≅ h_U^#) .

The two sides agree after Over.forget by underlyingIso, and by Over.comp_hom_of_terminal the remaining triangle need only be checked at the terminal sheaf, where yonedaIso was defined to make it commute.

def sheafFunctorToOverCompOverPostIso (hu : u.IsMorphismOfSites J K) :
    (Over.post (X := V) u).sheafPullback (Type u) (J.over V) (K.over (u.obj V)) ⋙
        sheafFunctorToOver (U := u.obj V) K ≅
      sheafFunctorToOver (U := V) J ⋙ Over.post (u.sheafPullback (Type u) J K) ⋙
        Over.map (yonedaIso J K u V hu).hom

CategoryTheory.SliceTopos.overPullbackCompSheafPullbackOverPostIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SliceTopos/InverseImage.lean, line 291. The attribute's comment: “Clause (b): the square of topoi commutes, (f')⁻¹ j_V⁻¹ ≅ j_U⁻¹ f⁻¹. Proved in 03CF's own generality, from u.IsMorphismOfSites alone. Clause (a) is Functor.isMorphismOfSites_overPost_of_isMorphismOfSites; clause (d) is sheafPushforwardContinuous_overPost_eq.”.

Stacks 03CF, clause (b): the square of topoi commutes.

  (f')⁻¹ j_V⁻¹ = j_U⁻¹ f⁻¹ .

Unlike clause (d) this pairs two inverse images, so it is not a statement about right adjoints and does not follow from sheafPushforwardContinuous_overPost_eq. It follows from clause (c) instead: Φ_U is fully faithful, so it is enough to prove the square after applying it, and there Stacks 04IQ (OverShriek.overPullbackCompSheafFunctorToOverIso) turns both j_V⁻¹ Φ_V and j_U⁻¹ Φ_U into toOver, i.e. into "product with h_V^#" and "product with h_U^#". What is left is toOverCompOverPostIso, that f⁻¹ carries one product to the other.

The statement does not mention the identification f⁻¹h_V^# ≅ h_U^#, so — unlike clause (c) — it does not depend on which identification is used.

def overPullbackCompSheafPullbackOverPostIso (hu : u.IsMorphismOfSites J K) :
    J.overPullback (Type u) V ⋙
        (Over.post (X := V) u).sheafPullback (Type u) (J.over V) (K.over (u.obj V)) ≅
      u.sheafPullback (Type u) J K ⋙ K.overPullback (Type u) (u.obj V)

CategoryTheory.SliceTopos.overPullbackCompSheafPullbackOverPostIso_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SliceTopos/InverseImage.lean, line 581. The attribute's comment: “Clause (b) is the Beck-Chevalley mate of clause (d), which is what makes its components computable.”.

Stacks 03CF's clause (b) is the Beck–Chevalley mate of its clause (d).

The comparison (f')^{-1}j_V^{-1} ≅ j_U^{-1}f^{-1} built from Stacks 00Y1 coincides with the mate of the strict identity f'_*j_U^{-1} = j_V^{-1}f_*. Since j_{U!} ⊣ j_U^{-1} is a bijection the two transformations may be compared through their adjuncts, and those agree by shriek_overPullbackCompSheafPullbackOverPostIso_hom_app_comp_counit and overPullbackCompSheafPullbackOverPostMate_comp_counit.

This is what gives clause (b) computable components: every statement about the comparison can now be read off the unit and counit composite defining the mate.

theorem overPullbackCompSheafPullbackOverPostIso_hom (hu : u.IsMorphismOfSites J K) :
    (overPullbackCompSheafPullbackOverPostIso J K u V hu).hom =
      overPullbackCompSheafPullbackOverPostMate J K u V

Tag 03EF, a lemma

Tag 03EF in the Stacks Project.

CategoryTheory.Functor.isContinuous_overPost_of_flat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SlicePost/Continuous.lean, line 97. The attribute's comment: “Continuity of u' : D/V ⥤ C/U under 03EF's hypotheses: 03EF assumes u left exact between sites with all finite limits, whence Over.post u is flat and this lemma applies. This is the continuity half of Functor.isMorphismOfSites_overPost.”.

Let u : C ⥤ D be a continuous functor of sites such that Over.post u : Over V ⥤ Over (u.obj V) is representably flat. Then Over.post u is continuous for the localized topologies J.over V and K.over (u.obj V).

theorem isContinuous_overPost_of_flat (u : C ⥤ D) [u.IsContinuous J K] (V : C)
    [RepresentablyFlat (Over.post (X := V) u)] :
    (Over.post (X := V) u).IsContinuous (J.over V) (K.over (u.obj V))

CategoryTheory.starCompOverPostIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SlicePost/MorphismOfSites.lean, line 78. The attribute's comment: “Commutativity of the diagram of 03EF: the two composites C ⥤ Over (u.obj V) of continuous functors around the square are isomorphic, which since morphisms of sites compose by composing their continuous functors (03CC) is what it means for the square of morphisms of sites to commute. The final clause of 03EF, that the induced diagram of topoi equals the diagram of 03CF, is NOT covered — see the module docstring.”.

For a functor u : C ⥤ D preserving binary products and V : C, the isomorphism Over.star V ⋙ Over.post u ≅ u ⋙ Over.star (u.obj V) of functors C ⥤ Over (u.obj V), whose component at X is Limits.prodComparison u V X : u.obj (V ⨯ X) ⟶ u.obj V ⨯ u.obj X.

noncomputable def starCompOverPostIso [HasBinaryProducts C] [HasBinaryProducts D] (u : C ⥤ D)
    [PreservesLimitsOfShape (Discrete WalkingPair) u] (V : C) :
    Over.star V ⋙ Over.post (X := V) u ≅ u ⋙ Over.star (u.obj V)

CategoryTheory.Functor.isMorphismOfSites_overPost, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SlicePost/MorphismOfSites.lean, line 110. The attribute's comment: “The left vertical arrow of 03EF's diagram: u' = Over.post u is a morphism of sites D/U → C/V under 03EF's hypotheses. This is 03CF's clause (a) in the special case where 03EF's hypotheses hold; clause (a) in the generality of 03CF is Functor.isMorphismOfSites_overPost_of_isMorphismOfSites in Sites/SlicePost/MorphismOfSitesGeneral.lean, proved there through 00Y1 as Stacks does.”. References: SGA 4 VI (7.4.13.6), “special case”.

If C and D have all finite limits and u : C ⥤ D is continuous and commutes with finite limits, then for V : C the localized functor Over.post u : Over V ⥤ Over (u.obj V) defines a morphism of sites D/U → C/V, where U = u.obj V.

theorem isMorphismOfSites_overPost [HasFiniteLimits C] [HasFiniteLimits D] (u : C ⥤ D)
    [u.IsContinuous J K] [PreservesFiniteLimits u] (V : C) :
    (Over.post (X := V) u).IsMorphismOfSites (J.over V) (K.over (u.obj V))

CategoryTheory.Functor.isMorphismOfSites_star, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SlicePost/MorphismOfSites.lean, line 121. The attribute's comment: “The two horizontal arrows j_U and j_V of 03EF's diagram: the localization functors X ↦ X ⨯ U of 03CE are morphisms of sites. Stated once, for an arbitrary site and object; the diagram of 03EF instantiates it at (C, J, V) and at (D, K, u.obj V).”.

On a site with binary products, the localization functor Over.star X : C ⥤ Over X, Y ↦ (Y ⨯ X ⟶ X), defines a morphism of sites C/X → C.

theorem isMorphismOfSites_star [HasBinaryProducts C] (X : C) :
    (Over.star X).IsMorphismOfSites J (J.over X)

CategoryTheory.sheafPushforwardContinuousStarOverPostIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SlicePost/MorphismOfSites.lean, line 146. The attribute's comment: “The induced diagram of morphisms of topoi commutes, on the pushforward side, for sheaves valued in any category. 03EF's final clause — that this diagram is EQUAL to 03CF's diagram of topoi — is NOT covered; 03CF's clause (b) is now proved in Sites/SliceTopos/InverseImage.lean, leaving one equation.”.

The isomorphism

  (Over.post u)_* ⋙ (Over.star V)_* ≅ (Over.star U)_* ⋙ u_* ,

of functors Sheaf (K.over U) A ⥤ Sheaf J A, for U = u.obj V and any category A, induced by starCompOverPostIso: the square of pushforwards on sheaves commutes.

noncomputable def sheafPushforwardContinuousStarOverPostIso [HasBinaryProducts C]
    [HasBinaryProducts D] (u : C ⥤ D) [PreservesLimitsOfShape (Discrete WalkingPair) u] (V : C)
    [u.IsContinuous J K]
    [(Over.post (X := V) u).IsContinuous (J.over V) (K.over (u.obj V))]
    (A : Type*) [Category A] :
    (Over.post (X := V) u).sheafPushforwardContinuous A (J.over V) (K.over (u.obj V)) ⋙
        (Over.star V).sheafPushforwardContinuous A J (J.over V) ≅
      (Over.star (u.obj V)).sheafPushforwardContinuous A K (K.over (u.obj V)) ⋙
        u.sheafPushforwardContinuous A J K

Tag 04IN, a lemma

Tag 04IN in the Stacks Project.

MorphismOfTopoi.relocalize, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/RelocalizationMorphism.lean, line 163. The attribute's comment: “the morphism of topoi f_c and the factorization f_c = f' ∘ j_{U/u(V)}”.

Stacks 04IN. Let f : E ⟶ D be a morphism of topoi, V an object of D, U an object of E and c : U ⟶ f⁻¹V. The morphism of topoi f_c : E/U ⟶ D/V is the composition

  f_c = f' ∘ j_{U/f⁻¹V}

of the relocalization morphism j_{U/f⁻¹V} : E/U ⟶ E/f⁻¹V of Stacks 03EH with the morphism f' : E/f⁻¹V ⟶ D/V of Stacks 04H1 (03CF); this factorization is Stacks 04IN's second assertion, and holds here by construction. Consequently

  (f_c)⁻¹ = Over.post f⁻¹ ⋙ Over.pullback c ,

see relocalize_inverseImage_obj.

noncomputable def relocalize {V : D} {U : E} (c : U ⟶ f.inverseImage.obj V)
    {p : Over U ⥤ Over (f.inverseImage.obj V)} (adj : Over.pullback c ⊣ p) :
    MorphismOfTopoi (Over U) (Over V)

MorphismOfTopoi.relocalize_inverseImage_obj, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/RelocalizationMorphism.lean, line 175. The attribute's comment: “the description of (f_c)^{-1} as a fibre product”.

Stacks 04IN, the description of (f_c)⁻¹: an object φ : H ⟶ V of D/V is sent to the fibre product

  (f⁻¹H ×_{f⁻¹φ, f⁻¹V, c} U ⟶ U) ,

the base change along c of f⁻¹φ.

lemma relocalize_inverseImage_obj {V : D} {U : E} (c : U ⟶ f.inverseImage.obj V)
    {p : Over U ⥤ Over (f.inverseImage.obj V)} (adj : Over.pullback c ⊣ p) (H : Over V) :
    (f.relocalize c adj).inverseImage.obj H =
      Over.mk (pullback.snd (f.inverseImage.map H.hom) c)

MorphismOfTopoi.relocalizeInverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/RelocalizationMorphism.lean, line 191. The attribute's comment: “commutativity of the first square, on inverse images”.

Stacks 04IN, commutativity of the first square: j_U⁻¹ ∘ f⁻¹ = (f_c)⁻¹ ∘ j_V⁻¹, where j_U⁻¹ = toOver U and j_V⁻¹ = toOver V.

The proof is the one Stacks gives: the square of Stacks 04H1 for f', namely f⁻¹ ⋙ toOver (f⁻¹V) ≅ toOver V ⋙ (f')⁻¹, is whiskered with the base change j_{U/f⁻¹V}⁻¹ = Over.pullback c, and the left-hand side collapses by toOverCompPullbackIso, the identity j_{U/f⁻¹V}⁻¹ ∘ j_{f⁻¹V}⁻¹ = j_U⁻¹ of Stacks 03EH.

noncomputable def relocalizeInverseImageIso {V : D} {U : E} (c : U ⟶ f.inverseImage.obj V)
    {p : Over U ⥤ Over (f.inverseImage.obj V)} (adj : Over.pullback c ⊣ p) :
    f.inverseImage ⋙ toOver U ≅ toOver V ⋙ (f.relocalize c adj).inverseImage

MorphismOfTopoi.relocalizeCompPullbackIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/RelocalizationMorphism.lean, line 214. The attribute's comment: “commutativity of the last square, on inverse images”.

Stacks 04IN, commutativity of the last square: given b : V' ⟶ V, a : U' ⟶ U and c' : U' ⟶ f⁻¹V' with c' ≫ f⁻¹b = a ≫ c, the square

  E/U' --j_{U'/U}--> E/U
   |f_{c'}            |f_c
  D/V' --j_{V'/V}--> D/V

commutes, i.e. (f_c)⁻¹ ∘ j_{U'/U}⁻¹ = j_{V'/V}⁻¹ ∘ (f_{c'})⁻¹ on inverse images.

This is Stacks' equality

  f⁻¹H ×_{f⁻¹V, c} U ×_U U' = f⁻¹(H ×_V V') ×_{f⁻¹V', c'} U' ,

obtained here by Beck–Chevalley for Over.post f⁻¹ (Over.postPullbackIso, which uses that f⁻¹ is left exact), the composition rule Over.pullbackComp for base change, and the hypothesis c' ≫ f⁻¹b = a ≫ c.

noncomputable def relocalizeCompPullbackIso {V V' : D} (b : V' ⟶ V) {U U' : E} (a : U' ⟶ U)
    (c : U ⟶ f.inverseImage.obj V) (c' : U' ⟶ f.inverseImage.obj V')
    (hc : c' ≫ f.inverseImage.map b = a ≫ c)
    {p : Over U ⥤ Over (f.inverseImage.obj V)} (adj : Over.pullback c ⊣ p)
    {p' : Over U' ⥤ Over (f.inverseImage.obj V')} (adj' : Over.pullback c' ⊣ p') :
    Over.pullback b ⋙ (f.relocalize c' adj').inverseImage ≅
      (f.relocalize c adj).inverseImage ⋙ Over.pullback a

Tag 03EG, a lemma

Tag 03EG in the Stacks Project.

overPost_comp_forget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/LocalizationComposite.lean, line 103. The attribute's comment: “the square of categories commutes: u' ⋙ j_V = j_U ⋙ u”.

Stacks 03EG, the square of categories. With V = u(U), the localized functor u' = Over.post u : C/U ⥤ D/V and the localization functors j_U = Over.forget U and j_V = Over.forget V form a commutative square, u' ⋙ j_V = j_U ⋙ u. Stacks calls this "clear"; in Lean the two composites are equal by rfl.

theorem overPost_comp_forget :
    (Over.post u : Over U ⥤ Over (u.obj U)) ⋙ Over.forget (u.obj U) = Over.forget U ⋙ u

isCocontinuous_overPost, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/LocalizationComposite.lean, line 118. The attribute's comment: “the left vertical arrow u' is cocontinuous”.

Stacks 03EG, the mathematical content. If u : C ⥤ D is cocontinuous then so is the localized functor u' = Over.post u : C/U ⥤ D/u(U), for the localized topologies J.over U and K.over (u.obj U).

Stacks proves this by transferring refinement data verbatim: a covering of u(U')/u(U) in D/u(U) is in particular a covering of u(U') in D, cocontinuity of u refines its u-image by a covering {U'_i → U'} of C, and the very same index map and comparison morphisms exhibit the refinement after every object is viewed over U, resp. over u(U). In Mathlib's sieve-theoretic formulation this is CategoryTheory.GrothendieckTopology.instIsCocontinuousOverObjPostOver.

theorem isCocontinuous_overPost :
    (Over.post u : Over U ⥤ Over (u.obj U)).IsCocontinuous (J.over U) (K.over (u.obj U))

sheafPushforwardCocontinuousOverPostIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/LocalizationComposite.lean, line 133. The attribute's comment: “the square of topoi commutes: f'_* ⋙ j_{V*} ≅ j_{U*} ⋙ f_*”.

Stacks 03EG, the square of topoi. Let f : Sh(C) ⟶ Sh(D) and f' : Sh(C/U) ⟶ Sh(D/u(U)) be the morphisms of topoi attached to u and to u' = Over.post u by Stacks 00XO, and let j_U : Sh(C/U) ⟶ Sh(C) and j_V : Sh(D/u(U)) ⟶ Sh(D) be those attached to the localization functors. Then the square of topoi commutes: there is a natural isomorphism f'_* ⋙ j_{V*} ≅ j_{U*} ⋙ f_* of functors Sh(C/U) ⥤ Sh(D).

Both composites compute the direct image of one and the same functor C/U ⥤ D, since u' ⋙ j_V = j_U ⋙ u by overPost_comp_forget; the isomorphism is therefore obtained by comparing each side with that direct image using Stacks 03L5.

noncomputable def sheafPushforwardCocontinuousOverPostIso :
    (Over.post u : Over U ⥤ Over (u.obj U)).sheafPushforwardCocontinuous (Type u)
          (J.over U) (K.over (u.obj U)) ⋙
        (Over.forget (u.obj U)).sheafPushforwardCocontinuous (Type u) (K.over (u.obj U)) K ≅
      (Over.forget U).sheafPushforwardCocontinuous (Type u) (J.over U) J ⋙
        u.sheafPushforwardCocontinuous (Type u) J K

Tag 0D5R, a lemma

Tag 0D5R in the Stacks Project.

CategoryTheory.Functor.exists_grothendieckTopology_costructuredArrow, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/AndMorphisms.lean, line 551. The attribute's comment: “The site of pairs (U, ψ : u(U) → V) for a cocontinuous u: j is continuous and cocontinuous, u' is cocontinuous, the resulting square of topoi commutes and f'_* j⁻¹ = j_V⁻¹ f_*. For sheaves of sets on small sites.”. References: SGA 3 IV (4.5.1), “partial, special case”; SGA 4 III (5.2), “special case”.

Let (C, J) and (D, K) be sites, let u : C ⥤ D be cocontinuous and let V be an object of D. Let {}^u_V I = CostructuredArrow u V be the category of pairs (U, ψ : u(U) ⟶ V) of Section 00XF, with the two projections j = CostructuredArrow.proj u V, (U, ψ) ↦ U, and u' = CostructuredArrow.toOver u V, (U, ψ) ↦ (ψ : u(U) ⟶ V). Then the square

  {}^u_V I --j--> C
     |            |
     u'           u
     v            v
    D/V --j_V---> D

commutes, and declaring a sieve of (U, ψ) to be covering when its image under j is a covering sieve of U:

1. this is a Grothendieck topology H on {}^u_V I, i.e. {}^u_V I is a site;
2. j is continuous and cocontinuous;
3. u' is cocontinuous;
4. the induced square of topoi commutes, j_* ⋙ f_* ≅ f'_* ⋙ j_{V*}, where f and f' are the morphisms of topoi of Stacks 00XO attached to the cocontinuous functors u and u'; and
5. f'_* ∘ j⁻¹ = j_V⁻¹ ∘ f_*, where the inverse images of the continuous and cocontinuous functors j and j_V are restriction (Stacks 00XR).

public theorem exists_grothendieckTopology_costructuredArrow {C : Type u} [SmallCategory C]
    {D : Type u} [SmallCategory D] (J : GrothendieckTopology C) (K : GrothendieckTopology D)
    (u : C ⥤ D) [u.IsCocontinuous J K] (V : D) :
    CostructuredArrow.proj u V ⋙ u = CostructuredArrow.toOver u V ⋙ Over.forget V ∧
      ∃ H : GrothendieckTopology (CostructuredArrow u V),
        (∀ (X : CostructuredArrow u V) (S : Sieve X),
            S ∈ H X ↔ Sieve.functorPushforward (CostructuredArrow.proj u V) S ∈ J X.left) ∧
          ∃ (_ : (CostructuredArrow.proj u V).IsContinuous H J) (_ :
            (CostructuredArrow.proj u V).IsCocontinuous H J) (_ :
            (CostructuredArrow.toOver u V).IsCocontinuous H (K.over V)),
            Nonempty
                ((CostructuredArrow.proj u V).sheafPushforwardCocontinuous (Type u) H J ⋙
                    u.sheafPushforwardCocontinuous (Type u) J K ≅
                  (CostructuredArrow.toOver u V).sheafPushforwardCocontinuous (Type u) H
                      (K.over V) ⋙
                    (Over.forget V).sheafPushforwardCocontinuous (Type u) (K.over V) K) ∧
              Nonempty
                ((CostructuredArrow.proj u V).sheafPushforwardContinuous (Type u) H J ⋙
                    (CostructuredArrow.toOver u V).sheafPushforwardCocontinuous (Type u) H
                      (K.over V) ≅
                  u.sheafPushforwardCocontinuous (Type u) J K ⋙
                    (Over.forget V).sheafPushforwardContinuous (Type u) (K.over V) K)

Tag 0FN1, a lemma

Tag 0FN1 in the Stacks Project.

CategoryTheory.Functor.nonempty_sheafPushforwardContinuousCompCocontinuousIso_and_leftAdjointCompPullbackIso_of_final, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/AndMorphisms.lean, line 214. The attribute's comment: “Beck–Chevalley for a commutative square of sites whose vertical functors are cocontinuous and whose horizontal functors are continuous: if the comparison functors {}^{u'}_{V'} I ⥤ {}^u_{v(V')} I are all cofinal then f'_* (g')⁻¹ = g⁻¹ f_*, and g'_! (f')⁻¹ = f⁻¹ g_! whenever the relevant left adjoints exist — a hypothesis of the second conjunct only, the first equality being the cofinality content and using no adjoint. For coefficients in an arbitrary category, the source's sheaves of sets being the case A = Type u; cocontinuity of the horizontal functors is not needed once their inverse images are read as restriction (Stacks 00XR).”.

Let (C', J'), (C, J), (D', K'), (D, K) be sites and consider a square of functors

  C' --v'--> C
  |          |
  u'         u
  v          v
  D' --v---> D

with u' ⋙ v = v' ⋙ u, where u and u' are cocontinuous — giving rise to morphisms of topoi f and f' with f_* = {}_su, f'_* = {}_su' (Stacks 00XO) — and v and v' are continuous, so that g⁻¹ = v^p and (g')⁻¹ = (v')^p are restriction (Stacks 00XR). Assume that for every object V' of D' the comparison functor

  {}^{u'}_{V'} I ⥤ {}^u_{v(V')} I,   (U', ψ) ↦ (v'(U'), v(ψ) : u(v'(U')) = v(u'(U')) ⟶ v(V')),

on the categories of Section 00XF is cofinal, i.e. final. Then f'_* ∘ (g')⁻¹ ≅ g⁻¹ ∘ f_*, and moreover g'_! ∘ (f')⁻¹ ≅ f⁻¹ ∘ g_! whenever the two restrictions have left adjoints g_!, g'_! and the two pushforwards have left adjoints f⁻¹, (f')⁻¹. This holds for sheaves with values in an arbitrary category A.

public theorem
  nonempty_sheafPushforwardContinuousCompCocontinuousIso_and_leftAdjointCompPullbackIso_of_final
    {C' : Type u₁} [Category.{v₁} C'] {C : Type u₂} [Category.{v₂} C] {D' : Type u₃}
    [Category.{v₃} D'] {D : Type u₄} [Category.{v₄} D] (A : Type u₅) [Category.{v₅} A]
    (J' : GrothendieckTopology C') (J : GrothendieckTopology C) (K' : GrothendieckTopology D')
    (K : GrothendieckTopology D) (u' : C' ⥤ D') (u : C ⥤ D) (v' : C' ⥤ C) (v : D' ⥤ D)
    [u.IsCocontinuous J K] [u'.IsCocontinuous J' K'] [v.IsContinuous K' K] [v'.IsContinuous J' J]
    [∀ F : Cᵒᵖ ⥤ A, u.op.HasPointwiseRightKanExtension F]
    [∀ F : C'ᵒᵖ ⥤ A, u'.op.HasPointwiseRightKanExtension F] (hsq : u' ⋙ v = v' ⋙ u)
    (hfinal :
      ∀ V' : D',
        (CostructuredArrow.map₂ (S := u') (T := V') (U := u) (V := v.obj V') (F := v') (G := v)
            (eqToHom hsq.symm) (𝟙 (v.obj V'))).Final) :
    Nonempty
        (v'.sheafPushforwardContinuous A J' J ⋙ u'.sheafPushforwardCocontinuous A J' K' ≅
          u.sheafPushforwardCocontinuous A J K ⋙ v.sheafPushforwardContinuous A K' K) ∧
      ∀ [(u.sheafPushforwardCocontinuous A J K).IsRightAdjoint]
        [(u'.sheafPushforwardCocontinuous A J' K').IsRightAdjoint]
        [(v'.sheafPushforwardContinuous A J' J).IsRightAdjoint]
        [(v.sheafPushforwardContinuous A K' K).IsRightAdjoint],
        Nonempty
          ((u'.sheafPushforwardCocontinuous A J' K').leftAdjoint ⋙ v'.sheafPullback A J' J ≅
            v.sheafPullback A K' K ⋙ (u.sheafPushforwardCocontinuous A J K).leftAdjoint)

Tag 0FN2, a lemma

Tag 0FN2 in the Stacks Project.

CategoryTheory.Functor.sheafPushforwardContinuous_comp_eq_and_nonempty_sheafPullbackCompIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/AndMorphisms.lean, line 699. The attribute's comment: “Exchange for a commutative square of sites whose horizontal functors u, u' are continuous and whose vertical functors v, v' are continuous (in the source, continuous and cocontinuous): f'_* (g')⁻¹ = g⁻¹ f_* on the nose, and g'_! (f')⁻¹ ≅ f⁻¹ g_!. For coefficients in an arbitrary category; cocontinuity of v, v' is not needed once their inverse images are read as restriction (Stacks 00XR).”.

Let (C', J'), (C, J), (D', K'), (D, K) be sites and consider a square of functors

  C' --v'--> C
  ↑          ↑
  u'         u
  D' --v---> D

with v ⋙ u = u' ⋙ v', where u and u' are continuous — giving rise to morphisms of sites f and f' with f_* = u^s, f'_* = (u')^s and f⁻¹ = u_s, (f')⁻¹ = (u')_s (Stacks 00X0) — and v and v' are continuous, so that g⁻¹ = v^p and (g')⁻¹ = (v')^p are restriction and g_!, g'_! are their left adjoints (Stacks 00XR, for v, v' also cocontinuous). Then f'_* ∘ (g')⁻¹ = g⁻¹ ∘ f_* and g'_! ∘ (f')⁻¹ ≅ f⁻¹ ∘ g_!.

public theorem sheafPushforwardContinuous_comp_eq_and_nonempty_sheafPullbackCompIso {C' : Type u₁}
    [Category.{v₁} C'] {C : Type u₂} [Category.{v₂} C] {D' : Type u₃} [Category.{v₃} D']
    {D : Type u₄} [Category.{v₄} D] (A : Type u₅) [Category.{v₅} A] (J' : GrothendieckTopology C')
    (J : GrothendieckTopology C) (K' : GrothendieckTopology D') (K : GrothendieckTopology D)
    (u : D ⥤ C) (u' : D' ⥤ C') (v : D' ⥤ D) (v' : C' ⥤ C) [u.IsContinuous K J]
    [u'.IsContinuous K' J'] [v.IsContinuous K' K] [v'.IsContinuous J' J]
    [(u.sheafPushforwardContinuous A K J).IsRightAdjoint]
    [(u'.sheafPushforwardContinuous A K' J').IsRightAdjoint]
    [(v.sheafPushforwardContinuous A K' K).IsRightAdjoint]
    [(v'.sheafPushforwardContinuous A J' J).IsRightAdjoint] (hsq : v ⋙ u = u' ⋙ v') :
    v'.sheafPushforwardContinuous A J' J ⋙ u'.sheafPushforwardContinuous A K' J' =
        u.sheafPushforwardContinuous A K J ⋙ v.sheafPushforwardContinuous A K' K ∧
      Nonempty
        (u'.sheafPullback A K' J' ⋙ v'.sheafPullback A J' J ≅
          v.sheafPullback A K' K ⋙ u.sheafPullback A K J)

Sources

• Section 7.28, Tag 04I8
• AxiomMath/Stacks at 5ed82d14

LeanCategoryTheory.Functor.isContinuous_overPost_of_preservesPullbacks · CategoryTheory.Functor.isContinuous_overPost_of_isContinuous · CategoryTheory.Functor.isMorphismOfSites_overPost_of_isMorphismOfSites · CategoryTheory.sheafPushforwardContinuous_overPost_eq · CategoryTheory.sheafPullbackOverPostIso · CategoryTheory.SliceTopos.sheafFunctorToOverCompOverPostIso · CategoryTheory.SliceTopos.overPullbackCompSheafPullbackOverPostIso · CategoryTheory.SliceTopos.overPullbackCompSheafPullbackOverPostIso_hom

Section7.29 Morphisms of topoi#

Section 7.29 of the Stacks Project, Tag 039Z. 7 tags here are carried by 8 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 03A0, a lemma

Tag 03A0 in the Stacks Project.

gInv_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Topos/ToposMorphismDefs.lean, line 223.

Stacks 03A0, the pullback half. Let C, D be sites and u : C ⥤ D a functor such that

1. u is cocontinuous;
2. u is continuous, in the form CoverPreserving J K u;
3. given a, b : U' ⟶ U in C with u a = u b, there is a covering of U' in C along which a and b agree;
4. given c : u U' ⟶ u U in D, there is a covering {f i : U' i ⟶ U'} in C and morphisms c i : U' i ⟶ U with u (c i) = u (f i) ≫ c;
5. every object of D admits a covering by objects u U i.

Then the morphism of topoi g : Sh(C) ⟶ Sh(D) attached to the cocontinuous functor u by Stacks 00XO is an equivalence: its pullback g^{-1} is an equivalence of categories. See gStar_isEquivalence for the direct image, and gEquivalence for the two packaged as an equivalence Sh(D) ≌ Sh(C).

theorem gInv_isEquivalence : (gInv C D J K u).IsEquivalence

gStar_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Topos/ToposMorphismDefs.lean, line 232.

Stacks 03A0, the direct-image half. In the situation of gInv_isEquivalence, the direct image g_* of the morphism of topoi of Stacks 00XO is an equivalence of categories as well; together with gInv_isEquivalence this says that the morphism of topoi g is an equivalence.

theorem gStar_isEquivalence : (gStar C D J K u).IsEquivalence

Tag 03CG, a definition

Tag 03CG in the Stacks Project.

IsSpecialCocontinuous, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Topos/ToposMorphismComp.lean, line 28.

A functor u : C ⥤ D from a site (C, J) to a site (D, K) is a special cocontinuous functor if it is cocontinuous and makes (C, J) a dense subsite of (D, K).

def IsSpecialCocontinuous {C : Type*} [Category C] {D : Type*} [Category D]
    (J : GrothendieckTopology C) (K : GrothendieckTopology D)
    (u : C ⥤ D) : Prop

Tag 03CH, a lemma

Tag 03CH in the Stacks Project.

DenseSubsiteOverSheafEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Topos/ToposEquivalence.lean, line 45.

Stacks 03CH.

Let (C, J) and (D, K) be sites and let u : C ⥤ D be a special cocontinuous functor, formalized in Mathlib as Functor.IsDenseSubsite J K u. Fix an object U : C. Then:

1. The square of underlying site functors commutes: Over.post u ⋙ Over.forget (u.obj U) = Over.forget U ⋙ u.

2. The induced functor Over.post u : Over U ⥤ Over (u.obj U) is again a special cocontinuous functor for the localized topologies J.over U and K.over (u.obj U).

3. Hence, for any target category A with the appropriate limits, both vertical arrows in the induced commutative diagram of sheaf categories are equivalences: Sheaf J A ≌ Sheaf K A (right vertical), and Sheaf (J.over U) A ≌ Sheaf (K.over (u.obj U)) A (left vertical).

The Prop below packages all three conclusions.

def DenseSubsiteOverSheafEquivalence
    (C : Type u) [Category.{v} C] (D : Type u') [Category.{v'} D]
    (J : GrothendieckTopology C) (K : GrothendieckTopology D)
    (u : C ⥤ D) (U : C)
    (A : Type w) [Category.{w'} A] : Prop

Tag 03A1, a lemma

Tag 03A1 in the Stacks Project.

CategoryTheory.GrothendieckTopology.exists_isDenseSubsite_subcanonical, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Topos/MorphismsOfTopoi.lean, line 766. The attribute's comment: “A full subcategory of Sh(C) with a set of objects which contains the sheafified representables and is closed under fibre products is a site, for the coverings whose coproduct is a surjection of sheaves; that site is subcanonical, U ↦ h_U^# is a special cocontinuous functor, and the induced equivalence of topoi matches the representables of the two sides. This is all five conclusions, with (5) stated for every object of the subcategory.”.

Let (C, J) be a site and let ι : C' ⥤ Sh(C) be a full subcategory of the category of sheaves of sets on C, with a set of objects, which is closed under fibre products and contains the sheafified representables: v : C ⥤ C' is a functor with v ⋙ ι ≅ h_{-}^#. Declare a covering of C' to be a family {F_i ⟶ F} of morphisms with ∐ F_i ⟶ F a surjection of sheaves. Then

1. these coverings are the coverings of a Grothendieck topology K on C', i.e. C' is a site;
2. K is subcanonical, i.e. representable presheaves on C' are sheaves;
3. v is a special cocontinuous functor, i.e. v.IsDenseSubsite J K, hence the induced morphism of topoi g : Sh(C) ⟶ Sh(C') is an equivalence;
4. g⁻¹ h_F = F for every object F of C'; and
5. g_* F = h_F for every object F of C'; along v this is g_* h_U^# = h_{v U} = h_{h_U^#}.

public theorem exists_isDenseSubsite_subcanonical {C : Type u} [Category.{v} C]
    (J : GrothendieckTopology C) {D : Type max u v} [SmallCategory D]
    (ι : D ⥤ Sheaf J (Type max u v)) [ι.Full] [ι.Faithful] [HasPullbacks D]
    [PreservesLimitsOfShape WalkingCospan ι] (v : C ⥤ D) (e : v ⋙ ι ≅ Sheaf.sheafifiedYoneda J) :
    ∃ K : GrothendieckTopology D,
      (∀ {X : D} {α : Type max u v} (Y : α → D) (p : ∀ a, Y a ⟶ X) {c : Cofan fun a ↦ ι.obj (Y a)}
          (hc : IsColimit c),
          Sieve.ofArrows Y p ∈ K X ↔ Epi (Cofan.IsColimit.desc hc fun a ↦ ι.map (p a))) ∧
        ∃ (_ : K.Subcanonical) (_ : v.IsDenseSubsite J K),
          Nonempty (K.yoneda ⋙ v.sheafPushforwardContinuous (Type max u v) J K ≅ ι) ∧
            Nonempty (ι ⋙ v.sheafPushforwardCocontinuous (Type max u v) J K ≅ K.yoneda)

Tag 03CI, a lemma

Tag 03CI in the Stacks Project.

CategoryTheory.GrothendieckTopology.exists_isDenseSubsite_subcanonical_hasFiniteLimits_representable, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Topos/MorphismsOfTopoi.lean, line 1432. The attribute's comment: “Any topos is equivalent, by a special cocontinuous functor, to the topos of sheaves on a site which is subcanonical, has all finite limits, has all subsheaves of representables representable, and on which a prescribed set of sheaves becomes representable. This is conclusions (1), (3), (4) and (5); conclusion (2) holds for every topology and is ofArrows_mem_iff_isLocallySurjective_sigmaDesc_uliftYoneda_map. The functor is also recorded to preserve all finite limits that exist in the given site.”. References: SGA 4 IV (1.2), “i) => i')”.

Let (C, J) be a site and let F : ι → Sheaf J (Type max u v) be a set of sheaves of sets on C. Then there is a site (D, K) and a special cocontinuous functor G : C ⥤ D (Stacks 03CG: a functor exhibiting (C, J) as a dense subsite of (D, K)), so that the induced morphism of topoi g : Sh(C) → Sh(D) is an equivalence, such that

1. K is subcanonical;
2. D has all finite limits, i.e. fibre products and a final object;
3. every subsheaf of a representable sheaf on D is representable; and
4. each g_* (F i) = (G.sheafPushforwardCocontinuous _ J K).obj (F i) is representable;

moreover G preserves all finite limits that exist in C.

public theorem exists_isDenseSubsite_subcanonical_hasFiniteLimits_representable {C : Type u}
    [Category.{v} C] (J : GrothendieckTopology C) {ι : Type max u v}
    (F : ι → Sheaf J (Type max u v)) :
    ∃ (D : Type max u v) (_ : SmallCategory D) (K : GrothendieckTopology D) (G : C ⥤ D) (_ :
      G.IsDenseSubsite J K) (_ : K.Subcanonical) (_ : HasFiniteLimits D)
      (_ : PreservesFiniteLimits G),
      (∀ (V : D) (ℱ : Sheaf K (Type max u v)) (i : ℱ ⟶ K.yoneda.obj V),
          Mono i → ℱ.obj.IsRepresentable) ∧
        (∀ i,
          ((G.sheafPushforwardCocontinuous (Type max u v) J K).obj
              (F i)).obj.IsRepresentable)

Tag 03A2, a lemma

Tag 03A2 in the Stacks Project.

MorphismOfTopoi.exists_isDenseSubsite_isMorphismOfSites_pushforward_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Topos/MorphismsOfTopoi.lean, line 1081. The attribute's comment: “Every morphism of topoi is the composition of the equivalence induced by a special cocontinuous functor with the morphism of topoi induced by a morphism of sites. The conclusion also records, from Stacks 03CJ, that u preserves the final object.”.

Let (C, J) and (D, K) be sites and let f : Sh(C) → Sh(D) be a morphism of topoi. Then there are a site (C', J') and functors v : C ⥤ C' and u : D ⥤ C' such that

1. v is a special cocontinuous functor, i.e. exhibits (C, J) as a dense subsite of (C', J'), so that the morphism of topoi g : Sh(C) → Sh(C') it induces is an equivalence;
2. u commutes with fibre products and with the final object, is continuous, and defines a morphism of sites C' → D, hence a morphism of topoi h : Sh(C') → Sh(D); and
3. f agrees with h ∘ g, in the sense that f_* is isomorphic to the composition of the pushforwards g_* = v.sheafPushforwardCocontinuous and h_* = u.sheafPushforwardContinuous.

public theorem exists_isDenseSubsite_isMorphismOfSites_pushforward_iso {C : Type u₁}
    [Category.{v₁} C] {D : Type u₁} [Category.{v₁} D] {J : GrothendieckTopology C}
    {K : GrothendieckTopology D}
    (f : MorphismOfTopoi (Sheaf J (Type max u₁ v₁)) (Sheaf K (Type max u₁ v₁))) :
    ∃ (C' : Type max u₁ v₁) (_ : SmallCategory C') (J' : GrothendieckTopology C') (v : C ⥤ C') (u :
      D ⥤ C') (_ : v.IsDenseSubsite J J') (_ : _root_.IsMorphismOfSites.{max u₁ v₁} u K J'),
      PreservesLimitsOfShape WalkingCospan u ∧
        PreservesLimitsOfShape (Discrete PEmpty.{1}) u ∧
          Nonempty
            (f.pushforward ≅
              v.sheafPushforwardCocontinuous (Type max u₁ v₁) J J' ⋙
                u.sheafPushforwardContinuous (Type max u₁ v₁) K J')

Tag 03CJ, a remark

Tag 03CJ in the Stacks Project.

MorphismOfTopoi.exists_twoSided_isDenseSubsite_representablyFlat, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Topos/ToposReplacement.lean, line 251. The attribute's comment: “Any morphism of topoi fits into a commutative square with two equivalences given by special cocontinuous functors and a morphism of topoi coming from a functor u : D' ⥤ C' to which Stacks 00X6 applies, with both C' and D' having all finite limits and subcanonical topologies, and with prescribed families of sheaves on C and on D becoming representable on C' and on D'.”.

Let (C, J) and (D, K) be sites and let f : Sh(C) → Sh(D) be a morphism of topoi. Then there are sites (C', J') and (D', K'), special cocontinuous functors v : C ⥤ C' and w : D ⥤ D', and a functor u : D' ⥤ C' such that

1. v and w exhibit (C, J) and (D, K) as dense subsites, so the morphisms of topoi g : Sh(C) → Sh(C') and e : Sh(D) → Sh(D') they induce are equivalences (Stacks 03A0);
2. J' and K' are subcanonical and C' and D' have all finite limits;
3. u is continuous, preserves all finite limits, is representably flat and defines a morphism of sites C' → D' — in other words Stacks 00X6 applies to u;
4. each g_*(F i) is a representable sheaf on C' and each e_*(G j) is a representable sheaf on D', for prescribed families of sheaves F on C and G on D; and
5. the square commutes: f_* ⋙ e_* is isomorphic to g_* ⋙ h_*, where h : Sh(C') → Sh(D') is the morphism of topoi attached to the morphism of sites u.

Conclusions (1)-(4) are the source's conclusions (1)-(4) and (5) is the commutativity of the square the source's remark is about.

theorem exists_twoSided_isDenseSubsite_representablyFlat {C : Type u} [SmallCategory C]
    {D : Type u} [SmallCategory D] {J : GrothendieckTopology C} {K : GrothendieckTopology D}
    (f : MorphismOfTopoi (Sheaf J (Type u)) (Sheaf K (Type u))) {ι : Type u}
    (F : ι → Sheaf J (Type u)) {κ : Type u} (G : κ → Sheaf K (Type u)) :
    ∃ (C' : Type u) (_ : SmallCategory C') (J' : GrothendieckTopology C') (D' : Type u)
      (_ : SmallCategory D') (K' : GrothendieckTopology D') (v : C ⥤ C') (w : D ⥤ D')
      (u : D' ⥤ C') (_ : v.IsDenseSubsite J J') (_ : w.IsDenseSubsite K K')
      (_ : HasFiniteLimits C') (_ : HasFiniteLimits D') (_ : J'.Subcanonical)
      (_ : K'.Subcanonical) (_ : u.IsContinuous K' J') (_ : PreservesFiniteLimits u)
      (_ : RepresentablyFlat u) (_ : u.IsMorphismOfSites K' J'),
      (∀ i, ((v.sheafPushforwardCocontinuous (Type u) J J').obj (F i)).obj.IsRepresentable) ∧
      (∀ j, ((w.sheafPushforwardCocontinuous (Type u) K K').obj (G j)).obj.IsRepresentable) ∧
      Nonempty
        (f.pushforward ⋙ w.sheafPushforwardCocontinuous (Type u) K K' ≅
          v.sheafPushforwardCocontinuous (Type u) J J' ⋙
            u.sheafPushforwardContinuous (Type u) K' J')

Sources

• Section 7.29, Tag 039Z
• AxiomMath/Stacks at 5ed82d14

LeangInv_isEquivalence · gStar_isEquivalence · IsSpecialCocontinuous · DenseSubsiteOverSheafEquivalence · CategoryTheory.GrothendieckTopology.exists_isDenseSubsite_subcanonical · CategoryTheory.GrothendieckTopology.exists_isDenseSubsite_subcanonical_hasFiniteLimits_representable · MorphismOfTopoi.exists_isDenseSubsite_isMorphismOfSites_pushforward_iso · MorphismOfTopoi.exists_twoSided_isDenseSubsite_representablyFlat

Section7.30 Localization of topoi#

Section 7.30 of the Stacks Project, Tag 04GY. 7 tags here are carried by 16 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 04GZ, a lemma

Tag 04GZ in the Stacks Project.

MorphismOfTopoi.overLocalization, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/ToposLocalization.lean, line 76. The attribute's comment: “the morphism of topoi j_F, and its inverse image”. References: SGA 4 IV (5.5), “Y = terminal object”; SGA 4 IV (5.2), “(5.2.1)”; SGA 4 IV (3.1.3), “special case”.

Stacks 04GZ. Let E be a topos and F an object of E. The localization morphism j_F : E/F ⟶ E is the morphism of topoi whose inverse image is j_F⁻¹ = toOver F, i.e. H ↦ (H × F ⟶ F), and whose pushforward j_{F,*} is a right adjoint of it.

def overLocalization (F : E) {p : Over F ⥤ E} (adj : toOver F ⊣ p) : MorphismOfTopoi (Over F) E

MorphismOfTopoi.overLocalization_inverseImage_obj, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/ToposLocalization.lean, line 89. The attribute's comment: “(1): the functor j_F^{-1} is H ↦ H × F / F”. References: SGA 4 IV (5.5), “Y terminal (f^* formula)”; SGA 4 IV (5.2), “b)”.

Stacks 04GZ (1). The inverse image of the localization morphism j_F is the functor H ↦ (H × F / F), the object of E/F given by the projection H × F ⟶ F.

lemma overLocalization_inverseImage_obj (F : E) {p : Over F ⥤ E} (adj : toOver F ⊣ p) (H : E) :
    (overLocalization F adj).inverseImage.obj H = Over.mk (snd H F)

MorphismOfTopoi.overLocalizationShriek, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/ToposLocalization.lean, line 98. The attribute's comment: “(2): the functor j_{F!} is the forgetful functor G/F ↦ G”. References: SGA 4 IV (5.5), “Y terminal (f_! ⊣ f^*)”; SGA 4 IV (5.2), “a)”.

Stacks 04GZ (2). The functor j_{F!} is the forgetful functor (G ⟶ F) ↦ G: it is left adjoint to j_F⁻¹, so that j_{F!} ⊣ j_F⁻¹ ⊣ j_{F,*} and j_F is a localization in the sense of Section 7.25 (tag 00XZ).

def overLocalizationShriek (F : E) {p : Over F ⥤ E} (adj : toOver F ⊣ p) :
    Over.forget F ⊣ (overLocalization F adj).inverseImage

Tag 04H0, a lemma

Tag 04H0 in the Stacks Project.

CategoryTheory.homPushforwardEquivRightInverse, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SliceTopos/OverHomEquiv.lean, line 93.

Stacks 04H0. Let E be a topos, F an object of E and j_{F,*} = p a pushforward for the localization j_F : E/F ⟶ E, i.e. a right adjoint of j_F⁻¹ = toOver F. For an object φ : G ⟶ F of E/F and any object A of E, the maps A ⟶ j_{F,*}(G/F) are in bijection with the morphisms α : F|_A ⟶ G|_A of E/A that are right inverse to φ|_A, restriction to A being (-)|_A = j_A⁻¹ = toOver A.

Taking A = h_U^# and using Γ(U, -) = Hom(h_U^#, -) this is Stacks 04H0: the sections of j_{F,*}(G/F) over U are the right inverses of φ|_U. The proof follows the Stacks one: the adjunction defining p identifies Hom(A, j_{F,*}(G/F)) with the fibre of φ ∘ (-) over the projection A ⊗ F ⟶ F, and interchanging the two factors turns that fibre into the set of right inverses of φ|_A.

Two things are not covered: the bijection is stated pointwise in A, its naturality in A (which is what makes the right-inverse description a description of the sheaf rather than of its individual section sets) being left implicit; and F|_A is read in the slice E/A, whereas Stacks reads it in Sh(C/U) via the equivalence Sh(C/U) ≃ Sh(C)/h_U^# of Stacks 00Y1, which is not yet available.

def homPushforwardEquivRightInverse [BraidedCategory E] {p : Over F ⥤ E} (adj : toOver F ⊣ p)
    (φ : G ⟶ F) (A : E) :
    (A ⟶ p.obj (Over.mk φ)) ≃
      { α : (toOver A).obj F ⟶ (toOver A).obj G // α ≫ (toOver A).map φ = 𝟙 _ }

Tag 0791, a lemma

Tag 0791 in the Stacks Project.

CategoryTheory.Presheaf.IsSheaf.app_fibers_inv_comp_unitInv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Topos/LocalizationOfTopoi.lean, line 881. The attribute's comment: “the fibre identification of j_!j^{-1}G is evaluation of the counit of j_!”.

Stacks 0791: the fibre identification of j_!j^{-1}G is evaluation of the shriek counit. Write E for the equivalence of sheafEquivalenceCostructuredArrowYoneda and T = E(j^{-1}G) for the object of Sh(C)/F whose source is j_!j^{-1}G. The equivalence identifies the fibre sheaf of T with j^{-1}G: on underlying presheaves the fibre sheaf of T is (U, s) ↦ {t ∈ T.left(U) | T.hom(t) = s} by the fibers field, and E.inverse (E T) ≅ T by the unit. This says that the identification sends a section t of j_!j^{-1}G over U lying in the fibre over s ∈ F(U) to its image under the counit of j_! ⊣ j^{-1}, a section of G over U.

This is the statement connecting the package's two descriptions of E. A comparison built from the fibre field — such as Stacks 04J4's identification of the inverse image of a relocalization with a base change — and one built from the counit of j_! — such as Stacks 04IE's identification of the inverse image of a localization with a product — are otherwise assertions about data that nothing relates, even though both come from the same E. Both sides here are morphisms out of the fibre presheaf of T, so comparing them needs no further transport.

theorem Presheaf.IsSheaf.app_fibers_inv_comp_unitInv {C : Type u} [Category.{v} C]
    {J : GrothendieckTopology C} {F : Cᵒᵖ ⥤ Type v} (hF : Presheaf.IsSheaf J F)
    [(CostructuredArrow.proj yoneda F).IsContinuous
      ((CostructuredArrow.proj yoneda F).restrictedTopology J) J]
    (G : Sheaf J (Type v)) (X : CostructuredArrow yoneda F)
    (p : OverArrows (hF.sheafEquivalenceCostructuredArrowYoneda.equivalence.functor.obj
        (((CostructuredArrow.proj yoneda F).sheafPushforwardContinuous (Type v)
          ((CostructuredArrow.proj yoneda F).restrictedTopology J) J).obj G)).hom.hom X.hom) :
    (hF.sheafEquivalenceCostructuredArrowYoneda.fibers.inv.app
          (hF.sheafEquivalenceCostructuredArrowYoneda.equivalence.functor.obj
            (((CostructuredArrow.proj yoneda F).sheafPushforwardContinuous (Type v)
              ((CostructuredArrow.proj yoneda F).restrictedTopology J) J).obj G)) ≫
        (hF.sheafEquivalenceCostructuredArrowYoneda.equivalence.unitInv.app
            (((CostructuredArrow.proj yoneda F).sheafPushforwardContinuous (Type v)
              ((CostructuredArrow.proj yoneda F).restrictedTopology J) J).obj G)).hom).app
        (op X) p =
      (hF.sheafEquivalenceCostructuredArrowYoneda.shriek.counit.app G).hom.app (op X.left)
        p.val

CategoryTheory.Presheaf.IsSheaf.app_fibers_inv_comp_homEquiv_shriek, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Topos/LocalizationOfTopoi.lean, line 916. The attribute's comment: “transposing across j_! ⊣ j^{-1} is evaluation on fibres”.

Stacks 0791: transposing across j_! ⊣ j^{-1} is evaluation on fibres. Let T be an object of Sh(C)/F and β : T.left ⟶ G a morphism of sheaves on C. Reading β as a morphism out of j_! of the fibre sheaf of T — which is what precomposing with the counit of the equivalence does — and transposing it across j_! ⊣ j^{-1} gives a morphism from the fibre sheaf of T to j^{-1}G. This says that that morphism sends a section t of T.left over U lying in the fibre over s ∈ F(U) to β(t).

This is the general form of app_fibers_inv_comp_unitInv, which is the case T = E(j^{-1}G), β the counit; it is what a comparison built from the fibers field has to be fed through in order to be compared with one built from the counit of j_!, since the underlying sheaf T.left of an object in the image of E has no description other than by its fibres. Everything in j_!'s adjunction cancels against the equivalence, so the content is exactly the fibre hom bijection of the source's proof.

theorem Presheaf.IsSheaf.app_fibers_inv_comp_homEquiv_shriek {C : Type u} [Category.{v} C]
    {J : GrothendieckTopology C} {F : Cᵒᵖ ⥤ Type v} (hF : Presheaf.IsSheaf J F)
    [(CostructuredArrow.proj yoneda F).IsContinuous
      ((CostructuredArrow.proj yoneda F).restrictedTopology J) J]
    (T : Over (⟨F, hF⟩ : Sheaf J (Type v))) (G : Sheaf J (Type v)) (β : T.left ⟶ G)
    (X : CostructuredArrow yoneda F) (p : OverArrows T.hom.hom X.hom) :
    (hF.sheafEquivalenceCostructuredArrowYoneda.fibers.inv.app T ≫
        (hF.sheafEquivalenceCostructuredArrowYoneda.shriek.homEquiv
            (hF.sheafEquivalenceCostructuredArrowYoneda.equivalence.inverse.obj T) G
            ((Over.forget (⟨F, hF⟩ : Sheaf J (Type v))).map
              (hF.sheafEquivalenceCostructuredArrowYoneda.equivalence.counit.app T) ≫
                β)).hom).app
        (op X) p =
      β.hom.app (op X.left) p.val

CategoryTheory.Presheaf.IsSheaf.exists_sheafEquivalence_costructuredArrow_yoneda, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Topos/LocalizationOfTopoi.lean, line 956. The attribute's comment: “Sheaves on the site C/F of pairs (U, s) with s ∈ F(U), whose coverings are those of C: C/F is a site, j is continuous and cocontinuous, the canonical equivalence PSh(C)/F ≌ PSh(C/F) matches sheaves with sheaves, and it restricts to an equivalence Sh(C/F) ≌ Sh(C)/F carrying j_! to Over.forget, i.e. turning j into j_F.”. References: SGA 4 III (5.2), “special case”.

Stacks 0791. Let (C, J) be a site and let F be a sheaf of sets on C. Let C/F = CostructuredArrow yoneda F be the category of pairs (U, s) with s ∈ F(U), with its projection j = CostructuredArrow.proj yoneda F to C, and declare a family {(U_i, s_i) ⟶ (U, s)} to be a covering when {U_i ⟶ U} is a covering of C, i.e. give C/F the topology j.restrictedTopology J generated by those families. Then:

1. C/F is a site with exactly those coverings: a sieve of (U, s) is covering for j.restrictedTopology J if and only if its image under j is a covering sieve of U;
2. the canonical equivalence Over F ≌ PSh(C/F) of overEquivPresheafCostructuredArrow matches sheaves with sheaves: for an object φ : G ⟶ F of PSh(C)/F, the presheaf (U, s) ↦ {t ∈ G(U) | φ(t) = s} on C/F is a sheaf if and only if G is a sheaf on C;
3. j is continuous and cocontinuous, so that it induces a morphism of topoi j : Sh(C/F) ⟶ Sh(C) with j^{-1} restriction (Stacks 00XR); and
4. there is an equivalence E : Sh(C/F) ≌ Sh(C)/F, namely the restriction of that canonical equivalence — E.inverse is (G, φ) ↦ ((U, s) ↦ {t ∈ G(U) | φ(t) = s}) on underlying presheaves — for which E.functor followed by Over.forget is left adjoint to j^{-1}, that is, is j_!. Since Over.forget is the j_{F!} of Stacks 04GZ, this is the assertion that E turns j into the localization morphism j_F.

public theorem Presheaf.IsSheaf.exists_sheafEquivalence_costructuredArrow_yoneda {C : Type u}
    [Category.{v} C] {J : GrothendieckTopology C} {F : Cᵒᵖ ⥤ Type v} (hF : Presheaf.IsSheaf J F) :
    (∀ (X : CostructuredArrow yoneda F) (S : Sieve X),
        S ∈ (CostructuredArrow.proj yoneda F).restrictedTopology J X ↔
          Sieve.functorPushforward (CostructuredArrow.proj yoneda F) S ∈ J X.left) ∧
      (∀ T : Over F,
        Presheaf.IsSheaf ((CostructuredArrow.proj yoneda F).restrictedTopology J)
            ((overEquivPresheafCostructuredArrow F).functor.obj T) ↔
          Presheaf.IsSheaf J T.left) ∧
      ∃ (_ :
        (CostructuredArrow.proj yoneda F).IsContinuous
          ((CostructuredArrow.proj yoneda F).restrictedTopology J) J)
        (_ :
        (CostructuredArrow.proj yoneda F).IsCocontinuous
          ((CostructuredArrow.proj yoneda F).restrictedTopology J) J)
        (E :
        Sheaf ((CostructuredArrow.proj yoneda F).restrictedTopology J) (Type v) ≌
          Over (⟨F, hF⟩ : Sheaf J (Type v))),
        Nonempty
            (E.inverse ⋙
                sheafToPresheaf ((CostructuredArrow.proj yoneda F).restrictedTopology J) (Type v) ≅
              Over.post (X := (⟨F, hF⟩ : Sheaf J (Type v))) (sheafToPresheaf J (Type v)) ⋙
                (overEquivPresheafCostructuredArrow F).functor) ∧
          Nonempty
            (E.functor ⋙ Over.forget (⟨F, hF⟩ : Sheaf J (Type v)) ⊣
              (CostructuredArrow.proj yoneda F).sheafPushforwardContinuous (Type v)
                ((CostructuredArrow.proj yoneda F).restrictedTopology J) J)

Tag 04IP, a definition

Tag 04IP in the Stacks Project.

toposLocalization, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SliceTopos/ToposLocalizationMorphism.lean, line 37. References: SGA 4 IV (5.1).

The localization of the topos of sheaves Sh(C, J) at a sheaf F is the slice (over) category Sh(C, J) / F. Objects are pairs (G, φ) where G is a sheaf on C and φ : G ⟶ F is a morphism of sheaves, and morphisms are commuting triangles over F.

abbrev toposLocalization (F : Sheaf J (Type (max u v)))

toposLocalizationMorphism, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SliceTopos/ToposLocalizationMorphism.lean, line 73. References: SGA 4 IV (5.2), “(5.2.1)”; SGA 3 I (1.6), “p_S clause: i_S ⊣ p_S”; SGA 4 IV (8.5).

The localization morphism j_F associated to the localization of the topos Sh(C, J) at the sheaf F (Stacks Project Tag 04IN).

We package the canonical Mathlib adjunction Over.forget F ⊣ Over.star F, which is the structural content of the morphism: - Over.forget F : Sh(C)/F ⥤ Sh(C) sends (G, φ : G ⟶ F) to G. This is the left adjoint (the "shriek" / étale-extension functor in the slice topos picture). - Over.star F : Sh(C) ⥤ Sh(C)/F sends G to the second projection (G × F, pr_F) : G × F ⟶ F. This is the right adjoint (the base-change / star functor).

The adjunction Over.forget F ⊣ Over.star F is exactly Over.forgetAdjStar in Mathlib, and it requires Sh(C, J) to have binary products.

noncomputable def toposLocalizationMorphism (F : Sheaf J (Type (max u v)))
    [Limits.HasBinaryProducts (Sheaf J (Type (max u v)))] :
    ToposAdjointPair (toposLocalization J F) (Sheaf J (Type (max u v)))

Tag 04IQ, a lemma

Tag 04IQ in the Stacks Project.

CategoryTheory.OverShriek.sheafFunctorToOverCompForgetIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/ToposComparison.lean, line 89. The attribute's comment: “j_{F!} = j_{U!} for F = h_U^#: the lower shrieks agree”.

Stacks 04IQ, on lower shrieks: j_{F!} ∘ Φ_U = j_{U!} for F = h_U^#.

The lower shriek of the localization morphism j_F of Stacks 04GZ is the forgetful functor Over.forget F (MorphismOfTopoi.overLocalizationShriek), so this says that the sheaf underlying Φ_U G is j_{U!}G.

def sheafFunctorToOverCompForgetIso :
    sheafFunctorToOver (U := U) J ⋙
        Over.forget ((presheafToSheaf J (Type v)).obj (yoneda.obj U)) ≅
      (Over.forget U).sheafPullback (Type v) (J.over U) J

CategoryTheory.OverShriek.overPullbackCompSheafFunctorToOverIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/ToposComparison.lean, line 109. The attribute's comment: “j_F^{-1} = j_U^{-1} for F = h_U^#: the inverse images agree”.

Stacks 04IQ, on inverse images: j_F^{-1} = j_U^{-1} for F = h_U^#, i.e. j_U^{-1} ⋙ Φ_U ≅ toOver F.

def overPullbackCompSheafFunctorToOverIso :
    J.overPullback (Type v) U ⋙ sheafFunctorToOver (U := U) J ≅
      toOver ((presheafToSheaf J (Type v)).obj (yoneda.obj U))

CategoryTheory.OverShriek.sheafFunctorToOverCompPushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/ToposComparison.lean, line 205. The attribute's comment: “j_{F,} = j_{U,} for F = h_U^#: the pushforwards agree”.

Stacks 04IQ, on pushforwards: j_{F,*} = j_{U,*} for F = h_U^#, i.e. Φ_U ⋙ j_{F,*} ≅ j_{U,*}.

Both pushforwards are taken as data, as in Stacks 04GZ, 04H0 and 04IR: p is a right adjoint of j_F^{-1} = toOver F and q a right adjoint of j_U^{-1}.

def sheafFunctorToOverCompPushforwardIso
    {p : Over ((presheafToSheaf J (Type v)).obj (yoneda.obj U)) ⥤ Sheaf J (Type v)}
    (adjp : toOver ((presheafToSheaf J (Type v)).obj (yoneda.obj U)) ⊣ p)
    {q : Sheaf (J.over U) (Type v) ⥤ Sheaf J (Type v)}
    (adjq : J.overPullback (Type v) U ⊣ q) :
    sheafFunctorToOver (U := U) J ⋙ p ≅ q

Tag 04IR, a lemma

Tag 04IR in the Stacks Project.

CategoryTheory.starIteratedSliceForwardIsoPullback, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SliceTopos/IteratedSlice.lean, line 58. The attribute's comment: “j = j_{G/F} and j^{-1}(H → F) = (H ×_F G → G)”. References: SGA 7 VII (2.0), “partial”.

Let s : G ⟶ F be a morphism of a topos E and write G/F for the corresponding object of the slice topos E/F. Localizing E/F at G/F produces the morphism of topoi whose inverse image is Over.star (Over.mk s); transporting it along the iterated slice equivalence (E/F)/(G/F) ≌ E/G identifies it with base change along s:

j⁻¹(H ⟶ F) = (H ×_F G ⟶ G).

Together with map_eq_forget_iteratedSlice (Stacks 03EH), which identifies the corresponding lower shriek with Over.map s, this is the assertion that j is the localization of E/F at G/F.

noncomputable def starIteratedSliceForwardIsoPullback [HasPullbacks E] :
    Over.star (Over.mk s) ⋙ (Over.mk s).iteratedSliceForward ≅ Over.pullback s

CategoryTheory.pushforwardIsoCompPushforward, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SliceTopos/IteratedSlice.lean, line 72. The attribute's comment: “j_{G,} = j_{F,} ∘ j_*”.

The pushforwards of the localizations satisfy j_{G,*} = j_{F,*} ∘ j_*.

The inverse images satisfy j_G⁻¹ = j⁻¹ ∘ j_F⁻¹, which is Over.starPullbackIsoStar; passing to right adjoints turns this into the stated identity between the pushforwards. The three pushforwards are given as data, since a general category with pullbacks and binary products need not have them (in a topos they exist, by Stacks 04GZ).

noncomputable def pushforwardIsoCompPushforward [HasPullbacks E] [HasBinaryProducts E]
    {pF : Over F ⥤ E} {pG : Over G ⥤ E} {p : Over G ⥤ Over F}
    (adjF : Over.star F ⊣ pF) (adjG : Over.star G ⊣ pG) (adj : Over.pullback s ⊣ p) :
    pG ≅ p ⋙ pF

Tag 04IS, a lemma

Tag 04IS in the Stacks Project.

CategoryTheory.OverShriek.relocalizeToposInverseImageIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/RelocalizeTopos.lean, line 80. The attribute's comment: “the inverse images of the two relocalizations agree, via 00Y1”.

Stacks 04IS, on inverse images. Under the identification of Stacks 00Y1, used in the forward direction Φ_U = sheafFunctorToOver J, the inverse image j^{-1} of the relocalization functor j = Over.map f of diagram (04IK) is the inverse image Over.star (h_V^#/h_U^#) ⋙ iteratedSliceForward of the localization of the topos Sh(C)/h_U^# at the object h_V^#/h_U^# of Stacks 04IR.

This is Stacks' proof: by Stacks 04IL the left-hand side is base change along h_f^#, and by Stacks 04IR so is the right-hand side.

def relocalizeToposInverseImageIso :
    (Over.map f).sheafPushforwardContinuous (Type v) (J.over V) (J.over U) ⋙
        sheafFunctorToOver (U := V) J ≅
      sheafFunctorToOver (U := U) J ⋙
        Over.star (Over.mk ((presheafToSheaf J (Type v)).map (yoneda.map f))) ⋙
          (Over.mk ((presheafToSheaf J (Type v)).map (yoneda.map f))).iteratedSliceForward

CategoryTheory.OverShriek.relocalizeToposShriekIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/RelocalizeTopos.lean, line 101. The attribute's comment: “the lower shrieks of the two relocalizations agree, via 00Y1”.

Stacks 04IS, on lower shrieks. Under the identification of Stacks 00Y1, used in the forward direction Φ_U = sheafFunctorToOver J, the lower shriek j_! of the relocalization functor j = Over.map f of diagram (04IK) is the lower shriek iteratedSliceBackward ⋙ Over.forget (h_V^#/h_U^#) of the localization of the topos Sh(C)/h_U^# at the object h_V^#/h_U^# of Stacks 04IR.

By Stacks 04IL the left-hand side is postcomposition with h_f^#, and by Over.iteratedSliceBackward_forget — the identity underlying Stacks 04IR's description of j_! — so is the right-hand side.

def relocalizeToposShriekIso :
    (Over.map f).sheafPullback (Type v) (J.over V) (J.over U) ⋙ sheafFunctorToOver (U := U) J ≅
      sheafFunctorToOver (U := V) J ⋙
        (Over.mk ((presheafToSheaf J (Type v)).map (yoneda.map f))).iteratedSliceBackward ⋙
          Over.forget (Over.mk ((presheafToSheaf J (Type v)).map (yoneda.map f)))

Sources

• Section 7.30, Tag 04GY
• AxiomMath/Stacks at 5ed82d14

LeanMorphismOfTopoi.overLocalization · MorphismOfTopoi.overLocalization_inverseImage_obj · MorphismOfTopoi.overLocalizationShriek · CategoryTheory.homPushforwardEquivRightInverse · CategoryTheory.Presheaf.IsSheaf.app_fibers_inv_comp_unitInv · CategoryTheory.Presheaf.IsSheaf.app_fibers_inv_comp_homEquiv_shriek · CategoryTheory.Presheaf.IsSheaf.exists_sheafEquivalence_costructuredArrow_yoneda · toposLocalization

Section7.31 Localization and morphisms of topoi#

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

Tag 04H1, a lemma

Tag 04H1 in the Stacks Project.

MorphismOfTopoi.over, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SliceTopos/OverPushforward.lean, line 61. The attribute's comment: “the morphism f' and the description of (f')⁻¹”. References: SGA 4 V (5.1).

Stacks 04H1. Let f : E ⟶ D be a morphism of topoi and G an object of D. Localizing E at F = f⁻¹G and D at G gives a morphism of topoi f' : E/F ⟶ D/G whose inverse image is Over.post f⁻¹, i.e.

(f')⁻¹(H ⟶ G) = (f⁻¹H ⟶ f⁻¹G) ,

which is the property characterizing f'. Its pushforward is (K ⟶ F) ↦ (f_*K ×_{f_*f⁻¹G} G ⟶ G), the right adjoint supplied by CategoryTheory.Over.postAdjunctionLeft, and its inverse image is left exact because f⁻¹ is.

noncomputable def over : MorphismOfTopoi (Over (f.inverseImage.obj G)) (Over G)

MorphismOfTopoi.inverseImageCompToOverIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SliceTopos/OverPushforward.lean, line 75. The attribute's comment: “commutativity of the square, on inverse images”.

Stacks 04H1, commutativity of the square on inverse images: j_F⁻¹ ∘ f⁻¹ = (f')⁻¹ ∘ j_G⁻¹, where j_G⁻¹ = toOver G and j_F⁻¹ = toOver (f⁻¹G). Concretely, f⁻¹ carries the product H ⊗ G over G to the product f⁻¹H ⊗ f⁻¹G over f⁻¹G; this is where the left exactness of f⁻¹ enters.

noncomputable def inverseImageCompToOverIso :
    f.inverseImage ⋙ toOver (f.inverseImage.obj G) ≅ toOver G ⋙ (f.over G).inverseImage

MorphismOfTopoi.toOverCompPushforwardIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SliceTopos/OverPushforward.lean, line 91. The attribute's comment: “f'_ j_F^{-1} = j_G^{-1} f_”.

Stacks 04H1: f'_* ∘ j_F⁻¹ = j_G⁻¹ ∘ f_*.

Both sides are right adjoints — of (f')⁻¹ ⋙ j_{F!} and of j_{G!} ⋙ f⁻¹ respectively — and those two left adjoints are equal on the nose by Over.post_forget_eq_forget_comp, so the identity follows from uniqueness of right adjoints.

noncomputable def toOverCompPushforwardIso :
    toOver (f.inverseImage.obj G) ⋙ (f.over G).pushforward ≅ f.pushforward ⋙ toOver G

Tag 04IU, a lemma

Tag 04IU in the Stacks Project.

CategoryTheory.SliceTopos.underlyingIso_hom_app_comp_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SliceTopos/LocalizationAndMorphismsOfTopoi.lean, line 435.

Stacks 04IU. Let u : C ⥤ D be a continuous functor between sites defining a morphism of sites, with induced morphism of topoi f : Sh(D) ⟶ Sh(C), let V be an object of C and put U = u V. Localizing the morphism of sites at V (Stacks 03CF) gives f' : Sh(D/U) ⟶ Sh(C/V) with (f')⁻¹ = u'_s for u' = Over.post u; localizing the morphism of topoi at the sheaf h_V^# (Stacks 04H1) gives f'' : Sh(D)/f⁻¹h_V^# ⟶ Sh(C)/h_V^# with (f'')⁻¹ = Over.post f⁻¹. Through the equivalences Φ_V, Φ_U of Stacks 00Y1 and the identification f⁻¹h_V^# ≅ h_U^# of Stacks 04D3 the two agree:

  (f')⁻¹ ⋙ Φ_U  ≅  Φ_V ⋙ (f'')⁻¹ ⋙ Over.map (04D3) .

Both sides become j_{U!}(f')⁻¹ ≅ f⁻¹j_{V!} after Over.forget h_U^#, canonically and for free, by underlyingIso; the content of the lemma, stated here, is that that canonical isomorphism respects the structure maps to h_U^#, the one on the right being computed with Stacks 04D3's identification. Feeding this equation to Over.natIsoOfForgetIso produces the displayed isomorphism of functors, hence the agreement of the diagram of Stacks 04H1 with the diagram of Stacks 03CF via the identifications j_F = j_U, j_G = j_V of Stacks 04IQ.

public theorem underlyingIso_hom_app_comp_hom {C : Type u} [SmallCategory C] {D : Type u}
    [SmallCategory D] {J : GrothendieckTopology C} {K : GrothendieckTopology D} {u : C ⥤ D}
    [u.IsContinuous J K]
    (hu : u.IsMorphismOfSites J K) (V : C) (H : Sheaf (J.over V) (Type u)) :
    (underlyingIso J K u V).hom.app H ≫
        ((sheafFunctorToOver (U := V) J ⋙
            (hu.morphismOfTopoi.over
                ((presheafToSheaf J (Type u)).obj (yoneda.obj V))).inverseImage ⋙
            Over.map (sheafPullbackSheafifyYonedaIso u J K V).hom).obj H).hom =
      (((Over.post (X := V) u).sheafPullback (Type u) (J.over V) (K.over (u.obj V)) ⋙
          sheafFunctorToOver (U := u.obj V) K).obj H).hom

Tag 04IV, a lemma

Tag 04IV in the Stacks Project.

relocalizeMorphismTopoiPullbackIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SliceTopos/RelocalizationPullback.lean, line 123.

Let F : D ⥤ C be a functor preserving the pullback of φ and b. Given φ : H ⟶ G, b : G' ⟶ G in D and a : Fbar' ⟶ Fbar, s : Fbar ⟶ F.obj G, s' : Fbar' ⟶ F.obj G' in C satisfying a ≫ s = s' ≫ F.map b, there is a canonical isomorphism (F.obj H ×_{F.obj G} Fbar) ×_{Fbar} Fbar' ≅ F.obj (H ×_G G') ×_{F.obj G'} Fbar'.

This is the formal pullback identity at the end of the proof, with the topos-theoretic inverse image f⁻¹ replaced by the generic pullback-preserving functor F.

noncomputable def relocalizeMorphismTopoiPullbackIso :
    pullback (pullback.snd (F.map φ) s) a ≅
      pullback (F.map (pullback.snd φ b)) s'

Tag 04IW, a lemma

Tag 04IW in the Stacks Project.

CategoryTheory.SliceTopos.isPullback_sheafFunctorToOver_overMap_overPost, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/SliceTopos/LocalizationAndMorphismsOfTopoi.lean, line 698.

Stacks 04IW. Let u : C ⥤ D be a continuous functor between sites defining a morphism of sites, with induced morphism of topoi f : Sh(D) ⟶ Sh(C), let V be an object of C, U an object of D and c : U ⟶ u V. Localizing the morphism of sites at c (Stacks 04IN) gives f_c : Sh(D/U) ⟶ Sh(C/V) with (f_c)⁻¹ = (Over.post u)_s ⋙ (Over.map c)^s; localizing the morphism of topoi at s : h_U^# ⟶ f⁻¹h_V^#, the morphism induced by c (Stacks 04IV), gives f_s : Sh(D)/h_U^# ⟶ Sh(C)/h_V^#, characterised by (f_s)⁻¹(H ⟶ h_V^#) = (f⁻¹H ×_{f⁻¹h_V^#, s} h_U^# ⟶ h_U^#).

Through the equivalences Φ_V, Φ_U of Stacks 00Y1 — the identifications j_G = j_V, j_F = j_U of Stacks 04IQ — the two agree: for every sheaf H on C/V the square

    Φ_U((f_c)⁻¹H) ---------> f⁻¹(j_{V!}H)
        |                          |
        |                          | f⁻¹(structure map)
        v                          v
      h_U^# ---------s---------> f⁻¹h_V^#

is cartesian, the top edge being the canonical comparison map assembled from Stacks 04IL (1) (Stacks 04IS), which identifies j_{U/u(V)}⁻¹ ⋙ Φ_U with Φ_{u(V)} ⋙ Over.pullback h_c^#, and underlyingIso (Stacks 04IU, Stacks 03CF), which identifies j_{u(V)!}(f')⁻¹H with f⁻¹j_{V!}H. Equivalently: Φ_U((f_c)⁻¹H) ≅ (f_s)⁻¹(Φ_V H) in Sh(D)/h_U^#, i.e. the diagram of topoi of Stacks 04IN agrees with the diagram of topoi of Stacks 04IV.

public theorem isPullback_sheafFunctorToOver_overMap_overPost {C : Type u} [SmallCategory C]
    {D : Type u} [SmallCategory D] {J : GrothendieckTopology C} {K : GrothendieckTopology D}
    {u : C ⥤ D} [u.IsContinuous J K] [HasFiniteLimits C] [PreservesFiniteLimits u]
    (V : C) {U : D} (c : U ⟶ u.obj V) (H : Sheaf (J.over V) (Type u)) :
    IsPullback
      (((inverseImageCompSheafFunctorToOverIso c K).hom.app
            (((Over.post (X := V) u).sheafPullback (Type u) (J.over V)
              (K.over (u.obj V))).obj H)).left ≫
          pullback.fst
              ((sheafFunctorToOver (U := u.obj V) K).obj
                (((Over.post (X := V) u).sheafPullback (Type u) (J.over V)
                  (K.over (u.obj V))).obj H)).hom
              ((presheafToSheaf K (Type u)).map (yoneda.map c)) ≫
            (underlyingIso J K u V).hom.app H)
      (((sheafFunctorToOver (U := U) K).obj
        (((Over.map c).sheafPushforwardContinuous (Type u) (K.over U) (K.over (u.obj V))).obj
          (((Over.post (X := V) u).sheafPullback (Type u) (J.over V)
            (K.over (u.obj V))).obj H))).hom)
      ((u.sheafPullback (Type u) J K).map ((sheafFunctorToOver (U := V) J).obj H).hom)
      ((presheafToSheaf K (Type u)).map (yoneda.map c) ≫
        (sheafPullbackSheafifyYonedaIso u J K V).inv)

Sources

• Section 7.31, Tag 04IT
• AxiomMath/Stacks at 5ed82d14

LeanMorphismOfTopoi.over · MorphismOfTopoi.inverseImageCompToOverIso · MorphismOfTopoi.toOverCompPushforwardIso · CategoryTheory.SliceTopos.underlyingIso_hom_app_comp_hom · relocalizeMorphismTopoiPullbackIso · CategoryTheory.SliceTopos.isPullback_sheafFunctorToOver_overMap_overPost

Section7.32 Points#

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

Tag 00Y4, a definition

Tag 00Y4 in the Stacks Project.

PointOfTopos, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/Defs.lean, line 27. References: SGA 4 IV (6.1).

A point of the topos Sh(C, J) is a morphism of topoi p : Sh(pt) → Sh(C, J), where Sh(pt) = Sets is modelled by Type w. Concretely, a point is an adjoint pair p⁻¹ ⊣ p_* with p⁻¹ : Sh(C, J) ⥤ Type w (the stalk functor) and p_* : Type w ⥤ Sh(C, J) (the skyscraper functor), such that p⁻¹ is left exact.

def PointOfTopos.{w, v, u} {C : Type u} [Category.{v} C] (J : GrothendieckTopology C) : Type _

Tag 04EH, an equation

Tag 04EH in the Stacks Project.

Declarations registered for the tag:

• CategoryTheory.GrothendieckTopology.Point.presheafFiber registered with add_to_stacks in StacksCore/CategoryTheory/Sites/Point/StalkAsColimit.lean, line 28 (StacksCore): “the stalk F_p = colim_{{(U, x)}ᵒᵖ} F(U) of a presheaf at a point of a site”. References: SGA 4 IV (6.8.7), “special case”; SGA 4 IV (6.10), “more general”; SGA 4 VIII (7.9.3).
• CategoryTheory.GrothendieckTopology.Point.toPresheafFiber registered with add_to_stacks in StacksCore/CategoryTheory/Sites/Point/StalkAsColimit.lean, line 30 (StacksCore): “the canonical map F(U) ⟶ F_p attached to a neighbourhood (U, x) of the point”.
• CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_w registered with add_to_stacks in StacksCore/CategoryTheory/Sites/Point/StalkAsColimit.lean, line 32 (StacksCore): “the canonical maps are compatible with morphisms of neighbourhoods”.

Tag 00Y5, a definition

Tag 00Y5 in the Stacks Project.

CategoryTheory.GrothendieckTopology.Point.fiber_jointly_surjective_of_ofArrows, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/Basic.lean, line 55. The attribute's comment: “(1)”.

Stacks 00Y5 (1) for Mathlib's notion of a point: for a covering family {U_i → U}_{i ∈ I} of a site C and a point Φ, the map ∐ u(U_i) → u(U) is surjective, i.e. every element of u(U) is the image of an element of some u(U_i).

Mathlib's Point.jointly_surjective field is stated for covering sieves, giving only some g : Y ⟶ U in the sieve; here the factorisation of g through one of the f i, which is what membership in Sieve.ofArrows means, is used to land in u(U_i).

theorem Point.fiber_jointly_surjective_of_ofArrows {I : Type*} {U : C} {Ui : I → C}
    (f : ∀ i, Ui i ⟶ U) (hf : Sieve.ofArrows Ui f ∈ J U) (x : Φ.fiber.obj U) :
    ∃ (i : I) (y : Φ.fiber.obj (Ui i)), Φ.fiber.map (f i) y = x

CategoryTheory.GrothendieckTopology.Point.fiber_pullbackComparison_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/Basic.lean, line 70. The attribute's comment: “(2)”.

Stacks 00Y5 (2) for Mathlib's notion of a point: the fiber functor turns fibre products into fibre products, i.e. the comparison map u(X ×_Z Y) → u(X) ×_{u(Z)} u(Y) is bijective.

Stacks assumes this for the members of a covering; Mathlib derives it — from cofilteredness of the category of elements of u — for every pair of morphisms with common target, which is the stronger statement proved here.

theorem Point.fiber_pullbackComparison_bijective [LocallySmall.{w} C]
    {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] :
    Function.Bijective (pullbackComparison Φ.fiber f g)

CategoryTheory.GrothendieckTopology.Point.sheafFiber_leftExact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/Basic.lean, line 81. The attribute's comment: “(3)”.

Stacks 00Y5 (3) for Mathlib's notion of a point: the stalk functor Sh(C) ⥤ Set, F ↦ F_p, is left exact.

Point.sheafFiber is Mathlib's stalk functor, sheafToPresheaf J _ ⋙ Φ.presheafFiber, the filtered colimit of the sections of F over the category of elements of u.

theorem Point.sheafFiber_leftExact [LocallySmall.{w} C] :
    PreservesFiniteLimits (Φ.sheafFiber (A := Type w))

Declarations registered for the tag:

• CategoryTheory.GrothendieckTopology.Point registered with add_to_stacks in StacksFrontier/CategoryTheory/Sites/Point/Basic.lean, line 39 (StacksFrontier): “Mathlib's definition of a point of a site: the fiber functor u : C ⥤ Type w together with the conditions making it a point. Mathlib assumes joint surjectivity on covering sieves (Stacks axiom (1)) and cofilteredness of the category of elements of the fiber, from which Stacks axioms (2) and (3) — exactness of the fiber and of the stalk functor on sheaves — follow rather than being assumed; see Point.fiber_jointly_surjective_of_ofArrows, Point.fiber_pullbackComparison_bijective and Point.sheafFiber_leftExact below.”. References: SGA 4 IV (6.3).

Tag 00Y6, a lemma

Tag 00Y6 in the Stacks Project.

Phi_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/StalkFunctor.lean, line 44. The attribute's comment: “isomorphism”.

Stacks 00Y6. The canonical map Φ_U : p U ⟶ (h_U)_p from the value of the point at U to the stalk of the representable presheaf h_U is bijective.

theorem Phi_bijective (p : C ⥤ Type u) (U : C) :
    Function.Bijective (theta p U)

Phi_naturality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/StalkFunctor.lean, line 52. The attribute's comment: “functoriality”.

Stacks 00Y6. The maps Φ_U are natural in U: they commute with p.map g on the source and with the stalk of yoneda.map g on the target.

theorem Phi_naturality (p : C ⥤ Type u) {U U' : C} (g : U ⟶ U') (x : p.obj U) :
    theta p U' (p.map g x) = (presheafStalk p).map (yoneda.map g) (theta p U x)

Tag 04EI, an equation

Tag 04EI in the Stacks Project.

pushforwardPresheaf04EI, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/PresheafPushforwardPoint.lean, line 27. References: SGA 4 I (1.3), “special case”.

Stacks 04EI. The presheaf u^p E attached to a functor u : C ⥤ Type and a type E: it sends an object U to the type of functions u U → E, and a morphism f : V ⟶ U to precomposition with u f.

def pushforwardPresheaf04EI {C : Type u} [Category.{v} C] (u : Functor C (Type v)) (E : Type v) :
    Functor Cᵒᵖ (Type v)

Tag 00Y7, a lemma

Tag 00Y7 in the Stacks Project.

PresheafPushforwardStalkAdjunction.presheafStalk_adjoint_presheafPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/StalkLeftAdjoint.lean, line 297.

Stacks 00Y7. For any functor u : C ⥤ Type w such that the appropriate colimits exist, the pushforward functor presheafPushforward u is a right adjoint to the stalk functor presheafStalk u.

theorem presheafStalk_adjoint_presheafPushforward
    (u : C ⥤ Type w)
    [HasColimitsOfShape u.Elementsᵒᵖ (Type w)] :
    Nonempty (presheafStalk u ⊣ presheafPushforward u)

Tag 00Y8, a lemma

Tag 00Y8 in the Stacks Project.

main_theorem00Y8, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/StalkExact.lean, line 43.

Stacks 00Y8, statement (3), narrow form.

Let C be a small category equipped with a Grothendieck topology J, let L : (Cᵒᵖ ⥤ Type v) ⥤ Type v be the "stalk-at-a-point" functor on presheaves, and let R : Type v ⥤ (Cᵒᵖ ⥤ Type v) be the "point-pushforward" functor. Assume:

• L ⊣ R (this packages tag 00Y8 statement (2) at the presheaf level: the stalk functor is left adjoint to the point-pushforward functor), and
• for every set E, the presheaf R.obj E is a sheaf for J (this is tag 00Y8 statement (1): u^p E is a sheaf).

Then for every presheaf F and every set E, precomposition by L.map (toSheafify J F) is a bijection (L.obj (sheafify J F) ⟶ E) → (L.obj F ⟶ E). By Yoneda this is the abstract content of tag 00Y8 statement (3): the canonical map F_p → (F^#)_p from the stalk of a presheaf to the stalk of its sheafification is an isomorphism in Type v.

theorem main_theorem00Y8
    {C : Type u} [SmallCategory C] (J : GrothendieckTopology C)
    [HasWeakSheafify J (Type v)]
    (L : (Cᵒᵖ ⥤ Type v) ⥤ Type v) (R : Type v ⥤ Cᵒᵖ ⥤ Type v)
    (adj : L ⊣ R)
    (hR : ∀ E : Type v, Presheaf.IsSheaf J (R.obj E))
    (F : Cᵒᵖ ⥤ Type v) (E : Type v) :
    Function.Bijective
      (fun g : L.obj (sheafify J F) ⟶ E => L.map (toSheafify J F) ≫ g)

Tag 00Y9, a definition

Tag 00Y9 in the Stacks Project.

pushforwardPoint, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/PushforwardPoint.lean, line 27. References: EGA IV (21.9.1), “more general”.

Stacks 00Y9. The pushforward p_* E of an object E along a point p of the site (C, J): the skyscraper sheaf at p with value E.

noncomputable def pushforwardPoint
    {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
    (p : J.Point) {A : Type*} [Category A] [Limits.HasProducts A] (E : A) :
    Sheaf J A

Tag 00YA, a lemma

Tag 00YA in the Stacks Project.

AlgebraicGeometry.RingedToposHom.targetSitePoint, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/AlgebraicGeometry/EtaleCohomology/RecoveringMorphisms/TargetSitePoint.lean, line 107. The attribute's comment: “(2), applied to the composite of a point of the source site with a morphism of ringed topoi”.

Stacks 00YA (2) along a morphism of ringed topoi. The point of the target site (D, K) whose stalk functor is the inverse image along f followed by the stalk functor of the point Φ of the source site.

def targetSitePoint (f : RingedToposHom X Y) (Φ : X.J.Point.{w}) : Y.J.Point.{w}

CategoryTheory.GrothendieckTopology.Point.pointOfTopos, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/Topos.lean, line 294. The attribute's comment: “(1): a point of the site defines a morphism of topoi Sh(pt) → Sh(C)”. References: SGA 4 IV (6.8.7), “(ii)”; SGA 4 IV (7.1), “more general”.

Stacks 00YA (1). Let p be a point of the site C, given by a fibre functor u = Φ.fiber. Then the pair of functors (p\_*, p^\{-1}) = (Φ.skyscraperSheafFunctor, Φ.sheafFiber) is a morphism of topoi Sh(pt) → Sh(C), i.e. a point of the topos Sh(C) in the sense of Stacks 00Y4.

The two functors are adjoint by Point.skyscraperSheafAdjunction, and p^{-1} is left exact by Point.sheafFiber_leftExact (Stacks 00Y5 (3)), which are exactly the two conditions in the definition of a morphism of topoi (Stacks 00XA).

noncomputable def pointOfTopos (Φ : Point.{w} J) : PointOfTopos.{w, v, u} J

CategoryTheory.GrothendieckTopology.Point.sheafFiberComparison, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/Topos.lean, line 372. The attribute's comment: “(2): the canonical comparison from the reconstructed stalk functor”.

The canonical comparison from the stalk functor to F, induced by a natural transformation on the sheafified representables. On a germ (U, x, σ) it is F(σ)(α_U(x)), viewing the section σ as a map out of h_U^#.

noncomputable def sheafFiberComparison : Φ.sheafFiber ⟶ F

PointOfTopos.exists_sitePoint_fiber_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/Topos.lean, line 523. The attribute's comment: “(2): reconstruction of the site point”.

Stacks 00YA (2). Every point p of the topos arises from a point of the site whose fiber functor is U ↦ p⁻¹(h_U^#) on the nose.

PointOfTopos.exists_sitePoint is the same reconstruction stated up to isomorphism of stalk functors; this form is the one consumers need when they have to transport along the identity of fibre functors with eqToIso.

theorem exists_sitePoint_fiber_eq {C : Type u} [Category.{v} C] {J : GrothendieckTopology C}
    (p : PointOfTopos.{max u v, v, u} J) :
    ∃ Φ : GrothendieckTopology.Point.{max u v} J,
      Φ.fiber = Sheaf.sheafifiedYoneda J ⋙ p.inverseImage

PointOfTopos.isIso_sheafFiberComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/Topos.lean, line 602. The attribute's comment: “(2): the canonical inverse-image comparison is an isomorphism”.

Stacks 00YA (2). The canonical comparison identifies the reconstructed stalk functor with p.inverseImage.

theorem isIso_sheafFiberComparison :
    IsIso (Φ.sheafFiberComparison p.inverseImage e.hom)

PointOfTopos.isIso_conjugate_sheafFiberComparison, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/Topos.lean, line 635. The attribute's comment: “(2): recovery of the pushforward by the adjoint mate”.

Stacks 00YA (2). The adjoint mate of the canonical comparison is an isomorphism p.pushforward ⟶ Φ.skyscraperSheafFunctor, recovering the pushforward compatibly with the given adjunctions.

theorem isIso_conjugate_sheafFiberComparison :
    IsIso (conjugateEquiv p.adj Φ.skyscraperSheafAdjunction
      (Φ.sheafFiberComparison p.inverseImage e.hom))

Tag 04EL, a lemma

Tag 04EL in the Stacks Project.

CategoryTheory.GrothendieckTopology.Point.exists_equivalence_isMorphismOfSites_pushforward_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/Points.lean, line 586.

Stacks 04EL. Let Φ be a point of a locally w-small site (C, J), with fibre functor u = Φ.fiber. Let ι : S ⥤ Type w be a full subcategory of the category of sets in which some object pt is a singleton, let K be the topology on S whose covering sieves are the jointly surjective ones, and suppose the fibre functor factors as u ⋙ ι for some u : C ⥤ S. Then

1. there is an equivalence i : Sh(pt) → Sh(S, K) whose inverse image is F ↦ F(pt), hence whose forward functor sends a set E to the sheaf V ↦ Mor(ι V, E);
2. u : C ⥤ S defines a morphism of sites f : (S, K) → (C, J); and
3. the composition Sh(pt) → Sh(S, K) → Sh(C, J) is the morphism of topoi (p_*, p⁻¹) of the point, in the sense that i_* ⋙ f_* is isomorphic to the skyscraper sheaf functor p_*.

public theorem exists_equivalence_isMorphismOfSites_pushforward_iso {C : Type u} [Category.{v} C]
    {J : GrothendieckTopology C} [LocallySmall.{w} C] (Φ : Point.{w} J) {S : Type w}
    [SmallCategory S] (ι : S ⥤ Type w) [ι.Full] [ι.Faithful] (pt : S) (hpt : Unique (ι.obj pt))
    (K : GrothendieckTopology S)
    (hK :
      ∀ (V : S) (R : Sieve V),
        R ∈ K V ↔ ∀ x : ι.obj V, ∃ (W : S) (f : W ⟶ V) (y : ι.obj W), R.arrows f ∧ ι.map f y = x)
    (u : C ⥤ S) (hu : u ⋙ ι ≅ Φ.fiber) :
    ∃ (e : Type w ≌ Sheaf K (Type w)) (_ : _root_.IsMorphismOfSites.{w} u J K),
      e.inverse = sheafToPresheaf K (Type w) ⋙ (evaluation Sᵒᵖ (Type w)).obj (Opposite.op pt) ∧
        Nonempty
          (e.functor ⋙ u.sheafPushforwardContinuous (Type w) J K ≅
            Φ.skyscraperSheafFunctor (A := Type w))

Tag 05UX, a lemma

Tag 05UX in the Stacks Project.

ToposPoint.epsilon_comp_eta, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/Skyscraper.lean, line 94.

Stacks 05UX. For any set E there are canonical maps E ⟶ (p_* E)_p ⟶ E whose composition is the identity of E.

Proof: apply naturality of the counit ε of p⁻¹ ⊣ p_* to the constant map i_e : PUnit → E, then evaluate at default : p⁻¹(p_*(PUnit)).

theorem epsilon_comp_eta (E : Type v) : p.epsilon E ∘ p.eta E = id

Tag 05UY, a lemma

Tag 05UY in the Stacks Project.

PointOfTopos.preservesLimitsOfSize_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/Topos.lean, line 216. The attribute's comment: “commutes with arbitrary limits”.

Stacks 05UY. The pushforward p_* of a point of a topos commutes with arbitrary limits, because it is a right adjoint.

theorem preservesLimitsOfSize_pushforward : PreservesLimitsOfSize.{w₁, w₂} p.pushforward

PointOfTopos.preservesFiniteLimits_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/Topos.lean, line 221. The attribute's comment: “is left exact”. References: SGA 4 IV (3.1.2), “point; finite limits”.

Stacks 05UY. The pushforward p_* of a point of a topos is left exact.

theorem preservesFiniteLimits_pushforward : PreservesFiniteLimits p.pushforward

PointOfTopos.faithful_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/Topos.lean, line 228. The attribute's comment: “is faithful”.

Stacks 05UY. The pushforward p_* of a point of a topos is faithful: the counit ε_E : p^{-1}p_*E → E is a (split) epimorphism, and ε is natural.

theorem faithful_pushforward : p.pushforward.Faithful

PointOfTopos.preservesEpimorphisms_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/Topos.lean, line 241. The attribute's comment: “transforms surjections into surjections. The other claim of the same sentence of the source — that p_* commutes with coequalizers — is FALSE and is not claimed anywhere in this file; see Point.subsingleton_fiber_of_preservesCoequalizers”.

Stacks 05UY. The pushforward p_* of a point of a topos transforms surjections into surjections: every epimorphism of sets is a split epimorphism, and a split epimorphism is carried to a split epimorphism by any functor.

theorem preservesEpimorphisms_pushforward : p.pushforward.PreservesEpimorphisms

PointOfTopos.reflectsMonomorphisms_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/Topos.lean, line 248. The attribute's comment: “reflects injections”.

Stacks 05UY. The pushforward p_* of a point of a topos reflects injections.

theorem reflectsMonomorphisms_pushforward : p.pushforward.ReflectsMonomorphisms

PointOfTopos.reflectsEpimorphisms_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/Topos.lean, line 254. The attribute's comment: “reflects surjections”.

Stacks 05UY. The pushforward p_* of a point of a topos reflects surjections.

theorem reflectsEpimorphisms_pushforward : p.pushforward.ReflectsEpimorphisms

PointOfTopos.reflectsIsomorphisms_pushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/Topos.lean, line 266. The attribute's comment: “reflects isomorphisms”.

Stacks 05UY. The pushforward p_* of a point of a topos reflects isomorphisms: it reflects both injections and surjections, and a map of sets which is both injective and surjective is bijective.

theorem reflectsIsomorphisms_pushforward : p.pushforward.ReflectsIsomorphisms

Sources

• Section 7.32, Tag 00Y3
• AxiomMath/Stacks at 5ed82d14

LeanPointOfTopos · CategoryTheory.GrothendieckTopology.Point.presheafFiber · CategoryTheory.GrothendieckTopology.Point.toPresheafFiber · CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_w · CategoryTheory.GrothendieckTopology.Point.fiber_jointly_surjective_of_ofArrows · CategoryTheory.GrothendieckTopology.Point.fiber_pullbackComparison_bijective · CategoryTheory.GrothendieckTopology.Point.sheafFiber_leftExact · CategoryTheory.GrothendieckTopology.Point

Section7.33 Constructing points#

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

Tag 0F4E, a lemma

Tag 0F4E in the Stacks Project.

preservesFiniteLimits_sheafFiber, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/StalkIso.lean, line 27.

Stacks 0F4E. Let Φ be a point of the site (C, J), i.e. a functor u : C ⥤ Type together with cofilteredness of its category of neighbourhoods. Then the stalk functor Sh(C) ⥤ Set at Φ is left exact, i.e. it preserves finite limits.

theorem preservesFiniteLimits_sheafFiber
    {C : Type u} [SmallCategory C] {J : GrothendieckTopology C}
    (Φ : J.Point) :
    Limits.PreservesFiniteLimits (Φ.sheafFiber (A := Type u))

Tag 00YB, a lemma

Tag 00YB in the Stacks Project.

StacksStalk.nbh_isCofiltered, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/NeighbourhoodsCofiltered.lean, line 70. The attribute's comment: “(1)”. References: SGA 4 IV (6.8.2), “special case”; SGA 4 IV (6.8.5), “partial”.

Statement 1 (Main, tag 00YB): under the hypotheses, the category of neighbourhoods Nbh(p) of p is cofiltered.

theorem nbh_isCofiltered [HasTerminal C] [HasPullbacks C]
    (u : C ⥤ Type w) (hu : IsPoint u) : IsCofiltered u.Elements

StacksStalk.sheafStalkFunctor_preservesFiniteLimits, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/NeighbourhoodsCofiltered.lean, line 106. The attribute's comment: “(2)”.

Statement 2 (Consequence, tag 00YB): under the hypotheses, the stalk functor on sheaves commutes with finite limits, i.e. it is left exact.

theorem sheafStalkFunctor_preservesFiniteLimits
    [HasTerminal C] [HasPullbacks C] (J : GrothendieckTopology C)
    (u : C ⥤ Type w) (hu : IsPoint u) :
    PreservesFiniteLimits
      (sheafToPresheaf J (Type w) ⋙ CategoryTheory.elementColimit u (Type w))

Tag 00YC, a proposition

Tag 00YC in the Stacks Project.

CategoryTheory.GrothendieckTopology.Point.ofPreservesFiniteLimits, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/OfPreservesFiniteLimits.lean, line 104. References: SGA 4 IV (6.3), “left exact ⇒ point”.

On a site in which finite limits exist, the point with fiber functor u : C ⥤ Type w, for u commuting with finite limits, with initially small category of elements, and jointly surjective on covering sieves.

def ofPreservesFiniteLimits (u : C ⥤ Type w) [PreservesFiniteLimits u]
    [InitiallySmall.{w} u.Elements] (hu : u.CoveringJointlySurjective J) :
    Point.{w} J

CategoryTheory.GrothendieckTopology.Point.equivFiber, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/OfPreservesFiniteLimits.lean, line 124. References: SGA 4 IV (6.3), “characterization”.

Let C be a site in which finite limits exist. Then the points of C correspond bijectively to the functors u : C ⥤ Type w such that

1. u commutes with finite limits, and
2. ∐ u(U_i) → u(U) is surjective for every covering {U_i → U} (in the sieve form Functor.CoveringJointlySurjective), and whose category of elements is initially small,

the bijection being Φ ↦ Φ.fiber in one direction and ofPreservesFiniteLimits in the other.

noncomputable def equivFiber :
    Point.{w} J ≃ {u : C ⥤ Type w //
      InitiallySmall.{w} u.Elements ∧ PreservesFiniteLimits u ∧
        u.CoveringJointlySurjective J}

Tag 00YD, a remark

Tag 00YD in the Stacks Project.

Counterexample.u_not_point, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/NonExactStalkCounterexample.lean, line 534.

Statement 3. Because the stalk functor ℱ ↦ ℱ_p fails to preserve monomorphisms (Statement 2), it fails to be left exact.

theorem u_not_point : ¬ PreservesFiniteLimits stalkFunctor

Sources

• Section 7.33, Tag 05UZ
• AxiomMath/Stacks at 5ed82d14

LeanpreservesFiniteLimits_sheafFiber · StacksStalk.nbh_isCofiltered · StacksStalk.sheafStalkFunctor_preservesFiniteLimits · CategoryTheory.GrothendieckTopology.Point.ofPreservesFiniteLimits · CategoryTheory.GrothendieckTopology.Point.equivFiber · Counterexample.u_not_point

Section7.34 Points and morphisms of topoi#

Section 7.34 of the Stacks Project, Tag 05V0. 3 tags here are carried by 10 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0F4F, a lemma

Tag 0F4F in the Stacks Project.

CategoryTheory.Stalk.presheafPushforward_stalk_iso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/StalkPresheafPushforward.lean, line 73.

Stacks 0F4F, packaged as the existence of the natural isomorphism (u_p F)_v ≅ F_{v ∘ u}.

theorem presheafPushforward_stalk_iso (u : C ⥤ D) (v : D ⥤ Type u) :
    Nonempty (u.op.lan ⋙ presheafStalk v ≅ presheafStalk (u ⋙ v))

Tag 05V1, a lemma

Tag 05V1 in the Stacks Project.

Stacks.Sheaves.StalkInverseImage.stalkAddEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/StalkInverseImageModules.lean, line 496. The attribute's comment: “for sheaves of modules, at a point of a site, for a morphism of topoi whose stalk functor at the target point is the inverse image followed by the stalk functor at the source point”.

The stalk at Φ of the inverse image along g of a sheaf of O-modules is the stalk of that sheaf at Ψ, as an isomorphism of additive groups. It is semilinear over Stacks.Sheaves.StalkInverseImage.stalkRingEquiv; see Stacks.Sheaves.StalkInverseImage.stalkAddEquiv_smul.

def stalkAddEquiv :
    (Stacks.sheafModuleFiber Ψ O).obj G ≃+
      (Stacks.sheafModuleFiber Φ (inverseImageRingSheaf g O)).obj
        ((inverseImageModules g O).obj G)

Stacks.Sheaves.StalkInverseImage.stalkAddEquiv_smul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/StalkInverseImageModules.lean, line 526. The attribute's comment: “semilinearity of the comparison, for sheaves of modules”.

The isomorphism of stalk modules is semilinear over the isomorphism of stalk rings: the stalk at Φ of the inverse image of G is the stalk of G at Ψ, with the scalars carried along O_Ψ ≅ (g⁻¹O)_Φ.

theorem stalkAddEquiv_smul (r : (Ψ.presheafFiber (A := RingCat.{w})).obj O.obj)
    (m : (Stacks.sheafModuleFiber Ψ O).obj G) :
    stalkAddEquiv g O Φ Ψ e G (r • m) =
      stalkRingEquiv g O Φ Ψ e r • stalkAddEquiv g O Φ Ψ e G m

Stacks.Sheaves.StalkInverseImage.stalkNatIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Algebra/Category/ModuleCat/Sheaf/StalkInverseImageModules.lean, line 600. The attribute's comment: “for sheaves of modules, as a natural isomorphism of stalk functors”.

The stalk functor at Ψ is the inverse image of sheaves of modules followed by the stalk functor at Φ and restriction of scalars along the isomorphism of stalk rings.

def stalkNatIso :
    Stacks.sheafModuleFiber Ψ O ≅
      inverseImageModules g O ⋙ Stacks.sheafModuleFiber Φ (inverseImageRingSheaf g O) ⋙
        ModuleCat.restrictScalars (stalkRingEquiv g O Φ Ψ e).toRingHom

Stacks.Sheaves.DerivedPullback.KFlatPullbackMorphismOfSites.targetStalkAddEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPullback/StalkOfInverseImageAtTheTargetPoint.lean, line 106. The attribute's comment: “for sheaves of modules, at the point of the target site attached to a point of the source site by part (2) of Stacks 00YA”.

Module-level Stacks 05V1 at the named point of the target site. The stalk at Φ of the inverse image of a sheaf of O'-modules is the stalk of that sheaf at Ψ, as an isomorphism of additive groups; it is semilinear over targetStalkRingEquiv.

def targetStalkAddEquiv :
    (Stacks.sheafModuleFiber (targetPoint f hu Φ)
        (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)).obj G ≃+
      (Stacks.sheafModuleFiber Φ
          (inverseImageRingSheaf (f.toToposHom hu)
            (Stacks.SheafOfModules.Tensor.ringSheaf Y.O))).obj
        ((inverseImageModules (f.toToposHom hu)
          (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)).obj G)

Stacks.Sheaves.DerivedPullback.KFlatPullbackMorphismOfSites.targetStalkAddEquiv_smul, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPullback/StalkOfInverseImageAtTheTargetPoint.lean, line 122. The attribute's comment: “semilinearity, at the point of the target site attached to a point of the source site”.

Stacks 05V1 for sheaves of modules at the named point. The isomorphism of stalk modules is semilinear over the isomorphism of stalk rings.

theorem targetStalkAddEquiv_smul
    (r : ((targetPoint f hu Φ).presheafFiber (A := RingCat.{u})).obj
      (Stacks.SheafOfModules.Tensor.ringSheaf Y.O).obj)
    (m : (Stacks.sheafModuleFiber (targetPoint f hu Φ)
      (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)).obj G) :
    targetStalkAddEquiv f hu Φ G (r • m) =
      targetStalkRingEquiv f hu Φ r • targetStalkAddEquiv f hu Φ G m

Stacks.Sheaves.DerivedPullback.KFlatPullbackMorphismOfSites.targetStalkNatIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cohomology/DerivedPullback/StalkOfInverseImageAtTheTargetPoint.lean, line 162. The attribute's comment: “for sheaves of modules, as a natural isomorphism of stalk functors, at the point of the target site attached to a point of the source site”.

Module-level Stacks 05V1 at the named point, as a natural isomorphism of stalk functors. The stalk functor at Ψ is the inverse image of sheaves of modules followed by the stalk functor at Φ and restriction of scalars along the isomorphism of stalk rings.

This is the form a statement about complexes consumes: CategoryTheory.NatIso.mapHomologicalComplex carries it to an isomorphism of the degreewise functors on cochain complexes.

def targetStalkNatIso :
    Stacks.sheafModuleFiber (targetPoint f hu Φ) (Stacks.SheafOfModules.Tensor.ringSheaf Y.O) ≅
      inverseImageModules (f.toToposHom hu) (Stacks.SheafOfModules.Tensor.ringSheaf Y.O) ⋙
        Stacks.sheafModuleFiber Φ
            (inverseImageRingSheaf (f.toToposHom hu) (Stacks.SheafOfModules.Tensor.ringSheaf Y.O)) ⋙
          ModuleCat.restrictScalars (targetStalkRingEquiv f hu Φ).toRingHom

point_morphism_sites, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/StalkAlongMorphism.lean, line 47.

Stacks 05V1. For a point q of (D, K) and a morphism of sites given by u : C ⥤ D, the stalk functor at the induced point q.comap u hu of (C, J) is isomorphic to taking the inverse image along u and then the stalk at q.

theorem point_morphism_sites
    {C : Type u₁} [Category.{v} C] {D : Type u₂} [Category.{v} D]
    {J : GrothendieckTopology C} {K : GrothendieckTopology D}
    (u : C ⥤ D) [RepresentablyFlat u] [u.IsContinuous J K]
    (hu : CoverPreserving J K u)
    (q : Point.{w} K)
    [InitiallySmall (u ⋙ q.fiber).Elements]
    (A : Type*) [Category.{v} A] [HasProducts.{w} A]
    [(u.sheafPushforwardContinuous A J K).IsRightAdjoint]
    [HasColimitsOfSize.{w, w} A] :
    Nonempty ((q.comap u hu).sheafFiber (A := A) ≅ u.sheafPullback A J K ⋙ q.sheafFiber)

Tag 05V2, a lemma

Tag 05V2 in the Stacks Project.

CategoryTheory.GrothendieckTopology.Point.sheafFiber_inverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/DenseSubsite/NatIsoTransport.lean, line 116. The attribute's comment: “at a point of the site”.

[Stacks Project, Tag 05V2] at a point of the site. For a morphism of topoi f from Sh(C, J) to Sh(D, K) and a point Φ of the site (C, J), the fibre at Φ of the inverse image of a sheaf ℱ on (D, K) is the stalk of ℱ at the composed point of Sh(D, K).

No bridge between the two notions of point has to be built: a point of a site already is a point of its topos, by CategoryTheory.GrothendieckTopology.Point.pointOfTopos (Stacks 00YA (1)), whose inverse image is the fibre functor on the nose (CategoryTheory.GrothendieckTopology.Point.pointOfTopos_inverseImage). So MorphismOfTopoi.stalk_inverseImage applies verbatim, and this statement is it.

theorem sheafFiber_inverseImage {D : Type u'} [Category.{v'} D] {K : GrothendieckTopology D}
    (f : MorphismOfTopoi (Sheaf J (Type w)) (Sheaf K (Type w))) (F : Sheaf K (Type w)) :
    Φ.sheafFiber.obj (f.inverseImage.obj F) = (f.compPoint Φ.pointOfTopos).stalk F

MorphismOfTopoi.stalk_inverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/ToposPoints.lean, line 47.

For a morphism of topoi f : Sh(D) → Sh(C), a point q of Sh(D) and a sheaf F on C, the stalk (f⁻¹ F)_q is the stalk F_{f ∘ q} at the composite point f.compPoint q.

theorem stalk_inverseImage (f : MorphismOfTopoi (Sheaf K (Type w)) (Sheaf J (Type w)))
    (q : PointOfTopos.{w, v', u'} K) (F : Sheaf J (Type w)) :
    q.stalk (f.inverseImage.obj F) = (f.compPoint q).stalk F

Sources

• Section 7.34, Tag 05V0
• AxiomMath/Stacks at 5ed82d14

LeanCategoryTheory.Stalk.presheafPushforward_stalk_iso · Stacks.Sheaves.StalkInverseImage.stalkAddEquiv · Stacks.Sheaves.StalkInverseImage.stalkAddEquiv_smul · Stacks.Sheaves.StalkInverseImage.stalkNatIso · Stacks.Sheaves.DerivedPullback.KFlatPullbackMorphismOfSites.targetStalkAddEquiv · Stacks.Sheaves.DerivedPullback.KFlatPullbackMorphismOfSites.targetStalkAddEquiv_smul · Stacks.Sheaves.DerivedPullback.KFlatPullbackMorphismOfSites.targetStalkNatIso · point_morphism_sites

Section7.35 Localization and points#

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

Tag 04H2, a lemma

Tag 04H2 in the Stacks Project.

CategoryTheory.GrothendieckTopology.Point.sheafFiberOverIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/LocalizedPoint.lean, line 107. References: SGA 4 IV (6.7), “point over (p,ξ), j_X”; SGA 4 IV (11.3.5), “partial”.

Stacks 04H2. The point q = Φ.over x of the localized site C/U lies above the point Φ of C: for every sheaf F on C the stalk of F at Φ agrees with the stalk of its restriction j_U⁻¹F = F.over U at q. In other words the triangle formed by q, Φ and the localization morphism j_U : Sh(C/U) ⟶ Sh(C) commutes.

noncomputable def sheafFiberOverIso :
    J.overPullback A X ⋙ (Φ.over x).sheafFiber ≅ Φ.sheafFiber

Tag 04H3, a lemma

Tag 04H3 in the Stacks Project.

CategoryTheory.FunctorToTypes.fromOverSubfunctor_injective, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/OverBijection.lean, line 115. The attribute's comment: “injectivity of x ↦ q_x”.

Stacks 04H3, injectivity: distinct elements x of u(U) give distinct points q_x of C/U, because x is recovered from v_x as the unique section over the final object U/U.

lemma fromOverSubfunctor_injective :
    Function.Injective (fun x : F.obj X => fromOverSubfunctor F x)

CategoryTheory.FunctorToTypes.exists_eq_fromOverSubfunctor, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/OverBijection.lean, line 127. The attribute's comment: “surjectivity of x ↦ q_x, from the cartesian squares v(V/U) = u(V) ×_{u(U)} v(U/U)”.

Stacks 04H3, surjectivity: a subfunctor of Over.forget U ⋙ u whose sections over the final object U/U form a singleton {x} and whose cartesian squares hold is v_x. This is the last paragraph of Stacks' proof: "the top horizontal map gives a bijection v(V/U) → {y ∈ u(V) | y ↦ x}".

lemma exists_eq_fromOverSubfunctor {S : Subfunctor (Over.forget X ⋙ F)} (hS : IsFromOver F X S) :
    ∃ x : F.obj X, S = fromOverSubfunctor F x

CategoryTheory.FunctorToTypes.fromOverSubfunctorEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/OverBijection.lean, line 150. The attribute's comment: “the correspondence u(U) ≃ subfunctors satisfying IsFromOver; the identification of those subfunctors with points of C/U over p is NOT proved (needs 00WJ, 00XM, 00YA)”.

Stacks 04H3. The construction of Stacks 04H2 gives a one to one correspondence

  u(U) ≃ {S : Subfunctor (Over.forget U ⋙ u) // IsFromOver u U S} ,   x ↦ v_x ,

between the elements of u(U) and the subfunctors S of Over.forget U ⋙ u satisfying the two conditions of IsFromOver.

WHAT THIS DOES NOT SAY. IsFromOver is the characterisation that Stacks' proof derives from j_U ∘ q = p; that derivation is not formalized here, so this equivalence is not yet an equivalence with "the fibre functors of the points of C/U lying over p". The missing step is to produce, from an isomorphism j_U⁻¹ ⋙ q.sheafFiber ≅ p.sheafFiber (the formalized reading of j_U ∘ q = p, cf. 04H2's sheafFiberOverIso), a subfunctor S with IsFromOver u U S and S.toFunctor = q.fiber. That needs exactness of sheafification (00WJ), the identification (j_U⁻¹h_V)^# = j_U⁻¹(h_V^#) (00XM) and u(V) = p⁻¹(h_V^#) (00YA), none of which is available in this repository. Until it lands, 04H3 is covered only up to that identification.

noncomputable def fromOverSubfunctorEquiv :
    F.obj X ≃ { S : Subfunctor (Over.forget X ⋙ F) // IsFromOver F X S }

Tag 04H4, a lemma

Tag 04H4 in the Stacks Project.

CategoryTheory.OverShriek.sheafFiberSigmaEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/OverShriekFiber.lean, line 203.

Stacks 04H4. Let C be a site, p a point of C given by u : C ⥤ Set, and U an object of C. For any sheaf F on C/U,

  (j_{U!}F)_p = ∐_x F_{q_x} ,

the coproduct being over the points q_x of C/U attached to the elements x of u(U) as in Stacks 04H2.

Here j_{U!} is (Over.forget U).sheafPullback, the left adjoint of the restriction j_U⁻¹ = GrothendieckTopology.overPullback, and the coproduct is the sigma type, which is the coproduct in Type v. The proof combines the presheaf-level statement presheafFiberSigmaEquiv with Stacks 03CD (OverShriek.sheafifyIso: j_{U!} of a sheafification is the sheafification of the coproduct presheaf) and Stacks 00Y8 (Point.presheafFiber and Point.sheafFiber agree across sheafification).

def sheafFiberSigmaEquiv (F : Sheaf (J.over U) (Type v)) :
    (Σ x : Φ.fiber.obj U, (Φ.over x).sheafFiber.obj F) ≃
      Φ.sheafFiber.obj (((Over.forget U).sheafPullback (Type v) (J.over U) J).obj F)

Sources

• Section 7.35, Tag 04EK
• AxiomMath/Stacks at 5ed82d14

LeanCategoryTheory.GrothendieckTopology.Point.sheafFiberOverIso · CategoryTheory.FunctorToTypes.fromOverSubfunctor_injective · CategoryTheory.FunctorToTypes.exists_eq_fromOverSubfunctor · CategoryTheory.FunctorToTypes.fromOverSubfunctorEquiv · CategoryTheory.OverShriek.sheafFiberSigmaEquiv

Section7.36 2-morphisms of topoi#

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

Tag 04I9, the section

Tag 04I9 in the Stacks Project.

TwoMorphismOfTopoi.hcomp, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Topos/TwoMorphismOfTopoi.lean, line 183. The attribute's comment: “horizontal composition s ⋆ t of 2-morphisms of topoi, and its two descriptions”.

Horizontal composition s ⋆ t of 2-morphisms of topoi: a 2-morphism from f' ∘ f to g' ∘ g, given on ℱ by either of the two composites f'_*f_*ℱ ⟶ g'_*g_*ℱ.

def hcomp (s : TwoMorphismOfTopoi f' g') (t : TwoMorphismOfTopoi f g) :
    TwoMorphismOfTopoi (f'.comp f) (g'.comp g)

Tag 04IA, a definition

Tag 04IA in the Stacks Project.

TwoMorphismOfTopoi, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Topos/TwoMorphismOfTopoi.lean, line 57. The attribute's comment: “a 2-morphism f ⇒ g of morphisms of topoi is a transformation f_ ⟶ g_”. References: SGA 4 IV (3.2); SGA 4 IV (3.3.2), “2-arrows”.

A 2-morphism from a morphism of topoi f : E → F to a morphism of topoi g : E → F is a transformation of functors t : f_* ⟶ g_*.

def TwoMorphismOfTopoi {E : Type u} [Category.{v} E] {F : Type u'} [Category.{v'} F]
    (f g : MorphismOfTopoi E F) : Type _

Sources

• Section 7.36, Tag 04I9
• AxiomMath/Stacks at 5ed82d14

LeanTwoMorphismOfTopoi.hcomp · TwoMorphismOfTopoi

Section7.37 Morphisms between points#

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

Tag 00YH, a lemma

Tag 00YH in the Stacks Project.

Stacks.Sites.PointStalk.tStalk, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/StalkFunctoriality.lean, line 94.

Tag 00YH, Lemma 7.37.1: the canonical natural transformation of stalk functors t_stalk : (-)_{p'} ⟹ (-)_p induced by t : u' → u. Its components are tStalkApp; naturality is tStalk_naturality (part 2).

noncomputable def tStalk (uu uu' : C ⥤ Type u) (t : uu' ⟶ uu) :
    presheafStalk uu' ⟶ presheafStalk uu

Stacks.Sites.PointStalk.tStalkApp_stalkMk, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/StalkFunctoriality.lean, line 104. The attribute's comment: “(1)”.

Part 1 (Well-defined + defining formula). The stalk transformation acts on a representative [(U, x', s)] by [(U, x', s)] ↦ [(U, t_U(x'), s)]; this is ι_tStalkApp at op ⟨U, x'⟩ applied to s, since (map t).op.obj (op ⟨U, x'⟩) is op ⟨U, t.app U x'⟩.

theorem tStalkApp_stalkMk (uu uu' : C ⥤ Type u) (t : uu' ⟶ uu) (F : Cᵒᵖ ⥤ Type u)
    (U : C) (x' : uu'.obj U) (s : F.obj (Opposite.op U)) :
    tStalkApp uu uu' t F (stalkMk uu' F U x' s) = stalkMk uu F U (t.app U x') s

Stacks.Sites.PointStalk.tStalkApp_theta, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/StalkFunctoriality.lean, line 117. The attribute's comment: “(3)”.

Part 3 (Compatibility with t, the agreement of Tag 00Y6). Under the canonical identifications θ^{u'}_U : u'(U) ≅ (h_U)_{p'} and θ^u_U : u(U) ≅ (h_U)_p, the map (t_stalk)_{h_U} : (h_U)_{p'} → (h_U)_p corresponds to t_U : u'(U) → u(U). Since θ is stalkMk … (𝟙 U), this is the case F := yoneda.obj U, s := 𝟙 U of tStalkApp_stalkMk.

theorem tStalkApp_theta (uu uu' : C ⥤ Type u) (t : uu' ⟶ uu) (U : C) (x' : uu'.obj U) :
    tStalkApp uu uu' t (yoneda.obj U) (theta uu' U x') = theta uu U (t.app U x')

Tag 00YI, a definition

Tag 00YI in the Stacks Project.

Declarations registered for the tag:

• CategoryTheory.GrothendieckTopology.Point.Hom registered with add_to_stacks in StacksCore/CategoryTheory/Sites/Point/EnoughPoints.lean, line 21 (StacksCore): “a morphism of points of a site is a transformation of the fibre functors in the opposite direction”.

Sources

• Section 7.37, Tag 00YG
• AxiomMath/Stacks at 5ed82d14

LeanStacks.Sites.PointStalk.tStalk · Stacks.Sites.PointStalk.tStalkApp_stalkMk · Stacks.Sites.PointStalk.tStalkApp_theta · CategoryTheory.GrothendieckTopology.Point.Hom

Section7.38 Sites with enough points#

Section 7.38 of the Stacks Project, Tag 00YJ. 6 tags here are carried by 10 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 00YK, a definition

Tag 00YK in the Stacks Project.

CategoryTheory.GrothendieckTopology.IsConservativeFamily, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/ConservativeFamily.lean, line 97. The attribute's comment: “(1)”. References: SGA 4 IV (6.4.1), “conservative family”.

Stacks 00YK (1). A family of points {p_i}_{i ∈ I} of a site (C, J) is conservative if every map of sheaves of sets φ : F ⟶ G which is an isomorphism on all the fibres F_{p_i} ⟶ G_{p_i} is an isomorphism.

def IsConservativeFamily {ι : Type t} (p : ι → Point.{w} J) : Prop

CategoryTheory.GrothendieckTopology.HasConservativeFamily, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/ConservativeFamily.lean, line 105. The attribute's comment: “(2)”. References: SGA 4 IV (6.4.1), “enough points”.

Stacks 00YK (2). A site (C, J) has enough points if there exists a conservative family of points. No smallness is required of the family; contrast CategoryTheory.GrothendieckTopology.HasEnoughPoints, which asks for a w-small one.

def HasConservativeFamily (J : GrothendieckTopology C) : Prop

Tag 00YL, a lemma

Tag 00YL in the Stacks Project.

CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.nonempty_isLimit_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/SitesWithEnoughPoints.lean, line 141. The attribute's comment: “(4): a cone over a finite diagram of sheaves is a limit if and only if it is one in every stalk at a conservative family of points.”.

Stacks 00YL (4). Let (C, J) be a site and let P be a conservative family of points of it. Let G : K ⥤ Sh(C) be a finite diagram of sheaves with values in A. Then a cone over G is a limit if and only if its image under every stalk functor F ↦ F_{p_i}, p_i ∈ P, is a limit.

public theorem nonempty_isLimit_iff {C : Type u} [Category.{v} C]
    {J : GrothendieckTopology C} {P : ObjectProperty (GrothendieckTopology.Point.{w} J)}
    (hP : P.IsConservativeFamilyOfPoints) {A : Type u'} [Category.{v'} A] [LocallySmall.{w} C]
    [HasColimitsOfSize.{w, w} A] [HasFiniteLimits A] [AB5OfSize.{w, w} A]
    {FC : A → A → Type*} {CC : A → Type w}
    [∀ X Y : A, FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory.{w} A FC]
    [(forget A).ReflectsIsomorphisms] [PreservesFilteredColimitsOfSize.{w, w} (forget A)]
    [J.HasSheafCompose (forget A)]
    {K : Type u''} [SmallCategory K] [FinCategory K] {G : K ⥤ Sheaf J A} (c : Cone G) :
    Nonempty (IsLimit c) ↔
      ∀ Φ : P.FullSubcategory, Nonempty (IsLimit ((Φ.obj.sheafFiber (A := A)).mapCone c))

Tag 00YM, a lemma

Tag 00YM in the Stacks Project.

stalkSet_map_germ, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/GermNaturality.lean, line 169.

Germ naturality (narrowed substantiation).

For distinct sections s ≠ s' ∈ F(U), the Stacks argument identifies an index i and a point x ∈ u_i(U) separating their germs in the stalk at p_i. The "Unwinding the definitions" step rests on the identity below: pushing a germ00YM along a sheaf morphism agrees with the germ00YM of the pushed section. The remaining categorical packaging (equalizer of representable maps, etc.) is deferred.

lemma stalkSet_map_germ {C : Type u} [SmallCategory C] (J : GrothendieckTopology C)
    (P : C ⥤ Type u)
    [P.IsContinuous J (GrothendieckTopology.trivial (Type u))]
    [(P.sheafPushforwardContinuous (Type u) J
        (GrothendieckTopology.trivial (Type u))).IsRightAdjoint]
    {F G : Sheaf J (Type u)} (φ : F ⟶ G) (U : C)
    (s : F.obj.obj (Opposite.op U)) (x : P.obj U) :
    (stalkSet J P).map φ (germ00YM J P F U s x)
      = germ00YM J P G U (φ.hom.app (Opposite.op U) s) x

Tag 04H6, a lemma

Tag 04H6 in the Stacks Project.

CategoryTheory.GrothendieckTopology.IsConservativeFamily.over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/ConservativeFamilyOver.lean, line 97.

Stacks 04H6. Let {p_i}_{i ∈ I} be a conservative family of points of a site (C, J), with fibre functors u_i, and let X be an object of C. Then the points q_{i,x} = (p i).over x of the localized site C/X of Stacks 04H2, for i ∈ I and x ∈ u_i(X), form a conservative family of points of C/X.

theorem IsConservativeFamily.over {ι : Type t} {p : ι → Point.{w} J}
    (hp : IsConservativeFamily p) (X : C) [HasSheafify (J.over X) (Type w)] :
    IsConservativeFamily (fun ix : Σ i, (p i).fiber.obj X ↦ (p ix.1).over ix.2)

CategoryTheory.GrothendieckTopology.HasConservativeFamily.over, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/ConservativeFamilyOver.lean, line 114. The attribute's comment: “in particular”.

Stacks 04H6, the "in particular": if a site (C, J) has enough points, i.e. a conservative family of points (Stacks 00YK (2)), then so does every localization C/X.

theorem HasConservativeFamily.over (h : HasConservativeFamily.{w} J) (X : C)
    [HasSheafify (J.over X) (Type w)] : HasConservativeFamily.{w} (J.over X)

Tag 06UL, a lemma

Tag 06UL in the Stacks Project.

CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.of_coversTop, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/Conservative.lean, line 95. References: SGA 4 IV (6.7.4), “second assertion”; SGA 4 IV (6.7.3), “converse direction”.

Stacks 06UL, the conservativity step. If the U_i cover the final object and each P i is a conservative family of points of C/U_i, then the pushed-forward family pointsOfLocalizations is a conservative family of points of C.

theorem ObjectProperty.IsConservativeFamilyOfPoints.of_coversTop
    (hU : J.CoversTop Ui) (hP : ∀ i, (P i).IsConservativeFamilyOfPoints) :
    (GrothendieckTopology.pointsOfLocalizations Ui P).IsConservativeFamilyOfPoints

CategoryTheory.GrothendieckTopology.hasEnoughPoints_of_coversTop, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/Conservative.lean, line 113. References: SGA 4 IV (6.7.3), “converse”; SGA 4 IV (6.7.4), “second assertion”.

Stacks 06UL. Let C be a site and {U_i}_{i ∈ I} a family of objects such that the U_i cover the final object (hypothesis (1), see the module docstring) and each localization C/U_i has enough points (hypothesis (2)). Then C has enough points.

theorem GrothendieckTopology.hasEnoughPoints_of_coversTop [Small.{w} I]
    (hU : J.CoversTop Ui) [∀ i, HasEnoughPoints.{w} (J.over (Ui i))] :
    HasEnoughPoints.{w} J

CategoryTheory.GrothendieckTopology.HasConservativeFamily.of_coversTop, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/ConservativeFamilyLocality.lean, line 51.

Stacks 06UL for CategoryTheory.GrothendieckTopology.HasConservativeFamily. If a family of objects covers the final object and each localization at a member of the family has a conservative family of points, then so does the site itself.

theorem HasConservativeFamily.of_coversTop (hU : J.CoversTop Ui)
    (hP : ∀ i, (J.over (Ui i)).HasConservativeFamily.{w}) :
    J.HasConservativeFamily.{w}

Tag 0F4G, a lemma

Tag 0F4G in the Stacks Project.

CategoryTheory.Functor.isMorphismOfSites_of_points, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/Exactness.lean, line 135.

Stacks 0F4G. Let u : C ⥤ D be a continuous functor of sites. Let {(q_i, v_i)} be a conservative family of points of D. If each functor u_i = v_i ∘ u defines a point of C, then u defines a morphism of sites f : D → C.

theorem isMorphismOfSites_of_points
    (hP : P.IsConservativeFamilyOfPoints)
    (Ψ : P.FullSubcategory → Point.{u} J)
    (hΨ : ∀ Φ : P.FullSubcategory, (Ψ Φ).fiber = u ⋙ Φ.obj.fiber) :
    u.IsMorphismOfSites J K

Sources

• Section 7.38, Tag 00YJ
• AxiomMath/Stacks at 5ed82d14

LeanCategoryTheory.GrothendieckTopology.IsConservativeFamily · CategoryTheory.GrothendieckTopology.HasConservativeFamily · CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.nonempty_isLimit_iff · stalkSet_map_germ · CategoryTheory.GrothendieckTopology.IsConservativeFamily.over · CategoryTheory.GrothendieckTopology.HasConservativeFamily.over · CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.of_coversTop · CategoryTheory.GrothendieckTopology.hasEnoughPoints_of_coversTop

Section7.39 Criterion for existence of points#

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

Tag 00YO, a lemma

Tag 00YO in the Stacks Project.

CategoryTheory.GrothendieckTopology.exists_refinement_of_ne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/CriterionForExistenceOfPoints/RefinementStep.lean, line 520. The attribute's comment: “The inductive step of Deligne's criterion: a cofiltered system can be refined so as to keep two germs of a separated presheaf distinct while a given section of u'(W) becomes covered by a given finite covering of W.”. References: SGA 4 VI (9.3).

Stacks 00YO. Let (C, J) be a site, let F be a separated presheaf of sets on C and let p : N ⥤ C be a cofiltered system in C, with associated fibre functor u'(X) = colim_j Mor(p j, X) and stalk functor F ↦ F_{p'} = colim_j F(p j). Let s ≠ s' be two germs in F_{p'}, represented by a, a' : F(p j₀), let {g k : Y k ⟶ W} be a finite covering of the site and let f : p j₀ ⟶ W represent a section of u'(W).

Then the system can be refined — there are a cofiltered system q : M ⥤ C, a fully faithful e : N ⥤ M and an isomorphism ε : e ⋙ q ≅ p exhibiting p as the restriction of q — in such a way that the two germs stay distinct in F_p and that the image of f in u(W) lies in the image of u(Y k) for one of the members g k : Y k ⟶ W of the covering.

public theorem exists_refinement_of_ne {C : Type u} [Category.{v} C] (J : GrothendieckTopology C)
    {F : Cᵒᵖ ⥤ Type w} (hF : Presieve.IsSeparated J F) {N : Type u₁} [SmallCategory N]
    [IsCofiltered N] (p : N ⥤ C) (j₀ : N) (a a' : F.obj (op (p.obj j₀)))
    (haa' : ∀ (j : N) (φ : j ⟶ j₀), F.map (p.map φ).op a ≠ F.map (p.map φ).op a') {W : C}
    {ι : Type t} [Finite ι] {Y : ι → C} (g : ∀ k, Y k ⟶ W) (hg : Sieve.ofArrows Y g ∈ J W)
    [∀ (X : C) (h : X ⟶ W) (k : ι), HasPullback h (g k)] (f : p.obj j₀ ⟶ W) :
    ∃ (M : Type u₁) (_ : SmallCategory M) (_ : IsCofiltered M) (q : M ⥤ C) (e : N ⥤ M) (_ : e.Full)
      (_ : e.Faithful) (ε : e ⋙ q ≅ p),
      (∀ (i : M) (ψ : i ⟶ e.obj j₀),
          F.map (q.map ψ ≫ ε.hom.app j₀).op a ≠ F.map (q.map ψ ≫ ε.hom.app j₀).op a') ∧
        ∃ (k : ι) (i : M) (ψ : i ⟶ e.obj j₀) (h : q.obj i ⟶ Y k),
          h ≫ g k = q.map ψ ≫ ε.hom.app j₀ ≫ f

Tag 00YP, a lemma

Tag 00YP in the Stacks Project.

CategoryTheory.GrothendieckTopology.exists_refinement_forall_covering_of_ne, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/CriterionForExistenceOfPoints/UniformRefinement.lean, line 669. The attribute's comment: “The main step of Deligne's criterion: a cofiltered system can be refined so as to keep two germs of a separated presheaf distinct while every section of u' becomes covered by every finite covering of the site.”. References: SGA 4 VI (9.2); SGA 4 VI (9.4).

Stacks 00YP. Let (C, J) be a site in which the members of a finite covering admit fibre products along arbitrary morphisms to its base (hpb), let F be a separated presheaf of sets on C and let p : N ⥤ C be a cofiltered system in C, with associated fibre functor u'(X) = colim_j Mor(p j, X) and stalk functor F ↦ F_{p'} = colim_j F(p j). Let s ≠ s' be two germs in F_{p'}, represented by a, a' : F(p j₀).

Then the system can be refined — there are a cofiltered system q : M ⥤ C, a fully faithful e : N ⥤ M and an isomorphism ε : e ⋙ q ≅ p exhibiting p as the restriction of q — in such a way that the two germs stay distinct in F_p and that, for every finite covering {g k : Y k ⟶ W} of the site and every section f : p j ⟶ W of u'(W), the image of f in u(W) lies in the image of u(Y k) for one of the members g k of the covering. Moreover the refined index category is no larger than the data it is assembled from: if C is w'-small with w'-small hom types and N is essentially w'-small, then so is M, so the refinement can in turn be fed back into the construction of a point of the site and the lemma iterated.

Unlike CategoryTheory.GrothendieckTopology.exists_refinement_of_ne (Stacks 00YO), the covering and the section are not fixed in advance: one refinement works for all of them at once.

public theorem exists_refinement_forall_covering_of_ne {C : Type u} [Category.{v} C] [Small.{w'} C]
    [LocallySmall.{w'} C] (J : GrothendieckTopology C) {F : Cᵒᵖ ⥤ Type w}
    (hF : Presieve.IsSeparated J F)
    (hpb :
      ∀ {W : C} {ι : Type t} [Finite ι] {Y : ι → C} (g : ∀ k, Y k ⟶ W),
        Sieve.ofArrows Y g ∈ J W → ∀ (X : C) (h : X ⟶ W) (k : ι), HasPullback h (g k))
    {N : Type u₁} [SmallCategory N] [IsCofiltered N] [EssentiallySmall.{w'} N] (p : N ⥤ C) (j₀ : N)
    (a a' : F.obj (op (p.obj j₀)))
    (haa' : ∀ (j : N) (φ : j ⟶ j₀), F.map (p.map φ).op a ≠ F.map (p.map φ).op a') :
    ∃ (M : Type (max u₁ u v)) (_ : SmallCategory M) (_ : IsCofiltered M) (_ :
      EssentiallySmall.{w'} M) (q : M ⥤ C) (e : N ⥤ M) (_ : e.Full) (_ : e.Faithful) (ε :
      e ⋙ q ≅ p),
      (∀ (i : M) (ψ : i ⟶ e.obj j₀),
          F.map (q.map ψ ≫ ε.hom.app j₀).op a ≠ F.map (q.map ψ ≫ ε.hom.app j₀).op a') ∧
        ∀ {W : C} {ι : Type t} [Finite ι] {Y : ι → C} (g : ∀ k, Y k ⟶ W),
          Sieve.ofArrows Y g ∈ J W →
            ∀ (j : N) (f : p.obj j ⟶ W),
              ∃ (k : ι) (i : M) (ψ : i ⟶ e.obj j) (h : q.obj i ⟶ Y k),
                h ≫ g k = q.map ψ ≫ ε.hom.app j ≫ f

Tag 00YQ, a proposition

Tag 00YQ in the Stacks Project.

CategoryTheory.GrothendieckTopology.hasEnoughPoints_of_exists_finite_refinement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/CriterionForExistenceOfPoints/DeligneCriterion.lean, line 734. The attribute's comment: “Deligne's criterion: a site with fibre products in which every covering has a finite refinement has enough points.”. References: SGA 4 VI (9.0); SGA 4 VI (9.5), “existence of points”; SGA 2 XIV (1.9), “special case”.

Stacks 00YQ (Deligne's criterion for the existence of enough points). Let (C, J) be a site in which fibre products exist and in which every covering sieve S of an object X admits a refinement by a finite covering — a finite family g k : Y k ⟶ X of morphisms of S which is again a covering of X. Then the site has enough points: there is a small family of points of (C, J) whose fibre functors jointly reflect isomorphisms of sheaves of sets.

The source asks for all finite limits in C; only the fibre products of the members of a finite covering along an arbitrary morphism are used, whence HasPullbacks C.

public theorem hasEnoughPoints_of_exists_finite_refinement {C : Type u} [Category.{v} C]
    [HasPullbacks C] [Small.{w} C] [LocallySmall.{w} C] (J : GrothendieckTopology C)
    [HasSheafify J (Type w)]
    (h :
      ∀ ⦃X : C⦄ (S : Sieve X),
        S ∈ J X →
          ∃ (ι : Type) (_ : Finite ι) (Y : ι → C) (g : ∀ k, Y k ⟶ X),
            Sieve.ofArrows Y g ≤ S ∧ Sieve.ofArrows Y g ∈ J X) :
    HasEnoughPoints.{w} J

Tag 0DW0, a lemma

Tag 0DW0 in the Stacks Project.

CategoryTheory.GrothendieckTopology.hasEnoughPoints_of_coversTop_of_exists_finite_refinement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Point/CriterionForExistenceOfPoints/DeligneCriterion.lean, line 896. The attribute's comment: “A site covered by objects whose localizations satisfy Deligne's criterion has enough points.”. References: SGA 2 XIV (1.9), “special case”; SGA 4 VI (4.12), “more general”; SGA 4 VI (9.0).

Stacks 0DW0. Let (C, J) be a site and let U : I → C be a family of objects, indexed by a w-small type, which covers the final object of the topos of sheaves on C: for every object W of C, the sieve of morphisms Z ⟶ W whose source Z admits a morphism to some U i is a covering sieve. Assume that each localized site C/U i satisfies the hypotheses of Deligne's criterion Stacks 00YQ: fibre products exist in C/U i, and every covering sieve S of an object X of C/U i admits a refinement by a finite covering, i.e. contains a finite family g k : Y k ⟶ X which is again a covering of X. Then (C, J) has enough points.

The finiteness condition is needed only on the localizations, so a site none of whose coverings admits a finite refinement can still have enough points, as soon as it is covered by objects whose localizations are coherent in Deligne's sense.

public theorem hasEnoughPoints_of_coversTop_of_exists_finite_refinement {C : Type u}
    [Category.{v} C] [LocallySmall.{w} C] {J : GrothendieckTopology C} {I : Type*} [Small.{w} I]
    {U : I → C} [∀ i, HasPullbacks (Over (U i))] [∀ i, Small.{w} (Over (U i))] (hU : J.CoversTop U)
    (h :
      ∀ (i : I) ⦃X : Over (U i)⦄ (S : Sieve X),
        S ∈ (J.over (U i)) X →
          ∃ (ι : Type) (_ : Finite ι) (Y : ι → Over (U i)) (g : ∀ k, Y k ⟶ X),
            Sieve.ofArrows Y g ≤ S ∧ Sieve.ofArrows Y g ∈ (J.over (U i)) X) :
    HasEnoughPoints.{w} J

Sources

• Section 7.39, Tag 00YN
• AxiomMath/Stacks at 5ed82d14

LeanCategoryTheory.GrothendieckTopology.exists_refinement_of_ne · CategoryTheory.GrothendieckTopology.exists_refinement_forall_covering_of_ne · CategoryTheory.GrothendieckTopology.hasEnoughPoints_of_exists_finite_refinement · CategoryTheory.GrothendieckTopology.hasEnoughPoints_of_coversTop_of_exists_finite_refinement

Section7.40 Weakly contractible objects#

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

Tag 090K, a lemma

Tag 090K in the Stacks Project.

hasRightInverse_iff_isLocallySurjective_surjective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/WeaklyContractible/Objects.lean, line 241.

Let C be a site with Grothendieck topology J, and let U be an object of C. The following are equivalent.

1. For every covering {U_i → U}_{i ∈ I} of U, the sheafified covering map π^# : ∐ h_{U_i}^# ⟶ h_U^# admits a right inverse (a section) σ, i.e. σ ≫ π^# = 𝟙.

2. For every surjection (locally surjective morphism) of sheaves of sets φ : F ⟶ G, the induced map on sections over U, φ_U : F(U) → G(U), is surjective.

theorem hasRightInverse_iff_isLocallySurjective_surjective :
    (∀ (I : Type v) (Ui : I → C) (f : ∀ i, Ui i ⟶ U),
        (Sieve.ofArrows Ui f) ∈ J U → Stacks.WeaklyContractible.HasRightInverse J Ui f) ↔
    (∀ (F G : Sheaf J (Type v)) (φ : F ⟶ G), Sheaf.IsLocallySurjective φ →
        Function.Surjective ((sheafToPresheaf J (Type v)).map φ |>.app (op U)))

Tag 090L, a definition

Tag 090L in the Stacks Project.

CategoryTheory.GrothendieckTopology.IsWeaklyContractible, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/WeaklyContractible.lean, line 52. The attribute's comment: “(1)”.

An object U of a site C is weakly contractible if every surjection of sheaves of sets on C is surjective on sections over U.

def IsWeaklyContractible (U : C) : Prop

CategoryTheory.GrothendieckTopology.HasEnoughObjects, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/WeaklyContractible.lean, line 68. The attribute's comment: “(3)”.

A site C has enough P objects, for a property P of objects of C, if every object U of C has a covering {U_i → U} with P (U_i) for all i.

def HasEnoughObjects (P : ObjectProperty C) : Prop

CategoryTheory.GrothendieckTopology.HasEnoughWeaklyContractibleObjects, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/WeaklyContractible.lean, line 75. The attribute's comment: “(2)”.

A site C has enough weakly contractible objects if every object has a covering by weakly contractible objects, i.e. if it has enough IsWeaklyContractible objects.

def HasEnoughWeaklyContractibleObjects : Prop

Sources

• Section 7.40, Tag 090J
• AxiomMath/Stacks at 5ed82d14

LeanhasRightInverse_iff_isLocallySurjective_surjective · CategoryTheory.GrothendieckTopology.IsWeaklyContractible · CategoryTheory.GrothendieckTopology.HasEnoughObjects · CategoryTheory.GrothendieckTopology.HasEnoughWeaklyContractibleObjects

Section7.41 Exactness properties of pushforward#

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

Tag 04D6, a lemma

Tag 04D6 in the Stacks Project.

exactness_properties_bundled, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Topos/ExactnessOfMorphism.lean, line 88. References: SGA 4 I (5.6), “iv) <=> v)”; SGA 4 I (6.4), “epic counit ⇒ ψ faithful”.

Stacks Tag 04D6 (abstract bundled form for an adjunction L ⊣ R, playing the role of a morphism of topoi f⁻¹ ⊣ f_*). Five of the eight sub-implications of the Stacks lemma in their topos-free formulation:

• (a) (2) ⇒ (1): R fully faithful implies R faithful;
• (b) (3) ⇒ (1): each component of the counit L∘R ⟶ id being an epimorphism implies R is faithful;
• (d) (9) ⇒ (3): if R reflects epimorphisms, then each component of the counit is an epimorphism (since the counit-image under R is split epi, hence epi);
• (g) (9) ⇒ (8), (10): a faithful functor reflects monomorphisms (8) and bijections (10) automatically; we record (8) here, and (10) follows by combining (8) with (9);
• (h) (7) ⇒ (2): counit pointwise iso implies R fully faithful;
• (h) (2) ⇒ (7): R fully faithful implies the counit is pointwise iso.

All six are immediate consequences of existing Mathlib lemmas: Adjunction.faithful_R_of_epi_counit_app, Adjunction.counit_epi_of_R_faithful, Adjunction.fullyFaithfulROfIsIsoCounit, Adjunction.counit_isIso_of_R_fully_faithful, Functor.reflectsMonomorphisms_of_faithful.

theorem exactness_properties_bundled :
    (R.FullyFaithful → R.Faithful) ∧
    ((∀ X, Epi (h.counit.app X)) → R.Faithful) ∧
    (R.ReflectsEpimorphisms → ∀ X, Epi (h.counit.app X)) ∧
    ((∀ X, IsIso (h.counit.app X)) → Nonempty R.FullyFaithful) ∧
    (R.FullyFaithful → ∀ X, IsIso (h.counit.app X))

Tag 04D7, a lemma

Tag 04D7 in the Stacks Project.

preservesEpi, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Topos/PreservesEpi.lean, line 67.

Stacks 04D7.

Let u : C ⥤ D be a continuous functor between sites (C, J) and (D, K). Assume u satisfies the section-lifting hypothesis of Stacks 04D7 (Hypothesis u J K): for every K-locally surjective morphism of type-valued sheaves on (D, K) and every section on u(U), sections lift locally on a J-cover of U. Then the pushforward functor u.sheafPushforwardContinuous (Type max u₂ v₂) J K : Sheaf K _ ⥤ Sheaf J _ preserves epimorphisms, i.e. transforms surjective maps of sheaves into surjective maps of sheaves.

theorem preservesEpi
    {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D]
    (u : C ⥤ D) (J : GrothendieckTopology C) (K : GrothendieckTopology D)
    [u.IsContinuous J K]
    (hyp : Hypothesis u J K) :
    (u.sheafPushforwardContinuous (Type max u₂ v₂) J K).PreservesEpimorphisms

Tag 04D9, a lemma

Tag 04D9 in the Stacks Project.

val_app_comp_eq_on_image_arrow, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Topos/PushforwardEquality.lean, line 38.

If u_*(f) = u_*(g), then f and g agree after restriction along any arrow u.obj U ⟶ V, by naturality applied to a congrArg on objects of the form u.obj U.

lemma val_app_comp_eq_on_image_arrow
    [u.IsContinuous J K] {X Y : Sheaf K A} (f g : X ⟶ Y)
    (h : (u.sheafPushforwardContinuous A J K).map f =
         (u.sheafPushforwardContinuous A J K).map g)
    {V : D} {U : C} (p : u.obj U ⟶ V) :
    f.hom.app (op V) ≫ Y.obj.map p.op = g.hom.app (op V) ≫ Y.obj.map p.op

Sources

• Section 7.41, Tag 04D5
• AxiomMath/Stacks at 5ed82d14

Leanexactness_properties_bundled · preservesEpi · val_app_comp_eq_on_image_arrow

Section7.42 Almost cocontinuous functors#

Section 7.42 of the Stacks Project, Tag 04B4. 6 tags here are carried by 7 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 04B5, a definition

Tag 04B5 in the Stacks Project.

SheafTheoreticallyEmpty, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cocontinuous/SheafTheoreticallyEmpty.lean, line 28.

Stacks 04B5. An object U of a site is sheaf theoretically empty if the sheafification of the canonical map ∅ ⟶ h_U from the initial presheaf to the presheaf represented by U is an isomorphism of sheaves.

def SheafTheoreticallyEmpty [HasWeakSheafify J (Type v)] (U : C) : Prop

Tag 04B6, a lemma

Tag 04B6 in the Stacks Project.

StacksSheafTheoreticallyEmpty.tfae_sheafTheoreticallyEmpty, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cocontinuous/EmptyPresheaf.lean, line 159.

Stacks 04B6. For an object U of a site (C, J) the following are equivalent: (1) U is sheaf theoretically empty, i.e. ∅^# ⟶ h_U^# is an isomorphism of sheaves; (2) every sheaf of sets has exactly one section over U; (3) ∅^#(U) has exactly one element; (4) ∅^#(U) is nonempty; (5) the empty sieve is a covering sieve of U.

theorem tfae_sheafTheoreticallyEmpty [HasWeakSheafify J (Type u)] (U : C) :
    TFAE [IsIso ((presheafToSheaf J (Type u)).map (emptyPresheafTo (yoneda.obj U))),
      ∀ F : Sheaf J (Type u), Subsingleton (F.obj.obj (op U)) ∧ Nonempty (F.obj.obj (op U)),
      Subsingleton ((sheafify J (emptyPresheaf (C := C))).obj (op U)) ∧
        Nonempty ((sheafify J (emptyPresheaf (C := C))).obj (op U)),
      Nonempty ((sheafify J (emptyPresheaf (C := C))).obj (op U)),
      (⊥ : Sieve U) ∈ J U]

StacksSheafTheoreticallyEmpty.isIso_map_emptyPresheafTo_of_hom, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cocontinuous/EmptyPresheaf.lean, line 177.

Stacks 04B6, final assertion. If U is sheaf theoretically empty, then so is U' for every morphism U' ⟶ U of C.

theorem isIso_map_emptyPresheafTo_of_hom [HasWeakSheafify J (Type u)] {U U' : C} (f : U' ⟶ U)
    (h : IsIso ((presheafToSheaf J (Type u)).map (emptyPresheafTo (yoneda.obj U)))) :
    IsIso ((presheafToSheaf J (Type u)).map (emptyPresheafTo (yoneda.obj U')))

Tag 04B7, a definition

Tag 04B7 in the Stacks Project.

IsAlmostCocontinuous, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cocontinuous/AlmostCocontinuousDefs.lean, line 35.

Stacks 04B7. A functor u : C ⥤ D between sites (C, J) and (D, K) is almost cocontinuous if for every object U of C and every covering sieve S of u U there is a covering sieve T of U such that each arrow f : V ⟶ U in T either has u V sheaf theoretically empty, or has u f in S.

def IsAlmostCocontinuous (u : C ⥤ D) (J : GrothendieckTopology C)
    (K : GrothendieckTopology D) : Prop

Tag 04B8, a lemma

Tag 04B8 in the Stacks Project.

isIso_sheafificationAdjunction_homEquiv_symm, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cocontinuous/AlmostCocontinuousCore.lean, line 76.

Formal core of Stacks 04B8. Suppose a sheaf E together with a presheaf morphism η₀ : F ⟶ (sheafToPresheaf J _).obj E satisfies the universal property of the sheafification of F: every presheaf morphism from F into the underlying presheaf of any sheaf H lifts uniquely through η₀. Then the canonical morphism (presheafToSheaf J).obj F ⟶ E obtained from η₀ via the sheafification adjunction's homEquiv is an isomorphism.

The Stacks 04B8 conclusion (u^p G)^# ≅ u^p (G^#) reduces to this purely formal statement once one verifies, using continuity and almost cocontinuity of u together with the "singleton on empty" hypothesis on G, that u.sheafPushforwardContinuous applied to G^# provides a solution to the universal property of the sheafification of u^p G. The Čech-cohomology argument establishing that universal property is the Stacks-side content of 04B8 and is not formalized here.

theorem isIso_sheafificationAdjunction_homEquiv_symm
    (J : GrothendieckTopology C)
    [HasWeakSheafify J (Type v)]
    (F : Cᵒᵖ ⥤ Type v)
    (E : Sheaf J (Type v))
    (η₀ : F ⟶ (sheafToPresheaf J (Type v)).obj E)
    (h_exists : ∀ (H : Sheaf J (Type v))
                  (α : F ⟶ (sheafToPresheaf J (Type v)).obj H),
        ∃ β : E ⟶ H, η₀ ≫ (sheafToPresheaf J (Type v)).map β = α)
    (h_unique : ∀ (H : Sheaf J (Type v)) (β₁ β₂ : E ⟶ H),
        η₀ ≫ (sheafToPresheaf J (Type v)).map β₁ =
          η₀ ≫ (sheafToPresheaf J (Type v)).map β₂ → β₁ = β₂) :
    IsIso (((sheafificationAdjunction J (Type v)).homEquiv _ _).symm η₀)

Tag 04B9, a lemma

Tag 04B9 in the Stacks Project.

CategoryTheory.Functor.preservesColimitsOfShape_sheafPushforwardContinuous_of_isAlmostCocontinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cocontinuous/AlmostCocontinuousFunctors.lean, line 418. The attribute's comment: “For u continuous and almost cocontinuous, u^s = u^p : Sh(D) → Sh(C) commutes with pushouts and coequalizers, and more generally with finite connected colimits.”.

Stacks 04B9. Let (C, J) and (D, K) be sites and let u : C ⥤ D be continuous and almost cocontinuous, and assume sheafification of Type w-valued presheaves on (D, K) inverts exactly the locally bijective morphisms. Then u^s = u^p : Sh(D) ⥤ Sh(C), restriction of sheaves of sets along u.op, preserves colimits of every connected shape I for which I-shaped colimits of sets exist — in particular pushouts (WalkingSpan) and coequalizers (WalkingParallelPair), and more generally every finite connected shape.

public theorem preservesColimitsOfShape_sheafPushforwardContinuous_of_isAlmostCocontinuous
    {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D] (u : C ⥤ D)
    (J : GrothendieckTopology C) (K : GrothendieckTopology D) [u.IsContinuous J K]
    (hu : IsAlmostCocontinuous u J K) [HasWeakSheafify J (Type w)] [HasWeakSheafify K (Type w)]
    [K.WEqualsLocallyBijective (Type w)] (I : Type t) [Category.{t'} I] [IsConnected I]
    [HasColimitsOfShape I (Type w)] :
    PreservesColimitsOfShape I (u.sheafPushforwardContinuous (Type w) J K)

Tag 04BA, a lemma

Tag 04BA in the Stacks Project.

CategoryTheory.Functor.IsMorphismOfSites.preservesColimitsOfShape_pushforward_morphismOfTopoi_of_isAlmostCocontinuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Cocontinuous/AlmostCocontinuousFunctors.lean, line 535. The attribute's comment: “For a morphism of sites f : D → C whose continuous functor u : C → D is almost cocontinuous, f_* commutes with pushouts and coequalizers, and more generally with finite connected colimits.”.

Stacks 04BA. Let f : D → C be a morphism of sites (Stacks 00X1) associated to the continuous functor u : C ⥤ D, so that f_* : Sh(D) ⥤ Sh(C) is the pushforward of the morphism of topoi attached to f (Stacks 00XC), namely restriction of sheaves of sets along u.op. If u is almost cocontinuous (Stacks 04B7), then f_* preserves colimits of every connected shape whose colimits exist — in particular pushouts and coequalizers, which are connected shapes.

public theorem preservesColimitsOfShape_pushforward_morphismOfTopoi_of_isAlmostCocontinuous
    {C : Type w} [SmallCategory C] {D : Type w} [SmallCategory D] {J : GrothendieckTopology C}
    {K : GrothendieckTopology D} {u : C ⥤ D} (hf : u.IsMorphismOfSites J K)
    (hu : IsAlmostCocontinuous u J K) (I : Type t) [Category.{t'} I] [IsConnected I]
    [HasColimitsOfShape I (Type w)] :
    PreservesColimitsOfShape I hf.morphismOfTopoi.pushforward

Sources

• Section 7.42, Tag 04B4
• AxiomMath/Stacks at 5ed82d14

LeanSheafTheoreticallyEmpty · StacksSheafTheoreticallyEmpty.tfae_sheafTheoreticallyEmpty · StacksSheafTheoreticallyEmpty.isIso_map_emptyPresheafTo_of_hom · IsAlmostCocontinuous · isIso_sheafificationAdjunction_homEquiv_symm · CategoryTheory.Functor.preservesColimitsOfShape_sheafPushforwardContinuous_of_isAlmostCocontinuous · CategoryTheory.Functor.IsMorphismOfSites.preservesColimitsOfShape_pushforward_morphismOfTopoi_of_isAlmostCocontinuous

Section7.43 Subtopoi#

Section 7.43 of the Stacks Project, Tag 08LT. 8 tags here are carried by 15 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 08LU, a definition

Tag 08LU in the Stacks Project.

MorphismOfTopoi.IsEmbedding, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Subtopos/Embedding.lean, line 37. References: SGA 4 IV (9.1.1), “a)”; SGA 4 IV (9.1), “embedding def”.

Stacks Project, Definition 7.43.1 (tag 08LU).

A morphism of topoi f : E → F is an embedding if its pushforward f_* is fully faithful.

def IsEmbedding (f : MorphismOfTopoi E F) : Prop

Tag 08LV, a definition

Tag 08LV in the Stacks Project.

IsSubtopos, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Subtopos/Defs.lean, line 50. References: SGA 4 IV (9.1), “subtopos def”; SGA 4 IV (9.1.1), “b)”.

Stacks Project, Definition 7.43.2 (tag 08LV).

A strictly full subcategory E ⊆ Sh(C, J), given by the property P of its objects, is a subtopos if there is an embedding of topoi f : Sh(D, K) → Sh(C, J), for some site (D, K), whose pushforward has E as its essential image.

Since a subcategory of Sh(C, J) cut out by a property of objects is automatically strictly full and closed under isomorphisms, no further condition on P is imposed; the equality f_*.essImage = P already forces it.

The site (D, K) is quantified over the same universes as (C, J). This is the case that occurs in practice — in Stacks 08LY, for instance, D is C itself carrying a finer topology — and it keeps the universe parameters of IsSubtopos determined by its arguments.

def IsSubtopos (J : GrothendieckTopology C) (P : ObjectProperty (Sheaf J (Type w))) : Prop

Tag 08LW, a lemma

Tag 08LW in the Stacks Project.

CategoryTheory.Sites.Subtopos.MorphismOfTopoi.isEmbedding_overLocalization_iff_isSubterminal, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Subtopos/Subtopoi.lean, line 183. The attribute's comment: “The localization j_F : E/F ⟶ E is an embedding of topoi, i.e. E/F is a subtopos of E, if and only if F is a subobject of the final object.”. References: SGA 4 IV (9.2.1), “(9.2.2) is an embedding”; SGA 4 VI (4.1), “open inclusion j”.

Stacks 08LW. Let E be a topos and F an object of E (in the source, a sheaf on a site C), and let j_F : E/F ⟶ E be the localization morphism of Stacks 04GZ, given by a right adjoint p of j_F⁻¹ = toOver F. Then j_F is an embedding of topoi — so that E/F is the subtopos j_{F,*}(E/F) of E — if and only if F is a subobject of the final object of E.

public theorem MorphismOfTopoi.isEmbedding_overLocalization_iff_isSubterminal {E : Type u}
    [Category.{v} E] [CartesianMonoidalCategory E] (F : E) {p : Over F ⥤ E}
    (adj : toOver F ⊣ p) :
    (MorphismOfTopoi.overLocalization F adj).IsEmbedding ↔ IsSubterminal F

Tag 08LX, a definition

Tag 08LX in the Stacks Project.

OpenSubtopos.IsOpenSubtopos, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Subtopos/Open.lean, line 97.

Open subtopos.

A strictly full subcategory E ⊂ Sh(C), modelled as an ObjectProperty (Sheaf J (Type w)) closed under isomorphisms, is an open subtopos of Sh(C) if there exists a subsheaf F of the terminal sheaf such that E is the subtopos Sh(C)/F. We capture "E is the subtopos Sh(C)/F" by an equivalence of categories P.FullSubcategory ≌ Over F compatible with the inclusion P.ι into Sh(C) and the canonical forgetful functor Over.forget F.

def IsOpenSubtopos [Limits.HasTerminal (Sheaf J (Type w))]
    (P : ObjectProperty (Sheaf J (Type w))) : Prop

Tag 08LY, a lemma

Tag 08LY in the Stacks Project.

CategoryTheory.Sites.Subtopos.isSubtopos_closedComplement, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Subtopos/Subtopoi.lean, line 585. The attribute's comment: “The full subcategory of sheaves G with F ⨯ G ⟶ F an isomorphism is a subtopos of Sh(C). Stated for an arbitrary sheaf F, the source's hypothesis that F be a subsheaf of the final object being unused in its proof.”. References: SGA 4 IV (9.3.1), “for any topos and open U”; SGA 4 IV (9.3.4), “partial”; SGA 4 VI (4.1), “partial”.

Stacks Project, Lemma 7.43.5 (tag 08LY). Let (C, J) be a site and let F be a sheaf of sets on it. The strictly full subcategory closedComplement F of Sh(C, J), consisting of the sheaves G for which the projection F ⨯ G ⟶ F is an isomorphism, is a subtopos of Sh(C, J): it is the essential image of the pushforward of an embedding of topoi.

The source assumes F to be a subsheaf of the final object, in which case this closed subtopos is complementary to the open subtopos Sh(C, J)/F of Stacks 08LW; the hypothesis is not needed, as closedComplement F depends on F only through the objects on which F has a section.

public theorem isSubtopos_closedComplement {C : Type u} [Category.{v} C]
    {J : GrothendieckTopology C} (F : Sheaf J (Type (max u v))) :
    IsSubtopos J (closedComplement F)

Tag 08LZ, a definition

Tag 08LZ in the Stacks Project.

IsClosedSubtopos, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Subtopos/Closed.lean, line 46. References: SGA 4 IV (9.3.1), “closed subtopos defn”; SGA 4 IV (9.3.5), “closed subtopos”.

Stacks Project, Definition 7.43.6 (tag 08LZ).

A strictly full subcategory E ⊆ Sh(C, J), given by the property P of its objects, is a closed subtopos if there is a subsheaf F of the final object of Sh(C, J) — that is, a sheaf F whose map to the terminal object is a monomorphism — such that E is the subtopos closedComplement F described in Stacks 08LY.

def IsClosedSubtopos (J : GrothendieckTopology C) (P : ObjectProperty (Sheaf J (Type w))) :
    Prop

Tag 08M0, a definition

Tag 08M0 in the Stacks Project.

MorphismOfTopoi.IsOpenImmersion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Subtopos/Immersions.lean, line 36. References: SGA 4 IV (9.2.1), “open embedding def”.

Stacks Project, Definition 7.43.7(1) (tag 08M0).

A morphism of topoi f : Sh(D, K) → Sh(C, J) is an open immersion if it is an embedding and the essential image of f_* is an open subtopos of Sh(C, J).

def IsOpenImmersion (f : MorphismOfTopoi (Sheaf K (Type w)) (Sheaf J (Type w))) : Prop

MorphismOfTopoi.IsClosedImmersion, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Subtopos/Immersions.lean, line 44. References: SGA 4 IV (9.3.5), “closed embedding”.

Stacks Project, Definition 7.43.7(2) (tag 08M0).

A morphism of topoi f : Sh(D, K) → Sh(C, J) is a closed immersion if it is an embedding and the essential image of f_* is a closed subtopos of Sh(C, J).

def IsClosedImmersion (f : MorphismOfTopoi (Sheaf K (Type w)) (Sheaf J (Type w))) : Prop

Tag 08M1, a lemma

Tag 08M1 in the Stacks Project.

MorphismOfTopoi.IsClosedImmersion.fullyFaithful, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Subtopos/ClosedImmersion.lean, line 174.

The pushforward of a closed immersion of topoi is fully faithful. This is the first assertion of Stacks 08M1; it already holds for an embedding.

noncomputable def fullyFaithful (hi : i.IsClosedImmersion) : i.pushforward.FullyFaithful

MorphismOfTopoi.IsClosedImmersion.preservesColimitsOfShape_walkingParallelPair, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Subtopos/ClosedImmersion.lean, line 197.

Stacks Project, Lemma 7.43.8 (tag 08M1). The pushforward of a closed immersion of topoi commutes with coequalizers.

lemma preservesColimitsOfShape_walkingParallelPair (hi : i.IsClosedImmersion) :
    PreservesColimitsOfShape WalkingParallelPair i.pushforward

MorphismOfTopoi.IsClosedImmersion.preservesColimitsOfShape_walkingSpan, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Subtopos/ClosedImmersion.lean, line 204.

Stacks Project, Lemma 7.43.8 (tag 08M1). The pushforward of a closed immersion of topoi commutes with pushouts.

lemma preservesColimitsOfShape_walkingSpan (hi : i.IsClosedImmersion) :
    PreservesColimitsOfShape WalkingSpan i.pushforward

MorphismOfTopoi.IsClosedImmersion.preservesEpimorphisms, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Subtopos/ClosedImmersion.lean, line 211.

Stacks Project, Lemma 7.43.8 (tag 08M1). The pushforward of a closed immersion of topoi transforms surjections into surjections.

lemma preservesEpimorphisms (hi : i.IsClosedImmersion) :
    i.pushforward.PreservesEpimorphisms

MorphismOfTopoi.IsClosedImmersion.reflectsMonomorphisms, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Subtopos/ClosedImmersion.lean, line 221.

Stacks Project, Lemma 7.43.8 (tag 08M1). The pushforward of a closed immersion of topoi reflects injections.

lemma reflectsMonomorphisms (hi : i.IsClosedImmersion) :
    i.pushforward.ReflectsMonomorphisms

MorphismOfTopoi.IsClosedImmersion.reflectsEpimorphisms, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Subtopos/ClosedImmersion.lean, line 229.

Stacks Project, Lemma 7.43.8 (tag 08M1). The pushforward of a closed immersion of topoi reflects surjections.

lemma reflectsEpimorphisms (hi : i.IsClosedImmersion) :
    i.pushforward.ReflectsEpimorphisms

MorphismOfTopoi.IsClosedImmersion.reflectsIsomorphisms, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Subtopos/ClosedImmersion.lean, line 237.

Stacks Project, Lemma 7.43.8 (tag 08M1). The pushforward of a closed immersion of topoi reflects bijections.

lemma reflectsIsomorphisms (hi : i.IsClosedImmersion) :
    i.pushforward.ReflectsIsomorphisms

Sources

• Section 7.43, Tag 08LT
• AxiomMath/Stacks at 5ed82d14

LeanMorphismOfTopoi.IsEmbedding · IsSubtopos · CategoryTheory.Sites.Subtopos.MorphismOfTopoi.isEmbedding_overLocalization_iff_isSubterminal · OpenSubtopos.IsOpenSubtopos · CategoryTheory.Sites.Subtopos.isSubtopos_closedComplement · IsClosedSubtopos · MorphismOfTopoi.IsOpenImmersion · MorphismOfTopoi.IsClosedImmersion

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.