# 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.

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.

structure CategoryTheory.Mat_ (C : Type u₁) :
Type (max 1 u₁)

An object in Mat_ C is a finite tuple of objects in C.

Instances For
def CategoryTheory.Mat_.Hom {C : Type u₁} [] (M : ) (N : ) :
Type v₁

A morphism in Mat_ C is a dependently typed matrix of morphisms.

Equations
• M.Hom N = DMatrix M N fun (i : M) (j : N) => M.X i N.X j
Instances For
def CategoryTheory.Mat_.Hom.id {C : Type u₁} [] (M : ) :
M.Hom M

The identity matrix consists of identity morphisms on the diagonal, and zeros elsewhere.

Equations
• = if h : i = j then else 0
Instances For
def CategoryTheory.Mat_.Hom.comp {C : Type u₁} [] {M : } {N : } {K : } (f : M.Hom N) (g : N.Hom K) :
M.Hom K

Composition of matrices using matrix multiplication.

Equations
Instances For
instance CategoryTheory.Mat_.instCategory {C : Type u₁} [] :
Equations
• CategoryTheory.Mat_.instCategory =
theorem CategoryTheory.Mat_.hom_ext {C : Type u₁} [] {M : } {N : } (f : M N) (g : M N) (H : ∀ (i : M) (j : N), f i j = g i j) :
f = g
theorem CategoryTheory.Mat_.id_def {C : Type u₁} [] (M : ) :
= fun (i j : M) => if h : i = j then else 0
theorem CategoryTheory.Mat_.id_apply {C : Type u₁} [] (M : ) (i : M) (j : M) :
= if h : i = j then else 0
@[simp]
theorem CategoryTheory.Mat_.id_apply_self {C : Type u₁} [] (M : ) (i : M) :
@[simp]
theorem CategoryTheory.Mat_.id_apply_of_ne {C : Type u₁} [] (M : ) (i : M) (j : M) (h : i j) :
theorem CategoryTheory.Mat_.comp_def {C : Type u₁} [] {M : } {N : } {K : } (f : M N) (g : N K) :
= fun (i : M) (k : K) => Finset.univ.sum fun (j : N) => CategoryTheory.CategoryStruct.comp (f i j) (g j k)
@[simp]
theorem CategoryTheory.Mat_.comp_apply {C : Type u₁} [] {M : } {N : } {K : } (f : M N) (g : N K) (i : M) (k : K) :
= Finset.univ.sum fun (j : N) => CategoryTheory.CategoryStruct.comp (f i j) (g j k)
instance CategoryTheory.Mat_.instInhabitedHom {C : Type u₁} [] (M : ) (N : ) :
Equations
• M.instInhabitedHom N = { default := fun (i : M) (j : N) => 0 }
instance CategoryTheory.Mat_.instAddCommGroupHom {C : Type u₁} [] (M : ) (N : ) :
Equations
• M.instAddCommGroupHom N = let_fun this := inferInstance; this
@[simp]
theorem CategoryTheory.Mat_.add_apply {C : Type u₁} [] {M : } {N : } (f : M N) (g : M N) (i : M) (j : N) :
(f + g) i j = f i j + g i j
Equations

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.

Equations
• =
@[simp]
theorem CategoryTheory.Functor.mapMat__obj_fintype {C : Type u₁} [] {D : Type u_1} [] (F : ) [F.Additive] (M : ) :
(F.mapMat_.obj M).fintype = M.fintype
@[simp]
theorem CategoryTheory.Functor.mapMat__obj_X {C : Type u₁} [] {D : Type u_1} [] (F : ) [F.Additive] (M : ) (i : M) :
(F.mapMat_.obj M).X i = F.obj (M.X i)
@[simp]
theorem CategoryTheory.Functor.mapMat__obj_ι {C : Type u₁} [] {D : Type u_1} [] (F : ) [F.Additive] (M : ) :
(F.mapMat_.obj M) = M
@[simp]
theorem CategoryTheory.Functor.mapMat__map {C : Type u₁} [] {D : Type u_1} [] (F : ) [F.Additive] :
∀ {X Y : } (f : X Y) (i : ((fun (M : ) => CategoryTheory.Mat_.mk M fun (i : M) => F.obj (M.X i)) X)) (j : ((fun (M : ) => CategoryTheory.Mat_.mk M fun (i : M) => F.obj (M.X i)) Y)), F.mapMat_.map f i j = F.map (f i j)
def CategoryTheory.Functor.mapMat_ {C : Type u₁} [] {D : Type u_1} [] (F : ) [F.Additive] :

