mathlib documentation

category_theory.preadditive.Mat

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.

structure category_theory.Mat_ (C : Type u₁) [category_theory.category C] [category_theory.preadditive C] :
Type (max 1 u₁)

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

Instances for category_theory.Mat_
@[nolint]

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

Equations

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

Equations
def category_theory.Mat_.hom.comp {C : Type u₁} [category_theory.category C] [category_theory.preadditive C] {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
theorem category_theory.Mat_.id_def {C : Type u₁} [category_theory.category C] [category_theory.preadditive C] (M : category_theory.Mat_ C) :
𝟙 M = λ (i j : M.ι), dite (i = j) (λ (h : i = j), category_theory.eq_to_hom _) (λ (h : ¬i = j), 0)
theorem category_theory.Mat_.id_apply {C : Type u₁} [category_theory.category C] [category_theory.preadditive C] (M : category_theory.Mat_ C) (i j : M.ι) :
𝟙 M i j = dite (i = j) (λ (h : i = j), category_theory.eq_to_hom _) (λ (h : ¬i = j), 0)
@[simp]
@[simp]
theorem category_theory.Mat_.id_apply_of_ne {C : Type u₁} [category_theory.category C] [category_theory.preadditive C] (M : category_theory.Mat_ C) (i j : M.ι) (h : i j) :
𝟙 M i j = 0
theorem category_theory.Mat_.comp_def {C : Type u₁} [category_theory.category C] [category_theory.preadditive C] {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₁} [category_theory.category C] [category_theory.preadditive C] {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
@[simp]
theorem category_theory.Mat_.add_apply {C : Type u₁} [category_theory.category C] [category_theory.preadditive C] {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__map {C : Type u₁} [category_theory.category C] [category_theory.preadditive C] {D : Type u_1} [category_theory.category D] [category_theory.preadditive D] (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)

A functor induces a functor of matrix categories.

Equations

The identity functor induces the identity functor on matrix categories.

Equations

Composite functors induce composite functors on matrix categories.

Equations
@[simp]
theorem category_theory.Mat_.embedding_map (C : Type u₁) [category_theory.category C] [category_theory.preadditive C] (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}.ι) :

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

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

Equations

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

Equations

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

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

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