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 η.

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.

@[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 (_ : (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index S (CategoryTheory.Functor.comp P F))).obj (CategoryTheory.Limits.WalkingMulticospan.left a) = (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index S (CategoryTheory.Functor.comp P F))).obj (CategoryTheory.Limits.WalkingMulticospan.left a))

@[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 (_ : (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index S (CategoryTheory.Functor.comp P F))).obj (CategoryTheory.Limits.WalkingMulticospan.right b) = (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index S (CategoryTheory.Functor.comp P F))).obj (CategoryTheory.Limits.WalkingMulticospan.right b))

@[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 (_ : (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index S (CategoryTheory.Functor.comp P F))).obj (CategoryTheory.Limits.WalkingMulticospan.left a) = (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index S (CategoryTheory.Functor.comp P F))).obj (CategoryTheory.Limits.WalkingMulticospan.left a))

@[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 (_ : (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index S (CategoryTheory.Functor.comp P F))).obj (CategoryTheory.Limits.WalkingMulticospan.right b) = (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index S (CategoryTheory.Functor.comp P F))).obj (CategoryTheory.Limits.WalkingMulticospan.right b))

@[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 (_ : (CategoryTheory.Functor.comp (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index S P)) F).obj (CategoryTheory.Limits.WalkingMulticospan.left a) = (CategoryTheory.Functor.comp (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index S P)) F).obj (CategoryTheory.Limits.WalkingMulticospan.left a))

@[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 (_ : (CategoryTheory.Functor.comp (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index S P)) F).obj (CategoryTheory.Limits.WalkingMulticospan.right b) = (CategoryTheory.Functor.comp (CategoryTheory.Limits.MulticospanIndex.multicospan (CategoryTheory.GrothendieckTopology.Cover.index S P)) F).obj (CategoryTheory.Limits.WalkingMulticospan.right b))

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.

theorem CategoryTheory.Presheaf.IsSheaf.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) [(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] {P : CategoryTheory.Functor Cᵒᵖ A} (hP : CategoryTheory.Presheaf.IsSheaf J P) : CategoryTheory.Presheaf.IsSheaf J (CategoryTheory.Functor.comp P F)

@[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) [(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] (G : CategoryTheory.Sheaf J A) : ((CategoryTheory.sheafCompose J F).obj G).val = CategoryTheory.Functor.comp G.val F

@[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) [(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] : ∀ {X Y : CategoryTheory.Sheaf J A} (η : X ⟶ Y), ((CategoryTheory.sheafCompose J F).map η).val = CategoryTheory.whiskerRight η.val F

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) [(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.Functor (CategoryTheory.Sheaf J A) (CategoryTheory.Sheaf J B)

Composing a sheaf with a functor preserving the appropriate limits yields a functor between sheaf categories.

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) [(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] [(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)) 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.

@[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} [(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.sheafCompose_map J (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id (CategoryTheory.sheafCompose J F)

@[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) [(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] [(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)) G] [(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)) H] : CategoryTheory.sheafCompose_map J (CategoryTheory.CategoryStruct.comp η γ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.sheafCompose_map J η) (CategoryTheory.sheafCompose_map J γ)