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.
Equations
- CategoryTheory.Mat_.Hom.id M i j = if h : i = j then CategoryTheory.eqToHom ⋯ else 0
Instances For
Composition of matrices using matrix multiplication.
Equations
- f.comp g i k = ∑ j : N.ι, CategoryTheory.CategoryStruct.comp (f i j) (g j k)
Instances For
Equations
- CategoryTheory.Mat_.instCategory = CategoryTheory.Category.mk ⋯ ⋯ ⋯
Equations
- M.instInhabitedHom N = { default := fun (i : M.ι) (j : N.ι) => 0 }
Equations
- CategoryTheory.Mat_.instPreadditive = { homGroup := inferInstance, add_comp := ⋯, comp_add := ⋯ }
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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The identity functor induces the identity functor on matrix categories.
Equations
- CategoryTheory.Functor.mapMatId = CategoryTheory.NatIso.ofComponents (fun (M : CategoryTheory.Mat_ C) => CategoryTheory.eqToIso ⋯) ⋯
Instances For
Composite functors induce composite functors on matrix categories.
Equations
- F.mapMatComp G = CategoryTheory.NatIso.ofComponents (fun (M : CategoryTheory.Mat_ C) => CategoryTheory.eqToIso ⋯) ⋯
Instances For
The embedding of C
into Mat_ C
as one-by-one matrices.
(We index the summands by PUnit
.)
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- CategoryTheory.Mat_.instInhabited C = { default := (CategoryTheory.Mat_.embedding C).obj default }
Every object in Mat_ C
is isomorphic to the biproduct of its summands.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Every M
is a direct sum of objects from C
, and F
preserves biproducts.
Equations
- CategoryTheory.Mat_.additiveObjIsoBiproduct F M = F.mapIso M.isoBiproductEmbedding ≪≫ F.mapBiproduct fun (i : M.ι) => (CategoryTheory.Mat_.embedding C).obj (M.X i)
Instances For
Any additive functor C ⥤ D
to a category D
with finite biproducts extends to
a functor Mat_ C ⥤ D
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
An additive functor C ⥤ D
factors through its lift to Mat_ C ⥤ D
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Mat_.lift F
is the unique additive functor L : Mat_ C ⥤ D
such that F ≅ embedding C ⋙ L
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Two additive functors Mat_ C ⥤ D
are naturally isomorphic if
their precompositions with embedding C
are naturally isomorphic as functors C ⥤ D
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Natural isomorphism needed in the construction of equivalenceSelfOfHasFiniteBiproducts
.
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A type synonym for Fintype
, which we will equip with a category structure
where the morphisms are matrices with components in R
.
Equations
Instances For
Equations
- CategoryTheory.instInhabitedMat R = id inferInstance
Equations
- CategoryTheory.instCoeSortMatType R = CategoryTheory.Bundled.coeSort
Equations
Equations
- CategoryTheory.Mat.instInhabitedHom R M N = { default := fun (x : ↑M) (x : ↑N) => 0 }
Auxiliary definition for CategoryTheory.Mat.equivalenceSingleObj
.
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
- CategoryTheory.Mat.equivalenceSingleObj R = (CategoryTheory.Mat.equivalenceSingleObjInverse R).asEquivalence.symm
Instances For
Equations
- CategoryTheory.Mat.instAddCommGroupHom R X Y = id inferInstance
Equations
- CategoryTheory.Mat.instPreadditive = { homGroup := inferInstance, add_comp := ⋯, comp_add := ⋯ }