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

class CategoryTheory.GrothendieckTopology.HasSheafCompose {C : Type u₁} [] {A : Type u₂} [] {B : Type u₃} [] (F : ) :

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

Instances
theorem CategoryTheory.GrothendieckTopology.HasSheafCompose.isSheaf {C : Type u₁} [] {A : Type u₂} [] {B : Type u₃} [] {F : } [self : J.HasSheafCompose F] (P : ) (hP : ) :

For every sheaf P, P ⋙ F is a sheaf.

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

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
instance CategoryTheory.instFaithfulSheafFunctorOppositeCompSheafComposeSheafToPresheaf {C : Type u₁} [] {A : Type u₂} [] {B : Type u₃} [] (F : ) [J.HasSheafCompose F] [F.Faithful] :
(.comp ).Faithful
Equations
• =
instance CategoryTheory.instFullSheafFunctorOppositeCompSheafComposeSheafToPresheafOfFaithful {C : Type u₁} [] {A : Type u₂} [] {B : Type u₃} [] (F : ) [J.HasSheafCompose F] [F.Faithful] [F.Full] :
(.comp ).Full
Equations
• =
instance CategoryTheory.instFaithfulSheafSheafCompose {C : Type u₁} [] {A : Type u₂} [] {B : Type u₃} [] (F : ) [J.HasSheafCompose F] [F.Faithful] :
.Faithful
Equations
• =
instance CategoryTheory.instFullSheafSheafComposeOfFaithful {C : Type u₁} [] {A : Type u₂} [] {B : Type u₃} [] (F : ) [J.HasSheafCompose F] [F.Full] [F.Faithful] :
.Full
Equations
• =
instance CategoryTheory.instReflectsIsomorphismsSheafSheafCompose {C : Type u₁} [] {A : Type u₂} [] {B : Type u₃} [] (F : ) [J.HasSheafCompose F] [F.ReflectsIsomorphisms] :
.ReflectsIsomorphisms
Equations
• =
def CategoryTheory.sheafCompose_map {C : Type u₁} [] {A : Type u₂} [] {B : Type u₃} [] {F : } {G : } (η : F G) [J.HasSheafCompose F] [J.HasSheafCompose 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
• = { app := fun (X : ) => { val := }, naturality := }
Instances For
@[simp]
theorem CategoryTheory.sheafCompose_id {C : Type u₁} [] {A : Type u₂} [] {B : Type u₃} [] {F : } [J.HasSheafCompose F] :
@[simp]
theorem CategoryTheory.sheafCompose_comp {C : Type u₁} [] {A : Type u₂} [] {B : Type u₃} [] {F : } {G : } (H : ) (η : F G) (γ : G H) [J.HasSheafCompose F] [J.HasSheafCompose G] [J.HasSheafCompose H] :
@[simp]
theorem CategoryTheory.GrothendieckTopology.Cover.multicospanComp_inv_app {C : Type u₁} [] {A : Type u₂} [] {B : Type u₃} [] (F : ) (P : ) {X : C} (S : J.Cover X✝) (X : CategoryTheory.Limits.WalkingMulticospan (S.index (P.comp F)).fstTo (S.index (P.comp F)).sndTo) :
.app X = (match X with | => CategoryTheory.Iso.refl (F.obj (P.obj (Opposite.op a.Y))) | => CategoryTheory.Iso.refl (F.obj (P.obj (Opposite.op b.r.Z)))).inv
@[simp]
theorem CategoryTheory.GrothendieckTopology.Cover.multicospanComp_hom_app {C : Type u₁} [] {A : Type u₂} [] {B : Type u₃} [] (F : ) (P : ) {X : C} (S : J.Cover X✝) (X : CategoryTheory.Limits.WalkingMulticospan (S.index (P.comp F)).fstTo (S.index (P.comp F)).sndTo) :
.app X = (match X with | => CategoryTheory.Iso.refl (F.obj (P.obj (Opposite.op a.Y))) | => CategoryTheory.Iso.refl (F.obj (P.obj (Opposite.op b.r.Z)))).hom
def CategoryTheory.GrothendieckTopology.Cover.multicospanComp {C : Type u₁} [] {A : Type u₂} [] {B : Type u₃} [] (F : ) (P : ) {X : C} (S : J.Cover X) :
(S.index (P.comp F)).multicospan (S.index P).multicospan.comp 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
def CategoryTheory.GrothendieckTopology.Cover.mapMultifork {C : Type u₁} [] {A : Type u₂} [] {B : Type u₃} [] (F : ) (P : ) {X : C} (S : J.Cover X) :
F.mapCone (S.multifork P) (S.multifork (P.comp 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
instance CategoryTheory.hasSheafCompose_of_preservesMulticospan {C : Type u₁} [] {A : Type u₂} [] {B : Type u₃} [] (F : ) [(X : C) → (S : J.Cover X) → (P : ) → CategoryTheory.Limits.PreservesLimit (S.index P).multicospan F] :
J.HasSheafCompose F

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

Equations
• =
instance CategoryTheory.hasSheafCompose_of_preservesLimitsOfSize {C : Type u₁} [] {A : Type u₂} [] {B : Type u₃} [] {F : } [] :
J.HasSheafCompose 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
• =
theorem CategoryTheory.Sheaf.isSeparated {C : Type u₁} [] {A : Type u₂} [] [J.HasSheafCompose ] (F : ) :
theorem CategoryTheory.Presheaf.IsSheaf.isSeparated {C : Type u₁} [] {A : Type u₂} [] {F : } [J.HasSheafCompose ] (hF : ) :