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₁)

• ι : Type
• F : Fintype s.ι
• X : s.ι → C

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

def CategoryTheory.Mat_.Hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (M : CategoryTheory.Mat_ C) (N : CategoryTheory.Mat_ C) : Type v₁

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

def CategoryTheory.Mat_.Hom.id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (M : CategoryTheory.Mat_ C) : CategoryTheory.Mat_.Hom M M

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

def CategoryTheory.Mat_.Hom.comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {M : CategoryTheory.Mat_ C} {N : CategoryTheory.Mat_ C} {K : CategoryTheory.Mat_ C} (f : CategoryTheory.Mat_.Hom M N) (g : CategoryTheory.Mat_.Hom N K) : CategoryTheory.Mat_.Hom M K

Composition of matrices using matrix multiplication.

instance CategoryTheory.Mat_.instCategoryMat_ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] : CategoryTheory.Category.{v₁, max 1 u₁} (CategoryTheory.Mat_ C)

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_def {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (M : CategoryTheory.Mat_ C) : CategoryTheory.CategoryStruct.id M = fun i j => if h : i = j then CategoryTheory.eqToHom (_ : CategoryTheory.Mat_.X M i = CategoryTheory.Mat_.X M j) else 0

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_self {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (M : CategoryTheory.Mat_ C) (i : M.ι) : CategoryTheory.CategoryStruct.id (CategoryTheory.Mat_ C) CategoryTheory.Category.toCategoryStruct M i i = CategoryTheory.CategoryStruct.id (CategoryTheory.Mat_.X M i)

@[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

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 k => Finset.sum Finset.univ fun j => 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 (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)

instance CategoryTheory.Mat_.instInhabitedHomMat_ToQuiverToCategoryStructInstCategoryMat_ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (M : CategoryTheory.Mat_ C) (N : CategoryTheory.Mat_ C) : Inhabited (M ⟶ N)

instance CategoryTheory.Mat_.instAddCommGroupHomMat_ToQuiverToCategoryStructInstCategoryMat_ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (M : CategoryTheory.Mat_ C) (N : CategoryTheory.Mat_ C) : AddCommGroup (M ⟶ N)

@[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

instance CategoryTheory.Mat_.instPreadditiveMat_InstCategoryMat_ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] : CategoryTheory.Preadditive (CategoryTheory.Mat_ C)

instance CategoryTheory.Mat_.hasFiniteBiproducts {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] : CategoryTheory.Limits.HasFiniteBiproducts (CategoryTheory.Mat_ C)

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.Functor.mapMat__obj_F {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] (M : CategoryTheory.Mat_ C) : ((CategoryTheory.Functor.mapMat_ F).obj M).F = M.F

@[simp]

theorem CategoryTheory.Functor.mapMat__obj_ι {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] (M : CategoryTheory.Mat_ C) : ((CategoryTheory.Functor.mapMat_ F).obj M).ι = M.ι

@[simp]

theorem CategoryTheory.Functor.mapMat__obj_X {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] (M : CategoryTheory.Mat_ C) (i : M.ι) : CategoryTheory.Mat_.X ((CategoryTheory.Functor.mapMat_ F).obj M) i = F.obj (CategoryTheory.Mat_.X M i)

def CategoryTheory.Functor.mapMat_ {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] : CategoryTheory.Functor (CategoryTheory.Mat_ C) (CategoryTheory.Mat_ D)

A functor induces a functor of matrix categories.

@[simp]

theorem CategoryTheory.Functor.mapMatId_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.Mat_ C) : CategoryTheory.Functor.mapMatId.inv.app X = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.mapMat_ (CategoryTheory.Functor.id C)).obj X)

@[simp]

theorem CategoryTheory.Functor.mapMatId_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (X : CategoryTheory.Mat_ C) : CategoryTheory.Functor.mapMatId.hom.app X = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.mapMat_ (CategoryTheory.Functor.id C)).obj X)

def CategoryTheory.Functor.mapMatId {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] : CategoryTheory.Functor.mapMat_ (CategoryTheory.Functor.id C) ≅ CategoryTheory.Functor.id (CategoryTheory.Mat_ C)

The identity functor induces the identity functor on matrix categories.

@[simp]

theorem CategoryTheory.Functor.mapMatComp_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u_1} [CategoryTheory.Category.{v₁, u_1} D] [CategoryTheory.Preadditive D] {E : Type u_2} [CategoryTheory.Category.{v₁, u_2} E] [CategoryTheory.Preadditive E] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] (G : CategoryTheory.Functor D E) [CategoryTheory.Functor.Additive G] (X : CategoryTheory.Mat_ C) : (CategoryTheory.Functor.mapMatComp F G).inv.app X = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.mapMat_ (CategoryTheory.Functor.comp F G)).obj X)

