THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file, we prove that sheafification is compatible with functors which preserve the correct limits and colimits.
noncomputable
def
category_theory.grothendieck_topology.sheafify_comp_iso
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w₁}
[category_theory.category D]
{E : Type w₂}
[category_theory.category E]
(F : D ⥤ E)
[∀ (α β : Type (max v u)) (fst snd : β → α), category_theory.limits.has_limits_of_shape (category_theory.limits.walking_multicospan fst snd) D]
[∀ (α β : Type (max v u)) (fst snd : β → α), category_theory.limits.has_limits_of_shape (category_theory.limits.walking_multicospan fst snd) E]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ E]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ F]
[Π (X : C) (W : J.cover X) (P : Cᵒᵖ ⥤ D), category_theory.limits.preserves_limit (W.index P).multicospan F]
(P : Cᵒᵖ ⥤ D) :
The isomorphism between the sheafification of P composed with F and
the sheafification of P ⋙ F.
Use the lemmas whisker_right_to_sheafify_sheafify_comp_iso_hom,
to_sheafify_comp_sheafify_comp_iso_inv and sheafify_comp_iso_inv_eq_sheafify_lift to reduce
the components of this isomorphisms to a state that can be handled using the universal property
of sheafification.
Equations
- J.sheafify_comp_iso F P = J.plus_comp_iso F (J.plus_obj P) ≪≫ (J.plus_functor E).map_iso (J.plus_comp_iso F P)
noncomputable
def
category_theory.grothendieck_topology.sheafification_whisker_left_iso
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w₁}
[category_theory.category D]
{E : Type w₂}
[category_theory.category E]
[∀ (α β : Type (max v u)) (fst snd : β → α), category_theory.limits.has_limits_of_shape (category_theory.limits.walking_multicospan fst snd) D]
[∀ (α β : Type (max v u)) (fst snd : β → α), category_theory.limits.has_limits_of_shape (category_theory.limits.walking_multicospan fst snd) E]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ E]
(P : Cᵒᵖ ⥤ D)
[Π (F : D ⥤ E) (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ F]
[Π (F : D ⥤ E) (X : C) (W : J.cover X) (P : Cᵒᵖ ⥤ D), category_theory.limits.preserves_limit (W.index P).multicospan F] :
(category_theory.whiskering_left Cᵒᵖ D E).obj (J.sheafify P) ≅ (category_theory.whiskering_left Cᵒᵖ D E).obj P ⋙ J.sheafification E
The isomorphism between the sheafification of P composed with F and
the sheafification of P ⋙ F, functorially in F.
Equations
- J.sheafification_whisker_left_iso P = J.plus_functor_whisker_left_iso (J.plus_obj P) ≪≫ category_theory.iso_whisker_right (J.plus_functor_whisker_left_iso P) (J.plus_functor E) ≪≫ ((category_theory.whiskering_left Cᵒᵖ D E).obj P).associator (J.plus_functor E) (J.plus_functor E)
@[simp]
theorem
category_theory.grothendieck_topology.sheafification_whisker_left_iso_hom_app
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w₁}
[category_theory.category D]
{E : Type w₂}
[category_theory.category E]
[∀ (α β : Type (max v u)) (fst snd : β → α), category_theory.limits.has_limits_of_shape (category_theory.limits.walking_multicospan fst snd) D]
[∀ (α β : Type (max v u)) (fst snd : β → α), category_theory.limits.has_limits_of_shape (category_theory.limits.walking_multicospan fst snd) E]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ E]
(P : Cᵒᵖ ⥤ D)
(F : D ⥤ E)
[Π (F : D ⥤ E) (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ F]
[Π (F : D ⥤ E) (X : C) (W : J.cover X) (P : Cᵒᵖ ⥤ D), category_theory.limits.preserves_limit (W.index P).multicospan F] :
(J.sheafification_whisker_left_iso P).hom.app F = (J.sheafify_comp_iso F P).hom
@[simp]
theorem
category_theory.grothendieck_topology.sheafification_whisker_left_iso_inv_app
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w₁}
[category_theory.category D]
{E : Type w₂}
[category_theory.category E]
[∀ (α β : Type (max v u)) (fst snd : β → α), category_theory.limits.has_limits_of_shape (category_theory.limits.walking_multicospan fst snd) D]
[∀ (α β : Type (max v u)) (fst snd : β → α), category_theory.limits.has_limits_of_shape (category_theory.limits.walking_multicospan fst snd) E]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ E]
(P : Cᵒᵖ ⥤ D)
(F : D ⥤ E)
[Π (F : D ⥤ E) (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ F]
[Π (F : D ⥤ E) (X : C) (W : J.cover X) (P : Cᵒᵖ ⥤ D), category_theory.limits.preserves_limit (W.index P).multicospan F] :
(J.sheafification_whisker_left_iso P).inv.app F = (J.sheafify_comp_iso F P).inv
noncomputable
def
category_theory.grothendieck_topology.sheafification_whisker_right_iso
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w₁}
[category_theory.category D]
{E : Type w₂}
[category_theory.category E]
(F : D ⥤ E)
[∀ (α β : Type (max v u)) (fst snd : β → α), category_theory.limits.has_limits_of_shape (category_theory.limits.walking_multicospan fst snd) D]
[∀ (α β : Type (max v u)) (fst snd : β → α), category_theory.limits.has_limits_of_shape (category_theory.limits.walking_multicospan fst snd) E]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ E]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ F]
[Π (X : C) (W : J.cover X) (P : Cᵒᵖ ⥤ D), category_theory.limits.preserves_limit (W.index P).multicospan F] :
J.sheafification D ⋙ (category_theory.whiskering_right Cᵒᵖ D E).obj F ≅ (category_theory.whiskering_right Cᵒᵖ D E).obj F ⋙ J.sheafification E
The isomorphism between the sheafification of P composed with F and
the sheafification of P ⋙ F, functorially in P.
Equations
- J.sheafification_whisker_right_iso F = (J.plus_functor D).associator (J.plus_functor D) ((category_theory.whiskering_right Cᵒᵖ D E).obj F) ≪≫ category_theory.iso_whisker_left (J.plus_functor D) (J.plus_functor_whisker_right_iso F) ≪≫ (((J.plus_functor D).associator ((category_theory.whiskering_right Cᵒᵖ D E).obj F) (J.plus_functor E)).symm ≪≫ category_theory.iso_whisker_right (J.plus_functor_whisker_right_iso F) (J.plus_functor E)) ≪≫ ((category_theory.whiskering_right Cᵒᵖ D E).obj F).associator (J.plus_functor E) (J.plus_functor E)
@[simp]
theorem
category_theory.grothendieck_topology.sheafification_whisker_right_iso_hom_app
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w₁}
[category_theory.category D]
{E : Type w₂}
[category_theory.category E]
(F : D ⥤ E)
[∀ (α β : Type (max v u)) (fst snd : β → α), category_theory.limits.has_limits_of_shape (category_theory.limits.walking_multicospan fst snd) D]
[∀ (α β : Type (max v u)) (fst snd : β → α), category_theory.limits.has_limits_of_shape (category_theory.limits.walking_multicospan fst snd) E]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ E]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ F]
[Π (X : C) (W : J.cover X) (P : Cᵒᵖ ⥤ D), category_theory.limits.preserves_limit (W.index P).multicospan F]
(P : Cᵒᵖ ⥤ D) :
(J.sheafification_whisker_right_iso F).hom.app P = (J.sheafify_comp_iso F P).hom
@[simp]
theorem
category_theory.grothendieck_topology.sheafification_whisker_right_iso_inv_app
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w₁}
[category_theory.category D]
{E : Type w₂}
[category_theory.category E]
(F : D ⥤ E)
[∀ (α β : Type (max v u)) (fst snd : β → α), category_theory.limits.has_limits_of_shape (category_theory.limits.walking_multicospan fst snd) D]
[∀ (α β : Type (max v u)) (fst snd : β → α), category_theory.limits.has_limits_of_shape (category_theory.limits.walking_multicospan fst snd) E]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ E]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ F]
[Π (X : C) (W : J.cover X) (P : Cᵒᵖ ⥤ D), category_theory.limits.preserves_limit (W.index P).multicospan F]
(P : Cᵒᵖ ⥤ D) :
(J.sheafification_whisker_right_iso F).inv.app P = (J.sheafify_comp_iso F P).inv
@[simp]
theorem
category_theory.grothendieck_topology.whisker_right_to_sheafify_sheafify_comp_iso_hom_assoc
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w₁}
[category_theory.category D]
{E : Type w₂}
[category_theory.category E]
(F : D ⥤ E)
[∀ (α β : Type (max v u)) (fst snd : β → α), category_theory.limits.has_limits_of_shape (category_theory.limits.walking_multicospan fst snd) D]
[∀ (α β : Type (max v u)) (fst snd : β → α), category_theory.limits.has_limits_of_shape (category_theory.limits.walking_multicospan fst snd) E]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ E]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ F]
[Π (X : C) (W : J.cover X) (P : Cᵒᵖ ⥤ D), category_theory.limits.preserves_limit (W.index P).multicospan F]
(P : Cᵒᵖ ⥤ D)
{X' : Cᵒᵖ ⥤ E}
(f' : J.sheafify (P ⋙ F) ⟶ X') :
category_theory.whisker_right (J.to_sheafify P) F ≫ (J.sheafify_comp_iso F P).hom ≫ f' = J.to_sheafify (P ⋙ F) ≫ f'
@[simp]
theorem
category_theory.grothendieck_topology.whisker_right_to_sheafify_sheafify_comp_iso_hom
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w₁}
[category_theory.category D]
{E : Type w₂}
[category_theory.category E]
(F : D ⥤ E)
[∀ (α β : Type (max v u)) (fst snd : β → α), category_theory.limits.has_limits_of_shape (category_theory.limits.walking_multicospan fst snd) D]
[∀ (α β : Type (max v u)) (fst snd : β → α), category_theory.limits.has_limits_of_shape (category_theory.limits.walking_multicospan fst snd) E]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ E]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ F]
[Π (X : C) (W : J.cover X) (P : Cᵒᵖ ⥤ D), category_theory.limits.preserves_limit (W.index P).multicospan F]
(P : Cᵒᵖ ⥤ D) :
category_theory.whisker_right (J.to_sheafify P) F ≫ (J.sheafify_comp_iso F P).hom = J.to_sheafify (P ⋙ F)
@[simp]
theorem
category_theory.grothendieck_topology.to_sheafify_comp_sheafify_comp_iso_inv_assoc
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w₁}
[category_theory.category D]
{E : Type w₂}
[category_theory.category E]
(F : D ⥤ E)
[∀ (α β : Type (max v u)) (fst snd : β → α), category_theory.limits.has_limits_of_shape (category_theory.limits.walking_multicospan fst snd) D]
[∀ (α β : Type (max v u)) (fst snd : β → α), category_theory.limits.has_limits_of_shape (category_theory.limits.walking_multicospan fst snd) E]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ E]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ F]
[Π (X : C) (W : J.cover X) (P : Cᵒᵖ ⥤ D), category_theory.limits.preserves_limit (W.index P).multicospan F]
(P : Cᵒᵖ ⥤ D)
{X' : Cᵒᵖ ⥤ E}
(f' : J.sheafify P ⋙ F ⟶ X') :
J.to_sheafify (P ⋙ F) ≫ (J.sheafify_comp_iso F P).inv ≫ f' = category_theory.whisker_right (J.to_sheafify P) F ≫ f'
@[simp]
theorem
category_theory.grothendieck_topology.to_sheafify_comp_sheafify_comp_iso_inv
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w₁}
[category_theory.category D]
{E : Type w₂}
[category_theory.category E]
(F : D ⥤ E)
[∀ (α β : Type (max v u)) (fst snd : β → α), category_theory.limits.has_limits_of_shape (category_theory.limits.walking_multicospan fst snd) D]
[∀ (α β : Type (max v u)) (fst snd : β → α), category_theory.limits.has_limits_of_shape (category_theory.limits.walking_multicospan fst snd) E]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ E]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ F]
[Π (X : C) (W : J.cover X) (P : Cᵒᵖ ⥤ D), category_theory.limits.preserves_limit (W.index P).multicospan F]
(P : Cᵒᵖ ⥤ D) :
J.to_sheafify (P ⋙ F) ≫ (J.sheafify_comp_iso F P).inv = category_theory.whisker_right (J.to_sheafify P) F
@[simp]
theorem
category_theory.grothendieck_topology.sheafify_comp_iso_inv_eq_sheafify_lift
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{D : Type w₁}
[category_theory.category D]
{E : Type w₂}
[category_theory.category E]
(F : D ⥤ E)
[∀ (α β : Type (max v u)) (fst snd : β → α), category_theory.limits.has_limits_of_shape (category_theory.limits.walking_multicospan fst snd) D]
[∀ (α β : Type (max v u)) (fst snd : β → α), category_theory.limits.has_limits_of_shape (category_theory.limits.walking_multicospan fst snd) E]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ D]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ E]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ F]
[Π (X : C) (W : J.cover X) (P : Cᵒᵖ ⥤ D), category_theory.limits.preserves_limit (W.index P).multicospan F]
(P : Cᵒᵖ ⥤ D)
[category_theory.concrete_category D]
[category_theory.limits.preserves_limits (category_theory.forget D)]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget D)]
[category_theory.reflects_isomorphisms (category_theory.forget D)] :
(J.sheafify_comp_iso F P).inv = J.sheafify_lift (category_theory.whisker_right (J.to_sheafify P) F) _