A functor induces a functor of matrix categories.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Functor.mapMatId_inv_app {C : Type u₁} [] (X : ) :
CategoryTheory.Functor.mapMatId.inv.app X = CategoryTheory.CategoryStruct.id (.mapMat_.obj X)
@[simp]
theorem CategoryTheory.Functor.mapMatId_hom_app {C : Type u₁} [] (X : ) :
CategoryTheory.Functor.mapMatId.hom.app X = CategoryTheory.CategoryStruct.id (.mapMat_.obj X)

The identity functor induces the identity functor on matrix categories.

Equations
Instances For
@[simp]
theorem CategoryTheory.Functor.mapMatComp_inv_app {C : Type u₁} [] {D : Type u_1} [] {E : Type u_2} [] (F : ) [F.Additive] (G : ) [G.Additive] (X : ) :
(F.mapMatComp G).inv.app X = CategoryTheory.CategoryStruct.id ((F.comp G).mapMat_.obj X)
@[simp]
theorem CategoryTheory.Functor.mapMatComp_hom_app {C : Type u₁} [] {D : Type u_1} [] {E : Type u_2} [] (F : ) [F.Additive] (G : ) [G.Additive] (X : ) :
(F.mapMatComp G).hom.app X = CategoryTheory.CategoryStruct.id ((F.comp G).mapMat_.obj X)
def CategoryTheory.Functor.mapMatComp {C : Type u₁} [] {D : Type u_1} [] {E : Type u_2} [] (F : ) [F.Additive] (G : ) [G.Additive] :
(F.comp G).mapMat_ F.mapMat_.comp G.mapMat_

Composite functors induce composite functors on matrix categories.

Equations
Instances For
@[simp]
theorem CategoryTheory.Mat_.embedding_map (C : Type u₁) [] :
∀ {X Y : C} (f : X Y) (x : ((fun (X : C) => CategoryTheory.Mat_.mk PUnit.{1} fun (x : PUnit.{1}) => X) X)) (x_1 : ((fun (X : C) => CategoryTheory.Mat_.mk PUnit.{1} fun (x : PUnit.{1}) => X) Y)), .map f x x_1 = f
@[simp]
theorem CategoryTheory.Mat_.embedding_obj_X (C : Type u₁) [] (X : C) :
∀ (x : PUnit.{1}), (.obj X).X x = X
@[simp]
theorem CategoryTheory.Mat_.embedding_obj_fintype (C : Type u₁) [] (X : C) :
(.obj X).fintype = PUnit.fintype
@[simp]
theorem CategoryTheory.Mat_.embedding_obj_ι (C : Type u₁) [] (X : C) :
(.obj X) = PUnit.{1}

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
• =
Equations
• =
Equations
• =
instance CategoryTheory.Mat_.instInhabited (C : Type u₁) [] [] :
Equations
• = { default := .obj default }
@[simp]
theorem CategoryTheory.Mat_.isoBiproductEmbedding_hom {C : Type u₁} [] (M : ) :
M.isoBiproductEmbedding.hom = CategoryTheory.Limits.biproduct.lift fun (i j : M) (k : (.obj (M.X i))) => if h : j = i then else 0
@[simp]
theorem CategoryTheory.Mat_.isoBiproductEmbedding_inv {C : Type u₁} [] (M : ) :
M.isoBiproductEmbedding.inv = CategoryTheory.Limits.biproduct.desc fun (i : M) (j : (.obj (M.X i))) (k : M) => if h : i = k then else 0
def CategoryTheory.Mat_.isoBiproductEmbedding {C : Type u₁} [] (M : ) :
M fun (i : M) => .obj (M.X i)

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
instance CategoryTheory.Mat_.instHasBiproductιObjEmbeddingXOfAdditive {C : Type u₁} [] {D : Type u₁} [] (F : ) [F.Additive] (M : ) :
CategoryTheory.Limits.HasBiproduct fun (i : M) => F.obj (.obj (M.X i))
Equations
• =
def CategoryTheory.Mat_.additiveObjIsoBiproduct {C : Type u₁} [] {D : Type u₁} [] (F : ) [F.Additive] (M : ) :
F.obj M fun (i : M) => F.obj (.obj (M.X i))

