Theorems · Definition · category theory

CategoryTheory.Limits.biproduct

{J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → (f : J → C) → [CategoryTheory.Limits.HasBiproduct f] → C

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.)

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Cited by

188 results in Mathlib

Foundations

Depth 6 from the axioms, rests on 11 definitions · uses Classical.choice

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphismsCategoryTheory.Limits.HasBiproduct