@[simp]

theorem CategoryTheory.Functor.mapMatComp_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u_1} [CategoryTheory.Category.{v₁, u_1} D] [CategoryTheory.Preadditive D] {E : Type u_2} [CategoryTheory.Category.{v₁, u_2} E] [CategoryTheory.Preadditive E] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] (G : CategoryTheory.Functor D E) [CategoryTheory.Functor.Additive G] (X : CategoryTheory.Mat_ C) : (CategoryTheory.Functor.mapMatComp F G).hom.app X = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.mapMat_ (CategoryTheory.Functor.comp F G)).obj X)

def CategoryTheory.Functor.mapMatComp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u_1} [CategoryTheory.Category.{v₁, u_1} D] [CategoryTheory.Preadditive D] {E : Type u_2} [CategoryTheory.Category.{v₁, u_2} E] [CategoryTheory.Preadditive E] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] (G : CategoryTheory.Functor D E) [CategoryTheory.Functor.Additive G] : CategoryTheory.Functor.mapMat_ (CategoryTheory.Functor.comp F G) ≅ CategoryTheory.Functor.comp (CategoryTheory.Functor.mapMat_ F) (CategoryTheory.Functor.mapMat_ G)

Composite functors induce composite functors on matrix categories.

@[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

@[simp]

theorem CategoryTheory.Mat_.embedding_obj_F (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (X : C) : ((CategoryTheory.Mat_.embedding C).obj X).F = PUnit.fintype

@[simp]

theorem CategoryTheory.Mat_.embedding_obj_X (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (X : C) : ∀ (x : PUnit.{1}), CategoryTheory.Mat_.X ((CategoryTheory.Mat_.embedding C).obj X) x = X

@[simp]

theorem CategoryTheory.Mat_.embedding_obj_ι (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (X : C) : ((CategoryTheory.Mat_.embedding C).obj X).ι = PUnit.{1}

def CategoryTheory.Mat_.embedding (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] : CategoryTheory.Functor C (CategoryTheory.Mat_ C)

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

instance CategoryTheory.Mat_.Embedding.instFaithfulMat_InstCategoryMat_Embedding (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] : CategoryTheory.Faithful (CategoryTheory.Mat_.embedding C)

instance CategoryTheory.Mat_.Embedding.instFullMat_InstCategoryMat_Embedding (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] : CategoryTheory.Full (CategoryTheory.Mat_.embedding C)

instance CategoryTheory.Mat_.Embedding.instAdditiveMat_InstCategoryMat_InstPreadditiveMat_InstCategoryMat_Embedding (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] : CategoryTheory.Functor.Additive (CategoryTheory.Mat_.embedding C)

instance CategoryTheory.Mat_.instInhabitedMat_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [Inhabited C] : Inhabited (CategoryTheory.Mat_ C)

@[simp]

theorem CategoryTheory.Mat_.isoBiproductEmbedding_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (M : CategoryTheory.Mat_ C) : (CategoryTheory.Mat_.isoBiproductEmbedding M).hom = CategoryTheory.Limits.biproduct.lift fun i j k => if h : j = i then CategoryTheory.eqToHom (_ : CategoryTheory.Mat_.X M j = CategoryTheory.Mat_.X M i) else 0

@[simp]

theorem CategoryTheory.Mat_.isoBiproductEmbedding_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (M : CategoryTheory.Mat_ C) : (CategoryTheory.Mat_.isoBiproductEmbedding M).inv = CategoryTheory.Limits.biproduct.desc fun i j k => if h : i = k then CategoryTheory.eqToHom (_ : CategoryTheory.Mat_.X M i = CategoryTheory.Mat_.X M k) else 0

def CategoryTheory.Mat_.isoBiproductEmbedding {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (M : CategoryTheory.Mat_ C) : M ≅ ⨁ fun i => (CategoryTheory.Mat_.embedding C).obj (CategoryTheory.Mat_.X M i)

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

instance CategoryTheory.Mat_.instHasBiproductιPreadditiveHasZeroMorphismsObjMat_ToQuiverToCategoryStructInstCategoryMat_ToQuiverToCategoryStructToPrefunctorObjToPrefunctorEmbeddingX {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor (CategoryTheory.Mat_ C) D) [CategoryTheory.Functor.Additive F] (M : CategoryTheory.Mat_ C) : CategoryTheory.Limits.HasBiproduct fun i => F.obj ((CategoryTheory.Mat_.embedding C).obj (CategoryTheory.Mat_.X M i))

def CategoryTheory.Mat_.additiveObjIsoBiproduct {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor (CategoryTheory.Mat_ C) D) [CategoryTheory.Functor.Additive F] (M : CategoryTheory.Mat_ C) : F.obj M ≅ ⨁ fun i => F.obj ((CategoryTheory.Mat_.embedding C).obj (CategoryTheory.Mat_.X M i))

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

@[simp]

theorem CategoryTheory.Mat_.additiveObjIsoBiproduct_hom_π_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor (CategoryTheory.Mat_ C) D) [CategoryTheory.Functor.Additive F] (M : CategoryTheory.Mat_ C) (i : M.ι) {Z : D} (h : F.obj ((CategoryTheory.Mat_.embedding C).obj (CategoryTheory.Mat_.X M i)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Mat_.additiveObjIsoBiproduct F M).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π (fun i => F.obj ((CategoryTheory.Mat_.embedding C).obj (CategoryTheory.Mat_.X M i))) i) h) = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.Mat_.isoBiproductEmbedding M).hom (CategoryTheory.Limits.biproduct.π (fun i => (CategoryTheory.Mat_.embedding C).obj (CategoryTheory.Mat_.X M i)) i))) h

