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]
: