# 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 category_theory.Mat_ (C : Type u₁)  :
Type (max 1 u₁)

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

Instances for category_theory.Mat_
@[nolint]
def category_theory.Mat_.hom {C : Type u₁} (M N : category_theory.Mat_ C) :
Type v₁

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

Equations
noncomputable def category_theory.Mat_.hom.id {C : Type u₁} (M : category_theory.Mat_ C) :
M.hom M

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

Equations
• = λ (i j : M.ι), dite (i = j) (λ (h : i = j), (λ (h : ¬i = j), 0)
def category_theory.Mat_.hom.comp {C : Type u₁} {M N K : category_theory.Mat_ C} (f : M.hom N) (g : N.hom K) :
M.hom K

Composition of matrices using matrix multiplication.

Equations
@[protected, instance]
noncomputable def category_theory.Mat_.category_theory.category {C : Type u₁}  :
Equations
theorem category_theory.Mat_.id_def {C : Type u₁} (M : category_theory.Mat_ C) :
𝟙 M = λ (i j : M.ι), dite (i = j) (λ (h : i = j), (λ (h : ¬i = j), 0)
theorem category_theory.Mat_.id_apply {C : Type u₁} (M : category_theory.Mat_ C) (i j : M.ι) :
𝟙 M i j = dite (i = j) (λ (h : i = j), (λ (h : ¬i = j), 0)
@[simp]
theorem category_theory.Mat_.id_apply_self {C : Type u₁} (M : category_theory.Mat_ C) (i : M.ι) :
𝟙 M i i = 𝟙 (M.X i)
@[simp]
theorem category_theory.Mat_.id_apply_of_ne {C : Type u₁} (M : category_theory.Mat_ C) (i j : M.ι) (h : i j) :
𝟙 M i j = 0
theorem category_theory.Mat_.comp_def {C : Type u₁} {M N K : category_theory.Mat_ C} (f : M N) (g : N K) :
f g = λ (i : M.ι) (k : K.ι), finset.univ.sum (λ (j : N.ι), f i j g j k)
@[simp]
theorem category_theory.Mat_.comp_apply {C : Type u₁} {M N K : category_theory.Mat_ C} (f : M N) (g : N K) (i : M.ι) (k : K.ι) :
(f g) i k = finset.univ.sum (λ (j : N.ι), f i j g j k)
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem category_theory.Mat_.add_apply {C : Type u₁} {M N : category_theory.Mat_ C} (f g : M N) (i : M.ι) (j : N.ι) :
(f + g) i j = f i j + g i j
@[protected, instance]

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

@[simp]
theorem category_theory.functor.map_Mat__obj_X {C : Type u₁} {D : Type u_1} (F : C D) [F.additive] (M : category_theory.Mat_ C) (i : M.ι) :
(F.map_Mat_.obj M).X i = F.obj (M.X i)
@[simp]
theorem category_theory.functor.map_Mat__map {C : Type u₁} {D : Type u_1} (F : C D) [F.additive] (M N : category_theory.Mat_ C) (f : M N) (i : {ι := M.ι, F := M.F, X := λ (i : M.ι), F.obj (M.X i)}.ι) (j : {ι := N.ι, F := N.F, X := λ (i : N.ι), F.obj (N.X i)}.ι) :
F.map_Mat_.map f i j = F.map (f i j)
@[simp]
theorem category_theory.functor.map_Mat__obj_ι {C : Type u₁} {D : Type u_1} (F : C D) [F.additive] (M : category_theory.Mat_ C) :
(F.map_Mat_.obj M).ι = M.ι
@[simp]
theorem category_theory.functor.map_Mat__obj_F {C : Type u₁} {D : Type u_1} (F : C D) [F.additive] (M : category_theory.Mat_ C) :
(F.map_Mat_.obj M).F = M.F
def category_theory.functor.map_Mat_ {C : Type u₁} {D : Type u_1} (F : C D) [F.additive] :

A functor induces a functor of matrix categories.

Equations
@[simp]
noncomputable def category_theory.functor.map_Mat_id {C : Type u₁}  :

The identity functor induces the identity functor on matrix categories.

Equations
@[simp]
@[simp]
theorem category_theory.functor.map_Mat_comp_hom_app {C : Type u₁} {D : Type u_1} {E : Type u_2} (F : C D) [F.additive] (G : D E) [G.additive] (X : category_theory.Mat_ C) :
(F.map_Mat_comp G).hom.app X = 𝟙 ((F G).map_Mat_.obj X)
noncomputable def category_theory.functor.map_Mat_comp {C : Type u₁} {D : Type u_1} {E : Type u_2} (F : C D) [F.additive] (G : D E) [G.additive] :

Composite functors induce composite functors on matrix categories.

Equations
@[simp]
theorem category_theory.functor.map_Mat_comp_inv_app {C : Type u₁} {D : Type u_1} {E : Type u_2} (F : C D) [F.additive] (G : D E) [G.additive] (X : category_theory.Mat_ C) :
(F.map_Mat_comp G).inv.app X = 𝟙 ((F G).map_Mat_.obj X)
@[simp]
theorem category_theory.Mat_.embedding_obj_X (C : Type u₁) (X : C) (_x : punit) :
.X _x = X
@[simp]
theorem category_theory.Mat_.embedding_obj_ι (C : Type u₁) (X : C) :
@[simp]
theorem category_theory.Mat_.embedding_map (C : Type u₁) (X Y : C) (f : X Y) (_x : {ι := punit, F := punit.fintype, X := λ (_x : punit), X}.ι) (_x_1 : {ι := punit, F := punit.fintype, X := λ (_x : punit), Y}.ι) :
_x _x_1 = f
@[simp]
theorem category_theory.Mat_.embedding_obj_F (C : Type u₁) (X : C) :
def category_theory.Mat_.embedding (C : Type u₁)  :

The embedding of C into Mat_ C as one-by-one matrices. (We index the summands by punit.)

Equations
Instances for category_theory.Mat_.embedding
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
noncomputable def category_theory.Mat_.inhabited (C : Type u₁) [inhabited C] :
Equations
noncomputable def category_theory.Mat_.iso_biproduct_embedding {C : Type u₁} (M : category_theory.Mat_ C) :
M λ (i : M.ι), (M.X i)

Every object in Mat_ C is isomorphic to the biproduct of its summands.

Equations
@[simp]
theorem category_theory.Mat_.iso_biproduct_embedding_inv {C : Type u₁} (M : category_theory.Mat_ C) :
M.iso_biproduct_embedding.inv = category_theory.limits.biproduct.desc (λ (i : M.ι) (j : (M.X i)).ι) (k : M.ι), dite (i = k) (λ (h : i = k), (λ (h : ¬i = k), 0))
@[simp]
theorem category_theory.Mat_.iso_biproduct_embedding_hom {C : Type u₁} (M : category_theory.Mat_ C) :
M.iso_biproduct_embedding.hom = category_theory.limits.biproduct.lift (λ (i j : M.ι) (k : (M.X i)).ι), dite (j = i) (λ (h : j = i), (λ (h : ¬j = i), 0))
noncomputable def category_theory.Mat_.additive_obj_iso_biproduct {C : Type u₁} {D : Type u₁} (F : D) [F.additive] (M : category_theory.Mat_ C) :
F.obj M λ (i : M.ι), F.obj (M.X i))

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

Equations
@[simp]
theorem category_theory.Mat_.additive_obj_iso_biproduct_inv {C : Type u₁} {D : Type u₁} (F : D) [F.additive] (M : category_theory.Mat_ C) :
= category_theory.limits.biproduct.desc (F.map_bicone (category_theory.limits.biproduct.bicone (λ (i : M.ι), (M.X i)))).ι F.map (category_theory.limits.biproduct.desc (λ (i : M.ι) (j : punit) (k : M.ι), dite (i = k) (λ (h : i = k), (λ (h : ¬i = k), 0)))
@[simp]
theorem category_theory.Mat_.additive_obj_iso_biproduct_hom {C : Type u₁} {D : Type u₁} (F : D) [F.additive] (M : category_theory.Mat_ C) :
= F.map (category_theory.limits.biproduct.lift (λ (i j : M.ι) (k : punit), dite (j = i) (λ (h : j = i), (λ (h : ¬j = i), 0))) category_theory.limits.biproduct.lift (F.map_bicone (category_theory.limits.biproduct.bicone (λ (i : M.ι), (M.X i)))).π
theorem category_theory.Mat_.additive_obj_iso_biproduct_naturality_assoc {C : Type u₁} {D : Type u₁} (F : D) [F.additive] {M N : category_theory.Mat_ C} (f : M N) {X' : D} (f' : ( λ (i : N.ι), F.obj (N.X i))) X') :
F.map f = category_theory.limits.biproduct.matrix (λ (i : M.ι) (j : N.ι), F.map (f i j))) f'
theorem category_theory.Mat_.additive_obj_iso_biproduct_naturality {C : Type u₁} {D : Type u₁} (F : D) [F.additive] {M N : category_theory.Mat_ C} (f : M N) :
= category_theory.limits.biproduct.matrix (λ (i : M.ι) (j : N.ι), F.map (f i j)))
theorem category_theory.Mat_.additive_obj_iso_biproduct_naturality' {C : Type u₁} {D : Type u₁} (F : D) [F.additive] {M N : category_theory.Mat_ C} (f : M N) :
= category_theory.limits.biproduct.matrix (λ (i : M.ι) (j : N.ι), F.map (f i j)))
theorem category_theory.Mat_.additive_obj_iso_biproduct_naturality'_assoc {C : Type u₁} {D : Type u₁} (F : D) [F.additive] {M N : category_theory.Mat_ C} (f : M N) {X' : D} (f' : F.obj N X') :
F.map f f' = category_theory.limits.biproduct.matrix (λ (i : M.ι) (j : N.ι), F.map (f i j)))
@[simp]
theorem category_theory.Mat_.lift_obj {C : Type u₁} {D : Type u₁} (F : C D) [F.additive] (X : category_theory.Mat_ C) :
= λ (i : X.ι), F.obj (X.X i)
noncomputable def category_theory.Mat_.lift {C : Type u₁} {D : Type u₁} (F : C D) [F.additive] :

