# mathlibdocumentation

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.

noncomputable def category_theory.grothendieck_topology.diagram_comp_iso {C : Type u} {D : Type w₁} {E : Type w₂} (F : D E) [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (α β : Type (max v u)) (fst snd : β → α), ] [Π (X : C) (W : J.cover X) (P : Cᵒᵖ D), ] (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
@[simp]
theorem category_theory.grothendieck_topology.diagram_comp_iso_hom_ι_assoc {C : Type u} {D : Type w₁} {E : Type w₂} (F : D E) [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (α β : Type (max v u)) (fst snd : β → α), ] [Π (X : C) (W : J.cover X) (P : Cᵒᵖ D), ] (P : Cᵒᵖ D) (X : C) (W : (J.cover X)ᵒᵖ) (i : .arrow) {X' : E} (f' : ((opposite.unop W).index (P F)).left i X') :
(J.diagram_comp_iso F P X).hom.app W i f' = F.map f'
@[simp]
theorem category_theory.grothendieck_topology.diagram_comp_iso_hom_ι {C : Type u} {D : Type w₁} {E : Type w₂} (F : D E) [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (α β : Type (max v u)) (fst snd : β → α), ] [Π (X : C) (W : J.cover X) (P : Cᵒᵖ D), ] (P : Cᵒᵖ D) (X : C) (W : (J.cover X)ᵒᵖ) (i : .arrow) :
(J.diagram_comp_iso F P X).hom.app W i = F.map
noncomputable def category_theory.grothendieck_topology.plus_comp_iso {C : Type u} {D : Type w₁} {E : Type w₂} (F : D E) [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (α β : Type (max v u)) (fst snd : β → α), ] [Π (X : C) (W : J.cover X) (P : Cᵒᵖ D), ] (P : Cᵒᵖ D) [∀ (X : C), ] [∀ (X : C), ] [Π (X : C), ] :
J.plus_obj P F J.plus_obj (P F)

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

Equations
@[simp]
theorem category_theory.grothendieck_topology.ι_plus_comp_iso_hom_assoc {C : Type u} {D : Type w₁} {E : Type w₂} (F : D E) [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (α β : Type (max v u)) (fst snd : β → α), ] [Π (X : C) (W : J.cover X) (P : Cᵒᵖ D), ] (P : Cᵒᵖ D) [∀ (X : C), ] [∀ (X : C), ] [Π (X : C), ] (X : Cᵒᵖ) (W : (J.cover (opposite.unop X))ᵒᵖ) {X' : E} (f' : (J.plus_obj (P F)).obj X X') :
@[simp]
theorem category_theory.grothendieck_topology.ι_plus_comp_iso_hom {C : Type u} {D : Type w₁} {E : Type w₂} (F : D E) [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (α β : Type (max v u)) (fst snd : β → α), ] [Π (X : C) (W : J.cover X) (P : Cᵒᵖ D), ] (P : Cᵒᵖ D) [∀ (X : C), ] [∀ (X : C), ] [Π (X : C), ] (X : Cᵒᵖ) (W : (J.cover (opposite.unop X))ᵒᵖ) :
@[simp]
theorem category_theory.grothendieck_topology.plus_comp_iso_whisker_left_assoc {C : Type u} {D : Type w₁} {E : Type w₂} [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (X : C), ] [∀ (X : C), ] {F G : D E} (η : F G) (P : Cᵒᵖ D) [Π (X : C), ] [Π (X : C) (W : J.cover X) (P : Cᵒᵖ D), ] [Π (X : C), ] [Π (X : C) (W : J.cover X) (P : Cᵒᵖ D), ] {X' : Cᵒᵖ E} (f' : J.plus_obj (P G) X') :
(J.plus_comp_iso G P).hom f' = (J.plus_comp_iso F P).hom f'
@[simp]
theorem category_theory.grothendieck_topology.plus_comp_iso_whisker_left {C : Type u} {D : Type w₁} {E : Type w₂} [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (X : C), ] [∀ (X : C), ] {F G : D E} (η : F G) (P : Cᵒᵖ D) [Π (X : C), ] [Π (X : C) (W : J.cover X) (P : Cᵒᵖ D), ] [Π (X : C), ] [Π (X : C) (W : J.cover X) (P : Cᵒᵖ D), ] :
@[simp]
theorem category_theory.grothendieck_topology.plus_functor_whisker_left_iso_hom_app {C : Type u} {D : Type w₁} {E : Type w₂} [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (X : C), ] [∀ (X : C), ] (P : Cᵒᵖ D) [Π (F : D E) (X : C), ] [Π (F : D E) (X : C) (W : J.cover X) (P : Cᵒᵖ D), ] (X : D E) :
X = (J.plus_comp_iso X P).hom
@[simp]
theorem category_theory.grothendieck_topology.plus_functor_whisker_left_iso_inv_app {C : Type u} {D : Type w₁} {E : Type w₂} [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (X : C), ] [∀ (X : C), ] (P : Cᵒᵖ D) [Π (F : D E) (X : C), ] [Π (F : D E) (X : C) (W : J.cover X) (P : Cᵒᵖ D), ] (X : D E) :
X = (J.plus_comp_iso X P).inv
noncomputable def category_theory.grothendieck_topology.plus_functor_whisker_left_iso {C : Type u} {D : Type w₁} {E : Type w₂} [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (X : C), ] [∀ (X : C), ] (P : Cᵒᵖ D) [Π (F : D E) (X : C), ] [Π (F : D E) (X : C) (W : J.cover X) (P : Cᵒᵖ D), ] :

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

Equations
@[simp]
theorem category_theory.grothendieck_topology.plus_comp_iso_whisker_right {C : Type u} {D : Type w₁} {E : Type w₂} (F : D E) [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (α β : Type (max v u)) (fst snd : β → α), ] [Π (X : C) (W : J.cover X) (P : Cᵒᵖ D), ] [∀ (X : C), ] [∀ (X : C), ] [Π (X : C), ] {P Q : Cᵒᵖ D} (η : P Q) :
@[simp]
theorem category_theory.grothendieck_topology.plus_comp_iso_whisker_right_assoc {C : Type u} {D : Type w₁} {E : Type w₂} (F : D E) [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (α β : Type (max v u)) (fst snd : β → α), ] [Π (X : C) (W : J.cover X) (P : Cᵒᵖ D), ] [∀ (X : C), ] [∀ (X : C), ] [Π (X : C), ] {P Q : Cᵒᵖ D} (η : P Q) {X' : Cᵒᵖ E} (f' : J.plus_obj (Q F) X') :
(J.plus_comp_iso F Q).hom f' = (J.plus_comp_iso F P).hom f'
noncomputable def category_theory.grothendieck_topology.plus_functor_whisker_right_iso {C : Type u} {D : Type w₁} {E : Type w₂} (F : D E) [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (α β : Type (max v u)) (fst snd : β → α), ] [Π (X : C) (W : J.cover X) (P : Cᵒᵖ D), ] [∀ (X : C), ] [∀ (X : C), ] [Π (X : C), ] :

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

Equations
@[simp]
theorem category_theory.grothendieck_topology.plus_functor_whisker_right_iso_inv_app {C : Type u} {D : Type w₁} {E : Type w₂} (F : D E) [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (α β : Type (max v u)) (fst snd : β → α), ] [Π (X : C) (W : J.cover X) (P : Cᵒᵖ D), ] [∀ (X : C), ] [∀ (X : C), ] [Π (X : C), ] (X : Cᵒᵖ D) :
X = (J.plus_comp_iso F X).inv
@[simp]
theorem category_theory.grothendieck_topology.plus_functor_whisker_right_iso_hom_app {C : Type u} {D : Type w₁} {E : Type w₂} (F : D E) [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (α β : Type (max v u)) (fst snd : β → α), ] [Π (X : C) (W : J.cover X) (P : Cᵒᵖ D), ] [∀ (X : C), ] [∀ (X : C), ] [Π (X : C), ] (X : Cᵒᵖ D) :
X = (J.plus_comp_iso F X).hom
@[simp]
theorem category_theory.grothendieck_topology.whisker_right_to_plus_comp_plus_comp_iso_hom_assoc {C : Type u} {D : Type w₁} {E : Type w₂} (F : D E) [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (α β : Type (max v u)) (fst snd : β → α), ] [Π (X : C) (W : J.cover X) (P : Cᵒᵖ D), ] (P : Cᵒᵖ D) [∀ (X : C), ] [∀ (X : C), ] [Π (X : C), ] {X' : Cᵒᵖ E} (f' : J.plus_obj (P F) X') :
(J.plus_comp_iso F P).hom f' = J.to_plus (P F) f'
@[simp]
theorem category_theory.grothendieck_topology.whisker_right_to_plus_comp_plus_comp_iso_hom {C : Type u} {D : Type w₁} {E : Type w₂} (F : D E) [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (α β : Type (max v u)) (fst snd : β → α), ] [Π (X : C) (W : J.cover X) (P : Cᵒᵖ D), ] (P : Cᵒᵖ D) [∀ (X : C), ] [∀ (X : C), ] [Π (X : C), ] :
(J.plus_comp_iso F P).hom = J.to_plus (P F)
@[simp]
theorem category_theory.grothendieck_topology.to_plus_comp_plus_comp_iso_inv {C : Type u} {D : Type w₁} {E : Type w₂} (F : D E) [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (α β : Type (max v u)) (fst snd : β → α), ] [Π (X : C) (W : J.cover X) (P : Cᵒᵖ D), ] (P : Cᵒᵖ D) [∀ (X : C), ] [∀ (X : C), ] [Π (X : C), ] :
J.to_plus (P F) (J.plus_comp_iso F P).inv =
theorem category_theory.grothendieck_topology.plus_comp_iso_inv_eq_plus_lift {C : Type u} {D : Type w₁} {E : Type w₂} (F : D E) [∀ (α β : Type (max v u)) (fst snd : β → α), ] [∀ (α β : Type (max v u)) (fst snd : β → α), ] [Π (X : C) (W : J.cover X) (P : Cᵒᵖ D), ] (P : Cᵒᵖ D) [∀ (X : C), ] [∀ (X : C), ] [Π (X : C), ] (hP : (J.plus_obj P F)) :
(J.plus_comp_iso F P).inv = J.plus_lift F) hP