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

def CategoryTheory.GrothendieckTopology.Cover.multicospanComp {C : Type u₁} [] {A : Type u₂} [] {B : Type u₃} [] (F : ) (P : ) {X : C} :

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.

Instances For
@[simp]
theorem CategoryTheory.GrothendieckTopology.Cover.multicospanComp_app_left {C : Type u₁} [] {A : Type u₂} [] {B : Type u₃} [] (F : ) (P : ) {X : C} :
= CategoryTheory.eqToIso (_ : ().obj () = ().obj ())
@[simp]
theorem CategoryTheory.GrothendieckTopology.Cover.multicospanComp_app_right {C : Type u₁} [] {A : Type u₂} [] {B : Type u₃} [] (F : ) (P : ) {X : C} :
= CategoryTheory.eqToIso (_ : ().obj () = ().obj ())
@[simp]
theorem CategoryTheory.GrothendieckTopology.Cover.multicospanComp_hom_app_left {C : Type u₁} [] {A : Type u₂} [] {B : Type u₃} [] (F : ) (P : ) {X : C} :
= CategoryTheory.eqToHom (_ : ().obj () = ().obj ())
@[simp]
theorem CategoryTheory.GrothendieckTopology.Cover.multicospanComp_hom_app_right {C : Type u₁} [] {A : Type u₂} [] {B : Type u₃} [] (F : ) (P : ) {X : C} :
= CategoryTheory.eqToHom (_ : ().obj () = ().obj ())
@[simp]
theorem CategoryTheory.GrothendieckTopology.Cover.multicospanComp_hom_inv_left {C : Type u₁} [] {A : Type u₂} [] {B : Type u₃} [] (F : ) (P : ) {X : C} :
= CategoryTheory.eqToHom (_ : ().obj () = ().obj ())
@[simp]
theorem CategoryTheory.GrothendieckTopology.Cover.multicospanComp_hom_inv_right {C : Type u₁} [] {A : Type u₂} [] {B : Type u₃} [] (F : ) (P : ) {X : C} :
= CategoryTheory.eqToHom (_ : ().obj () = ().obj ())
def CategoryTheory.GrothendieckTopology.Cover.mapMultifork {C : Type u₁} [] {A : Type u₂} [] {B : Type u₃} [] (F : ) (P : ) {X : C} :

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.

Instances For
theorem CategoryTheory.Presheaf.IsSheaf.comp {C : Type u₁} [] {A : Type u₂} [] {B : Type u₃} [] (F : ) [(X : C) → ] {P : } (hP : ) :
@[simp]
theorem CategoryTheory.sheafCompose_obj_val {C : Type u₁} [] {A : Type u₂} [] {B : Type u₃} [] (F : ) [(X : C) → ] (G : ) :
(().obj G).val =
@[simp]
theorem CategoryTheory.sheafCompose_map_val {C : Type u₁} [] {A : Type u₂} [] {B : Type u₃} [] (F : ) [(X : C) → ] :
∀ {X Y : } (η : X Y), (().map η).val =
def CategoryTheory.sheafCompose {C : Type u₁} [] {A : Type u₂} [] {B : Type u₃} [] (F : ) [(X : C) → ] :

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

Instances For
def CategoryTheory.sheafCompose_map {C : Type u₁} [] {A : Type u₂} [] {B : Type u₃} [] {F : } {G : } (η : F G) [(X : C) → ] [(X : C) → ] :

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.

Instances For
@[simp]
theorem CategoryTheory.sheafCompose_id {C : Type u₁} [] {A : Type u₂} [] {B : Type u₃} [] {F : } [(X : C) → ] :
@[simp]
theorem CategoryTheory.sheafCompose_comp {C : Type u₁} [] {A : Type u₂} [] {B : Type u₃} [] {F : } {G : } (H : ) (η : F G) (γ : G H) [(X : C) → ] [(X : C) → ] [(X : C) → ] :