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₁}
[category_theory.category C]
{A : Type u₂}
[category_theory.category A]
{B : Type u₃}
[category_theory.category B]
{J : category_theory.grothendieck_topology C}
(F : A ⥤ B)
(P : Cᵒᵖ ⥤ A)
{X : C}
(S : J.cover X) :
(S.index (P ⋙ F)).multicospan ≅ (S.index P).multicospan ⋙ F
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.grothendieck_topology.cover.multicospan_comp F P S = category_theory.nat_iso.of_components (λ (t : category_theory.limits.walking_multicospan (S.index (P ⋙ F)).fst_to (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.limits.walking_multicospan.right b) = category_theory.eq_to_iso _
- category_theory.grothendieck_topology.cover.multicospan_comp._match_1 F P S (category_theory.limits.walking_multicospan.left a) = category_theory.eq_to_iso _
@[simp]
theorem
category_theory.grothendieck_topology.cover.multicospan_comp_app_left
{C : Type u₁}
[category_theory.category C]
{A : Type u₂}
[category_theory.category A]
{B : Type u₃}
[category_theory.category B]
{J : category_theory.grothendieck_topology C}
(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₁}
[category_theory.category C]
{A : Type u₂}
[category_theory.category A]
{B : Type u₃}
[category_theory.category B]
{J : category_theory.grothendieck_topology C}
(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₁}
[category_theory.category C]
{A : Type u₂}
[category_theory.category A]
{B : Type u₃}
[category_theory.category B]
{J : category_theory.grothendieck_topology C}
(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₁}
[category_theory.category C]
{A : Type u₂}
[category_theory.category A]
{B : Type u₃}
[category_theory.category B]
{J : category_theory.grothendieck_topology C}
(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₁}
[category_theory.category C]
{A : Type u₂}
[category_theory.category A]
{B : Type u₃}
[category_theory.category B]
{J : category_theory.grothendieck_topology C}
(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₁}
[category_theory.category C]
{A : Type u₂}
[category_theory.category A]
{B : Type u₃}
[category_theory.category B]
{J : category_theory.grothendieck_topology C}
(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₁}
[category_theory.category C]
{A : Type u₂}
[category_theory.category A]
{B : Type u₃}
[category_theory.category B]
{J : category_theory.grothendieck_topology C}
(F : A ⥤ B)
(P : Cᵒᵖ ⥤ A)
{X : C}
(S : J.cover X) :
F.map_cone (S.multifork P) ≅ (category_theory.limits.cones.postcompose (category_theory.grothendieck_topology.cover.multicospan_comp F P S).hom).obj (S.multifork (P ⋙ 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.
theorem
category_theory.presheaf.is_sheaf.comp
{C : Type u₁}
[category_theory.category C]
{A : Type u₂}
[category_theory.category A]
{B : Type u₃}
[category_theory.category B]
{J : category_theory.grothendieck_topology C}
(F : A ⥤ B)
[Π (X : C) (S : J.cover X) (P : Cᵒᵖ ⥤ A), category_theory.limits.preserves_limit (S.index P).multicospan F]
{P : Cᵒᵖ ⥤ A}
(hP : category_theory.presheaf.is_sheaf J P) :
category_theory.presheaf.is_sheaf J (P ⋙ F)
def
category_theory.Sheaf_compose
{C : Type u₁}
[category_theory.category C]
{A : Type u₂}
[category_theory.category A]
{B : Type u₃}
[category_theory.category B]
(J : category_theory.grothendieck_topology C)
(F : A ⥤ B)
[Π (X : C) (S : J.cover X) (P : Cᵒᵖ ⥤ A), category_theory.limits.preserves_limit (S.index P).multicospan F] :
Composing a sheaf with a functor preserving the appropriate limits yields a functor between sheaf categories.
Equations
- category_theory.Sheaf_compose J F = {obj := λ (G : category_theory.Sheaf J A), {val := G.val ⋙ F, cond := _}, map := λ (G H : category_theory.Sheaf J A) (η : G ⟶ H), {val := category_theory.whisker_right η.val F}, map_id' := _, map_comp' := _}
Instances for category_theory.Sheaf_compose
@[simp]
theorem
category_theory.Sheaf_compose_obj_val
{C : Type u₁}
[category_theory.category C]
{A : Type u₂}
[category_theory.category A]
{B : Type u₃}
[category_theory.category B]
(J : category_theory.grothendieck_topology C)
(F : A ⥤ B)
[Π (X : C) (S : J.cover X) (P : Cᵒᵖ ⥤ A), category_theory.limits.preserves_limit (S.index P).multicospan F]
(G : category_theory.Sheaf J A) :
@[simp]
theorem
category_theory.Sheaf_compose_map_val
{C : Type u₁}
[category_theory.category C]
{A : Type u₂}
[category_theory.category A]
{B : Type u₃}
[category_theory.category B]
(J : category_theory.grothendieck_topology C)
(F : A ⥤ B)
[Π (X : C) (S : J.cover X) (P : Cᵒᵖ ⥤ A), category_theory.limits.preserves_limit (S.index P).multicospan F]
(G H : category_theory.Sheaf J A)
(η : G ⟶ H) :
((category_theory.Sheaf_compose J F).map η).val = category_theory.whisker_right η.val F