@[simp]

theorem CategoryTheory.Mat_.additiveObjIsoBiproduct_hom_π {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor (CategoryTheory.Mat_ C) D) [CategoryTheory.Functor.Additive F] (M : CategoryTheory.Mat_ C) (i : M.ι) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Mat_.additiveObjIsoBiproduct F M).hom (CategoryTheory.Limits.biproduct.π (fun i => F.obj ((CategoryTheory.Mat_.embedding C).obj (CategoryTheory.Mat_.X M i))) i) = F.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.Mat_.isoBiproductEmbedding M).hom (CategoryTheory.Limits.biproduct.π (fun i => (CategoryTheory.Mat_.embedding C).obj (CategoryTheory.Mat_.X M i)) i))

@[simp]

theorem CategoryTheory.Mat_.ι_additiveObjIsoBiproduct_inv_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor (CategoryTheory.Mat_ C) D) [CategoryTheory.Functor.Additive F] (M : CategoryTheory.Mat_ C) (i : M.ι) {Z : D} (h : F.obj M ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun i => F.obj ((CategoryTheory.Mat_.embedding C).obj (CategoryTheory.Mat_.X M i))) i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Mat_.additiveObjIsoBiproduct F M).inv h) = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun i => (CategoryTheory.Mat_.embedding C).obj (CategoryTheory.Mat_.X M i)) i) (CategoryTheory.Mat_.isoBiproductEmbedding M).inv)) h

@[simp]

theorem CategoryTheory.Mat_.ι_additiveObjIsoBiproduct_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor (CategoryTheory.Mat_ C) D) [CategoryTheory.Functor.Additive F] (M : CategoryTheory.Mat_ C) (i : M.ι) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun i => F.obj ((CategoryTheory.Mat_.embedding C).obj (CategoryTheory.Mat_.X M i))) i) (CategoryTheory.Mat_.additiveObjIsoBiproduct F M).inv = F.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun i => (CategoryTheory.Mat_.embedding C).obj (CategoryTheory.Mat_.X M i)) i) (CategoryTheory.Mat_.isoBiproductEmbedding M).inv)

theorem CategoryTheory.Mat_.additiveObjIsoBiproduct_naturality_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (F : CategoryTheory.Functor (CategoryTheory.Mat_ C) D) [CategoryTheory.Functor.Additive F] {M : CategoryTheory.Mat_ C} {N : CategoryTheory.Mat_ C} (f : M ⟶ N) {Z : D} (h : (⨁ fun i => F.obj ((CategoryTheory.Mat_.embedding C).obj (CategoryTheory.Mat_.X N i))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Mat_.additiveObjIsoBiproduct F N).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Mat_.additiveObjIsoBiproduct F M).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.matrix fun i j => F.map ((CategoryTheory.Mat_.embedding C).map (f i j))) h)

theorem CategoryTheory.Mat_.additiveObjIsoBiproduct_naturality {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (F : CategoryTheory.Functor (CategoryTheory.Mat_ C) D) [CategoryTheory.Functor.Additive F] {M : CategoryTheory.Mat_ C} {N : CategoryTheory.Mat_ C} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp (F.map f) (CategoryTheory.Mat_.additiveObjIsoBiproduct F N).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Mat_.additiveObjIsoBiproduct F M).hom (CategoryTheory.Limits.biproduct.matrix fun i j => F.map ((CategoryTheory.Mat_.embedding C).map (f i j)))

