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

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