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.

    Equations
    • M.Hom N = DMatrix M N fun (i : M) (j : N) => M.X i N.X j
    Instances For

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

      Equations
      Instances For

        Composition of matrices using matrix multiplication.

        Equations
        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_.comp_def {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) :
          CategoryTheory.CategoryStruct.comp f g = 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₁} [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 f g i k = Finset.univ.sum fun (j : N) => CategoryTheory.CategoryStruct.comp (f i j) (g j k)
          Equations
          • M.instInhabitedHom N = { default := fun (i : M) (j : N) => 0 }
          Equations
          • M.instAddCommGroupHom N = let_fun this := inferInstance; this
          @[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) :
          (f + g) i j = f i j + g i j
          Equations
          • CategoryTheory.Mat_.instPreadditive = { homGroup := inferInstance, add_comp := , comp_add := }

          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__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) [F.Additive] :
          ∀ {X Y : CategoryTheory.Mat_ C} (f : X Y) (i : ((fun (M : CategoryTheory.Mat_ C) => CategoryTheory.Mat_.mk M fun (i : M) => F.obj (M.X i)) X)) (j : ((fun (M : CategoryTheory.Mat_ C) => CategoryTheory.Mat_.mk M fun (i : M) => F.obj (M.X i)) Y)), F.mapMat_.map f i j = F.map (f i j)

          A functor induces a functor of matrix categories.

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

            The identity functor induces the identity functor on matrix categories.

            Equations
            Instances For

              Composite functors induce composite functors on matrix categories.

              Equations
              Instances For
                @[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 : 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)), (CategoryTheory.Mat_.embedding C).map f x x_1 = f

                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
                  @[simp]
                  theorem CategoryTheory.Mat_.isoBiproductEmbedding_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (M : CategoryTheory.Mat_ C) :
                  M.isoBiproductEmbedding.hom = CategoryTheory.Limits.biproduct.lift fun (i j : M) (k : ((CategoryTheory.Mat_.embedding C).obj (M.X i))) => if h : j = i then CategoryTheory.eqToHom else 0
                  @[simp]
                  theorem CategoryTheory.Mat_.isoBiproductEmbedding_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (M : CategoryTheory.Mat_ C) :
                  M.isoBiproductEmbedding.inv = CategoryTheory.Limits.biproduct.desc fun (i : M) (j : ((CategoryTheory.Mat_.embedding C).obj (M.X i))) (k : M) => if h : i = k then CategoryTheory.eqToHom else 0

                  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

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

                    Equations
                    Instances For

                      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

                        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

                          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

                            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

                              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
                              • One or more equations did not get rendered due to their size.
                              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.

                                Equations
                                Instances For
                                  Equations
                                  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 : M) => 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 M i j = if i = j then 1 else 0
                                  @[simp]
                                  theorem CategoryTheory.Mat.id_apply_of_ne (R : Type u) [Semiring R] (M : CategoryTheory.Mat R) (i : M) (j : M) (h : i j) :
                                  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 : M) (k : K) => Finset.univ.sum fun (j : N) => 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 f g i k = Finset.univ.sum fun (j : N) => f i j * g j k
                                  Equations

                                  Auxiliary definition for CategoryTheory.Mat.equivalenceSingleObj.

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

                                    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
                                    Instances For
                                      Equations
                                      @[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) :
                                      (f + g) i j = f i j + g i j
                                      Equations
                                      • CategoryTheory.Mat.instPreadditive = { homGroup := inferInstance, add_comp := , comp_add := }