theorem CategoryTheory.Mat_.additiveObjIsoBiproduct_naturality'_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (F : CategoryTheory.Functor (CategoryTheory.Mat_ C) D) [CategoryTheory.Functor.Additive F] {M : CategoryTheory.Mat_ C} {N : CategoryTheory.Mat_ C} (f : M ⟶ N) {Z : D} (h : F.obj N ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Mat_.additiveObjIsoBiproduct F M).inv (CategoryTheory.CategoryStruct.comp (F.map f) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.matrix fun i j => F.map ((CategoryTheory.Mat_.embedding C).map (f i j))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Mat_.additiveObjIsoBiproduct F N).inv h)

theorem CategoryTheory.Mat_.additiveObjIsoBiproduct_naturality' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (F : CategoryTheory.Functor (CategoryTheory.Mat_ C) D) [CategoryTheory.Functor.Additive F] {M : CategoryTheory.Mat_ C} {N : CategoryTheory.Mat_ C} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Mat_.additiveObjIsoBiproduct F M).inv (F.map f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.matrix fun i j => F.map ((CategoryTheory.Mat_.embedding C).map (f i j))) (CategoryTheory.Mat_.additiveObjIsoBiproduct F N).inv

@[simp]

theorem CategoryTheory.Mat_.lift_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] : ∀ {X Y : CategoryTheory.Mat_ C} (f : X ⟶ Y), (CategoryTheory.Mat_.lift F).map f = CategoryTheory.Limits.biproduct.matrix fun i j => F.map (f i j)

@[simp]

theorem CategoryTheory.Mat_.lift_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] (X : CategoryTheory.Mat_ C) : (CategoryTheory.Mat_.lift F).obj X = ⨁ fun i => F.obj (CategoryTheory.Mat_.X X i)

def CategoryTheory.Mat_.lift {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] : CategoryTheory.Functor (CategoryTheory.Mat_ C) D

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

instance CategoryTheory.Mat_.lift_additive {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] : CategoryTheory.Functor.Additive (CategoryTheory.Mat_.lift F)

@[simp]

theorem CategoryTheory.Mat_.embeddingLiftIso_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] (X : C) : (CategoryTheory.Mat_.embeddingLiftIso F).inv.app X = CategoryTheory.Limits.biproduct.lift fun x => CategoryTheory.CategoryStruct.id (F.obj X)

@[simp]

theorem CategoryTheory.Mat_.embeddingLiftIso_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] (X : C) : (CategoryTheory.Mat_.embeddingLiftIso F).hom.app X = CategoryTheory.Limits.biproduct.desc fun x => CategoryTheory.CategoryStruct.id (F.obj X)

def CategoryTheory.Mat_.embeddingLiftIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] : CategoryTheory.Functor.comp (CategoryTheory.Mat_.embedding C) (CategoryTheory.Mat_.lift F) ≅ F

An additive functor C ⥤ D factors through its lift to Mat_ C ⥤ D.

def CategoryTheory.Mat_.liftUnique {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Additive F] (L : CategoryTheory.Functor (CategoryTheory.Mat_ C) D) [CategoryTheory.Functor.Additive L] (α : CategoryTheory.Functor.comp (CategoryTheory.Mat_.embedding C) L ≅ F) : L ≅ CategoryTheory.Mat_.lift F

Mat_.lift F is the unique additive functor L : Mat_ C ⥤ D such that F ≅ embedding C ⋙ L.

def CategoryTheory.Mat_.ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] {F : CategoryTheory.Functor (CategoryTheory.Mat_ C) D} {G : CategoryTheory.Functor (CategoryTheory.Mat_ C) D} [CategoryTheory.Functor.Additive F] [CategoryTheory.Functor.Additive G] (α : CategoryTheory.Functor.comp (CategoryTheory.Mat_.embedding C) F ≅ CategoryTheory.Functor.comp (CategoryTheory.Mat_.embedding C) G) : F ≅ G

Two additive functors Mat_ C ⥤ D are naturally isomorphic if their precompositions with embedding C are naturally isomorphic as functors C ⥤ D.

def CategoryTheory.Mat_.equivalenceSelfOfHasFiniteBiproductsAux {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] : CategoryTheory.Functor.comp (CategoryTheory.Mat_.embedding C) (CategoryTheory.Functor.id (CategoryTheory.Mat_ C)) ≅ CategoryTheory.Functor.comp (CategoryTheory.Mat_.embedding C) (CategoryTheory.Functor.comp (CategoryTheory.Mat_.lift (CategoryTheory.Functor.id C)) (CategoryTheory.Mat_.embedding C))

