# mathlib3documentation

category_theory.sites.whiskering

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

def category_theory.grothendieck_topology.cover.multicospan_comp {C : Type u₁} {A : Type u₂} {B : Type u₃} (F : A B) (P : Cᵒᵖ A) {X : C} (S : J.cover X) :

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
• = category_theory.nat_iso.of_components (λ (t : (S.index (P F)).snd_to), category_theory.grothendieck_topology.cover.multicospan_comp._match_1 F P S t) _
• category_theory.grothendieck_topology.cover.multicospan_comp._match_1 F P S =
• category_theory.grothendieck_topology.cover.multicospan_comp._match_1 F P S =
@[simp]
theorem category_theory.grothendieck_topology.cover.multicospan_comp_app_left {C : Type u₁} {A : Type u₂} {B : Type u₃} (F : A B) (P : Cᵒᵖ A) {X : C} (S : J.cover X) (a : (S.index (P F)).L) :
@[simp]
theorem category_theory.grothendieck_topology.cover.multicospan_comp_app_right {C : Type u₁} {A : Type u₂} {B : Type u₃} (F : A B) (P : Cᵒᵖ A) {X : C} (S : J.cover X) (b : (S.index (P F)).R) :
@[simp]
theorem category_theory.grothendieck_topology.cover.multicospan_comp_hom_app_left {C : Type u₁} {A : Type u₂} {B : Type u₃} (F : A B) (P : Cᵒᵖ A) {X : C} (S : J.cover X) (a : (S.index (P F)).L) :
@[simp]
theorem category_theory.grothendieck_topology.cover.multicospan_comp_hom_app_right {C : Type u₁} {A : Type u₂} {B : Type u₃} (F : A B) (P : Cᵒᵖ A) {X : C} (S : J.cover X) (b : (S.index (P F)).R) :
@[simp]
theorem category_theory.grothendieck_topology.cover.multicospan_comp_hom_inv_left {C : Type u₁} {A : Type u₂} {B : Type u₃} (F : A B) (P : Cᵒᵖ A) {X : C} (S : J.cover X) (a : (S.index (P F)).L) :
@[simp]
theorem category_theory.grothendieck_topology.cover.multicospan_comp_hom_inv_right {C : Type u₁} {A : Type u₂} {B : Type u₃} (F : A B) (P : Cᵒᵖ A) {X : C} (S : J.cover X) (b : (S.index (P F)).R) :
def category_theory.grothendieck_topology.cover.map_multifork {C : Type u₁} {A : Type u₂} {B : Type u₃} (F : A B) (P : Cᵒᵖ A) {X : C} (S : J.cover X) :

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
theorem category_theory.presheaf.is_sheaf.comp {C : Type u₁} {A : Type u₂} {B : Type u₃} (F : A B) [Π (X : C) (S : J.cover X) (P : Cᵒᵖ A), ] {P : Cᵒᵖ A} (hP : P) :
def category_theory.Sheaf_compose {C : Type u₁} {A : Type u₂} {B : Type u₃} (F : A B) [Π (X : C) (S : J.cover X) (P : Cᵒᵖ A), ] :

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

Equations
Instances for category_theory.Sheaf_compose
@[simp]
theorem category_theory.Sheaf_compose_obj_val {C : Type u₁} {A : Type u₂} {B : Type u₃} (F : A B) [Π (X : C) (S : J.cover X) (P : Cᵒᵖ A), ] (G : A) :
.obj G).val = G.val F
@[simp]
theorem category_theory.Sheaf_compose_map_val {C : Type u₁} {A : Type u₂} {B : Type u₃} (F : A B) [Π (X : C) (S : J.cover X) (P : Cᵒᵖ A), ] (G H : A) (η : G H) :
.map η).val =