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

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

Instances

    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

      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
      Instances For

        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

          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

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

            Equations
            • =

            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
            • =