Documentation

Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Biproducts and binary biproducts #

We introduce the notion of (finite) biproducts and binary biproducts.

These are slightly unusual relative to the other shapes in the library, as they are simultaneously limits and colimits. (Zero objects are similar; they are "biterminal".)

For results about biproducts in preadditive categories see CategoryTheory.Preadditive.Biproducts.

In a category with zero morphisms, we model the (binary) biproduct of P Q : C using a BinaryBicone, which has a cone point X, and morphisms fst : X ⟶ P, snd : X ⟶ Q, inl : P ⟶ X and inr : X ⟶ Q, such that inlfst = 𝟙 P, inlsnd = 0, inrfst = 0, and inrsnd = 𝟙 Q. Such a BinaryBicone is a biproduct if the cone is a limit cone, and the cocone is a colimit cocone.

For biproducts indexed by a Fintype J, a bicone again consists of a cone point X and morphisms π j : X ⟶ F j and ι j : F j ⟶ X for each j, such that ι j ≫ π j' is the identity when j = j' and zero otherwise.

Notation #

As is already taken for the sum of types, we introduce the notation X ⊞ Y for a binary biproduct. We introduce ⨁ f for the indexed biproduct.

Implementation notes #

Prior to leanprover-community/mathlib#14046, HasFiniteBiproducts required a DecidableEq instance on the indexing type. As this had no pay-off (everything about limits is non-constructive in mathlib), and occasional cost (constructing decidability instances appropriate for constructions involving the indexing type), we made everything classical.

