Documentation

Mathlib.CategoryTheory.Sites.CoverLifting

Cocontinuous functors between sites. #

We define cocontinuous functors between sites as functors that pull covering sieves back to covering sieves. This concept is also known as cover-lifting or cover-reflecting functors. We use the original terminology and definition of SGA 4 III 2.1. However, the notion of cocontinuous functor should not be confused with the general definition of cocontinuous functors between categories as functors preserving small colimits.

Main definitions #

Main results #

References #

A functor G : (C, J) ⥤ (D, K) between sites is called cocontinuous (SGA 4 III 2.1) if for all covering sieves R in D, R.pullback G is a covering sieve in C.

Instances

    The identity functor on a site is cocontinuous.

    Equations
    • =

    The composition of two cocontinuous functors is cocontinuous.

    We will now prove that Ran G.op (ₚu) maps sheaves to sheaves if G is cocontinuous (SGA 4 III 2.2). This can also be be found in https://stacks.math.columbia.edu/tag/00XK. However, the proof given there uses the amalgamation definition of sheaves, and thus does not require that C or D has categorical pullbacks.

    For the following proof sketch, denotes the homs on C and D as in the topological analogy. By definition, the presheaf 𝒢 : Dᵒᵖ ⥤ A is a sheaf if for every sieve S of U : D, and every compatible family of morphisms X ⟶ 𝒢(V) for each V ⊆ U : S with a fixed source X, we can glue them into a morphism X ⟶ 𝒢(U).

    Since the presheaf 𝒢 := (Ran G.op).obj ℱ.val is defined via 𝒢(U) = lim_{G(V) ⊆ U} ℱ(V), for gluing the family x into a X ⟶ 𝒢(U), it suffices to provide a X ⟶ ℱ(Y) for each G(Y) ⊆ U. This can be done since { Y' ⊆ Y : G(Y') ⊆ U ∈ S} is a covering sieve for Y on C (by the cocontinuity G). Thus the morphisms X ⟶ 𝒢(G(Y')) ⟶ ℱ(Y') can be glued into a morphism X ⟶ ℱ(Y). This is done in get_sections.

    In glued_limit_cone, we verify these obtained sections are indeed compatible, and thus we obtain A X ⟶ 𝒢(U). The remaining work is to verify that this is indeed the amalgamation and is unique.

    The family of morphisms X ⟶ 𝒢(G(Y')) ⟶ ℱ(Y') defined on { Y' ⊆ Y : G(Y') ⊆ U ∈ S}.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      def CategoryTheory.RanIsSheafOfIsCocontinuous.getSection {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {G : CategoryTheory.Functor C D} {A : Type w} [CategoryTheory.Category.{w', w} A] [∀ (X : Dᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) A] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [G.IsCocontinuous J K] (ℱ : CategoryTheory.Sheaf J A) {X : A} {U : D} {S : CategoryTheory.Sieve U} (hS : S K.sieves U) {x : CategoryTheory.Presieve.FamilyOfElements (((CategoryTheory.ran G.op).obj .val).comp (CategoryTheory.coyoneda.obj { unop := X })) S.arrows} (hx : x.Compatible) (Y : CategoryTheory.StructuredArrow { unop := U } G.op) :
      X .val.obj Y.right

      Given a G(Y) ⊆ U, we can find a unique section X ⟶ ℱ(Y) that agrees with x.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        theorem CategoryTheory.RanIsSheafOfIsCocontinuous.getSection_is_unique {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {G : CategoryTheory.Functor C D} {A : Type w} [CategoryTheory.Category.{w', w} A] [∀ (X : Dᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) A] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [G.IsCocontinuous J K] (ℱ : CategoryTheory.Sheaf J A) {X : A} {U : D} {S : CategoryTheory.Sieve U} (hS : S K.sieves U) {x : CategoryTheory.Presieve.FamilyOfElements (((CategoryTheory.ran G.op).obj .val).comp (CategoryTheory.coyoneda.obj { unop := X })) S.arrows} (hx : x.Compatible) (Y : CategoryTheory.StructuredArrow { unop := U } G.op) {y : (((CategoryTheory.Functor.id (CategoryTheory.Functor Cᵒᵖ A)).obj .val).comp (CategoryTheory.coyoneda.obj { unop := X })).obj { unop := Y.right.unop }} (H : (CategoryTheory.RanIsSheafOfIsCocontinuous.pulledbackFamily S x Y).IsAmalgamation y) :
        def CategoryTheory.RanIsSheafOfIsCocontinuous.gluedLimitCone {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {G : CategoryTheory.Functor C D} {A : Type w} [CategoryTheory.Category.{w', w} A] [∀ (X : Dᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) A] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [G.IsCocontinuous J K] (ℱ : CategoryTheory.Sheaf J A) {X : A} {U : D} {S : CategoryTheory.Sieve U} (hS : S K.sieves U) {x : CategoryTheory.Presieve.FamilyOfElements (((CategoryTheory.ran G.op).obj .val).comp (CategoryTheory.coyoneda.obj { unop := X })) S.arrows} (hx : x.Compatible) :

        The limit cone in order to glue the sections obtained via get_section.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          def CategoryTheory.RanIsSheafOfIsCocontinuous.gluedSection {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {G : CategoryTheory.Functor C D} {A : Type w} [CategoryTheory.Category.{w', w} A] [∀ (X : Dᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) A] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [G.IsCocontinuous J K] (ℱ : CategoryTheory.Sheaf J A) {X : A} {U : D} {S : CategoryTheory.Sieve U} (hS : S K.sieves U) {x : CategoryTheory.Presieve.FamilyOfElements (((CategoryTheory.ran G.op).obj .val).comp (CategoryTheory.coyoneda.obj { unop := X })) S.arrows} (hx : x.Compatible) :
          X ((CategoryTheory.ran G.op).obj .val).obj { unop := U }

          The section obtained by passing glued_limit_cone into CategoryTheory.Limits.limit.lift.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            theorem CategoryTheory.RanIsSheafOfIsCocontinuous.helper {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] {G : CategoryTheory.Functor C D} {A : Type w} [CategoryTheory.Category.{w', w} A] [∀ (X : Dᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) A] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [G.IsCocontinuous J K] (ℱ : CategoryTheory.Sheaf J A) {X : A} {U : D} {S : CategoryTheory.Sieve U} (hS : S K.sieves U) {x : CategoryTheory.Presieve.FamilyOfElements (((CategoryTheory.ran G.op).obj .val).comp (CategoryTheory.coyoneda.obj { unop := X })) S.arrows} (hx : x.Compatible) {V : D} (f : V U) (y : X ((CategoryTheory.ran G.op).obj .val).obj { unop := V }) (W : CategoryTheory.StructuredArrow { unop := V } G.op) (H : ∀ {V' : C} {fV : G.obj V' V} (hV : S.arrows (CategoryTheory.CategoryStruct.comp fV f)), CategoryTheory.CategoryStruct.comp y (((CategoryTheory.ran G.op).obj .val).map fV.op) = x (CategoryTheory.CategoryStruct.comp fV f) hV) :

            A helper lemma for the following two lemmas. Basically stating that if the section y : X ⟶ 𝒢(V) coincides with x on G(V') for all G(V') ⊆ V ∈ S, then X ⟶ 𝒢(V) ⟶ ℱ(W) is indeed the section obtained in get_sections. That said, this is littered with some more categorical jargon in order to be applied in the following lemmas easier.

            Verify that the glued_section is an amalgamation of x.

            theorem CategoryTheory.RanIsSheafOfIsCocontinuous.gluedSection_is_unique {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] {G : CategoryTheory.Functor C D} {A : Type w} [CategoryTheory.Category.{w', w} A] [∀ (X : Dᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) A] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} [G.IsCocontinuous J K] (ℱ : CategoryTheory.Sheaf J A) {X : A} {U : D} {S : CategoryTheory.Sieve U} (hS : S K.sieves U) {x : CategoryTheory.Presieve.FamilyOfElements (((CategoryTheory.ran G.op).obj .val).comp (CategoryTheory.coyoneda.obj { unop := X })) S.arrows} (hx : x.Compatible) (y : (((CategoryTheory.ran G.op).obj .val).comp (CategoryTheory.coyoneda.obj { unop := X })).obj { unop := U }) (hy : x.IsAmalgamation y) :

            Verify that the amalgamation is indeed unique.

            If G is cocontinuous, then Ran G.op pushes sheaves to sheaves.

            This result is basically https://stacks.math.columbia.edu/tag/00XK, but without the condition that C or D has pullbacks.

            A cover-lifting functor induces a pushforward functor on categories of sheaves.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              noncomputable def CategoryTheory.Functor.sheafAdjunctionCocontinuous {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (G : CategoryTheory.Functor C D) (A : Type w) [CategoryTheory.Category.{w', w} A] [∀ (X : Dᵒᵖ), CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) A] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [G.IsCocontinuous J K] [G.IsContinuous J K] :
              G.sheafPushforwardContinuous A J K G.sheafPushforwardCocontinuous A J K

              Given a functor between sites that is continuous and cocontinuous, the pushforward for the continuous functor G is left adjoint to the pushforward for the cocontinuous functor G.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

                The natural isomorphism exhibiting compatibility between pushforward and sheafification.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For