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.

• ι : Type
• fintype : Fintype self.ι
• X : self.ι → 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.

Equations

• M.Hom N = DMatrix M.ι N.ι fun (i : M.ι) (j : N.ι) => M.X i ⟶ N.X j

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

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

Equations

• CategoryTheory.Mat_.Hom.id M i j = if h : i = j then CategoryTheory.eqToHom ⋯ else 0

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 : M.Hom N) (g : N.Hom K) : M.Hom K

Composition of matrices using matrix multiplication.

Equations

• f.comp g i k = Finset.univ.sum fun (j : N.ι) => CategoryTheory.CategoryStruct.comp (f i j) (g j k)

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

Equations

• CategoryTheory.Mat_.instCategory = CategoryTheory.Category.mk ⋯ ⋯ ⋯

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 : M.ι) => if h : i = j then CategoryTheory.eqToHom ⋯ 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 M i j = if h : i = j then CategoryTheory.eqToHom ⋯ 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 M i i = CategoryTheory.CategoryStruct.id (M.X 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 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 : 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)

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

Equations

• M.instInhabitedHom N = { default := fun (i : M.ι) (j : N.ι) => 0 }

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

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

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

Equations

• CategoryTheory.Mat_.instPreadditive = { homGroup := inferInstance, add_comp := ⋯, comp_add := ⋯ }

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.

Equations

• ⋯ = ⋯

@[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) [F.Additive] (M : CategoryTheory.Mat_ C) : (F.mapMat_.obj M).ι = M.ι

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

@[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) [F.Additive] (M : CategoryTheory.Mat_ C) (i : M.ι) : (F.mapMat_.obj M).X i = F.obj (M.X i)

@[simp]

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

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) [F.Additive] : CategoryTheory.Functor (CategoryTheory.Mat_ C) (CategoryTheory.Mat_ D)

A functor induces a functor of matrix categories.

Equations

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

@[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.id C).mapMat_.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.id C).mapMat_.obj X)

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

The identity functor induces the identity functor on matrix categories.

Equations

• CategoryTheory.Functor.mapMatId = CategoryTheory.NatIso.ofComponents (fun (M : CategoryTheory.Mat_ C) => CategoryTheory.eqToIso ⋯) ⋯

@[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) [F.Additive] (G : CategoryTheory.Functor D E) [G.Additive] (X : CategoryTheory.Mat_ C) : (F.mapMatComp G).hom.app X = CategoryTheory.CategoryStruct.id ((F.comp G).mapMat_.obj X)

@[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) [F.Additive] (G : CategoryTheory.Functor D E) [G.Additive] (X : CategoryTheory.Mat_ C) : (F.mapMatComp G).inv.app X = CategoryTheory.CategoryStruct.id ((F.comp G).mapMat_.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) [F.Additive] (G : CategoryTheory.Functor D E) [G.Additive] : (F.comp G).mapMat_ ≅ F.mapMat_.comp G.mapMat_

Composite functors induce composite functors on matrix categories.

Equations

• F.mapMatComp G = CategoryTheory.NatIso.ofComponents (fun (M : CategoryTheory.Mat_ C) => CategoryTheory.eqToIso ⋯) ⋯

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

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

@[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_.embedding C).obj X).X x = X

@[simp]

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

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

Equations

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• CategoryTheory.Mat_.instInhabited C = { default := (CategoryTheory.Mat_.embedding C).obj default }

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

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

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

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.

instance CategoryTheory.Mat_.instHasBiproductιObjEmbeddingXOfAdditive {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) [F.Additive] (M : CategoryTheory.Mat_ C) : CategoryTheory.Limits.HasBiproduct fun (i : M.ι) => F.obj ((CategoryTheory.Mat_.embedding C).obj (M.X i))

Equations

• ⋯ = ⋯

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) [F.Additive] (M : CategoryTheory.Mat_ C) : F.obj M ≅ ⨁ fun (i : M.ι) => F.obj ((CategoryTheory.Mat_.embedding C).obj (M.X i))

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

Equations

• CategoryTheory.Mat_.additiveObjIsoBiproduct F M = (F.mapIso M.isoBiproductEmbedding).trans (F.mapBiproduct fun (i : M.ι) => (CategoryTheory.Mat_.embedding C).obj (M.X i))