structure CategoryTheory.Limits.Bicone {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : JC) :
Type (max (max uC uC') w)

A c : Bicone F is:

  • an object c.pt and
  • morphisms π j : pt ⟶ F j and ι j : F j ⟶ pt for each j,
  • such that ι j ≫ π j' is the identity when j = j' and zero otherwise.
  • pt : C

    A c : Bicone F is:

    • an object c.pt and
    • morphisms π j : pt ⟶ F j and ι j : F j ⟶ pt for each j,
    • such that ι j ≫ π j' is the identity when j = j' and zero otherwise.
  • π : (j : J) → self.pt F j

    A c : Bicone F is:

    • an object c.pt and
    • morphisms π j : pt ⟶ F j and ι j : F j ⟶ pt for each j,
    • such that ι j ≫ π j' is the identity when j = j' and zero otherwise.
  • ι : (j : J) → F j self.pt

    A c : Bicone F is:

    • an object c.pt and
    • morphisms π j : pt ⟶ F j and ι j : F j ⟶ pt for each j,
    • such that ι j ≫ π j' is the identity when j = j' and zero otherwise.
  • ι_π : ∀ (j j' : J), CategoryTheory.CategoryStruct.comp (self j) (self j') = if h : j = j' then CategoryTheory.eqToHom else 0

    A c : Bicone F is:

    • an object c.pt and
    • morphisms π j : pt ⟶ F j and ι j : F j ⟶ pt for each j,
    • such that ι j ≫ π j' is the identity when j = j' and zero otherwise.
Instances For

    A bicone morphism between two bicones for the same diagram is a morphism of the bicone points which commutes with the cone and cocone legs.

    Instances For

      The category of bicones on a given diagram.

      Equations
      @[simp]
      theorem CategoryTheory.Limits.Bicones.ext_hom_hom {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : JC} {c : CategoryTheory.Limits.Bicone F} {c' : CategoryTheory.Limits.Bicone F} (φ : c.pt c'.pt) (wι : autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp (c j) φ.hom = c' j) _auto✝) (wπ : autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp φ.hom (c' j) = c j) _auto✝) :
      (CategoryTheory.Limits.Bicones.ext φ ).hom.hom = φ.hom
      @[simp]
      theorem CategoryTheory.Limits.Bicones.ext_inv_hom {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : JC} {c : CategoryTheory.Limits.Bicone F} {c' : CategoryTheory.Limits.Bicone F} (φ : c.pt c'.pt) (wι : autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp (c j) φ.hom = c' j) _auto✝) (wπ : autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp φ.hom (c' j) = c j) _auto✝) :
      (CategoryTheory.Limits.Bicones.ext φ ).inv.hom = φ.inv
      def CategoryTheory.Limits.Bicones.ext {J : Type w} {C : Type uC} [CategoryTheory.Category.{uC', uC} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : JC} {c : CategoryTheory.Limits.Bicone F} {c' : CategoryTheory.Limits.Bicone F} (φ : c.pt c'.pt) (wι : autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp (c j) φ.hom = c' j) _auto✝) (wπ : autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp φ.hom (c' j) = c j) _auto✝) :
      c c'

      To give an isomorphism between cocones, it suffices to give an isomorphism between their vertices which commutes with the cocone maps.

      Equations
      • CategoryTheory.Limits.Bicones.ext φ = { hom := { hom := φ.hom, := , := }, inv := { hom := φ.inv, := , := }, hom_inv_id := , inv_hom_id := }
      Instances For

        A functor G : C ⥤ D sends bicones over F to bicones over G.obj ∘ F functorially.

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

          Extract the cone from a bicone.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[inline, reducible]

            A shorthand for toConeFunctor.obj

            Equations
            Instances For

              Extract the cocone from a bicone.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[inline, reducible]

                A shorthand for toCoconeFunctor.obj

                Equations
                Instances For

                  We can turn any limit cone over a discrete collection of objects into a bicone.

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

                    We can turn any colimit cocone over a discrete collection of objects into a bicone.

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

                      Structure witnessing that a bicone is both a limit cone and a colimit cocone.

                      Instances For
                        theorem CategoryTheory.Limits.Bicone.IsBilimit.ext_iff {J : Type w} {C : Type uC} :
                        ∀ {inst : CategoryTheory.Category.{uC', uC} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C} {F : JC} {B : CategoryTheory.Limits.Bicone F} (x y : CategoryTheory.Limits.Bicone.IsBilimit B), x = y x.isLimit = y.isLimit x.isColimit = y.isColimit
                        theorem CategoryTheory.Limits.Bicone.IsBilimit.ext {J : Type w} {C : Type uC} :
                        ∀ {inst : CategoryTheory.Category.{uC', uC} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C} {F : JC} {B : CategoryTheory.Limits.Bicone F} (x y : CategoryTheory.Limits.Bicone.IsBilimit B), x.isLimit = y.isLimitx.isColimit = y.isColimitx = y

                        Whisker a bicone with an equivalence between the indexing types.

                        Equations
                        Instances For

                          Taking the cocone of a whiskered bicone results in a cone isomorphic to one gained by whiskering the cocone and precomposing with a suitable isomorphism.

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

                            Whiskering a bicone with an equivalence between types preserves being a bilimit bicone.

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

                              A bicone over F : J → C, which is both a limit cone and a colimit cocone.

                              Instances For

                                HasBiproduct F expresses the mere existence of a bicone which is simultaneously a limit and a colimit of the diagram F.

                                Instances

                                  C has biproducts of shape J if we have a limit and a colimit, with the same cone points, of every function F : J → C.

                                  Instances

                                    HasFiniteBiproducts C represents a choice of biproduct for every family of objects in C indexed by a finite type.

                                    Instances

                                      The isomorphism between the specified limit and the specified colimit for a functor with a bilimit.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        @[inline, reducible]

                                        biproduct f computes the biproduct of a family of elements f. (It is defined as an abbreviation for limit (Discrete.functor f), so for most facts about biproduct f, you will just use general facts about limits and colimits.)

                                        Equations
                                        Instances For

                                          biproduct f computes the biproduct of a family of elements f. (It is defined as an abbreviation for limit (Discrete.functor f), so for most facts about biproduct f, you will just use general facts about limits and colimits.)

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            @[inline, reducible]

                                            The projection onto a summand of a biproduct.

                                            Equations
                                            Instances For
                                              @[inline, reducible]

                                              The inclusion into a summand of a biproduct.

                                              Equations
                                              Instances For

                                                Note that as this lemma has an if in the statement, we include a DecidableEq argument. This means you may not be able to simp using this lemma unless you open scoped Classical.

                                                @[inline, reducible]

                                                Given a collection of maps into the summands, we obtain a map into the biproduct.

                                                Equations
                                                Instances For
                                                  @[inline, reducible]

                                                  Given a collection of maps out of the summands, we obtain a map out of the biproduct.

                                                  Equations
                                                  Instances For
                                                    @[inline, reducible]

                                                    Given a collection of maps between corresponding summands of a pair of biproducts indexed by the same type, we obtain a map between the biproducts.

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      @[inline, reducible]

                                                      An alternative to biproduct.map constructed via colimits. This construction only exists in order to show it is equal to biproduct.map.

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

                                                        The canonical isomorphism between the chosen biproduct and the chosen product.

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

                                                          The canonical isomorphism between the chosen biproduct and the chosen coproduct.

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

                                                            Given a collection of isomorphisms between corresponding summands of a pair of biproducts indexed by the same type, we obtain an isomorphism between the biproducts.

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

                                                              Two biproducts which differ by an equivalence in the indexing type, and up to isomorphism in the factors, are isomorphic.

                                                              Unfortunately there are two natural ways to define each direction of this isomorphism (because it is true for both products and coproducts separately). We give the alternative definitions as lemmas below.

                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                instance CategoryTheory.Limits.instHasBiproductSigmaFstSnd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_3} (f : ιType u_2) (g : (i : ι) → f iC) [∀ (i : ι), CategoryTheory.Limits.HasBiproduct (g i)] [CategoryTheory.Limits.HasBiproduct fun (i : ι) => g i] :
                                                                CategoryTheory.Limits.HasBiproduct fun (p : (i : ι) × f i) => g p.fst p.snd
                                                                Equations
                                                                • =
                                                                @[simp]
                                                                theorem CategoryTheory.Limits.biproductBiproductIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_3} (f : ιType u_2) (g : (i : ι) → f iC) [∀ (i : ι), CategoryTheory.Limits.HasBiproduct (g i)] [CategoryTheory.Limits.HasBiproduct fun (i : ι) => g i] :
                                                                @[simp]
                                                                theorem CategoryTheory.Limits.biproductBiproductIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_3} (f : ιType u_2) (g : (i : ι) → f iC) [∀ (i : ι), CategoryTheory.Limits.HasBiproduct (g i)] [CategoryTheory.Limits.HasBiproduct fun (i : ι) => g i] :
                                                                (CategoryTheory.Limits.biproductBiproductIso f g).inv = CategoryTheory.Limits.biproduct.lift fun (i : ι) => CategoryTheory.Limits.biproduct.lift fun (x : f i) => CategoryTheory.Limits.biproduct.π (fun (p : (i : ι) × f i) => g p.fst p.snd) { fst := i, snd := x }
                                                                def CategoryTheory.Limits.biproductBiproductIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {ι : Type u_3} (f : ιType u_2) (g : (i : ι) → f iC) [∀ (i : ι), CategoryTheory.Limits.HasBiproduct (g i)] [CategoryTheory.Limits.HasBiproduct fun (i : ι) => g i] :
                                                                ( fun (i : ι) => g i) fun (p : (i : ι) × f i) => g p.fst p.snd

                                                                An iterated biproduct is a biproduct over a sigma type.

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

                                                                  The canonical morphism from the biproduct over a restricted index type to the biproduct of the full index type.

                                                                  Equations
                                                                  Instances For

                                                                    The kernel of biproduct.π f i is the inclusion from the biproduct which omits i from the index set J into the biproduct over J.

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

                                                                      The kernel of biproduct.π f i is Subtype.restrict {i}ᶜ f.

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

                                                                        The cokernel of biproduct.ι f i is the projection from the biproduct over the index set J onto the biproduct omitting i.

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

                                                                          The cokernel of biproduct.ι f i is Subtype.restrict {i}ᶜ f.

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

                                                                            The limit cone exhibiting Subtype.restrict pᶜ f as the kernel of biproduct.toSubtype f p

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

                                                                              The colimit cocone exhibiting Subtype.restrict pᶜ f as the cokernel of biproduct.fromSubtype f p

                                                                              Equations
                                                                              • One or more equations did not get rendered due to their size.
                                                                              Instances For
                                                                                def CategoryTheory.Limits.biproduct.matrix {J : Type} [Finite J] {K : Type} [Finite K] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] {f : JC} {g : KC} (m : (j : J) → (k : K) → f j g k) :
                                                                                f g

                                                                                Convert a (dependently typed) matrix to a morphism of biproducts.

                                                                                Equations
                                                                                Instances For

                                                                                  Extract the matrix components from a morphism of biproducts.

                                                                                  Equations
                                                                                  • One or more equations did not get rendered due to their size.
                                                                                  Instances For
                                                                                    @[simp]
                                                                                    theorem CategoryTheory.Limits.biproduct.matrixEquiv_apply {J : Type} [Finite J] {K : Type} [Finite K] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] {f : JC} {g : KC} (m : f g) (j : J) (k : K) :
                                                                                    CategoryTheory.Limits.biproduct.matrixEquiv m j k = CategoryTheory.Limits.biproduct.components m j k
                                                                                    @[simp]
                                                                                    theorem CategoryTheory.Limits.biproduct.matrixEquiv_symm_apply {J : Type} [Finite J] {K : Type} [Finite K] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteBiproducts C] {f : JC} {g : KC} (m : (j : J) → (k : K) → f j g k) :
                                                                                    CategoryTheory.Limits.biproduct.matrixEquiv.symm m = CategoryTheory.Limits.biproduct.matrix m

                                                                                    Morphisms between direct sums are matrices.

                                                                                    Equations
                                                                                    • CategoryTheory.Limits.biproduct.matrixEquiv = { toFun := CategoryTheory.Limits.biproduct.components, invFun := CategoryTheory.Limits.biproduct.matrix, left_inv := , right_inv := }
                                                                                    Instances For

                                                                                      Biproducts are unique up to isomorphism. This already follows because bilimits are limits, but in the case of biproducts we can give an isomorphism with particularly nice definitional properties, namely that biproduct.lift b.π and biproduct.desc b.ι are inverses of each other.

                                                                                      Equations
                                                                                      Instances For

                                                                                        The limit bicone for the biproduct over an index type with exactly one term.

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

                                                                                          A biproduct over an index type with exactly one term is just the object over that term.

                                                                                          Equations
                                                                                          Instances For

                                                                                            A binary bicone for a pair of objects P Q : C consists of the cone point X, maps from X to both P and Q, and maps from both P and Q to X, so that inlfst = 𝟙 P, inlsnd = 0, inrfst = 0, and inrsnd = 𝟙 Q

                                                                                            • pt : C

                                                                                              A binary bicone for a pair of objects P Q : C consists of the cone point X, maps from X to both P and Q, and maps from both P and Q to X, so that inlfst = 𝟙 P, inlsnd = 0, inrfst = 0, and inrsnd = 𝟙 Q

                                                                                            • fst : self.pt P

                                                                                              A binary bicone for a pair of objects P Q : C consists of the cone point X, maps from X to both P and Q, and maps from both P and Q to X, so that inlfst = 𝟙 P, inlsnd = 0, inrfst = 0, and inrsnd = 𝟙 Q

                                                                                            • snd : self.pt Q

                                                                                              A binary bicone for a pair of objects P Q : C consists of the cone point X, maps from X to both P and Q, and maps from both P and Q to X, so that inlfst = 𝟙 P, inlsnd = 0, inrfst = 0, and inrsnd = 𝟙 Q

                                                                                            • inl : P self.pt

                                                                                              A binary bicone for a pair of objects P Q : C consists of the cone point X, maps from X to both P and Q, and maps from both P and Q to X, so that inlfst = 𝟙 P, inlsnd = 0, inrfst = 0, and inrsnd = 𝟙 Q

                                                                                            • inr : Q self.pt

                                                                                              A binary bicone for a pair of objects P Q : C consists of the cone point X, maps from X to both P and Q, and maps from both P and Q to X, so that inlfst = 𝟙 P, inlsnd = 0, inrfst = 0, and inrsnd = 𝟙 Q

                                                                                            • A binary bicone for a pair of objects P Q : C consists of the cone point X, maps from X to both P and Q, and maps from both P and Q to X, so that inlfst = 𝟙 P, inlsnd = 0, inrfst = 0, and inrsnd = 𝟙 Q

                                                                                            • inl_snd : CategoryTheory.CategoryStruct.comp self.inl self.snd = 0

                                                                                              A binary bicone for a pair of objects P Q : C consists of the cone point X, maps from X to both P and Q, and maps from both P and Q to X, so that inlfst = 𝟙 P, inlsnd = 0, inrfst = 0, and inrsnd = 𝟙 Q

                                                                                            • inr_fst : CategoryTheory.CategoryStruct.comp self.inr self.fst = 0

                                                                                              A binary bicone for a pair of objects P Q : C consists of the cone point X, maps from X to both P and Q, and maps from both P and Q to X, so that inlfst = 𝟙 P, inlsnd = 0, inrfst = 0, and inrsnd = 𝟙 Q

                                                                                            • A binary bicone for a pair of objects P Q : C consists of the cone point X, maps from X to both P and Q, and maps from both P and Q to X, so that inlfst = 𝟙 P, inlsnd = 0, inrfst = 0, and inrsnd = 𝟙 Q

                                                                                            Instances For

                                                                                              A binary bicone morphism between two binary bicones for the same diagram is a morphism of the binary bicone points which commutes with the cone and cocone legs.

                                                                                              Instances For

                                                                                                The category of binary bicones on a given diagram.

                                                                                                Equations

                                                                                                To give an isomorphism between cocones, it suffices to give an isomorphism between their vertices which commutes with the cocone maps.

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

                                                                                                  A functor F : C ⥤ D sends binary bicones for P and Q to binary bicones for G.obj P and G.obj Q functorially.

                                                                                                  Equations
                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                  Instances For
                                                                                                    @[simp]
                                                                                                    theorem CategoryTheory.Limits.BinaryBicone.toBiconeFunctor_map_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X : C} {Y : C} :
                                                                                                    ∀ {X_1 Y_1 : CategoryTheory.Limits.BinaryBicone X Y} (f : X_1 Y_1), (CategoryTheory.Limits.BinaryBicone.toBiconeFunctor.map f).hom = f.hom
                                                                                                    @[simp]
                                                                                                    theorem CategoryTheory.Limits.BinaryBicone.toBiconeFunctor_obj_pt {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X : C} {Y : C} (b : CategoryTheory.Limits.BinaryBicone X Y) :
                                                                                                    (CategoryTheory.Limits.BinaryBicone.toBiconeFunctor.obj b).pt = b.pt
                                                                                                    @[inline, reducible]

                                                                                                    A shorthand for toBiconeFunctor.obj

                                                                                                    Equations
                                                                                                    Instances For

                                                                                                      A binary bicone is a limit cone if and only if the corresponding bicone is a limit cone.

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

                                                                                                        A binary bicone is a colimit cocone if and only if the corresponding bicone is a colimit cocone.

                                                                                                        Equations
                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                        Instances For
                                                                                                          @[simp]
                                                                                                          theorem CategoryTheory.Limits.Bicone.toBinaryBiconeFunctor_map_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X : C} {Y : C} :
                                                                                                          ∀ {X_1 Y_1 : CategoryTheory.Limits.Bicone (CategoryTheory.Limits.pairFunction X Y)} (f : X_1 Y_1), (CategoryTheory.Limits.Bicone.toBinaryBiconeFunctor.map f).hom = f.hom
                                                                                                          @[simp]

                                                                                                          Convert a Bicone over a function on WalkingPair to a BinaryBicone.

                                                                                                          Equations
                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                          Instances For
                                                                                                            @[inline, reducible]

                                                                                                            A shorthand for toBinaryBiconeFunctor.obj

                                                                                                            Equations
                                                                                                            Instances For

                                                                                                              A bicone over a pair is a limit cone if and only if the corresponding binary bicone is a limit cone.

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

                                                                                                                A bicone over a pair is a colimit cocone if and only if the corresponding binary bicone is a colimit cocone.

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

                                                                                                                  Structure witnessing that a binary bicone is a limit cone and a limit cocone.

                                                                                                                  Instances For

                                                                                                                    A binary bicone is a bilimit bicone if and only if the corresponding bicone is a bilimit.

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

                                                                                                                      A bicone over a pair is a bilimit bicone if and only if the corresponding binary bicone is a bilimit.

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

                                                                                                                        A bicone over P Q : C, which is both a limit cone and a colimit cocone.

                                                                                                                        Instances For

                                                                                                                          HasBinaryBiproduct P Q expresses the mere existence of a bicone which is simultaneously a limit and a colimit of the diagram pair P Q.

                                                                                                                          Instances

                                                                                                                            HasBinaryBiproducts C represents the existence of a bicone which is simultaneously a limit and a colimit of the diagram pair P Q, for every P Q : C.

                                                                                                                            Instances

                                                                                                                              A category with finite biproducts has binary biproducts.

                                                                                                                              This is not an instance as typically in concrete categories there will be an alternative construction with nicer definitional properties.

                                                                                                                              The isomorphism between the specified binary product and the specified binary coproduct for a pair for a binary biproduct.

                                                                                                                              Equations
                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                              Instances For
                                                                                                                                @[inline, reducible]

                                                                                                                                An arbitrary choice of biproduct of a pair of objects.

                                                                                                                                Equations
                                                                                                                                Instances For

                                                                                                                                  An arbitrary choice of biproduct of a pair of objects.

                                                                                                                                  Equations
                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                  Instances For
                                                                                                                                    @[inline, reducible]

                                                                                                                                    The projection onto the first summand of a binary biproduct.

                                                                                                                                    Equations
                                                                                                                                    Instances For
                                                                                                                                      @[inline, reducible]

                                                                                                                                      The projection onto the second summand of a binary biproduct.

                                                                                                                                      Equations
                                                                                                                                      Instances For
                                                                                                                                        @[inline, reducible]

                                                                                                                                        The inclusion into the first summand of a binary biproduct.

                                                                                                                                        Equations
                                                                                                                                        Instances For
                                                                                                                                          @[inline, reducible]

                                                                                                                                          The inclusion into the second summand of a binary biproduct.

                                                                                                                                          Equations
                                                                                                                                          Instances For
                                                                                                                                            @[inline, reducible]

                                                                                                                                            Given a pair of maps into the summands of a binary biproduct, we obtain a map into the binary biproduct.

                                                                                                                                            Equations
                                                                                                                                            Instances For
                                                                                                                                              @[inline, reducible]

                                                                                                                                              Given a pair of maps out of the summands of a binary biproduct, we obtain a map out of the binary biproduct.

                                                                                                                                              Equations
                                                                                                                                              Instances For
                                                                                                                                                @[inline, reducible]

                                                                                                                                                Given a pair of maps between the summands of a pair of binary biproducts, we obtain a map between the binary biproducts.

                                                                                                                                                Equations
                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                Instances For
                                                                                                                                                  @[inline, reducible]

                                                                                                                                                  An alternative to biprod.map constructed via colimits. This construction only exists in order to show it is equal to biprod.map.

                                                                                                                                                  Equations
                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                  Instances For
                                                                                                                                                    theorem CategoryTheory.Limits.biprod.hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X : C} {Y : C} {Z : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] (f : Z X Y) (g : Z X Y) (h₀ : CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.fst = CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.biprod.fst) (h₁ : CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.snd = CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.biprod.snd) :
                                                                                                                                                    f = g
                                                                                                                                                    theorem CategoryTheory.Limits.biprod.hom_ext' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X : C} {Y : C} {Z : C} [CategoryTheory.Limits.HasBinaryBiproduct X Y] (f : X Y Z) (g : X Y Z) (h₀ : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl f = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl g) (h₁ : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr f = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr g) :
                                                                                                                                                    f = g

                                                                                                                                                    The canonical isomorphism between the chosen biproduct and the chosen product.

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

                                                                                                                                                      The canonical isomorphism between the chosen biproduct and the chosen coproduct.

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

                                                                                                                                                        Given a pair of isomorphisms between the summands of a pair of binary biproducts, we obtain an isomorphism between the binary biproducts.

                                                                                                                                                        Equations
                                                                                                                                                        Instances For

                                                                                                                                                          Binary biproducts are unique up to isomorphism. This already follows because bilimits are limits, but in the case of biproducts we can give an isomorphism with particularly nice definitional properties, namely that biprod.lift b.fst b.snd and biprod.desc b.inl b.inr are inverses of each other.

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

                                                                                                                                                            The kernel of biprod.fst : X ⊞ Y ⟶ X is Y.

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

                                                                                                                                                              The kernel of biprod.snd : X ⊞ Y ⟶ Y is X.

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

                                                                                                                                                                The cokernel of biprod.inl : X ⟶ X ⊞ Y is Y.

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

                                                                                                                                                                  The cokernel of biprod.inr : Y ⟶ X ⊞ Y is X.

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

                                                                                                                                                                    If Y is a zero object, X ≅ X ⊞ Y for any X.

                                                                                                                                                                    Equations
                                                                                                                                                                    Instances For

                                                                                                                                                                      If X is a zero object, Y ≅ X ⊞ Y for any Y.

                                                                                                                                                                      Equations
                                                                                                                                                                      Instances For

                                                                                                                                                                        The braiding isomorphism which swaps a binary biproduct.

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

                                                                                                                                                                          An alternative formula for the braiding isomorphism which swaps a binary biproduct, using the fact that the biproduct is a coproduct.

                                                                                                                                                                          Equations
                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                          Instances For
                                                                                                                                                                            @[simp]
                                                                                                                                                                            theorem CategoryTheory.Limits.biprod.symmetry'_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] (P : C) (Q : C) {Z : C} (h : P Q Z) :
                                                                                                                                                                            CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.lift CategoryTheory.Limits.biprod.snd CategoryTheory.Limits.biprod.fst) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.lift CategoryTheory.Limits.biprod.snd CategoryTheory.Limits.biprod.fst) h) = h
                                                                                                                                                                            @[simp]
                                                                                                                                                                            theorem CategoryTheory.Limits.biprod.symmetry' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] (P : C) (Q : C) :
                                                                                                                                                                            CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.lift CategoryTheory.Limits.biprod.snd CategoryTheory.Limits.biprod.fst) (CategoryTheory.Limits.biprod.lift CategoryTheory.Limits.biprod.snd CategoryTheory.Limits.biprod.fst) = CategoryTheory.CategoryStruct.id (P Q)
                                                                                                                                                                            @[simp]
                                                                                                                                                                            theorem CategoryTheory.Limits.biprod.associator_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] (P : C) (Q : C) (R : C) :
                                                                                                                                                                            (CategoryTheory.Limits.biprod.associator P Q R).hom = CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.fst) (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.snd) CategoryTheory.Limits.biprod.snd)
                                                                                                                                                                            @[simp]
                                                                                                                                                                            theorem CategoryTheory.Limits.biprod.associator_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] (P : C) (Q : C) (R : C) :
                                                                                                                                                                            (CategoryTheory.Limits.biprod.associator P Q R).inv = CategoryTheory.Limits.biprod.lift (CategoryTheory.Limits.biprod.lift CategoryTheory.Limits.biprod.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd CategoryTheory.Limits.biprod.fst)) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd CategoryTheory.Limits.biprod.snd)

                                                                                                                                                                            The associator isomorphism which associates a binary biproduct.

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

                                                                                                                                                                              An object is indecomposable if it cannot be written as the biproduct of two nonzero objects.

                                                                                                                                                                              Equations
                                                                                                                                                                              Instances For