Documentation

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

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

Instances For

    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.

      Instances For
        theorem CategoryTheory.Mat_.hom_ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {M : CategoryTheory.Mat_ C} {N : CategoryTheory.Mat_ C} (f : M N) (g : M N) (H : ∀ (i : M) (j : N), f i j = g i j) :
        f = g
        theorem CategoryTheory.Mat_.id_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (M : CategoryTheory.Mat_ C) (i : M) (j : M) :
        CategoryTheory.CategoryStruct.id (CategoryTheory.Mat_ C) CategoryTheory.Category.toCategoryStruct M i j = if h : i = j then CategoryTheory.eqToHom (_ : CategoryTheory.Mat_.X M i = CategoryTheory.Mat_.X M j) else 0
        @[simp]
        theorem CategoryTheory.Mat_.id_apply_of_ne {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (M : CategoryTheory.Mat_ C) (i : M) (j : M) (h : i j) :
        CategoryTheory.CategoryStruct.id (CategoryTheory.Mat_ C) CategoryTheory.Category.toCategoryStruct M i j = 0
        @[simp]
        theorem CategoryTheory.Mat_.comp_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {M : CategoryTheory.Mat_ C} {N : CategoryTheory.Mat_ C} {K : CategoryTheory.Mat_ C} (f : M N) (g : N K) (i : M) (k : K) :
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Mat_ C) CategoryTheory.Category.toCategoryStruct M N K f g i k = Finset.sum Finset.univ fun j => CategoryTheory.CategoryStruct.comp (f i j) (g j k)
        @[simp]
        theorem CategoryTheory.Mat_.add_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {M : CategoryTheory.Mat_ C} {N : CategoryTheory.Mat_ C} (f : M N) (g : M N) (i : M) (j : N) :
        ((M N) + (M N)) (M N) instHAdd f g i j = f i j + g i j

        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.

        @[simp]
        theorem CategoryTheory.Functor.mapMat__map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u_1} [CategoryTheory.Category.{v₁, u_1} D] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] :
        ∀ {X Y : CategoryTheory.Mat_ C} (f : X Y) (i : ((fun M => CategoryTheory.Mat_.mk M fun i => F.obj (CategoryTheory.Mat_.X M i)) X).ι) (j : ((fun M => CategoryTheory.Mat_.mk M fun i => F.obj (CategoryTheory.Mat_.X M i)) Y).ι), (CategoryTheory.Mat_ C).map CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.Mat_ D) CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.Functor.mapMat_ F).toPrefunctor X Y f i j = F.map (f i j)
        @[simp]
        theorem CategoryTheory.Mat_.embedding_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] :
        ∀ {X Y : C} (f : X Y) (x : ((fun X => CategoryTheory.Mat_.mk PUnit.{1} fun x => X) X).ι) (x_1 : ((fun X => CategoryTheory.Mat_.mk PUnit.{1} fun x => X) Y).ι), C.map CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.Mat_ C) CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.Mat_.embedding C).toPrefunctor X Y f x x_1 = f

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

        Instances For

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

          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.

            Instances For
              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.

              Instances For
                theorem CategoryTheory.Mat.hom_ext {R : Type u} [Semiring R] {X : CategoryTheory.Mat R} {Y : CategoryTheory.Mat R} (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) [Semiring R] (M : CategoryTheory.Mat R) :
                CategoryTheory.CategoryStruct.id M = fun i j => if i = j then 1 else 0
                theorem CategoryTheory.Mat.id_apply (R : Type u) [Semiring R] (M : CategoryTheory.Mat R) (i : M) (j : M) :
                CategoryTheory.CategoryStruct.id (CategoryTheory.Mat R) CategoryTheory.Category.toCategoryStruct M i j = if i = j then 1 else 0
                @[simp]
                theorem CategoryTheory.Mat.id_apply_self (R : Type u) [Semiring R] (M : CategoryTheory.Mat R) (i : M) :
                CategoryTheory.CategoryStruct.id (CategoryTheory.Mat R) CategoryTheory.Category.toCategoryStruct M i i = 1
                @[simp]
                theorem CategoryTheory.Mat.id_apply_of_ne (R : Type u) [Semiring R] (M : CategoryTheory.Mat R) (i : M) (j : M) (h : i j) :
                CategoryTheory.CategoryStruct.id (CategoryTheory.Mat R) CategoryTheory.Category.toCategoryStruct M i j = 0
                theorem CategoryTheory.Mat.comp_def (R : Type u) [Semiring R] {M : CategoryTheory.Mat R} {N : CategoryTheory.Mat R} {K : CategoryTheory.Mat R} (f : M N) (g : N K) :
                CategoryTheory.CategoryStruct.comp f g = fun i k => Finset.sum Finset.univ fun j => f i j * g j k
                @[simp]
                theorem CategoryTheory.Mat.comp_apply (R : Type u) [Semiring R] {M : CategoryTheory.Mat R} {N : CategoryTheory.Mat R} {K : CategoryTheory.Mat R} (f : M N) (g : N K) (i : M) (k : K) :
                CategoryTheory.CategoryStruct.comp (CategoryTheory.Mat R) CategoryTheory.Category.toCategoryStruct M N K f g i k = Finset.sum Finset.univ fun j => f i j * g j k
                @[simp]
                theorem CategoryTheory.Mat.equivalenceSingleObjInverse_map (R : Type) [Ring R] :
                ∀ {X Y : CategoryTheory.Mat_ (CategoryTheory.SingleObj Rᵐᵒᵖ)} (f : X Y) (i : ↑((fun X => FintypeCat.of X) X)) (j : ↑((fun X => FintypeCat.of X) Y)), (CategoryTheory.Mat_ (CategoryTheory.SingleObj Rᵐᵒᵖ)).map CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.Mat R) CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.Mat.equivalenceSingleObjInverse R).toPrefunctor X Y f i j = MulOpposite.unop (f i j)

                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.

                Instances For
                  @[simp]
                  theorem CategoryTheory.Mat.add_apply {R : Type} [Ring R] {M : CategoryTheory.Mat R} {N : CategoryTheory.Mat R} (f : M N) (g : M N) (i : M) (j : N) :
                  ((M N) + (M N)) (M N) instHAdd f g i j = f i j + g i j