Additive structure of morphism-ideal quotients

Quotienting an additive category by a two-sided morphism ideal preserves zero objects and finite biproducts. These instances allow the quotient to be used as an additive category, not just as a category with additive hom groups. The quotient functor preserves these biproducts by Mathlib's Functor.preservesFiniteBiproductsOfAdditive; its standard biproduct comparison isomorphisms therefore apply without a separate choice of sums in the quotient.

The constructions reuse Mathlib's Functor.hasZeroObject_of_additive, Functor.hasFiniteProducts_of_additive_of_essSurj, and biproduct preservation API.

References

• M. Auslander, I. Reiten, S. Smalø, Representation Theory of Artin Algebras, Chapter IV, Section 1.
• D. Happel, Triangulated Categories in the Representation Theory of Finite Dimensional Algebras, Section I.2.

instance TauCeti.MorphismIdeal.instHasZeroObjectQuotient {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) [CategoryTheory.Limits.HasZeroObject C] : CategoryTheory.Limits.HasZeroObject I.Quotient

A quotient by a morphism ideal has a zero object whenever the original category does.

instance TauCeti.MorphismIdeal.instHasFiniteBiproductsQuotientOfHasFiniteProducts {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) [CategoryTheory.Limits.HasFiniteProducts C] : CategoryTheory.Limits.HasFiniteBiproducts I.Quotient

Finite biproducts descend to the quotient by a morphism ideal.

instance TauCeti.MorphismIdeal.instHasBinaryBiproductsQuotientOfHasBinaryProducts {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) [CategoryTheory.Limits.HasBinaryProducts C] : CategoryTheory.Limits.HasBinaryBiproducts I.Quotient

Binary biproducts descend even without a zero object in the original category.