Documentation

Mathlib.CategoryTheory.Preadditive.Biproducts

Basic facts about biproducts in preadditive categories. #

In (or between) preadditive categories,

There are connections between this material and the special case of the category whose morphisms are matrices over a ring, in particular the Schur complement (see Mathlib.LinearAlgebra.Matrix.SchurComplement). In particular, the declarations CategoryTheory.Biprod.isoElim, CategoryTheory.Biprod.gaussian and Matrix.invertibleOfFromBlocks₁₁Invertible are all closely related.

In a preadditive category, we can construct a biproduct for f : J β†’ C from any bicone b for f satisfying total : βˆ‘ j : J, b.Ο€ j ≫ b.ΞΉ j = πŸ™ b.X.

(That is, such a bicone is a limit cone and a colimit cocone.)

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

    In a preadditive category, we can construct a biproduct for f : J β†’ C from any bicone b for f satisfying total : βˆ‘ j : J, b.Ο€ j ≫ b.ΞΉ j = πŸ™ b.X.

    (That is, such a bicone is a limit cone and a colimit cocone.)

    In a preadditive category, any finite bicone which is a limit cone is in fact a bilimit bicone.

    Equations
    Instances For

      We can turn any limit cone over a pair into a bilimit bicone.

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

        In a preadditive category, any finite bicone which is a colimit cocone is in fact a bilimit bicone.

        Equations
        Instances For

          We can turn any limit cone over a pair into a bilimit bicone.

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

            In a preadditive category, if the product over f : J β†’ C exists, then the biproduct over f exists.

            In a preadditive category, if the coproduct over f : J β†’ C exists, then the biproduct over f exists.

            @[simp]

            In any preadditive category, any biproduct satsifies βˆ‘ j : J, biproduct.Ο€ f j ≫ biproduct.ΞΉ f j = πŸ™ (⨁ f)

            Reindex a categorical biproduct via an equivalence of the index types.

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

              In a preadditive category, we can construct a binary biproduct for X Y : C from any binary bicone b satisfying total : b.fst ≫ b.inl + b.snd ≫ b.inr = πŸ™ b.X.

              (That is, such a bicone is a limit cone and a colimit cocone.)

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

                In a preadditive category, we can construct a binary biproduct for X Y : C from any binary bicone b satisfying total : b.fst ≫ b.inl + b.snd ≫ b.inr = πŸ™ b.X.

                (That is, such a bicone is a limit cone and a colimit cocone.)

                We can turn any limit cone over a pair into a bicone.

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

                  In a preadditive category, any binary bicone which is a limit cone is in fact a bilimit bicone.

                  Equations
                  Instances For

                    In a preadditive category, if the product of X and Y exists, then the binary biproduct of X and Y exists.

                    We can turn any colimit cocone over a pair into a bicone.

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

                      In a preadditive category, any binary bicone which is a colimit cocone is in fact a bilimit bicone.

                      Equations
                      Instances For

                        We can turn any colimit cocone over a pair into a bilimit bicone.

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

                          In a preadditive category, if the coproduct of X and Y exists, then the binary biproduct of X and Y exists.

                          @[simp]
                          theorem CategoryTheory.Limits.biprod.total {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X : C} {Y : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] :
                          CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.inl + CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd CategoryTheory.Limits.biprod.inr = CategoryTheory.CategoryStruct.id (X ⊞ Y)

                          In any preadditive category, any binary biproduct satsifies biprod.fst ≫ biprod.inl + biprod.snd ≫ biprod.inr = πŸ™ (X ⊞ Y).

                          theorem CategoryTheory.Limits.biprod.map_eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {W : C} {X : C} {Y : C} {Z : C} {f : W ⟢ Y} {g : X ⟢ Z} :
                          CategoryTheory.Limits.biprod.map f g = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.inl) + CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd (CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.biprod.inr)

                          Every split mono f with a cokernel induces a binary bicone with f as its inl and the cokernel map as its snd. We will show in is_bilimit_binary_bicone_of_split_mono_of_cokernel that this binary bicone is in fact already a biproduct.

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

                            If b is a binary bicone such that b.inl is a kernel of b.snd, then b is a bilimit bicone.

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

                              If b is a binary bicone such that b.inr is a kernel of b.fst, then b is a bilimit bicone.

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

                                If b is a binary bicone such that b.fst is a cokernel of b.inr, then b is a bilimit bicone.

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

                                  If b is a binary bicone such that b.snd is a cokernel of b.inl, then b is a bilimit bicone.

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

                                    Every split epi f with a kernel induces a binary bicone with f as its snd and the kernel map as its inl. We will show in binary_bicone_of_is_split_mono_of_cokernel that this binary bicone is in fact already a biproduct.

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

                                      The bicone constructed in binaryBiconeOfIsSplitEpiOfKernel is a bilimit. This is a version of the splitting lemma that holds in all preadditive categories.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        theorem CategoryTheory.Preadditive.ext {C : Type u} :
                                        βˆ€ {inst : CategoryTheory.Category.{v, u} C} (x y : CategoryTheory.Preadditive C), CategoryTheory.Preadditive.homGroup = CategoryTheory.Preadditive.homGroup β†’ x = y
                                        theorem CategoryTheory.Preadditive.ext_iff {C : Type u} :
                                        βˆ€ {inst : CategoryTheory.Category.{v, u} C} (x y : CategoryTheory.Preadditive C), x = y ↔ CategoryTheory.Preadditive.homGroup = CategoryTheory.Preadditive.homGroup

                                        The existence of binary biproducts implies that there is at most one preadditive structure.

                                        Equations
                                        • β‹― = β‹―
                                        def CategoryTheory.Biprod.ofComponents {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : C} {Xβ‚‚ : C} {Y₁ : C} {Yβ‚‚ : C} (f₁₁ : X₁ ⟢ Y₁) (f₁₂ : X₁ ⟢ Yβ‚‚) (f₂₁ : Xβ‚‚ ⟢ Y₁) (fβ‚‚β‚‚ : Xβ‚‚ ⟢ Yβ‚‚) :
                                        X₁ ⊞ Xβ‚‚ ⟢ Y₁ ⊞ Yβ‚‚

                                        The "matrix" morphism X₁ ⊞ Xβ‚‚ ⟢ Y₁ ⊞ Yβ‚‚ with specified components.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          @[simp]
                                          theorem CategoryTheory.Biprod.inl_ofComponents {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : C} {Xβ‚‚ : C} {Y₁ : C} {Yβ‚‚ : C} (f₁₁ : X₁ ⟢ Y₁) (f₁₂ : X₁ ⟢ Yβ‚‚) (f₂₁ : Xβ‚‚ ⟢ Y₁) (fβ‚‚β‚‚ : Xβ‚‚ ⟢ Yβ‚‚) :
                                          CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.Biprod.ofComponents f₁₁ f₁₂ f₂₁ fβ‚‚β‚‚) = CategoryTheory.CategoryStruct.comp f₁₁ CategoryTheory.Limits.biprod.inl + CategoryTheory.CategoryStruct.comp f₁₂ CategoryTheory.Limits.biprod.inr
                                          @[simp]
                                          theorem CategoryTheory.Biprod.inr_ofComponents {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : C} {Xβ‚‚ : C} {Y₁ : C} {Yβ‚‚ : C} (f₁₁ : X₁ ⟢ Y₁) (f₁₂ : X₁ ⟢ Yβ‚‚) (f₂₁ : Xβ‚‚ ⟢ Y₁) (fβ‚‚β‚‚ : Xβ‚‚ ⟢ Yβ‚‚) :
                                          CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.Biprod.ofComponents f₁₁ f₁₂ f₂₁ fβ‚‚β‚‚) = CategoryTheory.CategoryStruct.comp f₂₁ CategoryTheory.Limits.biprod.inl + CategoryTheory.CategoryStruct.comp fβ‚‚β‚‚ CategoryTheory.Limits.biprod.inr
                                          @[simp]
                                          theorem CategoryTheory.Biprod.ofComponents_fst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : C} {Xβ‚‚ : C} {Y₁ : C} {Yβ‚‚ : C} (f₁₁ : X₁ ⟢ Y₁) (f₁₂ : X₁ ⟢ Yβ‚‚) (f₂₁ : Xβ‚‚ ⟢ Y₁) (fβ‚‚β‚‚ : Xβ‚‚ ⟢ Yβ‚‚) :
                                          CategoryTheory.CategoryStruct.comp (CategoryTheory.Biprod.ofComponents f₁₁ f₁₂ f₂₁ fβ‚‚β‚‚) CategoryTheory.Limits.biprod.fst = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst f₁₁ + CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd f₂₁
                                          @[simp]
                                          theorem CategoryTheory.Biprod.ofComponents_snd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : C} {Xβ‚‚ : C} {Y₁ : C} {Yβ‚‚ : C} (f₁₁ : X₁ ⟢ Y₁) (f₁₂ : X₁ ⟢ Yβ‚‚) (f₂₁ : Xβ‚‚ ⟢ Y₁) (fβ‚‚β‚‚ : Xβ‚‚ ⟢ Yβ‚‚) :
                                          CategoryTheory.CategoryStruct.comp (CategoryTheory.Biprod.ofComponents f₁₁ f₁₂ f₂₁ fβ‚‚β‚‚) CategoryTheory.Limits.biprod.snd = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst f₁₂ + CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd fβ‚‚β‚‚
                                          @[simp]
                                          theorem CategoryTheory.Biprod.ofComponents_eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : C} {Xβ‚‚ : C} {Y₁ : C} {Yβ‚‚ : C} (f : X₁ ⊞ Xβ‚‚ ⟢ Y₁ ⊞ Yβ‚‚) :
                                          CategoryTheory.Biprod.ofComponents (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.fst)) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.snd)) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.fst)) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.snd)) = f
                                          @[simp]
                                          theorem CategoryTheory.Biprod.ofComponents_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : C} {Xβ‚‚ : C} {Y₁ : C} {Yβ‚‚ : C} {Z₁ : C} {Zβ‚‚ : C} (f₁₁ : X₁ ⟢ Y₁) (f₁₂ : X₁ ⟢ Yβ‚‚) (f₂₁ : Xβ‚‚ ⟢ Y₁) (fβ‚‚β‚‚ : Xβ‚‚ ⟢ Yβ‚‚) (g₁₁ : Y₁ ⟢ Z₁) (g₁₂ : Y₁ ⟢ Zβ‚‚) (g₂₁ : Yβ‚‚ ⟢ Z₁) (gβ‚‚β‚‚ : Yβ‚‚ ⟢ Zβ‚‚) :
                                          CategoryTheory.CategoryStruct.comp (CategoryTheory.Biprod.ofComponents f₁₁ f₁₂ f₂₁ fβ‚‚β‚‚) (CategoryTheory.Biprod.ofComponents g₁₁ g₁₂ g₂₁ gβ‚‚β‚‚) = CategoryTheory.Biprod.ofComponents (CategoryTheory.CategoryStruct.comp f₁₁ g₁₁ + CategoryTheory.CategoryStruct.comp f₁₂ g₂₁) (CategoryTheory.CategoryStruct.comp f₁₁ g₁₂ + CategoryTheory.CategoryStruct.comp f₁₂ gβ‚‚β‚‚) (CategoryTheory.CategoryStruct.comp f₂₁ g₁₁ + CategoryTheory.CategoryStruct.comp fβ‚‚β‚‚ g₂₁) (CategoryTheory.CategoryStruct.comp f₂₁ g₁₂ + CategoryTheory.CategoryStruct.comp fβ‚‚β‚‚ gβ‚‚β‚‚)
                                          def CategoryTheory.Biprod.unipotentUpper {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : C} {Xβ‚‚ : C} (r : X₁ ⟢ Xβ‚‚) :
                                          X₁ ⊞ Xβ‚‚ β‰… X₁ ⊞ Xβ‚‚

                                          The unipotent upper triangular matrix

                                          (1 r)
                                          (0 1)
                                          

                                          as an isomorphism.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            def CategoryTheory.Biprod.unipotentLower {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : C} {Xβ‚‚ : C} (r : Xβ‚‚ ⟢ X₁) :
                                            X₁ ⊞ Xβ‚‚ β‰… X₁ ⊞ Xβ‚‚

                                            The unipotent lower triangular matrix

                                            (1 0)
                                            (r 1)
                                            

                                            as an isomorphism.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              def CategoryTheory.Biprod.gaussian' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : C} {Xβ‚‚ : C} {Y₁ : C} {Yβ‚‚ : C} (f₁₁ : X₁ ⟢ Y₁) (f₁₂ : X₁ ⟢ Yβ‚‚) (f₂₁ : Xβ‚‚ ⟢ Y₁) (fβ‚‚β‚‚ : Xβ‚‚ ⟢ Yβ‚‚) [CategoryTheory.IsIso f₁₁] :
                                              (L : X₁ ⊞ Xβ‚‚ β‰… X₁ ⊞ Xβ‚‚) Γ—' (R : Y₁ ⊞ Yβ‚‚ β‰… Y₁ ⊞ Yβ‚‚) Γ—' (gβ‚‚β‚‚ : Xβ‚‚ ⟢ Yβ‚‚) Γ—' CategoryTheory.CategoryStruct.comp L.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Biprod.ofComponents f₁₁ f₁₂ f₂₁ fβ‚‚β‚‚) R.hom) = CategoryTheory.Limits.biprod.map f₁₁ gβ‚‚β‚‚

                                              If f is a morphism X₁ ⊞ Xβ‚‚ ⟢ Y₁ ⊞ Yβ‚‚ whose X₁ ⟢ Y₁ entry is an isomorphism, then we can construct isomorphisms L : X₁ ⊞ Xβ‚‚ β‰… X₁ ⊞ Xβ‚‚ and R : Y₁ ⊞ Yβ‚‚ β‰… Y₁ ⊞ Yβ‚‚ so that L.hom ≫ g ≫ R.hom is diagonal (with X₁ ⟢ Y₁ component still f), via Gaussian elimination.

                                              (This is the version of Biprod.gaussian written in terms of components.)

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                def CategoryTheory.Biprod.gaussian {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : C} {Xβ‚‚ : C} {Y₁ : C} {Yβ‚‚ : C} (f : X₁ ⊞ Xβ‚‚ ⟢ Y₁ ⊞ Yβ‚‚) [CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.fst))] :
                                                (L : X₁ ⊞ Xβ‚‚ β‰… X₁ ⊞ Xβ‚‚) Γ—' (R : Y₁ ⊞ Yβ‚‚ β‰… Y₁ ⊞ Yβ‚‚) Γ—' (gβ‚‚β‚‚ : Xβ‚‚ ⟢ Yβ‚‚) Γ—' CategoryTheory.CategoryStruct.comp L.hom (CategoryTheory.CategoryStruct.comp f R.hom) = CategoryTheory.Limits.biprod.map (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.fst)) gβ‚‚β‚‚

                                                If f is a morphism X₁ ⊞ Xβ‚‚ ⟢ Y₁ ⊞ Yβ‚‚ whose X₁ ⟢ Y₁ entry is an isomorphism, then we can construct isomorphisms L : X₁ ⊞ Xβ‚‚ β‰… X₁ ⊞ Xβ‚‚ and R : Y₁ ⊞ Yβ‚‚ β‰… Y₁ ⊞ Yβ‚‚ so that L.hom ≫ g ≫ R.hom is diagonal (with X₁ ⟢ Y₁ component still f), via Gaussian elimination.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  def CategoryTheory.Biprod.isoElim' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : C} {Xβ‚‚ : C} {Y₁ : C} {Yβ‚‚ : C} (f₁₁ : X₁ ⟢ Y₁) (f₁₂ : X₁ ⟢ Yβ‚‚) (f₂₁ : Xβ‚‚ ⟢ Y₁) (fβ‚‚β‚‚ : Xβ‚‚ ⟢ Yβ‚‚) [CategoryTheory.IsIso f₁₁] [CategoryTheory.IsIso (CategoryTheory.Biprod.ofComponents f₁₁ f₁₂ f₂₁ fβ‚‚β‚‚)] :
                                                  Xβ‚‚ β‰… Yβ‚‚

                                                  If X₁ ⊞ Xβ‚‚ β‰… Y₁ ⊞ Yβ‚‚ via a two-by-two matrix whose X₁ ⟢ Y₁ entry is an isomorphism, then we can construct an isomorphism Xβ‚‚ β‰… Yβ‚‚, via Gaussian elimination.

                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    def CategoryTheory.Biprod.isoElim {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : C} {Xβ‚‚ : C} {Y₁ : C} {Yβ‚‚ : C} (f : X₁ ⊞ Xβ‚‚ β‰… Y₁ ⊞ Yβ‚‚) [CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp f.hom CategoryTheory.Limits.biprod.fst))] :
                                                    Xβ‚‚ β‰… Yβ‚‚

                                                    If f is an isomorphism X₁ ⊞ Xβ‚‚ β‰… Y₁ ⊞ Yβ‚‚ whose X₁ ⟢ Y₁ entry is an isomorphism, then we can construct an isomorphism Xβ‚‚ β‰… Yβ‚‚, via Gaussian elimination.

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

                                                      If f : ⨁ S ⟢ ⨁ T is an isomorphism, and s is a non-trivial summand of the source, then there is some t in the target so that the s, t matrix entry of f is nonzero.

                                                      Equations
                                                      Instances For

                                                        A functor between preadditive categories that preserves (zero morphisms and) finite biproducts preserves finite products.

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

                                                          A functor between preadditive categories that preserves (zero morphisms and) finite biproducts preserves finite products.

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

                                                            A functor between preadditive categories that preserves (zero morphisms and) finite products preserves finite biproducts.

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

                                                              If the (product-like) biproduct comparison for F and f is a monomorphism, then F preserves the biproduct of f. For the converse, see mapBiproduct.

                                                              Equations
                                                              Instances For

                                                                If the (coproduct-like) biproduct comparison for F and f is an epimorphism, then F preserves the biproduct of F and f. For the converse, see mapBiproduct.

                                                                Equations
                                                                Instances For

                                                                  A functor between preadditive categories that preserves (zero morphisms and) finite biproducts preserves finite coproducts.

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

                                                                    A functor between preadditive categories that preserves (zero morphisms and) finite biproducts preserves finite coproducts.

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

                                                                      A functor between preadditive categories that preserves (zero morphisms and) finite coproducts preserves finite biproducts.

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

                                                                        A functor between preadditive categories that preserves (zero morphisms and) binary biproducts preserves binary products.

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

                                                                          A functor between preadditive categories that preserves (zero morphisms and) binary biproducts preserves binary products.

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

                                                                            A functor between preadditive categories that preserves (zero morphisms and) binary products preserves binary biproducts.

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

                                                                              If the (product-like) biproduct comparison for F, X and Y is a monomorphism, then F preserves the biproduct of X and Y. For the converse, see map_biprod.

                                                                              Equations
                                                                              Instances For

                                                                                If the (coproduct-like) biproduct comparison for F, X and Y is an epimorphism, then F preserves the biproduct of X and Y. For the converse, see mapBiprod.

                                                                                Equations
                                                                                Instances For

                                                                                  A functor between preadditive categories that preserves (zero morphisms and) binary biproducts preserves binary coproducts.

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

                                                                                    A functor between preadditive categories that preserves (zero morphisms and) binary biproducts preserves binary coproducts.

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

                                                                                      A functor between preadditive categories that preserves (zero morphisms and) binary coproducts preserves binary biproducts.

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