Commit 2021-04-16 17:35 ea4dce03View on Github →
feat(category_theory): the additive envelope, Mat_ C (#6845)
Matrices over a category.
C is a preadditive category,
Mat_ C is the preadditive categoriy
whose objects are finite tuples of objects in
whose morphisms are matrices of morphisms from
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
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
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.