Documentation

Mathlib.CategoryTheory.Sites.Plus

The plus construction for presheaves. #

This file contains the construction of P⁺, for a presheaf P : Cᵒᵖ ⥤ D where C is endowed with a grothendieck topology J.

See https://stacks.math.columbia.edu/tag/00W1 for details.

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

The diagram whose colimit defines the values of plus.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem CategoryTheory.GrothendieckTopology.diagram_obj {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] (P : Functor Cᵒᵖ D) (X : C) (S : (J.Cover X)ᵒᵖ) :
    (J.diagram P X).obj S = Limits.multiequalizer ((Opposite.unop S).index P)
    @[simp]
    theorem CategoryTheory.GrothendieckTopology.diagram_map {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] (P : Functor Cᵒᵖ D) (X : C) {S x✝ : (J.Cover X)ᵒᵖ} (f : S x✝) :
    (J.diagram P X).map f = Limits.Multiequalizer.lift ((Opposite.unop x✝).index P) ((fun (S : (J.Cover X)ᵒᵖ) => Limits.multiequalizer ((Opposite.unop S).index P)) S) (fun (I : ((Opposite.unop x✝).index P).L) => Limits.Multiequalizer.ι ((Opposite.unop S).index P) (Cover.Arrow.map I f.unop))
    def CategoryTheory.GrothendieckTopology.diagramPullback {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] (P : Functor Cᵒᵖ D) {X Y : C} (f : X Y) :
    J.diagram P Y (J.pullback f).op.comp (J.diagram P X)

    A helper definition used to define the morphisms for plus.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem CategoryTheory.GrothendieckTopology.diagramPullback_app {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] (P : Functor Cᵒᵖ D) {X Y : C} (f : X Y) (S : (J.Cover Y)ᵒᵖ) :
      (J.diagramPullback P f).app S = Limits.Multiequalizer.lift ((Opposite.unop ((J.pullback f).op.obj S)).index P) ((J.diagram P Y).obj S) (fun (I : ((Opposite.unop ((J.pullback f).op.obj S)).index P).L) => Limits.Multiequalizer.ι ((Opposite.unop S).index P) (Cover.Arrow.base I))
      def CategoryTheory.GrothendieckTopology.diagramNatTrans {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] {P Q : Functor Cᵒᵖ D} (η : P Q) (X : C) :
      J.diagram P X J.diagram Q X

      A natural transformation P ⟶ Q induces a natural transformation between diagrams whose colimits define the values of plus.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem CategoryTheory.GrothendieckTopology.diagramNatTrans_app {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] {P Q : Functor Cᵒᵖ D} (η : P Q) (X : C) (W : (J.Cover X)ᵒᵖ) :
        (J.diagramNatTrans η X).app W = Limits.Multiequalizer.lift ((Opposite.unop W).index Q) ((J.diagram P X).obj W) (fun (x : ((Opposite.unop W).index Q).L) => CategoryStruct.comp (Limits.Multiequalizer.ι ((Opposite.unop W).index P) x) (η.app (Opposite.op x.Y)))
        @[simp]
        theorem CategoryTheory.GrothendieckTopology.diagramNatTrans_id {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] (X : C) (P : Functor Cᵒᵖ D) :
        J.diagramNatTrans (CategoryStruct.id P) X = CategoryStruct.id (J.diagram P X)
        @[simp]
        theorem CategoryTheory.GrothendieckTopology.diagramNatTrans_zero {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] [Preadditive D] (X : C) (P Q : Functor Cᵒᵖ D) :
        J.diagramNatTrans 0 X = 0
        @[simp]
        theorem CategoryTheory.GrothendieckTopology.diagramNatTrans_comp {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] {P Q R : Functor Cᵒᵖ D} (η : P Q) (γ : Q R) (X : C) :
        J.diagramNatTrans (CategoryStruct.comp η γ) X = CategoryStruct.comp (J.diagramNatTrans η X) (J.diagramNatTrans γ X)
        def CategoryTheory.GrothendieckTopology.diagramFunctor {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{max v u, w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] (X : C) :
        Functor (Functor Cᵒᵖ D) (Functor (J.Cover X)ᵒᵖ D)

        J.diagram P, as a functor in P.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem CategoryTheory.GrothendieckTopology.diagramFunctor_map {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{max v u, w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] (X : C) {X✝ Y✝ : Functor Cᵒᵖ D} (η : X✝ Y✝) :
          (J.diagramFunctor D X).map η = J.diagramNatTrans η X
          @[simp]
          theorem CategoryTheory.GrothendieckTopology.diagramFunctor_obj {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{max v u, w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] (X : C) (P : Functor Cᵒᵖ D) :
          (J.diagramFunctor D X).obj P = J.diagram P X
          def CategoryTheory.GrothendieckTopology.plusObj {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] (P : Functor Cᵒᵖ D) [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] :

          The plus construction, associating a presheaf to any presheaf. See plusFunctor below for a functorial version.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            def CategoryTheory.GrothendieckTopology.plusMap {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, 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] {P Q : Functor Cᵒᵖ D} (η : P Q) :
            J.plusObj P J.plusObj Q

            An auxiliary definition used in plus below.

            Equations
            Instances For
              @[simp]
              theorem CategoryTheory.GrothendieckTopology.plusMap_id {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, 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] (P : Functor Cᵒᵖ D) :
              J.plusMap (CategoryStruct.id P) = CategoryStruct.id (J.plusObj P)
              @[simp]
              theorem CategoryTheory.GrothendieckTopology.plusMap_zero {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, 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] [Preadditive D] (P Q : Functor Cᵒᵖ D) :
              J.plusMap 0 = 0
              @[simp]
              theorem CategoryTheory.GrothendieckTopology.plusMap_comp {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, 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] {P Q R : Functor Cᵒᵖ D} (η : P Q) (γ : Q R) :
              J.plusMap (CategoryStruct.comp η γ) = CategoryStruct.comp (J.plusMap η) (J.plusMap γ)
              theorem CategoryTheory.GrothendieckTopology.plusMap_comp_assoc {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, 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] {P Q R : Functor Cᵒᵖ D} (η : P Q) (γ : Q R) {Z : Functor Cᵒᵖ D} (h : J.plusObj R Z) :
              CategoryStruct.comp (J.plusMap (CategoryStruct.comp η γ)) h = CategoryStruct.comp (J.plusMap η) (CategoryStruct.comp (J.plusMap γ) h)
              def CategoryTheory.GrothendieckTopology.plusFunctor {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{max v u, 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] :

              The plus construction, a functor sending P to J.plusObj P.

              Equations
              Instances For
                @[simp]
                theorem CategoryTheory.GrothendieckTopology.plusFunctor_obj {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{max v u, 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] (P : Functor Cᵒᵖ D) :
                (J.plusFunctor D).obj P = J.plusObj P
                @[simp]
                theorem CategoryTheory.GrothendieckTopology.plusFunctor_map {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{max v u, 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] {X✝ Y✝ : Functor Cᵒᵖ D} (η : X✝ Y✝) :
                (J.plusFunctor D).map η = J.plusMap η
                def CategoryTheory.GrothendieckTopology.toPlus {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] (P : Functor Cᵒᵖ D) [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] :
                P J.plusObj P

                The canonical map from P to J.plusObj P. See toPlusNatTrans for a functorial version.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[simp]
                  theorem CategoryTheory.GrothendieckTopology.toPlus_naturality {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, 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] {P Q : Functor Cᵒᵖ D} (η : P Q) :
                  CategoryStruct.comp η (J.toPlus Q) = CategoryStruct.comp (J.toPlus P) (J.plusMap η)
                  @[simp]
                  theorem CategoryTheory.GrothendieckTopology.toPlus_naturality_assoc {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, 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] {P Q : Functor Cᵒᵖ D} (η : P Q) {Z : Functor Cᵒᵖ D} (h : J.plusObj Q Z) :
                  CategoryStruct.comp η (CategoryStruct.comp (J.toPlus Q) h) = CategoryStruct.comp (J.toPlus P) (CategoryStruct.comp (J.plusMap η) h)
                  def CategoryTheory.GrothendieckTopology.toPlusNatTrans {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{max v u, 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] :
                  Functor.id (Functor Cᵒᵖ D) J.plusFunctor D

                  The natural transformation from the identity functor to plus.

                  Equations
                  Instances For
                    @[simp]
                    theorem CategoryTheory.GrothendieckTopology.toPlusNatTrans_app {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (D : Type w) [Category.{max v u, 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] (P : Functor Cᵒᵖ D) :
                    (J.toPlusNatTrans D).app P = J.toPlus P
                    @[simp]
                    theorem CategoryTheory.GrothendieckTopology.plusMap_toPlus {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] (P : Functor Cᵒᵖ D) [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] :
                    J.plusMap (J.toPlus P) = J.toPlus (J.plusObj P)

                    (P ⟶ P⁺)⁺ = P⁺ ⟶ P⁺⁺

                    theorem CategoryTheory.GrothendieckTopology.isIso_toPlus_of_isSheaf {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] (P : Functor Cᵒᵖ D) [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] (hP : Presheaf.IsSheaf J P) :
                    IsIso (J.toPlus P)
                    def CategoryTheory.GrothendieckTopology.isoToPlus {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] (P : Functor Cᵒᵖ D) [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] (hP : Presheaf.IsSheaf J P) :
                    P J.plusObj P

                    The natural isomorphism between P and P⁺ when P is a sheaf.

                    Equations
                    Instances For
                      @[simp]
                      theorem CategoryTheory.GrothendieckTopology.isoToPlus_hom {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] (P : Functor Cᵒᵖ D) [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] (hP : Presheaf.IsSheaf J P) :
                      (J.isoToPlus P hP).hom = J.toPlus P
                      def CategoryTheory.GrothendieckTopology.plusLift {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, 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] {P Q : Functor Cᵒᵖ D} (η : P Q) (hQ : Presheaf.IsSheaf J Q) :
                      J.plusObj P Q

                      Lift a morphism P ⟶ Q to P⁺ ⟶ Q when Q is a sheaf.

                      Equations
                      Instances For
                        @[simp]
                        theorem CategoryTheory.GrothendieckTopology.toPlus_plusLift {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, 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] {P Q : Functor Cᵒᵖ D} (η : P Q) (hQ : Presheaf.IsSheaf J Q) :
                        CategoryStruct.comp (J.toPlus P) (J.plusLift η hQ) = η
                        @[simp]
                        theorem CategoryTheory.GrothendieckTopology.toPlus_plusLift_assoc {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, 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] {P Q : Functor Cᵒᵖ D} (η : P Q) (hQ : Presheaf.IsSheaf J Q) {Z : Functor Cᵒᵖ D} (h : Q Z) :
                        CategoryStruct.comp (J.toPlus P) (CategoryStruct.comp (J.plusLift η hQ) h) = CategoryStruct.comp η h
                        theorem CategoryTheory.GrothendieckTopology.plusLift_unique {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, 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] {P Q : Functor Cᵒᵖ D} (η : P Q) (hQ : Presheaf.IsSheaf J Q) (γ : J.plusObj P Q) (hγ : CategoryStruct.comp (J.toPlus P) γ = η) :
                        γ = J.plusLift η hQ
                        theorem CategoryTheory.GrothendieckTopology.plus_hom_ext {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, 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] {P Q : Functor Cᵒᵖ D} (η γ : J.plusObj P Q) (hQ : Presheaf.IsSheaf J Q) (h : CategoryStruct.comp (J.toPlus P) η = CategoryStruct.comp (J.toPlus P) γ) :
                        η = γ
                        @[simp]
                        theorem CategoryTheory.GrothendieckTopology.isoToPlus_inv {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, w} D] [∀ (P : Functor Cᵒᵖ D) (X : C) (S : J.Cover X), Limits.HasMultiequalizer (S.index P)] (P : Functor Cᵒᵖ D) [∀ (X : C), Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] (hP : Presheaf.IsSheaf J P) :
                        (J.isoToPlus P hP).inv = J.plusLift (CategoryStruct.id P) hP
                        @[simp]
                        theorem CategoryTheory.GrothendieckTopology.plusMap_plusLift {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, 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] {P Q R : Functor Cᵒᵖ D} (η : P Q) (γ : Q R) (hR : Presheaf.IsSheaf J R) :
                        CategoryStruct.comp (J.plusMap η) (J.plusLift γ hR) = J.plusLift (CategoryStruct.comp η γ) hR
                        instance CategoryTheory.GrothendieckTopology.plusFunctor_preservesZeroMorphisms {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type w} [Category.{max v u, 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] [Preadditive D] :
                        (J.plusFunctor D).PreservesZeroMorphisms