The category of ind-objects is preadditive #
@[instance_reducible]
noncomputable instance CategoryTheory.instPreadditiveInd {C : Type u} [SmallCategory C] [Preadditive C] [Limits.HasFiniteColimits C] :
Preadditive (Ind C)
Equations
- One or more equations did not get rendered due to their size.
instance CategoryTheory.instHasFiniteBiproductsInd {C : Type u} [SmallCategory C] [Preadditive C] [Limits.HasFiniteColimits C] :