Any additive functor C ⥤ D to a category D with finite biproducts extends to a functor Mat_ C ⥤ D.

Equations
Instances for category_theory.Mat_.lift
@[simp]
theorem category_theory.Mat_.lift_map {C : Type u₁} {D : Type u₁} (F : C D) [F.additive] (X Y : category_theory.Mat_ C) (f : X Y) :
= category_theory.limits.biproduct.matrix (λ (i : X.ι) (j : Y.ι), F.map (f i j))
@[protected, instance]
def category_theory.Mat_.lift_additive {C : Type u₁} {D : Type u₁} (F : C D) [F.additive] :
noncomputable def category_theory.Mat_.embedding_lift_iso {C : Type u₁} {D : Type u₁} (F : C D) [F.additive] :

An additive functor C ⥤ D factors through its lift to Mat_ C ⥤ D.

Equations
@[simp]
theorem category_theory.Mat_.embedding_lift_iso_hom_app {C : Type u₁} {D : Type u₁} (F : C D) [F.additive] (X : C) :
@[simp]
theorem category_theory.Mat_.embedding_lift_iso_inv_app {C : Type u₁} {D : Type u₁} (F : C D) [F.additive] (X : C) :
noncomputable def category_theory.Mat_.lift_unique {C : Type u₁} {D : Type u₁} (F : C D) [F.additive] (L : D) [L.additive] (α : F) :

