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".
- isSheaf : ∀ (P : CategoryTheory.Functor Cᵒᵖ A), CategoryTheory.Presheaf.IsSheaf J P → CategoryTheory.Presheaf.IsSheaf J (P.comp F)
For every sheaf
P
,P ⋙ F
is a sheaf.
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
- CategoryTheory.sheafCompose_map J η = { app := fun (x : CategoryTheory.Sheaf J A) => { val := CategoryTheory.whiskerLeft x.val η }, naturality := ⋯ }
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
- CategoryTheory.GrothendieckTopology.Cover.mapMultifork F P S = CategoryTheory.Limits.Cones.ext (CategoryTheory.Iso.refl (F.mapCone (S.multifork P)).pt) ⋯
Instances For
Composing a sheaf with a functor preserving the limit of (S.index P).multicospan
yields a functor
between sheaf categories.
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.