Matrices over a category. #
When C
is a preadditive category, Mat_ C
is the preadditive category
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
.
Future work #
We should provide a more convenient Mat R
, when R
is a ring,
as a category with objects n : FinType
,
and whose morphisms are matrices with components in R
.
Ideally this would conveniently interact with both Mat_
and Matrix
.
A morphism in Mat_ C
is a dependently typed matrix of morphisms.
Instances For
The identity matrix consists of identity morphisms on the diagonal, and zeros elsewhere.
Instances For
Composition of matrices using matrix multiplication.
Instances For
We now prove that Mat_ C
has finite biproducts.
Be warned, however, that Mat_ C
is not necessarily Krull-Schmidt,
and so the internal indexing of a biproduct may have nothing to do with the external indexing,
even though the construction we give uses a sigma type.
See however isoBiproductEmbedding
.
A functor induces a functor of matrix categories.
Instances For
The identity functor induces the identity functor on matrix categories.
Instances For
Composite functors induce composite functors on matrix categories.
Instances For
The embedding of C
into Mat_ C
as one-by-one matrices.
(We index the summands by punit
.)
Instances For
Every object in Mat_ C
is isomorphic to the biproduct of its summands.
Instances For
Every M
is a direct sum of objects from C
, and F
preserves biproducts.
Instances For
Any additive functor C ⥤ D
to a category D
with finite biproducts extends to
a functor Mat_ C ⥤ D
.
Instances For
An additive functor C ⥤ D
factors through its lift to Mat_ C ⥤ D
.
Instances For
Mat_.lift F
is the unique additive functor L : Mat_ C ⥤ D
such that F ≅ embedding C ⋙ L
.
Instances For
Two additive functors Mat_ C ⥤ D
are naturally isomorphic if
their precompositions with embedding C
are naturally isomorphic as functors C ⥤ D
.
Instances For
Natural isomorphism needed in the construction of equivalenceSelfOfHasFiniteBiproducts
.
Instances For
A preadditive category that already has finite biproducts is equivalent to its additive envelope.
Note that we only prove this for a large category; otherwise there are universe issues that I haven't attempted to sort out.
Instances For
A type synonym for Fintype
, which we will equip with a category structure
where the morphisms are matrices with components in R
.
Instances For
Auxiliary definition for CategoryTheory.Mat.equivalenceSingleObj
.
Instances For
The categorical equivalence between the category of matrices over a ring, and the category of matrices over that ring considered as a single-object category.