Mat_.lift F is the unique additive functor L : Mat_ C ⥤ D such that F ≅ embedding C ⋙ L.

Equations
@[ext]
noncomputable def category_theory.Mat_.ext {C : Type u₁} {D : Type u₁} {F G : D} [F.additive] [G.additive]  :
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

Natural isomorphism needed in the construction of equivalence_self_of_has_finite_biproducts.

Equations
noncomputable def category_theory.Mat_.equivalence_self_of_has_finite_biproducts (C : Type (u₁+1))  :

Note that we only prove this for a large category; otherwise there are universe issues that I haven't attempted to sort out.

Equations
@[simp]
@[simp]
@[nolint]
def category_theory.Mat (R : 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 category_theory.Mat
@[protected, instance]
def category_theory.Mat.inhabited (R : Type u) :
@[protected, instance]
def category_theory.Mat.has_coe_to_sort (R : Type u) :
(Type u)
Equations
@[protected, instance]
noncomputable def category_theory.Mat.category (R : Type u) [semiring R] :
Equations
theorem category_theory.Mat.id_def (R : Type u) [semiring R] (M : category_theory.Mat R) :
𝟙 M = λ (i j : M), dite (i = j) (λ (h : i = j), 1) (λ (h : ¬i = j), 0)
theorem category_theory.Mat.id_apply (R : Type u) [semiring R] (M : category_theory.Mat R) (i j : M) :
𝟙 M i j = dite (i = j) (λ (h : i = j), 1) (λ (h : ¬i = j), 0)
@[simp]
theorem category_theory.Mat.id_apply_self (R : Type u) [semiring R] (M : category_theory.Mat R) (i : M) :
𝟙 M i i = 1
@[simp]
theorem category_theory.Mat.id_apply_of_ne (R : Type u) [semiring R] (M : category_theory.Mat R) (i j : M) (h : i j) :
𝟙 M i j = 0
theorem category_theory.Mat.comp_def (R : Type u) [semiring R] {M N K : category_theory.Mat R} (f : M N) (g : N K) :
f g = λ (i : M) (k : K), finset.univ.sum (λ (j : N), f i j * g j k)
@[simp]
theorem category_theory.Mat.comp_apply (R : Type u) [semiring R] {M N K : category_theory.Mat R} (f : M N) (g : N K) (i : M) (k : K) :
(f g) i k = finset.univ.sum (λ (j : N), f i j * g j k)
@[protected, instance]
Equations

Auxiliary definition for category_theory.Mat.equivalence_single_obj.

Equations
Instances for category_theory.Mat.equivalence_single_obj_inverse
@[simp]
theorem category_theory.Mat.equivalence_single_obj_inverse_map (R : Type) [ring R] (f : X Y) (i : (Fintype.of X.ι)) (j : (Fintype.of Y.ι)) :
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
noncomputable def category_theory.Mat.equivalence_single_obj (R : Type) [ring R] :

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
@[protected, instance]
Equations