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
        def CategoryTheory.Mat_.Hom.comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {M N K : CategoryTheory.Mat_ C} (f : M.Hom N) (g : N.Hom K) :
        M.Hom K

        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 N : CategoryTheory.Mat_ C} (f 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 N K : CategoryTheory.Mat_ C} (f : M N) (g : N K) :
          CategoryTheory.CategoryStruct.comp f g = fun (i : M) (k : K) => 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 N K : CategoryTheory.Mat_ C} (f : M N) (g : N K) (i : M) (k : K) :
          Equations
          • M.instInhabitedHom N = { default := fun (i : M) (j : N) => 0 }
          Equations
          • M.instAddCommGroupHom N = id inferInstance
          @[simp]
          theorem CategoryTheory.Mat_.add_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {M N : CategoryTheory.Mat_ C} (f 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.

          A functor induces a functor of matrix categories.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[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)

            The identity functor induces the identity functor on matrix categories.

            Equations
            Instances For

              Composite functors induce composite functors on matrix categories.

              Equations
              Instances For

                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_.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✝¹ : ((fun (X : C) => CategoryTheory.Mat_.mk PUnit.{1} fun (x : PUnit.{1}) => X) Y✝)) :
                  (CategoryTheory.Mat_.embedding C).map f x✝ x✝¹ = f

                  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
                    @[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) (x : ((CategoryTheory.Mat_.embedding C).obj (M.X i))) (k : M) => if h : i = k then CategoryTheory.eqToHom else 0
                    @[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) (x : ((CategoryTheory.Mat_.embedding C).obj (M.X i))) => if h : j = i then CategoryTheory.eqToHom else 0

                    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 Y : CategoryTheory.Mat R} (f 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 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 j : M) (h : i j) :
                                  theorem CategoryTheory.Mat.comp_def (R : Type u) [Semiring R] {M N K : CategoryTheory.Mat R} (f : M N) (g : N K) :
                                  CategoryTheory.CategoryStruct.comp f g = fun (i : M) (k : K) => j : N, f i j * g j k
                                  @[simp]
                                  theorem CategoryTheory.Mat.comp_apply (R : Type u) [Semiring R] {M N K : CategoryTheory.Mat R} (f : M N) (g : N K) (i : M) (k : K) :
                                  CategoryTheory.CategoryStruct.comp f g i k = 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
                                      @[simp]
                                      theorem CategoryTheory.Mat.add_apply {R : Type} [Ring R] {M N : CategoryTheory.Mat R} (f 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 := }