Left exactness of sheafification

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

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 : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] {X : C} {K : Type (max v u)} [CategoryTheory.SmallCategory K] {F : CategoryTheory.Functor K (CategoryTheory.Functor Cᵒᵖ D)} {W : J.Cover X} (i : W.Arrow) (E : CategoryTheory.Limits.Cone (F.comp ((J.diagramFunctor D X).comp ((CategoryTheory.evaluation (J.Cover X)ᵒᵖ D).obj (Opposite.op W))))) : CategoryTheory.Limits.Cone (F.comp ((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.

Equations

• One or more equations did not get rendered due to their size.

@[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 : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] {X : C} {K : Type (max v u)} [CategoryTheory.SmallCategory K] {F : CategoryTheory.Functor K (CategoryTheory.Functor Cᵒᵖ D)} {W : J.Cover X} (i : W.Arrow) (E : CategoryTheory.Limits.Cone (F.comp ((J.diagramFunctor D X).comp ((CategoryTheory.evaluation (J.Cover X)ᵒᵖ D).obj (Opposite.op W))))) (k : K) : (CategoryTheory.GrothendieckTopology.coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation i E).π.app k = CategoryTheory.CategoryStruct.comp (E.π.app k) (CategoryTheory.Limits.Multiequalizer.ι (W.index (F.obj k)) i)

@[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 : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] {X : C} {K : Type (max v u)} [CategoryTheory.SmallCategory K] {F : CategoryTheory.Functor K (CategoryTheory.Functor Cᵒᵖ D)} {W : J.Cover X} (i : W.Arrow) (E : CategoryTheory.Limits.Cone (F.comp ((J.diagramFunctor D X).comp ((CategoryTheory.evaluation (J.Cover X)ᵒᵖ D).obj (Opposite.op W))))) : (CategoryTheory.GrothendieckTopology.coneCompEvaluationOfConeCompDiagramFunctorCompEvaluation i E).pt = E.pt

def CategoryTheory.GrothendieckTopology.liftToDiagramLimitObjAux {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 : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] {X : C} {K : Type (max v u)} [CategoryTheory.SmallCategory K] [CategoryTheory.Limits.HasLimitsOfShape K D] {W : (J.Cover X)ᵒᵖ} (F : CategoryTheory.Functor K (CategoryTheory.Functor Cᵒᵖ D)) (E : CategoryTheory.Limits.Cone (F.comp ((J.diagramFunctor D X).comp ((CategoryTheory.evaluation (J.Cover X)ᵒᵖ D).obj W)))) (i : (Opposite.unop W).Arrow) : E.pt ⟶ (CategoryTheory.Limits.limit F).obj (Opposite.op i.Y)

Auxiliary definition for liftToDiagramLimitObj.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.GrothendieckTopology.liftToDiagramLimitObjAux_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 : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] {X : C} {K : Type (max v u)} [CategoryTheory.SmallCategory K] [CategoryTheory.Limits.HasLimitsOfShape K D] {W : (J.Cover X)ᵒᵖ} (F : CategoryTheory.Functor K (CategoryTheory.Functor Cᵒᵖ D)) (E : CategoryTheory.Limits.Cone (F.comp ((J.diagramFunctor D X).comp ((CategoryTheory.evaluation (J.Cover X)ᵒᵖ D).obj W)))) (i : (Opposite.unop W).Arrow) (k : K) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.liftToDiagramLimitObjAux F E i) ((CategoryTheory.Limits.limit.π F k).app (Opposite.op i.Y)) = CategoryTheory.CategoryStruct.comp (E.π.app k) (CategoryTheory.Limits.Multiequalizer.ι ((Opposite.unop W).index (F.obj k)) i)

@[simp]

theorem CategoryTheory.GrothendieckTopology.liftToDiagramLimitObjAux_fac_assoc {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 : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] {X : C} {K : Type (max v u)} [CategoryTheory.SmallCategory K] [CategoryTheory.Limits.HasLimitsOfShape K D] {W : (J.Cover X)ᵒᵖ} (F : CategoryTheory.Functor K (CategoryTheory.Functor Cᵒᵖ D)) (E : CategoryTheory.Limits.Cone (F.comp ((J.diagramFunctor D X).comp ((CategoryTheory.evaluation (J.Cover X)ᵒᵖ D).obj W)))) (i : (Opposite.unop W).Arrow) (k : K) {Z : D} (h : (F.obj k).obj (Opposite.op i.Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.liftToDiagramLimitObjAux F E i) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.limit.π F k).app (Opposite.op i.Y)) h) = CategoryTheory.CategoryStruct.comp (E.π.app k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι ((Opposite.unop W).index (F.obj k)) i) h)

