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 η
.
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
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
Composing a sheaf with a functor preserving the appropriate limits yields a functor between sheaf categories.
Instances For
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.