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 G.op.ran : (Cᵒᵖ ⥤ A) ⥤ (Dᵒᵖ ⥤ A) maps sheaves to sheaves when G : C ⥤ D is a cocontinuous functor.

    We do not follow the proofs in SGA 4 III 2.2 or https://stacks.math.columbia.edu/tag/00XK. Instead, we verify as directly as possible that if F : Cᵒᵖ ⥤ A is a sheaf, then G.op.ran.obj F is a sheaf. in order to do this, we use the "multifork" characterization of sheaves which involves limits in the category A. As G.op.ran.obj F is the chosen right Kan extension of F along G.op : Cᵒᵖ ⥤ Dᵒᵖ, we actually verify that any pointwise right Kan extension of F along G.op is a sheaf.

    Auxiliary definition for lift.

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

      Auxiliary definition for isLimitMultifork

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        theorem CategoryTheory.RanIsSheafOfIsCocontinuous.hom_ext {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] {J : CategoryTheory.GrothendieckTopology C} (K : CategoryTheory.GrothendieckTopology D) [G.IsCocontinuous J K] {F : CategoryTheory.Functor Cᵒᵖ A} (hF : CategoryTheory.Presheaf.IsSheaf J F) {R : CategoryTheory.Functor Dᵒᵖ A} {α : G.op.comp R F} (hR : (CategoryTheory.Functor.RightExtension.mk R α).IsPointwiseRightKanExtension) {X : D} {S : K.Cover X} {W : A} {f : W R.obj (Opposite.op X)} {g : W R.obj (Opposite.op X)} (h : ∀ (i : S.Arrow), CategoryTheory.CategoryStruct.comp f (R.map i.f.op) = CategoryTheory.CategoryStruct.comp g (R.map i.f.op)) :
        f = g

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

        This is SGA 4 III 2.2. An alternative reference is https://stacks.math.columbia.edu/tag/00XK (where results are obtained under the additional assumption that C and D have pullbacks).

        A cocontinuous functor induces a pushforward functor on categories of sheaves.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem CategoryTheory.Functor.sheafPushforwardCocontinuousCompSheafToPresheafIso_hom {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] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [G.IsCocontinuous J K] [∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] :
          (G.sheafPushforwardCocontinuousCompSheafToPresheafIso A J K).hom = CategoryTheory.CategoryStruct.id ((G.sheafPushforwardCocontinuous A J K).comp (CategoryTheory.sheafToPresheaf K A))
          @[simp]
          theorem CategoryTheory.Functor.sheafPushforwardCocontinuousCompSheafToPresheafIso_inv {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] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [G.IsCocontinuous J K] [∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] :
          (G.sheafPushforwardCocontinuousCompSheafToPresheafIso A J K).inv = CategoryTheory.CategoryStruct.id ((G.sheafPushforwardCocontinuous A J K).comp (CategoryTheory.sheafToPresheaf K A))

          G.sheafPushforwardCocontinuous A J K : Sheaf J A ⥤ Sheaf K A is induced by the right Kan extension functor G.op.ran on presheaves.

          Equations
          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] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] [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
              theorem CategoryTheory.Functor.sheafAdjunctionCocontinuous_unit_app_val {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] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] [G.IsCocontinuous J K] [G.IsContinuous J K] (F : CategoryTheory.Sheaf K A) :
              ((G.sheafAdjunctionCocontinuous A J K).unit.app F).val = (G.op.ranAdjunction A).unit.app F.val
              theorem CategoryTheory.Functor.sheafAdjunctionCocontinuous_counit_app_val {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] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] [G.IsCocontinuous J K] [G.IsContinuous J K] (F : CategoryTheory.Sheaf J A) :
              ((G.sheafAdjunctionCocontinuous A J K).counit.app F).val = (G.op.ranAdjunction A).counit.app F.val
              theorem CategoryTheory.Functor.sheafAdjunctionCocontinuous_homEquiv_apply_val {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] (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] [G.IsCocontinuous J K] [G.IsContinuous J K] {F : CategoryTheory.Sheaf K A} {H : CategoryTheory.Sheaf J A} (f : (G.sheafPushforwardContinuous A J K).obj F H) :
              (((G.sheafAdjunctionCocontinuous A J K).homEquiv F H) f).val = ((G.op.ranAdjunction A).homEquiv F.val H.val) f.val

              The natural isomorphism exhibiting compatibility between pushforward and sheafification.

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