Left exactness of sheafification

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

@[simp]

theorem CategoryTheory.GrothendieckTopology.coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation_pt {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] {X : C} {K : Type (max v u)} [CategoryTheory.SmallCategory K] {F : CategoryTheory.Functor K (CategoryTheory.Functor Cᵒᵖ D)} {W : CategoryTheory.GrothendieckTopology.Cover J X} (i : CategoryTheory.GrothendieckTopology.Cover.Arrow W) (E : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F (CategoryTheory.Functor.comp (CategoryTheory.GrothendieckTopology.diagramFunctor J D X) ((CategoryTheory.evaluation (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D).obj (Opposite.op W))))) : (CategoryTheory.GrothendieckTopology.coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation i E).pt = E.pt

@[simp]

theorem CategoryTheory.GrothendieckTopology.coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation_π_app {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] {X : C} {K : Type (max v u)} [CategoryTheory.SmallCategory K] {F : CategoryTheory.Functor K (CategoryTheory.Functor Cᵒᵖ D)} {W : CategoryTheory.GrothendieckTopology.Cover J X} (i : CategoryTheory.GrothendieckTopology.Cover.Arrow W) (E : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F (CategoryTheory.Functor.comp (CategoryTheory.GrothendieckTopology.diagramFunctor J D X) ((CategoryTheory.evaluation (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D).obj (Opposite.op W))))) (k : K) : (CategoryTheory.GrothendieckTopology.coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation i E).π.app k = CategoryTheory.CategoryStruct.comp (E.π.app k) (CategoryTheory.Limits.Multiequalizer.ι (CategoryTheory.GrothendieckTopology.Cover.index W (F.obj k)) i)

def CategoryTheory.GrothendieckTopology.coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] {X : C} {K : Type (max v u)} [CategoryTheory.SmallCategory K] {F : CategoryTheory.Functor K (CategoryTheory.Functor Cᵒᵖ D)} {W : CategoryTheory.GrothendieckTopology.Cover J X} (i : CategoryTheory.GrothendieckTopology.Cover.Arrow W) (E : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F (CategoryTheory.Functor.comp (CategoryTheory.GrothendieckTopology.diagramFunctor J D X) ((CategoryTheory.evaluation (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D).obj (Opposite.op W))))) : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F ((CategoryTheory.evaluation Cᵒᵖ D).obj (Opposite.op i.Y)))

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

@[inline, reducible]

abbrev CategoryTheory.GrothendieckTopology.liftToDiagramLimitObj {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] {X : C} {K : Type (max v u)} [CategoryTheory.SmallCategory K] [CategoryTheory.Limits.HasLimitsOfShape K D] {W : (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ} (F : CategoryTheory.Functor K (CategoryTheory.Functor Cᵒᵖ D)) (E : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F (CategoryTheory.Functor.comp (CategoryTheory.GrothendieckTopology.diagramFunctor J D X) ((CategoryTheory.evaluation (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D).obj W)))) : E.pt ⟶ (CategoryTheory.GrothendieckTopology.diagram J (CategoryTheory.Limits.limit F) X).obj W

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

instance CategoryTheory.GrothendieckTopology.preservesLimit_diagramFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] (X : C) (K : Type (max v u)) [CategoryTheory.SmallCategory K] [CategoryTheory.Limits.HasLimitsOfShape K D] (F : CategoryTheory.Functor K (CategoryTheory.Functor Cᵒᵖ D)) : CategoryTheory.Limits.PreservesLimit F (CategoryTheory.GrothendieckTopology.diagramFunctor J D X)

instance CategoryTheory.GrothendieckTopology.preservesLimitsOfShape_diagramFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] (X : C) (K : Type (max v u)) [CategoryTheory.SmallCategory K] [CategoryTheory.Limits.HasLimitsOfShape K D] : CategoryTheory.Limits.PreservesLimitsOfShape K (CategoryTheory.GrothendieckTopology.diagramFunctor J D X)

instance CategoryTheory.GrothendieckTopology.preservesLimits_diagramFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] (X : C) [CategoryTheory.Limits.HasLimits D] : CategoryTheory.Limits.PreservesLimits (CategoryTheory.GrothendieckTopology.diagramFunctor J D X)

