# Commit 2021-04-16 17:35 ea4dce03

View on Github →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`

.