mathlib documentation

category_theory.sites.compatible_plus

In this file, we prove that the plus functor is compatible with functors which preserve the correct limits and colimits.

See category_theory/sites/compatible_sheafification for the compatibility of sheafification, which follows easily from the content in this file.

source
noncomputable def category_theory.grothendieck_topology.diagram_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) (W : J.cover X) (P : Cᵒᵖ ⥤ D), category_theory.limits.preserves_limit (W.index P).multicospan F] (P : Cᵒᵖ ⥤ D) (X : C) :
J.diagram P X ⋙ F ≅ J.diagram (P ⋙ F) X

The diagram used to define P⁺, composed with F, is isomorphic to the diagram used to define P ⋙ F.

Equations
source
@[simp]
theorem category_theory.grothendieck_topology.diagram_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) (W : J.cover X) (P : Cᵒᵖ ⥤ D), category_theory.limits.preserves_limit (W.index P).multicospan F] (P : Cᵒᵖ ⥤ D) (X : C) (W : (J.cover X)ᵒᵖ) (i : (opposite.unop W).arrow) {X' : E} (f' : ((opposite.unop W).index (P ⋙ F)).left i ⟶ X') :
(J.diagram_comp_iso F P X).hom.app W ≫ category_theory.limits.multiequalizer.ι ((opposite.unop W).index (P ⋙ F)) i ≫ f' = F.map (category_theory.limits.multiequalizer.ι ((opposite.unop W).index P) i) ≫ f'
source
@[simp]
theorem category_theory.grothendieck_topology.diagram_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) (W : J.cover X) (P : Cᵒᵖ ⥤ D), category_theory.limits.preserves_limit (W.index P).multicospan F] (P : Cᵒᵖ ⥤ D) (X : C) (W : (J.cover X)ᵒᵖ) (i : (opposite.unop W).arrow) :
(J.diagram_comp_iso F P X).hom.app W ≫ category_theory.limits.multiequalizer.ι ((opposite.unop W).index (P ⋙ F)) i = F.map (category_theory.limits.multiequalizer.ι ((opposite.unop W).index P) i)
source
noncomputable def category_theory.grothendieck_topology.plus_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) (W : J.cover X) (P : Cᵒᵖ ⥤ D), category_theory.limits.preserves_limit (W.index P).multicospan F] (P : Cᵒᵖ ⥤ D) [∀ (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] :
J.plus_obj P ⋙ F ≅ J.plus_obj (P ⋙ F)

The isomorphism between P⁺ ⋙ F and (P ⋙ F)⁺.

Equations
source
@[simp]
theorem category_theory.grothendieck_topology.ι_plus_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) (W : J.cover X) (P : Cᵒᵖ ⥤ D), category_theory.limits.preserves_limit (W.index P).multicospan F] (P : Cᵒᵖ ⥤ D) [∀ (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 (opposite.unop X))ᵒᵖ) {X' : E} (f' : (J.plus_obj (P ⋙ F)).obj X ⟶ X') :
F.map (category_theory.limits.colimit.ι (J.diagram P (opposite.unop X)) W) ≫ (J.plus_comp_iso F P).hom.app X ≫ f' = (J.diagram_comp_iso F P (opposite.unop X)).hom.app W ≫ category_theory.limits.colimit.ι (J.diagram (P ⋙ F) (opposite.unop X)) W ≫ f'
source
@[simp]
theorem category_theory.grothendieck_topology.ι_plus_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) (W : J.cover X) (P : Cᵒᵖ ⥤ D), category_theory.limits.preserves_limit (W.index P).multicospan F] (P : Cᵒᵖ ⥤ D) [∀ (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 (opposite.unop X))ᵒᵖ) :
F.map (category_theory.limits.colimit.ι (J.diagram P (opposite.unop X)) W) ≫ (J.plus_comp_iso F P).hom.app X = (J.diagram_comp_iso F P (opposite.unop X)).hom.app W ≫ category_theory.limits.colimit.ι (J.diagram (P ⋙ F) (opposite.unop X)) W
source
@[simp]
theorem category_theory.grothendieck_topology.plus_comp_iso_whisker_left_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] [∀ (α β : 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] {F G : D ⥤ E} (η : F ⟶ G) (P : Cᵒᵖ ⥤ D) [Π (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] [Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ G] [Π (X : C) (W : J.cover X) (P : Cᵒᵖ ⥤ D), category_theory.limits.preserves_limit (W.index P).multicospan G] {X' : Cᵒᵖ ⥤ E} (f' : J.plus_obj (P ⋙ G) ⟶ X') :
category_theory.whisker_left (J.plus_obj P) η ≫ (J.plus_comp_iso G P).hom ≫ f' = (J.plus_comp_iso F P).hom ≫ J.plus_map (category_theory.whisker_left P η) ≫ f'
source
@[simp]
theorem category_theory.grothendieck_topology.plus_comp_iso_whisker_left {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] {F G : D ⥤ E} (η : F ⟶ G) (P : Cᵒᵖ ⥤ D) [Π (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] [Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ G] [Π (X : C) (W : J.cover X) (P : Cᵒᵖ ⥤ D), category_theory.limits.preserves_limit (W.index P).multicospan G] :
category_theory.whisker_left (J.plus_obj P) η ≫ (J.plus_comp_iso G P).hom = (J.plus_comp_iso F P).hom ≫ J.plus_map (category_theory.whisker_left P η)
source
@[simp]
theorem category_theory.grothendieck_topology.plus_functor_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) (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] (X : D ⥤ E) :
(J.plus_functor_whisker_left_iso P).hom.app X = (J.plus_comp_iso X P).hom
source
@[simp]
theorem category_theory.grothendieck_topology.plus_functor_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) (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] (X : D ⥤ E) :
(J.plus_functor_whisker_left_iso P).inv.app X = (J.plus_comp_iso X P).inv
source
noncomputable def category_theory.grothendieck_topology.plus_functor_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.plus_obj P) ≅ (category_theory.whiskering_left Cᵒᵖ D E).obj P ⋙ J.plus_functor E

The isomorphism between P⁺ ⋙ F and (P ⋙ F)⁺, functorially in F.

Equations
source
@[simp]
theorem category_theory.grothendieck_topology.plus_comp_iso_whisker_right {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) (W : J.cover X) (P : Cᵒᵖ ⥤ D), category_theory.limits.preserves_limit (W.index P).multicospan F] [∀ (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] {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) :
category_theory.whisker_right (J.plus_map η) F ≫ (J.plus_comp_iso F Q).hom = (J.plus_comp_iso F P).hom ≫ J.plus_map (category_theory.whisker_right η F)
source
@[simp]
theorem category_theory.grothendieck_topology.plus_comp_iso_whisker_right_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) (W : J.cover X) (P : Cᵒᵖ ⥤ D), category_theory.limits.preserves_limit (W.index P).multicospan F] [∀ (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] {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) {X' : Cᵒᵖ ⥤ E} (f' : J.plus_obj (Q ⋙ F) ⟶ X') :
category_theory.whisker_right (J.plus_map η) F ≫ (J.plus_comp_iso F Q).hom ≫ f' = (J.plus_comp_iso F P).hom ≫ J.plus_map (category_theory.whisker_right η F) ≫ f'
source
noncomputable def category_theory.grothendieck_topology.plus_functor_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) (W : J.cover X) (P : Cᵒᵖ ⥤ D), category_theory.limits.preserves_limit (W.index P).multicospan F] [∀ (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] :
J.plus_functor D ⋙ (category_theory.whiskering_right Cᵒᵖ D E).obj F ≅ (category_theory.whiskering_right Cᵒᵖ D E).obj F ⋙ J.plus_functor E

The isomorphism between P⁺ ⋙ F and (P ⋙ F)⁺, functorially in P.

Equations
source
@[simp]
theorem category_theory.grothendieck_topology.plus_functor_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) (W : J.cover X) (P : Cᵒᵖ ⥤ D), category_theory.limits.preserves_limit (W.index P).multicospan F] [∀ (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ᵒᵖ ⥤ D) :
(J.plus_functor_whisker_right_iso F).inv.app X = (J.plus_comp_iso F X).inv
source
@[simp]
theorem category_theory.grothendieck_topology.plus_functor_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) (W : J.cover X) (P : Cᵒᵖ ⥤ D), category_theory.limits.preserves_limit (W.index P).multicospan F] [∀ (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ᵒᵖ ⥤ D) :
(J.plus_functor_whisker_right_iso F).hom.app X = (J.plus_comp_iso F X).hom
source
@[simp]
theorem category_theory.grothendieck_topology.whisker_right_to_plus_comp_plus_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) (W : J.cover X) (P : Cᵒᵖ ⥤ D), category_theory.limits.preserves_limit (W.index P).multicospan F] (P : Cᵒᵖ ⥤ D) [∀ (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ᵒᵖ ⥤ E} (f' : J.plus_obj (P ⋙ F) ⟶ X') :
category_theory.whisker_right (J.to_plus P) F ≫ (J.plus_comp_iso F P).hom ≫ f' = J.to_plus (P ⋙ F) ≫ f'
source
@[simp]
theorem category_theory.grothendieck_topology.whisker_right_to_plus_comp_plus_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) (W : J.cover X) (P : Cᵒᵖ ⥤ D), category_theory.limits.preserves_limit (W.index P).multicospan F] (P : Cᵒᵖ ⥤ D) [∀ (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] :
category_theory.whisker_right (J.to_plus P) F ≫ (J.plus_comp_iso F P).hom = J.to_plus (P ⋙ F)
source
@[simp]
theorem category_theory.grothendieck_topology.to_plus_comp_plus_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) (W : J.cover X) (P : Cᵒᵖ ⥤ D), category_theory.limits.preserves_limit (W.index P).multicospan F] (P : Cᵒᵖ ⥤ D) [∀ (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] :
J.to_plus (P ⋙ F) ≫ (J.plus_comp_iso F P).inv = category_theory.whisker_right (J.to_plus P) F
source
theorem category_theory.grothendieck_topology.plus_comp_iso_inv_eq_plus_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) (W : J.cover X) (P : Cᵒᵖ ⥤ D), category_theory.limits.preserves_limit (W.index P).multicospan F] (P : Cᵒᵖ ⥤ D) [∀ (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] (hP : category_theory.presheaf.is_sheaf J (J.plus_obj P ⋙ F)) :
(J.plus_comp_iso F P).inv = J.plus_lift (category_theory.whisker_right (J.to_plus P) F) hP