def CategoryTheory.GrothendieckTopology.liftToPlusObjLimitObj {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [CategoryTheory.ConcreteCategory D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] {K : Type (max v u)} [CategoryTheory.SmallCategory K] [CategoryTheory.FinCategory K] [CategoryTheory.Limits.HasLimitsOfShape K D] [CategoryTheory.Limits.PreservesLimitsOfShape K (CategoryTheory.forget D)] [CategoryTheory.Limits.ReflectsLimitsOfShape K (CategoryTheory.forget D)] (F : CategoryTheory.Functor K (CategoryTheory.Functor Cᵒᵖ D)) (X : C) (S : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F (CategoryTheory.Functor.comp (CategoryTheory.GrothendieckTopology.plusFunctor J D) ((CategoryTheory.evaluation Cᵒᵖ D).obj (Opposite.op X))))) : S.pt ⟶ (CategoryTheory.GrothendieckTopology.plusObj J (CategoryTheory.Limits.limit F)).obj (Opposite.op X)

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

theorem CategoryTheory.GrothendieckTopology.liftToPlusObjLimitObj_fac {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [CategoryTheory.ConcreteCategory D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] {K : Type (max v u)} [CategoryTheory.SmallCategory K] [CategoryTheory.FinCategory K] [CategoryTheory.Limits.HasLimitsOfShape K D] [CategoryTheory.Limits.PreservesLimitsOfShape K (CategoryTheory.forget D)] [CategoryTheory.Limits.ReflectsLimitsOfShape K (CategoryTheory.forget D)] (F : CategoryTheory.Functor K (CategoryTheory.Functor Cᵒᵖ D)) (X : C) (S : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F (CategoryTheory.Functor.comp (CategoryTheory.GrothendieckTopology.plusFunctor J D) ((CategoryTheory.evaluation Cᵒᵖ D).obj (Opposite.op X))))) (k : K) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.liftToPlusObjLimitObj F X S) ((CategoryTheory.GrothendieckTopology.plusMap J (CategoryTheory.Limits.limit.π F k)).app (Opposite.op X)) = S.π.app k

instance CategoryTheory.GrothendieckTopology.preservesLimitsOfShape_plusFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [CategoryTheory.ConcreteCategory D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] (K : Type (max v u)) [CategoryTheory.SmallCategory K] [CategoryTheory.FinCategory K] [CategoryTheory.Limits.HasLimitsOfShape K D] [CategoryTheory.Limits.PreservesLimitsOfShape K (CategoryTheory.forget D)] [CategoryTheory.Limits.ReflectsLimitsOfShape K (CategoryTheory.forget D)] : CategoryTheory.Limits.PreservesLimitsOfShape K (CategoryTheory.GrothendieckTopology.plusFunctor J D)

instance CategoryTheory.GrothendieckTopology.preserveFiniteLimits_plusFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [CategoryTheory.ConcreteCategory D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.Limits.HasFiniteLimits D] [CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] : CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.GrothendieckTopology.plusFunctor J D)

instance CategoryTheory.GrothendieckTopology.preservesLimitsOfShape_sheafification {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [CategoryTheory.ConcreteCategory D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] (K : Type (max v u)) [CategoryTheory.SmallCategory K] [CategoryTheory.FinCategory K] [CategoryTheory.Limits.HasLimitsOfShape K D] [CategoryTheory.Limits.PreservesLimitsOfShape K (CategoryTheory.forget D)] [CategoryTheory.Limits.ReflectsLimitsOfShape K (CategoryTheory.forget D)] : CategoryTheory.Limits.PreservesLimitsOfShape K (CategoryTheory.GrothendieckTopology.sheafification J D)

instance CategoryTheory.GrothendieckTopology.preservesFiniteLimits_sheafification {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [CategoryTheory.ConcreteCategory D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.Limits.HasFiniteLimits D] [CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] : CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.GrothendieckTopology.sheafification J D)

instance CategoryTheory.preservesLimitsOfShape_presheafToSheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [CategoryTheory.ConcreteCategory D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] (K : Type (max v u)) [CategoryTheory.SmallCategory K] [CategoryTheory.FinCategory K] [CategoryTheory.Limits.HasLimitsOfShape K D] : CategoryTheory.Limits.PreservesLimitsOfShape K (CategoryTheory.presheafToSheaf J D)

instance CategoryTheory.preservesfiniteLimits_presheafToSheaf {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{max v u, w} D] [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : CategoryTheory.GrothendieckTopology.Cover J X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ D] [CategoryTheory.ConcreteCategory D] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover J X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget D)] [CategoryTheory.Limits.HasFiniteLimits D] : CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.presheafToSheaf J D)