feat(category_theory): the additive envelope, Mat_ C (#6845)

Matrices over a category.

When C is a preadditive category, Mat_ C is the preadditive categoriy whose objects are finite tuples of objects in C, and whose morphisms are matrices of morphisms from C. There is a functor Mat_.embedding : C ⥤ Mat_ C sending morphisms to one-by-one matrices. Mat_ C has finite biproducts.

The additive envelope

We show that this construction is the "additive envelope" of C, in the sense that any additive functor F : C ⥤ D to a category D with biproducts lifts to a functor Mat_.lift F : Mat_ C ⥤ D, Moreover, this functor is unique (up to natural isomorphisms) amongst functors L : Mat_ C ⥤ D such that embedding C ⋙ L ≅ F. (As we don't have 2-category theory, we can't explicitly state that Mat_ C is the initial object in the 2-category of categories under C which have biproducts.) As a consequence, when C already has finite biproducts we have Mat_ C ≌ C.