Theorems · Definition · category theory

CategoryTheory.Limits.biproductBiproductIso

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_3} →
        (f : ι → Type u_2) →
          (g : (i : ι) → f i → C) →
            [inst_2 : ∀ (i : ι), CategoryTheory.Limits.HasBiproduct (g i)] →
              [inst_3 : CategoryTheory.Limits.HasBiproduct fun i => ⨁ g i] →
                (⨁ fun i => ⨁ g i) ≅ ⨁ fun p => g p.fst p.snd

An iterated biproduct is a biproduct over a sigma type.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphismsCategoryTheory.Limits.HasBiproductCategoryTheory.Limits.HasBiproduct