@[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) [F.Additive] (M : CategoryTheory.Mat_ C) (i : M.ι) {Z : D} (h : F.obj ((CategoryTheory.Mat_.embedding C).obj (M.X i)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Mat_.additiveObjIsoBiproduct F M).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π (fun (i : M.ι) => F.obj ((CategoryTheory.Mat_.embedding C).obj (M.X i))) i) h) = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.CategoryStruct.comp M.isoBiproductEmbedding.hom (CategoryTheory.Limits.biproduct.π (fun (i : M.ι) => (CategoryTheory.Mat_.embedding C).obj (M.X 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) [F.Additive] (M : CategoryTheory.Mat_ C) (i : M.ι) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Mat_.additiveObjIsoBiproduct F M).hom (CategoryTheory.Limits.biproduct.π (fun (i : M.ι) => F.obj ((CategoryTheory.Mat_.embedding C).obj (M.X i))) i) = F.map (CategoryTheory.CategoryStruct.comp M.isoBiproductEmbedding.hom (CategoryTheory.Limits.biproduct.π (fun (i : M.ι) => (CategoryTheory.Mat_.embedding C).obj (M.X 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) [F.Additive] (M : CategoryTheory.Mat_ C) (i : M.ι) {Z : D} (h : F.obj M ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun (i : M.ι) => F.obj ((CategoryTheory.Mat_.embedding C).obj (M.X 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 : M.ι) => (CategoryTheory.Mat_.embedding C).obj (M.X i)) i) M.isoBiproductEmbedding.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) [F.Additive] (M : CategoryTheory.Mat_ C) (i : M.ι) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun (i : M.ι) => F.obj ((CategoryTheory.Mat_.embedding C).obj (M.X i))) i) (CategoryTheory.Mat_.additiveObjIsoBiproduct F M).inv = F.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι (fun (i : M.ι) => (CategoryTheory.Mat_.embedding C).obj (M.X i)) i) M.isoBiproductEmbedding.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) [F.Additive] {M : CategoryTheory.Mat_ C} {N : CategoryTheory.Mat_ C} (f : M ⟶ N) {Z : D} (h : (⨁ fun (i : N.ι) => F.obj ((CategoryTheory.Mat_.embedding C).obj (N.X 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 : M.ι) (j : N.ι) => 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) [F.Additive] {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 : M.ι) (j : N.ι) => 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) [F.Additive] {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 : M.ι) (j : N.ι) => 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) [F.Additive] {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 : M.ι) (j : N.ι) => F.map ((CategoryTheory.Mat_.embedding C).map (f i j))) (CategoryTheory.Mat_.additiveObjIsoBiproduct F N).inv

@[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) [F.Additive] (X : CategoryTheory.Mat_ C) : (CategoryTheory.Mat_.lift F).obj X = ⨁ fun (i : X.ι) => F.obj (X.X i)

@[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) [F.Additive] : ∀ {X Y : CategoryTheory.Mat_ C} (f : X ⟶ Y), (CategoryTheory.Mat_.lift F).map f = CategoryTheory.Limits.biproduct.matrix fun (i : X.ι) (j : Y.ι) => F.map (f i j)

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) [F.Additive] : 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.

Equations

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

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) [F.Additive] : (CategoryTheory.Mat_.lift F).Additive

Equations

• ⋯ = ⋯

@[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) [F.Additive] (X : C) : (CategoryTheory.Mat_.embeddingLiftIso F).hom.app X = CategoryTheory.Limits.biproduct.desc fun (x : PUnit.{1}) => CategoryTheory.CategoryStruct.id (F.obj X)

@[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) [F.Additive] (X : C) : (CategoryTheory.Mat_.embeddingLiftIso F).inv.app X = CategoryTheory.Limits.biproduct.lift fun (x : PUnit.{1}) => 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) [F.Additive] : (CategoryTheory.Mat_.embedding C).comp (CategoryTheory.Mat_.lift F) ≅ F

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.

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) [F.Additive] (L : CategoryTheory.Functor (CategoryTheory.Mat_ C) D) [L.Additive] (α : (CategoryTheory.Mat_.embedding C).comp 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.

Equations

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

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} [F.Additive] [G.Additive] (α : (CategoryTheory.Mat_.embedding C).comp F ≅ (CategoryTheory.Mat_.embedding C).comp 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.

Equations

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

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

Natural isomorphism needed in the construction of equivalenceSelfOfHasFiniteBiproducts.

Equations

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

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.

Equations

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

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

Equations

• CategoryTheory.Mat x = FintypeCat

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

Equations

• CategoryTheory.instInhabitedMat R = id inferInstance

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

Equations

• CategoryTheory.instCoeSortMatType R = CategoryTheory.Bundled.coeSort

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

Equations

• CategoryTheory.instCategoryMatOfSemiring R = CategoryTheory.Category.mk ⋯ ⋯ ⋯

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_self (R : Type u) [Semiring R] (M : CategoryTheory.Mat R) (i : ↑M) : CategoryTheory.CategoryStruct.id 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 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 : ↑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

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

Equations

• CategoryTheory.Mat.instInhabitedHom R M N = { default := fun (x : ↑M) (x : ↑N) => 0 }

@[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 : CategoryTheory.Mat_ (CategoryTheory.SingleObj Rᵐᵒᵖ)) => FintypeCat.of X.ι) X)) (j : ↑((fun (X : CategoryTheory.Mat_ (CategoryTheory.SingleObj Rᵐᵒᵖ)) => FintypeCat.of X.ι) Y)), (CategoryTheory.Mat.equivalenceSingleObjInverse R).map 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.

Equations

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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.

Equations

• CategoryTheory.Mat.equivalenceSingleObj R = (CategoryTheory.Mat.equivalenceSingleObjInverse R).asEquivalence.symm

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

Equations

• CategoryTheory.Mat.instAddCommGroupHom R X Y = let_fun this := inferInstance; this

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

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

Equations

• CategoryTheory.Mat.instPreadditive = { homGroup := inferInstance, add_comp := ⋯, comp_add := ⋯ }