# mathlibdocumentation

category_theory.sites.left_exact

# Left exactness of sheafification #

In this file we show that sheafification commutes with finite limits.

@[simp]
theorem category_theory.grothendieck_topology.cone_comp_evaluation_of_cone_comp_diagram_functor_comp_evaluation_π_app {C : Type (max v u)} {D : Type w} [∀ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] {X : C} {K : Type (max v u)} {F : K Cᵒᵖ D} {W : J.cover X} (i : W.arrow) (E : category_theory.limits.cone (F X D).obj (opposite.op W))) (k : K) :
@[simp]
theorem category_theory.grothendieck_topology.cone_comp_evaluation_of_cone_comp_diagram_functor_comp_evaluation_X {C : Type (max v u)} {D : Type w} [∀ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] {X : C} {K : Type (max v u)} {F : K Cᵒᵖ D} {W : J.cover X} (i : W.arrow) (E : category_theory.limits.cone (F X D).obj (opposite.op W))) :
noncomputable def category_theory.grothendieck_topology.cone_comp_evaluation_of_cone_comp_diagram_functor_comp_evaluation {C : Type (max v u)} {D : Type w} [∀ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] {X : C} {K : Type (max v u)} {F : K Cᵒᵖ D} {W : J.cover X} (i : W.arrow) (E : category_theory.limits.cone (F X D).obj (opposite.op W))) :

An auxiliary definition to be used in the proof of the fact that J.diagram_functor D X preserves limits.

Equations
@[reducible]
noncomputable def category_theory.grothendieck_topology.lift_to_diagram_limit_obj {C : Type (max v u)} {D : Type w} [∀ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] {X : C} {K : Type (max v u)} {W : (J.cover X)ᵒᵖ} (F : K Cᵒᵖ D) (E : category_theory.limits.cone (F X D).obj W)) :
E.X X).obj W

An auxiliary definition to be used in the proof of the fact that J.diagram_functor D X preserves limits.

@[protected, instance]
noncomputable def category_theory.grothendieck_topology.diagram_functor.category_theory.limits.preserves_limit {C : Type (max v u)} {D : Type w} [∀ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] (X : C) (K : Type (max v u)) (F : K Cᵒᵖ D) :
Equations
@[protected, instance]
noncomputable def category_theory.grothendieck_topology.diagram_functor.category_theory.limits.preserves_limits_of_shape {C : Type (max v u)} {D : Type w} [∀ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] (X : C) (K : Type (max v u))  :
Equations
@[protected, instance]
noncomputable def category_theory.grothendieck_topology.diagram_functor.category_theory.limits.preserves_limits {C : Type (max v u)} {D : Type w} [∀ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] (X : C)  :
Equations
noncomputable def category_theory.grothendieck_topology.lift_to_plus_obj_limit_obj {C : Type (max v u)} {D : Type w} [∀ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [∀ (X : C), ] [Π (X : C), ] {K : Type (max v u)} (F : K Cᵒᵖ D) (X : C) (S : category_theory.limits.cone (F J.plus_functor D (opposite.op X))) :

An auxiliary definition to be used in the proof that J.plus_functor D commutes with finite limits.

Equations
theorem category_theory.grothendieck_topology.lift_to_plus_obj_limit_obj_fac {C : Type (max v u)} {D : Type w} [∀ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [∀ (X : C), ] [Π (X : C), ] {K : Type (max v u)} (F : K Cᵒᵖ D) (X : C) (S : category_theory.limits.cone (F J.plus_functor D (opposite.op X))) (k : K) :
@[protected, instance]
noncomputable def category_theory.grothendieck_topology.plus_functor.category_theory.limits.preserves_limits_of_shape {C : Type (max v u)} {D : Type w} [∀ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [∀ (X : C), ] [Π (X : C), ] (K : Type (max v u))  :
Equations
@[protected, instance]
noncomputable def category_theory.grothendieck_topology.plus_functor.category_theory.limits.preserves_finite_limits {C : Type (max v u)} {D : Type w} [∀ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [∀ (X : C), ] [Π (X : C), ]  :
Equations
@[protected, instance]
noncomputable def category_theory.grothendieck_topology.sheafification.category_theory.limits.preserves_limits_of_shape {C : Type (max v u)} {D : Type w} [∀ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [∀ (X : C), ] [Π (X : C), ] (K : Type (max v u))  :
Equations
@[protected, instance]
noncomputable def category_theory.grothendieck_topology.sheafification.category_theory.limits.preserves_finite_limits {C : Type (max v u)} {D : Type w} [∀ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [∀ (X : C), ] [Π (X : C), ]  :
Equations
@[protected, instance]
noncomputable def category_theory.presheaf_to_Sheaf.limits.preserves_limits_of_shape {C : Type (max v u)} {D : Type w} [∀ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [∀ (X : C), ] [Π (X : C), ] (K : Type (max v u))  :
Equations
@[protected, instance]
noncomputable def category_theory.presheaf_to_Sheaf.limits.preserves_finite_limits {C : Type (max v u)} {D : Type w} [∀ (P : Cᵒᵖ D) (X : C) (S : J.cover X), ] [∀ (X : C), ] [Π (X : C), ]  :
Equations