Documentation

Mathlib.CategoryTheory.Sites.Whiskering

In this file we construct the functor Sheaf J A ⥤ Sheaf J B between sheaf categories obtained by composition with a functor F : A ⥤ B.

In order for the sheaf condition to be preserved, F must preserve the correct limits. The lemma Presheaf.IsSheaf.comp says that composition with such an F indeed preserves the sheaf condition.

The functor between sheaf categories is called sheafCompose J F. Given a natural transformation η : F ⟶ G, we obtain a natural transformation sheafCompose J F ⟶ sheafCompose J G, which we call sheafCompose_map J η.

source
class CategoryTheory.GrothendieckTopology.HasSheafCompose {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {B : Type u₃} [CategoryTheory.Category.{v₃, u₃} B] (J : CategoryTheory.GrothendieckTopology C) (F : CategoryTheory.Functor A B) :
Prop

Describes the property of a functor to "preserve sheaves".

Instances
    source
    @[simp]
    theorem CategoryTheory.sheafCompose_map_val {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {B : Type u₃} [CategoryTheory.Category.{v₃, u₃} B] (J : CategoryTheory.GrothendieckTopology C) (F : CategoryTheory.Functor A B) [CategoryTheory.GrothendieckTopology.HasSheafCompose J F] :
    ∀ {X Y : CategoryTheory.Sheaf J A} (η : X ⟶ Y), ((CategoryTheory.sheafCompose J F).map η).val = CategoryTheory.whiskerRight η.val F
    source
    @[simp]
    theorem CategoryTheory.sheafCompose_obj_val {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {B : Type u₃} [CategoryTheory.Category.{v₃, u₃} B] (J : CategoryTheory.GrothendieckTopology C) (F : CategoryTheory.Functor A B) [CategoryTheory.GrothendieckTopology.HasSheafCompose J F] (G : CategoryTheory.Sheaf J A) :
    ((CategoryTheory.sheafCompose J F).obj G).val = CategoryTheory.Functor.comp G.val F
    source
    def CategoryTheory.sheafCompose {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {B : Type u₃} [CategoryTheory.Category.{v₃, u₃} B] (J : CategoryTheory.GrothendieckTopology C) (F : CategoryTheory.Functor A B) [CategoryTheory.GrothendieckTopology.HasSheafCompose J F] :
    CategoryTheory.Functor (CategoryTheory.Sheaf J A) (CategoryTheory.Sheaf J B)

    Composing a functor which HasSheafCompose, yields a functor between sheaf categories.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def CategoryTheory.sheafCompose_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {B : Type u₃} [CategoryTheory.Category.{v₃, u₃} B] (J : CategoryTheory.GrothendieckTopology C) {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor A B} (η : F ⟶ G) [CategoryTheory.GrothendieckTopology.HasSheafCompose J F] [CategoryTheory.GrothendieckTopology.HasSheafCompose J G] :
      CategoryTheory.sheafCompose J F ⟶ CategoryTheory.sheafCompose J G

      If η : F ⟶ G is a natural transformation then we obtain a morphism of functors sheafCompose J F ⟶ sheafCompose J G by whiskering with η on the level of presheaves.

      Equations
      Instances For
        source
        @[simp]
        theorem CategoryTheory.sheafCompose_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {B : Type u₃} [CategoryTheory.Category.{v₃, u₃} B] (J : CategoryTheory.GrothendieckTopology C) {F : CategoryTheory.Functor A B} [CategoryTheory.GrothendieckTopology.HasSheafCompose J F] :
        CategoryTheory.sheafCompose_map J (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id (CategoryTheory.sheafCompose J F)
        source
        @[simp]
        theorem CategoryTheory.sheafCompose_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {B : Type u₃} [CategoryTheory.Category.{v₃, u₃} B] (J : CategoryTheory.GrothendieckTopology C) {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor A B} (H : CategoryTheory.Functor A B) (η : F ⟶ G) (γ : G ⟶ H) [CategoryTheory.GrothendieckTopology.HasSheafCompose J F] [CategoryTheory.GrothendieckTopology.HasSheafCompose J G] [CategoryTheory.GrothendieckTopology.HasSheafCompose J H] :
        CategoryTheory.sheafCompose_map J (CategoryTheory.CategoryStruct.comp η γ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.sheafCompose_map J η) (CategoryTheory.sheafCompose_map J γ)
        source
        def CategoryTheory.GrothendieckTopology.Cover.multicospanComp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {B : Type u₃} [CategoryTheory.Category.{v₃, u₃} B] {J : CategoryTheory.GrothendieckTopology C} (F : CategoryTheory.Functor A B) (P : CategoryTheory.Functor Cᵒᵖ A) {X : C} (S : CategoryTheory.GrothendieckTopology.Cover J X) :
        CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index S (CategoryTheory.Functor.comp P F)) ≅ CategoryTheory.Functor.comp (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index S P)) F

        The multicospan associated to a cover S : J.Cover X and a presheaf of the form P ⋙ F is isomorphic to the composition of the multicospan associated to S and P, composed with F.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.GrothendieckTopology.Cover.multicospanComp_app_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {B : Type u₃} [CategoryTheory.Category.{v₃, u₃} B] {J : CategoryTheory.GrothendieckTopology C} (F : CategoryTheory.Functor A B) (P : CategoryTheory.Functor Cᵒᵖ A) {X : C} (S : CategoryTheory.GrothendieckTopology.Cover J X) (a : (CategoryTheory.GrothendieckTopology.Cover.index S (CategoryTheory.Functor.comp P F)).L) :
          (CategoryTheory.GrothendieckTopology.Cover.multicospanComp F P S).app (CategoryTheory.Limits.WalkingMulticospan.left a) = CategoryTheory.eqToIso ⋯
          source
          @[simp]
          theorem CategoryTheory.GrothendieckTopology.Cover.multicospanComp_app_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {B : Type u₃} [CategoryTheory.Category.{v₃, u₃} B] {J : CategoryTheory.GrothendieckTopology C} (F : CategoryTheory.Functor A B) (P : CategoryTheory.Functor Cᵒᵖ A) {X : C} (S : CategoryTheory.GrothendieckTopology.Cover J X) (b : (CategoryTheory.GrothendieckTopology.Cover.index S (CategoryTheory.Functor.comp P F)).R) :
          (CategoryTheory.GrothendieckTopology.Cover.multicospanComp F P S).app (CategoryTheory.Limits.WalkingMulticospan.right b) = CategoryTheory.eqToIso ⋯
          source
          @[simp]
          theorem CategoryTheory.GrothendieckTopology.Cover.multicospanComp_hom_app_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {B : Type u₃} [CategoryTheory.Category.{v₃, u₃} B] {J : CategoryTheory.GrothendieckTopology C} (F : CategoryTheory.Functor A B) (P : CategoryTheory.Functor Cᵒᵖ A) {X : C} (S : CategoryTheory.GrothendieckTopology.Cover J X) (a : (CategoryTheory.GrothendieckTopology.Cover.index S (CategoryTheory.Functor.comp P F)).L) :
          (CategoryTheory.GrothendieckTopology.Cover.multicospanComp F P S).hom.app (CategoryTheory.Limits.WalkingMulticospan.left a) = CategoryTheory.eqToHom ⋯
          source
          @[simp]
          theorem CategoryTheory.GrothendieckTopology.Cover.multicospanComp_hom_app_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {B : Type u₃} [CategoryTheory.Category.{v₃, u₃} B] {J : CategoryTheory.GrothendieckTopology C} (F : CategoryTheory.Functor A B) (P : CategoryTheory.Functor Cᵒᵖ A) {X : C} (S : CategoryTheory.GrothendieckTopology.Cover J X) (b : (CategoryTheory.GrothendieckTopology.Cover.index S (CategoryTheory.Functor.comp P F)).R) :
          (CategoryTheory.GrothendieckTopology.Cover.multicospanComp F P S).hom.app (CategoryTheory.Limits.WalkingMulticospan.right b) = CategoryTheory.eqToHom ⋯
          source
          @[simp]
          theorem CategoryTheory.GrothendieckTopology.Cover.multicospanComp_hom_inv_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {B : Type u₃} [CategoryTheory.Category.{v₃, u₃} B] {J : CategoryTheory.GrothendieckTopology C} (F : CategoryTheory.Functor A B) (P : CategoryTheory.Functor Cᵒᵖ A) {X : C} (S : CategoryTheory.GrothendieckTopology.Cover J X) (a : (CategoryTheory.GrothendieckTopology.Cover.index S (CategoryTheory.Functor.comp P F)).L) :
          (CategoryTheory.GrothendieckTopology.Cover.multicospanComp F P S).inv.app (CategoryTheory.Limits.WalkingMulticospan.left a) = CategoryTheory.eqToHom ⋯
          source
          @[simp]
          theorem CategoryTheory.GrothendieckTopology.Cover.multicospanComp_hom_inv_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {B : Type u₃} [CategoryTheory.Category.{v₃, u₃} B] {J : CategoryTheory.GrothendieckTopology C} (F : CategoryTheory.Functor A B) (P : CategoryTheory.Functor Cᵒᵖ A) {X : C} (S : CategoryTheory.GrothendieckTopology.Cover J X) (b : (CategoryTheory.GrothendieckTopology.Cover.index S (CategoryTheory.Functor.comp P F)).R) :
          (CategoryTheory.GrothendieckTopology.Cover.multicospanComp F P S).inv.app (CategoryTheory.Limits.WalkingMulticospan.right b) = CategoryTheory.eqToHom ⋯
          source
          def CategoryTheory.GrothendieckTopology.Cover.mapMultifork {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {B : Type u₃} [CategoryTheory.Category.{v₃, u₃} B] {J : CategoryTheory.GrothendieckTopology C} (F : CategoryTheory.Functor A B) (P : CategoryTheory.Functor Cᵒᵖ A) {X : C} (S : CategoryTheory.GrothendieckTopology.Cover J X) :
          F.mapCone (CategoryTheory.GrothendieckTopology.Cover.multifork S P) ≅ (CategoryTheory.Limits.Cones.postcompose (CategoryTheory.GrothendieckTopology.Cover.multicospanComp F P S).hom).obj (CategoryTheory.GrothendieckTopology.Cover.multifork S (CategoryTheory.Functor.comp P F))

          Mapping the multifork associated to a cover S : J.Cover X and a presheaf P with respect to a functor F is isomorphic (upto a natural isomorphism of the underlying functors) to the multifork associated to S and P ⋙ F.

          Equations
          Instances For
            source
            instance CategoryTheory.hasSheafCompose_of_preservesMulticospan {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {B : Type u₃} [CategoryTheory.Category.{v₃, u₃} B] (J : CategoryTheory.GrothendieckTopology C) (F : CategoryTheory.Functor A B) [(X : C) → (S : CategoryTheory.GrothendieckTopology.Cover J X) → (P : CategoryTheory.Functor Cᵒᵖ A) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index S P)) F] :
            CategoryTheory.GrothendieckTopology.HasSheafCompose J F

            Composing a sheaf with a functor preserving the limit of (S.index P).multicospan yields a functor between sheaf categories.

            Equations
            • ⋯ = ⋯
            source
            instance CategoryTheory.hasSheafCompose_of_preservesLimitsOfSize {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] {B : Type u₃} [CategoryTheory.Category.{v₃, u₃} B] (J : CategoryTheory.GrothendieckTopology C) {F : CategoryTheory.Functor A B} [CategoryTheory.Limits.PreservesLimitsOfSize.{v₁, max u₁ v₁, v₂, v₃, u₂, u₃} F] :
            CategoryTheory.GrothendieckTopology.HasSheafCompose J F

            Composing a sheaf with a functor preserving limits of the same size as the hom sets in C yields a functor between sheaf categories.

            Note: the size of the limit that F is required to preserve in hasSheafCompose_of_preservesMulticospan is in general larger than this.

            Equations
            • ⋯ = ⋯