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`.
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
