mathlib documentation


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.is_sheaf.comp says that composition with such an F indeed preserves the sheaf condition.

The functor between sheaf categories is called Sheaf_compose J F. Given a natural transformation η : F ⟶ G, we obtain a natural transformation Sheaf_compose J F ⟶ Sheaf_compose J G, which we call Sheaf_compose_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.


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.


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

Instances for category_theory.Sheaf_compose