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 (v₁+1) u₁)

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

@[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
  • f.comp g = λ (i : M.ι) (k : K.ι), ∑ (j : N.ι), f i j g j k
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.ι), ∑ (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 = ∑ (j : N.ι), f i j g j k
@[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
@[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, D := λ (a b : M.ι), M.D a b, X := λ (i : M.ι), F.obj (M.X i)}.ι) (j : {ι := N.ι, F := N.F, D := λ (a b : N.ι), N.D a b, 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
@[simp]

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, D := λ (a b : punit), punit.decidable_eq a b, X := λ (_x : punit), X}.ι) (_x_1 : {ι := punit, F := punit.fintype, D := λ (a b : punit), punit.decidable_eq a b, X := λ (_x : punit), Y}.ι) :

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

Equations

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

Equations

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

Equations