Theorems · Definition · category theory

CategoryTheory.Limits.biproduct.uniqueUpToIso

{J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        (f : J → C) →
          [inst_2 : CategoryTheory.Limits.HasBiproduct f] →
            {b : CategoryTheory.Limits.Bicone f} → b.IsBilimit → (b.pt ≅ ⨁ f)

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.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Cited by

2 results in Mathlib

Foundations

Depth 36 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphismsCategoryTheory.Limits.HasBiproduct