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).toPrefunctor.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).toPrefunctor.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.toPrefunctor.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).toPrefunctor.obj (Opposite.op W))))) : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp F ((CategoryTheory.evaluation Cᵒᵖ D).toPrefunctor.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.

@[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).toPrefunctor.obj W)))) : E.pt ⟶ (CategoryTheory.GrothendieckTopology.diagram J (CategoryTheory.Limits.limit F) X).toPrefunctor.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 : 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)

Equations

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

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)

Equations

• CategoryTheory.GrothendieckTopology.preservesLimitsOfShape_diagramFunctor X K = CategoryTheory.Limits.PreservesLimitsOfShape.mk

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)

Equations

• CategoryTheory.GrothendieckTopology.preservesLimits_diagramFunctor X = CategoryTheory.Limits.PreservesLimitsOfSize.mk

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).toPrefunctor.obj (Opposite.op X))))) : S.pt ⟶ (CategoryTheory.GrothendieckTopology.plusObj J (CategoryTheory.Limits.limit F)).toPrefunctor.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 : 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).toPrefunctor.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)

Equations

• CategoryTheory.GrothendieckTopology.preservesLimitsOfShape_plusFunctor K = CategoryTheory.Limits.PreservesLimitsOfShape.mk

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)

Equations

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

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)

Equations

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

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)

Equations

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

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 w') [CategoryTheory.SmallCategory K] [CategoryTheory.FinCategory K] [CategoryTheory.Limits.HasLimitsOfShape K D] : CategoryTheory.Limits.PreservesLimitsOfShape K (CategoryTheory.plusPlusSheaf J D)

Equations

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

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.plusPlusSheaf J D)

Equations

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

instance CategoryTheory.instHasWeakSheafify_2 {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.HasWeakSheafify J D

Equations

• (_ : CategoryTheory.HasWeakSheafify J D) = (_ : Nonempty (CategoryTheory.IsRightAdjoint (CategoryTheory.sheafToPresheaf 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 : 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.plusPlusSheaf J D ≅ CategoryTheory.presheafToSheaf J D

plusPlusSheaf is isomorphic to an arbitrary choice of left adjoint.

Equations

• CategoryTheory.plusPlusSheafIsoPresheafToSheaf J D = CategoryTheory.Adjunction.leftAdjointUniq (CategoryTheory.plusPlusAdjunction J D) (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 : 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.GrothendieckTopology.sheafification J 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 : 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)] (P : CategoryTheory.Functor Cᵒᵖ D) : CategoryTheory.GrothendieckTopology.sheafify J 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)

instance CategoryTheory.instHasSheafify {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.HasSheafify J D

Equations

• (_ : CategoryTheory.HasSheafify J D) = (_ : CategoryTheory.HasSheafify J D)

instance CategoryTheory.instFinitaryExtensiveSheafInstCategorySheaf {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.FinitaryExtensive D] [CategoryTheory.Limits.HasFiniteCoproducts D] [CategoryTheory.Limits.HasPullbacks D] : CategoryTheory.FinitaryExtensive (CategoryTheory.Sheaf J D)

Equations

• (_ : CategoryTheory.FinitaryExtensive (CategoryTheory.Sheaf J D)) = (_ : CategoryTheory.FinitaryExtensive (CategoryTheory.Sheaf J D))

instance CategoryTheory.instAdhesiveSheafInstCategorySheaf {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.Adhesive D] [CategoryTheory.Limits.HasPullbacks D] [CategoryTheory.Limits.HasPushouts D] : CategoryTheory.Adhesive (CategoryTheory.Sheaf J D)

Equations

• (_ : CategoryTheory.Adhesive (CategoryTheory.Sheaf J D)) = (_ : CategoryTheory.Adhesive (CategoryTheory.Sheaf J D))

instance CategoryTheory.SheafOfTypes.finitary_extensive {C : Type u} [CategoryTheory.SmallCategory C] (J : CategoryTheory.GrothendieckTopology C) : CategoryTheory.FinitaryExtensive (CategoryTheory.Sheaf J (Type u))

Equations

• (_ : CategoryTheory.FinitaryExtensive (CategoryTheory.Sheaf J (Type u))) = (_ : CategoryTheory.FinitaryExtensive (CategoryTheory.Sheaf J (Type u)))

instance CategoryTheory.SheafOfTypes.adhesive {C : Type u} [CategoryTheory.SmallCategory C] (J : CategoryTheory.GrothendieckTopology C) : CategoryTheory.Adhesive (CategoryTheory.Sheaf J (Type u))

Equations

• (_ : CategoryTheory.Adhesive (CategoryTheory.Sheaf J (Type u))) = (_ : CategoryTheory.Adhesive (CategoryTheory.Sheaf J (Type u)))

instance CategoryTheory.SheafOfTypes.balanced {C : Type u} [CategoryTheory.SmallCategory C] (J : CategoryTheory.GrothendieckTopology C) : CategoryTheory.Balanced (CategoryTheory.Sheaf J (Type u))

Equations

• (_ : CategoryTheory.Balanced (CategoryTheory.Sheaf J (Type u))) = (_ : CategoryTheory.Balanced (CategoryTheory.Sheaf J (Type u)))