Every M is a direct sum of objects from C, and F preserves biproducts.

Equations
• = (F.mapIso M.isoBiproductEmbedding).trans (F.mapBiproduct fun (i : M) => .obj (M.X i))
Instances For
@[simp]
theorem CategoryTheory.Mat_.additiveObjIsoBiproduct_hom_π_assoc {C : Type u₁} [] {D : Type u₁} [] (F : ) [F.Additive] (M : ) (i : M) {Z : D} (h : F.obj (.obj (M.X i)) Z) :
@[simp]
theorem CategoryTheory.Mat_.additiveObjIsoBiproduct_hom_π {C : Type u₁} [] {D : Type u₁} [] (F : ) [F.Additive] (M : ) (i : M) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π (fun (i : M) => F.obj (.obj (M.X i))) i) = F.map (CategoryTheory.CategoryStruct.comp M.isoBiproductEmbedding.hom (CategoryTheory.Limits.biproduct.π (fun (i : M) => .obj (M.X i)) i))
@[simp]
theorem CategoryTheory.Mat_.ι_additiveObjIsoBiproduct_inv_assoc {C : Type u₁} [] {D : Type u₁} [] (F : ) [F.Additive] (M : ) (i : M) {Z : D} (h : F.obj M Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun (i : M) => F.obj (.obj (M.X i))) i) = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun (i : M) => .obj (M.X i)) i) M.isoBiproductEmbedding.inv)) h
@[simp]
theorem CategoryTheory.Mat_.ι_additiveObjIsoBiproduct_inv {C : Type u₁} [] {D : Type u₁} [] (F : ) [F.Additive] (M : ) (i : M) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun (i : M) => F.obj (.obj (M.X i))) i) = F.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun (i : M) => .obj (M.X i)) i) M.isoBiproductEmbedding.inv)
theorem CategoryTheory.Mat_.additiveObjIsoBiproduct_naturality_assoc {C : Type u₁} [] {D : Type u₁} [] (F : ) [F.Additive] {M : } {N : } (f : M N) {Z : D} (h : ( fun (i : N) => F.obj (.obj (N.X i))) Z) :
theorem CategoryTheory.Mat_.additiveObjIsoBiproduct_naturality {C : Type u₁} [] {D : Type u₁} [] (F : ) [F.Additive] {M : } {N : } (f : M N) :
= CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.matrix fun (i : M) (j : N) => F.map (.map (f i j)))
theorem CategoryTheory.Mat_.additiveObjIsoBiproduct_naturality'_assoc {C : Type u₁} [] {D : Type u₁} [] (F : ) [F.Additive] {M : } {N : } (f : M N) {Z : D} (h : F.obj N Z) :
= CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.matrix fun (i : M) (j : N) => F.map (.map (f i j)))
theorem CategoryTheory.Mat_.additiveObjIsoBiproduct_naturality' {C : Type u₁} [] {D : Type u₁} [] (F : ) [F.Additive] {M : } {N : } (f : M N) :
= CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.matrix fun (i : M) (j : N) => F.map (.map (f i j)))
@[simp]
theorem CategoryTheory.Mat_.lift_map {C : Type u₁} [] {D : Type u₁} [] (F : ) [F.Additive] :
∀ {X Y : } (f : X Y), .map f = CategoryTheory.Limits.biproduct.matrix fun (i : X) (j : Y) => F.map (f i j)
@[simp]
theorem CategoryTheory.Mat_.lift_obj {C : Type u₁} [] {D : Type u₁} [] (F : ) [F.Additive] (X : ) :
.obj X = fun (i : X) => F.obj (X.X i)
def CategoryTheory.Mat_.lift {C : Type u₁} [] {D : Type u₁} [] (F : ) [F.Additive] :

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
instance CategoryTheory.Mat_.lift_additive {C : Type u₁} [] {D : Type u₁} [] (F : ) [F.Additive] :
Equations
• =
@[simp]
theorem CategoryTheory.Mat_.embeddingLiftIso_hom_app {C : Type u₁} [] {D : Type u₁} [] (F : ) [F.Additive] (X : C) :
@[simp]
theorem CategoryTheory.Mat_.embeddingLiftIso_inv_app {C : Type u₁} [] {D : Type u₁} [] (F : ) [F.Additive] (X : C) :
def CategoryTheory.Mat_.embeddingLiftIso {C : Type u₁} [] {D : Type u₁} [] (F : ) [F.Additive] :
F

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
def CategoryTheory.Mat_.liftUnique {C : Type u₁} [] {D : Type u₁} [] (F : ) [F.Additive] (L : ) [L.Additive] (α : .comp L F) :

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
def CategoryTheory.Mat_.ext {C : Type u₁} [] {D : Type u₁} [] {F : } {G : } [F.Additive] [G.Additive] (α : .comp F .comp G) :
F G

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

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
@[simp]
@[simp]
def CategoryTheory.Mat :
Type u → Type (u + 1)

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
• = id inferInstance
Equations
• = CategoryTheory.Bundled.coeSort
theorem CategoryTheory.Mat.hom_ext {R : Type u} [] {X : } {Y : } (f : X Y) (g : X Y) (h : ∀ (i : X) (j : Y), f i j = g i j) :
f = g
theorem CategoryTheory.Mat.id_def (R : Type u) [] (M : ) :
= fun (i j : M) => if i = j then 1 else 0
theorem CategoryTheory.Mat.id_apply (R : Type u) [] (M : ) (i : M) (j : M) :
= if i = j then 1 else 0
@[simp]
theorem CategoryTheory.Mat.id_apply_self (R : Type u) [] (M : ) (i : M) :
@[simp]
theorem CategoryTheory.Mat.id_apply_of_ne (R : Type u) [] (M : ) (i : M) (j : M) (h : i j) :
theorem CategoryTheory.Mat.comp_def (R : Type u) [] {M : } {N : } {K : } (f : M N) (g : N K) :
= fun (i : M) (k : K) => Finset.univ.sum fun (j : N) => f i j * g j k
@[simp]
theorem CategoryTheory.Mat.comp_apply (R : Type u) [] {M : } {N : } {K : } (f : M N) (g : N K) (i : M) (k : K) :
= Finset.univ.sum fun (j : N) => f i j * g j k
instance CategoryTheory.Mat.instInhabitedHom (R : Type u) [] (M : ) (N : ) :
Equations
• = { default := fun (x : M) (x : N) => 0 }
@[simp]
theorem CategoryTheory.Mat.equivalenceSingleObjInverse_map (R : Type) [Ring R] :
∀ {X Y : } (f : X Y) (i : ((fun (X : ) => ) X)) (j : ((fun (X : ) => ) Y)), = MulOpposite.unop (f i j)

Auxiliary definition for CategoryTheory.Mat.equivalenceSingleObj.

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• =
Equations
• =
Equations
• =

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
• = .asEquivalence.symm
Instances For
instance CategoryTheory.Mat.instAddCommGroupHom (R : Type) [Ring R] (X : ) (Y : ) :
Equations
• = let_fun this := inferInstance; this
@[simp]
theorem CategoryTheory.Mat.add_apply {R : Type} [Ring R] {M : } {N : } (f : M N) (g : M N) (i : M) (j : N) :
(f + g) i j = f i j + g i j
Equations