Natural isomorphism needed in the construction of equivalenceSelfOfHasFiniteBiproducts.

def CategoryTheory.Mat_.equivalenceSelfOfHasFiniteBiproducts (C : Type (u₁ + 1)) [CategoryTheory.LargeCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] : CategoryTheory.Mat_ C ≌ C

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.

@[simp]

theorem CategoryTheory.Mat_.equivalenceSelfOfHasFiniteBiproducts_functor {C : Type (u₁ + 1)} [CategoryTheory.LargeCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] : (CategoryTheory.Mat_.equivalenceSelfOfHasFiniteBiproducts C).functor = CategoryTheory.Mat_.lift (CategoryTheory.Functor.id C)

@[simp]

theorem CategoryTheory.Mat_.equivalenceSelfOfHasFiniteBiproducts_inverse {C : Type (u₁ + 1)} [CategoryTheory.LargeCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] : (CategoryTheory.Mat_.equivalenceSelfOfHasFiniteBiproducts C).inverse = CategoryTheory.Mat_.embedding C

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.

instance CategoryTheory.instInhabitedMat (R : Type u) : Inhabited (CategoryTheory.Mat R)

instance CategoryTheory.instCoeSortMatType (R : Type u) : CoeSort (CategoryTheory.Mat R) (Type u)

instance CategoryTheory.instCategoryMat (R : Type u) [Semiring R] : CategoryTheory.Category.{u, u + 1} (CategoryTheory.Mat R)

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

instance CategoryTheory.Mat.instInhabitedHomMatToQuiverToCategoryStructInstCategoryMat (R : Type u) [Semiring R] (M : CategoryTheory.Mat R) (N : CategoryTheory.Mat R) : Inhabited (M ⟶ N)

@[simp]

theorem CategoryTheory.Mat.equivalenceSingleObjInverse_obj (R : Type) [Ring R] (X : CategoryTheory.Mat_ (CategoryTheory.SingleObj Rᵐᵒᵖ)) : (CategoryTheory.Mat.equivalenceSingleObjInverse R).obj X = FintypeCat.of X.ι

@[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)

def CategoryTheory.Mat.equivalenceSingleObjInverse (R : Type) [Ring R] : CategoryTheory.Functor (CategoryTheory.Mat_ (CategoryTheory.SingleObj Rᵐᵒᵖ)) (CategoryTheory.Mat R)

Auxiliary definition for CategoryTheory.Mat.equivalenceSingleObj.

instance CategoryTheory.Mat.instFaithfulMat_SingleObjMulOppositeInstCategoryMat_CategoryMonoidToMonoidToMonoidWithZeroToSemiringInstPreadditiveSingleObjCategoryToMonoidToMonoidWithZeroToSemiringRingMatInstCategoryMatEquivalenceSingleObjInverse (R : Type) [Ring R] : CategoryTheory.Faithful (CategoryTheory.Mat.equivalenceSingleObjInverse R)

instance CategoryTheory.Mat.instFullMat_SingleObjMulOppositeInstCategoryMat_CategoryMonoidToMonoidToMonoidWithZeroToSemiringInstPreadditiveSingleObjCategoryToMonoidToMonoidWithZeroToSemiringRingMatInstCategoryMatEquivalenceSingleObjInverse (R : Type) [Ring R] : CategoryTheory.Full (CategoryTheory.Mat.equivalenceSingleObjInverse R)

instance CategoryTheory.Mat.instEssSurjMat_SingleObjMulOppositeMatInstCategoryMat_CategoryMonoidToMonoidToMonoidWithZeroToSemiringInstPreadditiveSingleObjCategoryToMonoidToMonoidWithZeroToSemiringRingInstCategoryMatEquivalenceSingleObjInverse (R : Type) [Ring R] : CategoryTheory.EssSurj (CategoryTheory.Mat.equivalenceSingleObjInverse R)

def CategoryTheory.Mat.equivalenceSingleObj (R : Type) [Ring R] : CategoryTheory.Mat R ≌ CategoryTheory.Mat_ (CategoryTheory.SingleObj Rᵐᵒᵖ)

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.

instance CategoryTheory.Mat.instAddCommGroupHomMatToQuiverToCategoryStructInstCategoryMatToSemiring (R : Type) [Ring R] (X : CategoryTheory.Mat R) (Y : CategoryTheory.Mat R) : AddCommGroup (X ⟶ Y)

@[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

instance CategoryTheory.Mat.instPreadditiveMatInstCategoryMatToSemiring {R : Type} [Ring R] : CategoryTheory.Preadditive (CategoryTheory.Mat R)