@[reducible, inline]

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 : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] {X : C} {K : Type (max v u)} [CategoryTheory.SmallCategory K] [CategoryTheory.Limits.HasLimitsOfShape K D] {W : (J.Cover X)ᵒᵖ} (F : CategoryTheory.Functor K (CategoryTheory.Functor Cᵒᵖ D)) (E : CategoryTheory.Limits.Cone (F.comp ((J.diagramFunctor D X).comp ((CategoryTheory.evaluation (J.Cover X)ᵒᵖ D).obj W)))) : E.pt ⟶ (J.diagram (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.

Equations

• One or more equations did not get rendered due to their size.

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 : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index 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 (J.diagramFunctor 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 : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] (X : C) (K : Type (max v u)) [CategoryTheory.SmallCategory K] [CategoryTheory.Limits.HasLimitsOfShape K D] : CategoryTheory.Limits.PreservesLimitsOfShape K (J.diagramFunctor 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 : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] (X : C) [CategoryTheory.Limits.HasLimits D] : CategoryTheory.Limits.PreservesLimits (J.diagramFunctor 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 : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [CategoryTheory.ConcreteCategory D] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover 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 (F.comp ((J.plusFunctor D).comp ((CategoryTheory.evaluation Cᵒᵖ D).obj (Opposite.op X))))) : S.pt ⟶ (J.plusObj (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.

Equations

• One or more equations did not get rendered due to their size.

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 : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [CategoryTheory.ConcreteCategory D] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover 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 (F.comp ((J.plusFunctor D).comp ((CategoryTheory.evaluation Cᵒᵖ D).obj (Opposite.op X))))) (k : K) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.liftToPlusObjLimitObj F X S) ((J.plusMap (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 : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [CategoryTheory.ConcreteCategory D] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover 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 (J.plusFunctor 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 : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [CategoryTheory.ConcreteCategory D] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.Limits.HasFiniteLimits D] [CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.forget D)] [(CategoryTheory.forget D).ReflectsIsomorphisms] : CategoryTheory.Limits.PreservesFiniteLimits (J.plusFunctor 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 : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [CategoryTheory.ConcreteCategory D] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover 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 (J.sheafification 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 : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [CategoryTheory.ConcreteCategory D] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.Limits.HasFiniteLimits D] [CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.forget D)] [(CategoryTheory.forget D).ReflectsIsomorphisms] : CategoryTheory.Limits.PreservesFiniteLimits (J.sheafification 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 : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [CategoryTheory.ConcreteCategory D] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [(CategoryTheory.forget D).ReflectsIsomorphisms] (K : Type w') [CategoryTheory.SmallCategory K] [CategoryTheory.FinCategory K] [CategoryTheory.Limits.HasLimitsOfShape K D] : CategoryTheory.Limits.PreservesLimitsOfShape K (CategoryTheory.plusPlusSheaf 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 : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [CategoryTheory.ConcreteCategory D] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [(CategoryTheory.forget D).ReflectsIsomorphisms] [CategoryTheory.Limits.HasFiniteLimits D] : CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.plusPlusSheaf J D)

def CategoryTheory.plusPlusSheafIsoPresheafToSheaf {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 : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [CategoryTheory.ConcreteCategory D] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [(CategoryTheory.forget D).ReflectsIsomorphisms] : CategoryTheory.plusPlusSheaf J D ≅ CategoryTheory.presheafToSheaf J D

plusPlusSheaf is isomorphic to an arbitrary choice of left adjoint.

Equations

• CategoryTheory.plusPlusSheafIsoPresheafToSheaf J D = (CategoryTheory.plusPlusAdjunction J D).leftAdjointUniq (CategoryTheory.sheafificationAdjunction J D)

def CategoryTheory.plusPlusFunctorIsoSheafification {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 : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [CategoryTheory.ConcreteCategory D] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [(CategoryTheory.forget D).ReflectsIsomorphisms] : J.sheafification D ≅ CategoryTheory.sheafification J D

plusPlusFunctor is isomorphic to sheafification.

Equations

• CategoryTheory.plusPlusFunctorIsoSheafification J D = CategoryTheory.isoWhiskerRight (CategoryTheory.plusPlusSheafIsoPresheafToSheaf J D) (CategoryTheory.sheafToPresheaf J D)

def CategoryTheory.plusPlusIsoSheafify {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 : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [CategoryTheory.ConcreteCategory D] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [(CategoryTheory.forget D).ReflectsIsomorphisms] (P : CategoryTheory.Functor Cᵒᵖ D) : J.sheafify P ≅ CategoryTheory.sheafify J P

plusPlus is isomorphic to sheafify.

Equations

• CategoryTheory.plusPlusIsoSheafify J D P = (CategoryTheory.sheafToPresheaf J D).mapIso ((CategoryTheory.plusPlusSheafIsoPresheafToSheaf J D).app P)

@[simp]

theorem CategoryTheory.toSheafify_plusPlusIsoSheafify_hom {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 : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [CategoryTheory.ConcreteCategory D] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [(CategoryTheory.forget D).ReflectsIsomorphisms] (P : CategoryTheory.Functor Cᵒᵖ D) : CategoryTheory.CategoryStruct.comp (J.toSheafify P) (CategoryTheory.plusPlusIsoSheafify J D P).hom = CategoryTheory.toSheafify J P

@[simp]

theorem CategoryTheory.toSheafify_plusPlusIsoSheafify_hom_assoc {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 : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [CategoryTheory.ConcreteCategory D] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [(CategoryTheory.forget D).ReflectsIsomorphisms] (P : CategoryTheory.Functor Cᵒᵖ D) {Z : CategoryTheory.Functor Cᵒᵖ D} (h : CategoryTheory.sheafify J P ⟶ Z) : CategoryTheory.CategoryStruct.comp (J.toSheafify P) (CategoryTheory.CategoryStruct.comp (CategoryTheory.plusPlusIsoSheafify J D P).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J P) h

instance CategoryTheory.instHasSheafifyOfHasFiniteLimits {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 : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)] [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [CategoryTheory.ConcreteCategory D] [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)] [(CategoryTheory.forget D).ReflectsIsomorphisms] [CategoryTheory.Limits.HasFiniteLimits D] : CategoryTheory.HasSheafify J D

instance CategoryTheory.instFinitaryExtensiveSheafOfHasPullbacksOfHasSheafify {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] [CategoryTheory.FinitaryExtensive D] [CategoryTheory.Limits.HasPullbacks D] [CategoryTheory.HasSheafify J D] : CategoryTheory.FinitaryExtensive (CategoryTheory.Sheaf J D)

instance CategoryTheory.instAdhesiveSheafOfHasPullbacksOfHasPushoutsOfHasSheafify {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w} [CategoryTheory.Category.{w', w} D] [CategoryTheory.Adhesive D] [CategoryTheory.Limits.HasPullbacks D] [CategoryTheory.Limits.HasPushouts D] [CategoryTheory.HasSheafify J D] : CategoryTheory.Adhesive (CategoryTheory.Sheaf J D)

instance CategoryTheory.SheafOfTypes.finitary_extensive {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasSheafify J (Type w)] : CategoryTheory.FinitaryExtensive (CategoryTheory.Sheaf J (Type w))

instance CategoryTheory.SheafOfTypes.adhesive {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasSheafify J (Type w)] : CategoryTheory.Adhesive (CategoryTheory.Sheaf J (Type w))

instance CategoryTheory.SheafOfTypes.balanced {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasSheafify J (Type w)] : CategoryTheory.Balanced (CategoryTheory.Sheaf J (Type w))