Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes

deleted theorem matrix.add_apply
deleted theorem matrix.neg_apply
deleted theorem matrix.sub_apply
deleted theorem matrix.zero_apply
added theorem dmatrix.add_apply
added def dmatrix.col
added theorem dmatrix.ext
added theorem dmatrix.ext_iff
added def
added theorem dmatrix.map_add
added theorem dmatrix.map_apply
added theorem dmatrix.map_map
added theorem dmatrix.map_sub
added theorem dmatrix.map_zero
added theorem dmatrix.neg_apply
added def dmatrix.row
added theorem dmatrix.sub_apply
added theorem dmatrix.zero_apply
added def dmatrix