Documentation

Mathlib.CategoryTheory.Preadditive.Indization

The category of ind-objects is preadditive #

source
noncomputable instance CategoryTheory.instPreadditiveInd {C : Type u} [SmallCategory C] [Preadditive C] [Limits.HasFiniteColimits C] :
Preadditive (Ind C)
Equations
    source
    instance CategoryTheory.instHasFiniteBiproductsInd {C : Type u} [SmallCategory C] [Preadditive C] [Limits.HasFiniteColimits C] :
    Limits.HasFiniteBiproducts (Ind C)