Left exactness of sheafification

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

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

@[simp]

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

@[simp]

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

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

Auxiliary definition for liftToDiagramLimitObj.

@[simp]

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

@[simp]

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

@[reducible, inline]

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

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

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

def CategoryTheory.GrothendieckTopology.liftToPlusObjLimitObj {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{t, w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [HasForget D] [∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)] [∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ] {K : Type s} [SmallCategory K] [FinCategory K] [Limits.HasLimitsOfShape K D] [Limits.PreservesLimitsOfShape K (forget D)] [Limits.ReflectsLimitsOfShape K (forget D)] (F : Functor K (Functor Cᵒᵖ D)) (X : C) (S : Limits.Cone (F.comp ((J.plusFunctor D).comp ((evaluation Cᵒᵖ D).obj (Opposite.op X))))) : S.pt ⟶ (J.plusObj (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} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{t, w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] [HasForget D] [∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)] [∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ] {K : Type s} [SmallCategory K] [FinCategory K] [Limits.HasLimitsOfShape K D] [Limits.PreservesLimitsOfShape K (forget D)] [Limits.ReflectsLimitsOfShape K (forget D)] (F : Functor K (Functor Cᵒᵖ D)) (X : C) (S : Limits.Cone (F.comp ((J.plusFunctor D).comp ((evaluation Cᵒᵖ D).obj (Opposite.op X))))) (k : K) : CategoryStruct.comp (liftToPlusObjLimitObj F X S) ((J.plusMap (Limits.limit.π F k)).app (Opposite.op X)) = S.π.app k

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

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

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

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

instance CategoryTheory.preservesLimitsOfShape_presheafToSheaf {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{t, w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory D FD] [∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)] [(forget D).ReflectsIsomorphisms] [∀ {X : C} (S : J.Cover X), Limits.PreservesLimitsOfShape (Limits.WalkingMulticospan S.shape) (forget D)] (K : Type w') [SmallCategory K] [FinCategory K] [Limits.HasLimitsOfShape K D] [Limits.PreservesLimits (forget D)] [∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ] : Limits.PreservesLimitsOfShape K (plusPlusSheaf J D)

instance CategoryTheory.preservesFiniteLimits_presheafToSheaf {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type w} [Category.{t, w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory D FD] [∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)] [(forget D).ReflectsIsomorphisms] [∀ {X : C} (S : J.Cover X), Limits.PreservesLimitsOfShape (Limits.WalkingMulticospan S.shape) (forget D)] [Limits.PreservesLimits (forget D)] [∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ] [Limits.HasFiniteLimits D] : Limits.PreservesFiniteLimits (plusPlusSheaf J D)

def CategoryTheory.plusPlusSheafIsoPresheafToSheaf {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{t, w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory D FD] [∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)] [(forget D).ReflectsIsomorphisms] [∀ {X : C} (S : J.Cover X), Limits.PreservesLimitsOfShape (Limits.WalkingMulticospan S.shape) (forget D)] : plusPlusSheaf J D ≅ presheafToSheaf J D

plusPlusSheaf is isomorphic to an arbitrary choice of left adjoint.

def CategoryTheory.plusPlusFunctorIsoSheafification {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{t, w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory D FD] [∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)] [(forget D).ReflectsIsomorphisms] [∀ {X : C} (S : J.Cover X), Limits.PreservesLimitsOfShape (Limits.WalkingMulticospan S.shape) (forget D)] : J.sheafification D ≅ sheafification J D

plusPlusFunctor is isomorphic to sheafification.

def CategoryTheory.plusPlusIsoSheafify {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{t, w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory D FD] [∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)] [(forget D).ReflectsIsomorphisms] [∀ {X : C} (S : J.Cover X), Limits.PreservesLimitsOfShape (Limits.WalkingMulticospan S.shape) (forget D)] (P : Functor Cᵒᵖ D) : J.sheafify P ≅ sheafify J P

plusPlus is isomorphic to sheafify.

@[simp]

theorem CategoryTheory.toSheafify_plusPlusIsoSheafify_hom {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{t, w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory D FD] [∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)] [(forget D).ReflectsIsomorphisms] [∀ {X : C} (S : J.Cover X), Limits.PreservesLimitsOfShape (Limits.WalkingMulticospan S.shape) (forget D)] (P : Functor Cᵒᵖ D) : CategoryStruct.comp (J.toSheafify P) (plusPlusIsoSheafify J D P).hom = toSheafify J P

@[simp]

theorem CategoryTheory.toSheafify_plusPlusIsoSheafify_hom_assoc {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{t, w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory D FD] [∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)] [(forget D).ReflectsIsomorphisms] [∀ {X : C} (S : J.Cover X), Limits.PreservesLimitsOfShape (Limits.WalkingMulticospan S.shape) (forget D)] (P : Functor Cᵒᵖ D) {Z : Functor Cᵒᵖ D} (h : sheafify J P ⟶ Z) : CategoryStruct.comp (J.toSheafify P) (CategoryStruct.comp (plusPlusIsoSheafify J D P).hom h) = CategoryStruct.comp (toSheafify J P) h

instance CategoryTheory.instHasSheafifyOfPreservesLimitsForgetOfHasFiniteLimitsOfSmallOppositeCover {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{t, w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {FD : D → D → Type u_1} {CD : D → Type t} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory D FD] [∀ (X : C), Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)] [(forget D).ReflectsIsomorphisms] [∀ {X : C} (S : J.Cover X), Limits.PreservesLimitsOfShape (Limits.WalkingMulticospan S.shape) (forget D)] [Limits.PreservesLimits (forget D)] [Limits.HasFiniteLimits D] [∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ] : HasSheafify J D

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

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

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

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

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