Matrices over a category. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
category_theory.Mat_
(C : Type u₁)
[category_theory.category C]
[category_theory.preadditive C] :
Type (max 1 u₁)
An object in Mat_ C is a finite tuple of objects in C.
Instances for category_theory.Mat_
@[nolint]
def
category_theory.Mat_.hom
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
(M N : category_theory.Mat_ C) :
Type v₁
A morphism in Mat_ C is a dependently typed matrix of morphisms.
noncomputable
def
category_theory.Mat_.hom.id
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
(M : category_theory.Mat_ C) :
M.hom M
The identity matrix consists of identity morphisms on the diagonal, and zeros elsewhere.
Equations
- category_theory.Mat_.hom.id M = λ (i j : M.ι), dite (i = j) (λ (h : i = j), category_theory.eq_to_hom _) (λ (h : ¬i = j), 0)
def
category_theory.Mat_.hom.comp
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
{M N K : category_theory.Mat_ C}
(f : M.hom N)
(g : N.hom K) :
M.hom K
Composition of matrices using matrix multiplication.
@[protected, instance]
noncomputable
def
category_theory.Mat_.category_theory.category
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C] :
Equations
- category_theory.Mat_.category_theory.category = {to_category_struct := {to_quiver := {hom := category_theory.Mat_.hom _inst_2}, id := category_theory.Mat_.hom.id _inst_2, comp := λ (M N K : category_theory.Mat_ C) (f : M ⟶ N) (g : N ⟶ K), category_theory.Mat_.hom.comp f g}, id_comp' := _, comp_id' := _, assoc' := _}
theorem
category_theory.Mat_.id_def
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
(M : category_theory.Mat_ C) :
theorem
category_theory.Mat_.id_apply
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
(M : category_theory.Mat_ C)
(i j : M.ι) :
@[simp]
theorem
category_theory.Mat_.id_apply_self
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
(M : category_theory.Mat_ C)
(i : M.ι) :
@[simp]
theorem
category_theory.Mat_.id_apply_of_ne
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
(M : category_theory.Mat_ C)
(i j : M.ι)
(h : i ≠ j) :
theorem
category_theory.Mat_.comp_def
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
{M N K : category_theory.Mat_ C}
(f : M ⟶ N)
(g : N ⟶ K) :
@[simp]
theorem
category_theory.Mat_.comp_apply
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
{M N K : category_theory.Mat_ C}
(f : M ⟶ N)
(g : N ⟶ K)
(i : M.ι)
(k : K.ι) :
@[protected, instance]
def
category_theory.Mat_.quiver.hom.inhabited
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
(M N : category_theory.Mat_ C) :
@[protected, instance]
def
category_theory.Mat_.category_theory.preadditive
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C] :
Equations
- category_theory.Mat_.category_theory.preadditive = {hom_group := λ (M N : category_theory.Mat_ C), id dmatrix.add_comm_group, add_comp' := _, comp_add' := _}
@[simp]
theorem
category_theory.Mat_.add_apply
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
{M N : category_theory.Mat_ C}
(f g : M ⟶ N)
(i : M.ι)
(j : N.ι) :
@[protected, instance]
def
category_theory.Mat_.has_finite_biproducts
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive 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 iso_biproduct_embedding.
@[simp]
theorem
category_theory.functor.map_Mat__obj_X
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u_1}
[category_theory.category D]
[category_theory.preadditive D]
(F : C ⥤ D)
[F.additive]
(M : category_theory.Mat_ C)
(i : M.ι) :
@[simp]
theorem
category_theory.functor.map_Mat__map
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u_1}
[category_theory.category D]
[category_theory.preadditive D]
(F : C ⥤ D)
[F.additive]
(M N : category_theory.Mat_ C)
(f : M ⟶ N)
(i : {ι := M.ι, F := M.F, X := λ (i : M.ι), F.obj (M.X i)}.ι)
(j : {ι := N.ι, F := N.F, X := λ (i : N.ι), F.obj (N.X i)}.ι) :
@[simp]
theorem
category_theory.functor.map_Mat__obj_ι
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u_1}
[category_theory.category D]
[category_theory.preadditive D]
(F : C ⥤ D)
[F.additive]
(M : category_theory.Mat_ C) :
@[simp]
theorem
category_theory.functor.map_Mat__obj_F
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u_1}
[category_theory.category D]
[category_theory.preadditive D]
(F : C ⥤ D)
[F.additive]
(M : category_theory.Mat_ C) :
def
category_theory.functor.map_Mat_
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u_1}
[category_theory.category D]
[category_theory.preadditive D]
(F : C ⥤ D)
[F.additive] :
A functor induces a functor of matrix categories.
Equations
- F.map_Mat_ = {obj := λ (M : category_theory.Mat_ C), {ι := M.ι, F := M.F, X := λ (i : M.ι), F.obj (M.X i)}, map := λ (M N : category_theory.Mat_ C) (f : M ⟶ N) (i : {ι := M.ι, F := M.F, X := λ (i : M.ι), F.obj (M.X i)}.ι) (j : {ι := N.ι, F := N.F, X := λ (i : N.ι), F.obj (N.X i)}.ι), F.map (f i j), map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.functor.map_Mat_id_hom_app
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
(X : category_theory.Mat_ C) :
noncomputable
def
category_theory.functor.map_Mat_id
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C] :
(𝟭 C).map_Mat_ ≅ 𝟭 (category_theory.Mat_ C)
The identity functor induces the identity functor on matrix categories.
Equations
- category_theory.functor.map_Mat_id = category_theory.nat_iso.of_components (λ (M : category_theory.Mat_ C), category_theory.eq_to_iso _) category_theory.functor.map_Mat_id._proof_2
@[simp]
theorem
category_theory.functor.map_Mat_id_inv_app
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
(X : category_theory.Mat_ C) :
@[simp]
theorem
category_theory.functor.map_Mat_comp_hom_app
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u_1}
[category_theory.category D]
[category_theory.preadditive D]
{E : Type u_2}
[category_theory.category E]
[category_theory.preadditive E]
(F : C ⥤ D)
[F.additive]
(G : D ⥤ E)
[G.additive]
(X : category_theory.Mat_ C) :
noncomputable
def
category_theory.functor.map_Mat_comp
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u_1}
[category_theory.category D]
[category_theory.preadditive D]
{E : Type u_2}
[category_theory.category E]
[category_theory.preadditive E]
(F : C ⥤ D)
[F.additive]
(G : D ⥤ E)
[G.additive] :
Composite functors induce composite functors on matrix categories.
Equations
- F.map_Mat_comp G = category_theory.nat_iso.of_components (λ (M : category_theory.Mat_ C), category_theory.eq_to_iso _) _
@[simp]
theorem
category_theory.functor.map_Mat_comp_inv_app
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u_1}
[category_theory.category D]
[category_theory.preadditive D]
{E : Type u_2}
[category_theory.category E]
[category_theory.preadditive E]
(F : C ⥤ D)
[F.additive]
(G : D ⥤ E)
[G.additive]
(X : category_theory.Mat_ C) :
@[simp]
theorem
category_theory.Mat_.embedding_obj_X
(C : Type u₁)
[category_theory.category C]
[category_theory.preadditive C]
(X : C)
(_x : punit) :
((category_theory.Mat_.embedding C).obj X).X _x = X
@[simp]
theorem
category_theory.Mat_.embedding_obj_ι
(C : Type u₁)
[category_theory.category C]
[category_theory.preadditive C]
(X : C) :
((category_theory.Mat_.embedding C).obj X).ι = punit
@[simp]
theorem
category_theory.Mat_.embedding_map
(C : Type u₁)
[category_theory.category C]
[category_theory.preadditive C]
(X Y : C)
(f : X ⟶ Y)
(_x : {ι := punit, F := punit.fintype, X := λ (_x : punit), X}.ι)
(_x_1 : {ι := punit, F := punit.fintype, X := λ (_x : punit), Y}.ι) :
(category_theory.Mat_.embedding C).map f _x _x_1 = f
@[simp]
theorem
category_theory.Mat_.embedding_obj_F
(C : Type u₁)
[category_theory.category C]
[category_theory.preadditive C]
(X : C) :
((category_theory.Mat_.embedding C).obj X).F = punit.fintype
def
category_theory.Mat_.embedding
(C : Type u₁)
[category_theory.category C]
[category_theory.preadditive C] :
The embedding of C into Mat_ C as one-by-one matrices.
(We index the summands by punit.)
Equations
- category_theory.Mat_.embedding C = {obj := λ (X : C), {ι := punit, F := punit.fintype, X := λ (_x : punit), X}, map := λ (X Y : C) (f : X ⟶ Y) (_x : {ι := punit, F := punit.fintype, X := λ (_x : punit), X}.ι) (_x : {ι := punit, F := punit.fintype, X := λ (_x : punit), Y}.ι), f, map_id' := _, map_comp' := _}
Instances for category_theory.Mat_.embedding
@[protected, instance]
@[protected, instance]
def
category_theory.Mat_.embedding.category_theory.full
(C : Type u₁)
[category_theory.category C]
[category_theory.preadditive C] :
Equations
- category_theory.Mat_.embedding.category_theory.full C = {preimage := λ (X Y : C) (f : (category_theory.Mat_.embedding C).obj X ⟶ (category_theory.Mat_.embedding C).obj Y), f punit.star punit.star, witness' := _}
@[protected, instance]
@[protected, instance]
noncomputable
def
category_theory.Mat_.inhabited
(C : Type u₁)
[category_theory.category C]
[category_theory.preadditive C]
[inhabited C] :
Equations
noncomputable
def
category_theory.Mat_.iso_biproduct_embedding
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
(M : category_theory.Mat_ C) :
Every object in Mat_ C is isomorphic to the biproduct of its summands.
Equations
- M.iso_biproduct_embedding = {hom := category_theory.limits.biproduct.lift (λ (i j : M.ι) (k : ((category_theory.Mat_.embedding C).obj (M.X i)).ι), dite (j = i) (λ (h : j = i), category_theory.eq_to_hom _) (λ (h : ¬j = i), 0)), inv := category_theory.limits.biproduct.desc (λ (i : M.ι) (j : ((category_theory.Mat_.embedding C).obj (M.X i)).ι) (k : M.ι), dite (i = k) (λ (h : i = k), category_theory.eq_to_hom _) (λ (h : ¬i = k), 0)), hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.Mat_.iso_biproduct_embedding_inv
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
(M : category_theory.Mat_ C) :
M.iso_biproduct_embedding.inv = category_theory.limits.biproduct.desc (λ (i : M.ι) (j : ((category_theory.Mat_.embedding C).obj (M.X i)).ι) (k : M.ι), dite (i = k) (λ (h : i = k), category_theory.eq_to_hom _) (λ (h : ¬i = k), 0))
@[simp]
theorem
category_theory.Mat_.iso_biproduct_embedding_hom
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
(M : category_theory.Mat_ C) :
M.iso_biproduct_embedding.hom = category_theory.limits.biproduct.lift (λ (i j : M.ι) (k : ((category_theory.Mat_.embedding C).obj (M.X i)).ι), dite (j = i) (λ (h : j = i), category_theory.eq_to_hom _) (λ (h : ¬j = i), 0))
noncomputable
def
category_theory.Mat_.additive_obj_iso_biproduct
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u₁}
[category_theory.category D]
[category_theory.preadditive D]
(F : category_theory.Mat_ C ⥤ D)
[F.additive]
(M : category_theory.Mat_ C) :
Every M is a direct sum of objects from C, and F preserves biproducts.
Equations
- category_theory.Mat_.additive_obj_iso_biproduct F M = F.map_iso M.iso_biproduct_embedding ≪≫ F.map_biproduct (λ (i : M.ι), (category_theory.Mat_.embedding C).obj (M.X i))
@[simp]
theorem
category_theory.Mat_.additive_obj_iso_biproduct_inv
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u₁}
[category_theory.category D]
[category_theory.preadditive D]
(F : category_theory.Mat_ C ⥤ D)
[F.additive]
(M : category_theory.Mat_ C) :
(category_theory.Mat_.additive_obj_iso_biproduct F M).inv = category_theory.limits.biproduct.desc (F.map_bicone (category_theory.limits.biproduct.bicone (λ (i : M.ι), (category_theory.Mat_.embedding C).obj (M.X i)))).ι ≫ F.map (category_theory.limits.biproduct.desc (λ (i : M.ι) (j : punit) (k : M.ι), dite (i = k) (λ (h : i = k), category_theory.eq_to_hom _) (λ (h : ¬i = k), 0)))
@[simp]
theorem
category_theory.Mat_.additive_obj_iso_biproduct_hom
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u₁}
[category_theory.category D]
[category_theory.preadditive D]
(F : category_theory.Mat_ C ⥤ D)
[F.additive]
(M : category_theory.Mat_ C) :
(category_theory.Mat_.additive_obj_iso_biproduct F M).hom = F.map (category_theory.limits.biproduct.lift (λ (i j : M.ι) (k : punit), dite (j = i) (λ (h : j = i), category_theory.eq_to_hom _) (λ (h : ¬j = i), 0))) ≫ category_theory.limits.biproduct.lift (F.map_bicone (category_theory.limits.biproduct.bicone (λ (i : M.ι), (category_theory.Mat_.embedding C).obj (M.X i)))).π
theorem
category_theory.Mat_.additive_obj_iso_biproduct_naturality_assoc
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u₁}
[category_theory.category D]
[category_theory.preadditive D]
[category_theory.limits.has_finite_biproducts D]
(F : category_theory.Mat_ C ⥤ D)
[F.additive]
{M N : category_theory.Mat_ C}
(f : M ⟶ N)
{X' : D}
(f' : (⨁ λ (i : N.ι), F.obj ((category_theory.Mat_.embedding C).obj (N.X i))) ⟶ X') :
F.map f ≫ (category_theory.Mat_.additive_obj_iso_biproduct F N).hom ≫ f' = (category_theory.Mat_.additive_obj_iso_biproduct F M).hom ≫ category_theory.limits.biproduct.matrix (λ (i : M.ι) (j : N.ι), F.map ((category_theory.Mat_.embedding C).map (f i j))) ≫ f'
theorem
category_theory.Mat_.additive_obj_iso_biproduct_naturality
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u₁}
[category_theory.category D]
[category_theory.preadditive D]
[category_theory.limits.has_finite_biproducts D]
(F : category_theory.Mat_ C ⥤ D)
[F.additive]
{M N : category_theory.Mat_ C}
(f : M ⟶ N) :
F.map f ≫ (category_theory.Mat_.additive_obj_iso_biproduct F N).hom = (category_theory.Mat_.additive_obj_iso_biproduct F M).hom ≫ category_theory.limits.biproduct.matrix (λ (i : M.ι) (j : N.ι), F.map ((category_theory.Mat_.embedding C).map (f i j)))
theorem
category_theory.Mat_.additive_obj_iso_biproduct_naturality'
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u₁}
[category_theory.category D]
[category_theory.preadditive D]
[category_theory.limits.has_finite_biproducts D]
(F : category_theory.Mat_ C ⥤ D)
[F.additive]
{M N : category_theory.Mat_ C}
(f : M ⟶ N) :
(category_theory.Mat_.additive_obj_iso_biproduct F M).inv ≫ F.map f = category_theory.limits.biproduct.matrix (λ (i : M.ι) (j : N.ι), F.map ((category_theory.Mat_.embedding C).map (f i j))) ≫ (category_theory.Mat_.additive_obj_iso_biproduct F N).inv
theorem
category_theory.Mat_.additive_obj_iso_biproduct_naturality'_assoc
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u₁}
[category_theory.category D]
[category_theory.preadditive D]
[category_theory.limits.has_finite_biproducts D]
(F : category_theory.Mat_ C ⥤ D)
[F.additive]
{M N : category_theory.Mat_ C}
(f : M ⟶ N)
{X' : D}
(f' : F.obj N ⟶ X') :
(category_theory.Mat_.additive_obj_iso_biproduct F M).inv ≫ F.map f ≫ f' = category_theory.limits.biproduct.matrix (λ (i : M.ι) (j : N.ι), F.map ((category_theory.Mat_.embedding C).map (f i j))) ≫ (category_theory.Mat_.additive_obj_iso_biproduct F N).inv ≫ f'
@[simp]
theorem
category_theory.Mat_.lift_obj
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u₁}
[category_theory.category D]
[category_theory.preadditive D]
[category_theory.limits.has_finite_biproducts D]
(F : C ⥤ D)
[F.additive]
(X : category_theory.Mat_ C) :
noncomputable
def
category_theory.Mat_.lift
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u₁}
[category_theory.category D]
[category_theory.preadditive D]
[category_theory.limits.has_finite_biproducts D]
(F : C ⥤ D)
[F.additive] :
Any additive functor C ⥤ D to a category D with finite biproducts extends to
a functor Mat_ C ⥤ D.
Equations
- category_theory.Mat_.lift F = {obj := λ (X : category_theory.Mat_ C), ⨁ λ (i : X.ι), F.obj (X.X i), map := λ (X Y : category_theory.Mat_ C) (f : X ⟶ Y), category_theory.limits.biproduct.matrix (λ (i : X.ι) (j : Y.ι), F.map (f i j)), map_id' := _, map_comp' := _}
Instances for category_theory.Mat_.lift
@[simp]
theorem
category_theory.Mat_.lift_map
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u₁}
[category_theory.category D]
[category_theory.preadditive D]
[category_theory.limits.has_finite_biproducts D]
(F : C ⥤ D)
[F.additive]
(X Y : category_theory.Mat_ C)
(f : X ⟶ Y) :
(category_theory.Mat_.lift F).map f = category_theory.limits.biproduct.matrix (λ (i : X.ι) (j : Y.ι), F.map (f i j))
@[protected, instance]
def
category_theory.Mat_.lift_additive
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u₁}
[category_theory.category D]
[category_theory.preadditive D]
[category_theory.limits.has_finite_biproducts D]
(F : C ⥤ D)
[F.additive] :
noncomputable
def
category_theory.Mat_.embedding_lift_iso
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u₁}
[category_theory.category D]
[category_theory.preadditive D]
[category_theory.limits.has_finite_biproducts D]
(F : C ⥤ D)
[F.additive] :
An additive functor C ⥤ D factors through its lift to Mat_ C ⥤ D.
Equations
- category_theory.Mat_.embedding_lift_iso F = category_theory.nat_iso.of_components (λ (X : C), {hom := category_theory.limits.biproduct.desc (λ (P : ((category_theory.Mat_.embedding C).obj X).ι), 𝟙 (F.obj X)), inv := category_theory.limits.biproduct.lift (λ (P : ((category_theory.Mat_.embedding C).obj X).ι), 𝟙 (F.obj X)), hom_inv_id' := _, inv_hom_id' := _}) _
@[simp]
theorem
category_theory.Mat_.embedding_lift_iso_hom_app
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u₁}
[category_theory.category D]
[category_theory.preadditive D]
[category_theory.limits.has_finite_biproducts D]
(F : C ⥤ D)
[F.additive]
(X : C) :
(category_theory.Mat_.embedding_lift_iso F).hom.app X = category_theory.limits.biproduct.desc (λ (P : punit), 𝟙 (F.obj X))
@[simp]
theorem
category_theory.Mat_.embedding_lift_iso_inv_app
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u₁}
[category_theory.category D]
[category_theory.preadditive D]
[category_theory.limits.has_finite_biproducts D]
(F : C ⥤ D)
[F.additive]
(X : C) :
(category_theory.Mat_.embedding_lift_iso F).inv.app X = category_theory.limits.biproduct.lift (λ (P : punit), 𝟙 (F.obj X))
noncomputable
def
category_theory.Mat_.lift_unique
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u₁}
[category_theory.category D]
[category_theory.preadditive D]
[category_theory.limits.has_finite_biproducts D]
(F : C ⥤ D)
[F.additive]
(L : category_theory.Mat_ C ⥤ D)
[L.additive]
(α : category_theory.Mat_.embedding C ⋙ L ≅ F) :
Mat_.lift F is the unique additive functor L : Mat_ C ⥤ D such that F ≅ embedding C ⋙ L.
Equations
- category_theory.Mat_.lift_unique F L α = category_theory.nat_iso.of_components (λ (M : category_theory.Mat_ C), category_theory.Mat_.additive_obj_iso_biproduct L M ≪≫ category_theory.limits.biproduct.map_iso (λ (i : M.ι), α.app (M.X i)) ≪≫ category_theory.limits.biproduct.map_iso (λ (i : M.ι), (category_theory.Mat_.embedding_lift_iso F).symm.app (M.X i)) ≪≫ (category_theory.Mat_.additive_obj_iso_biproduct (category_theory.Mat_.lift F) M).symm) _
@[ext]
noncomputable
def
category_theory.Mat_.ext
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
{D : Type u₁}
[category_theory.category D]
[category_theory.preadditive D]
[category_theory.limits.has_finite_biproducts D]
{F G : category_theory.Mat_ C ⥤ D}
[F.additive]
[G.additive]
(α : category_theory.Mat_.embedding C ⋙ F ≅ category_theory.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.
noncomputable
def
category_theory.Mat_.equivalence_self_of_has_finite_biproducts_aux
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_biproducts C] :
Natural isomorphism needed in the construction of equivalence_self_of_has_finite_biproducts.
Equations
- category_theory.Mat_.equivalence_self_of_has_finite_biproducts_aux = (category_theory.Mat_.embedding C).right_unitor ≪≫ (category_theory.Mat_.embedding C).left_unitor.symm ≪≫ category_theory.iso_whisker_right (category_theory.Mat_.embedding_lift_iso (𝟭 C)).symm (category_theory.Mat_.embedding C) ≪≫ (category_theory.Mat_.embedding C).associator (category_theory.Mat_.lift (𝟭 C)) (category_theory.Mat_.embedding C)
noncomputable
def
category_theory.Mat_.equivalence_self_of_has_finite_biproducts
(C : Type (u₁+1))
[category_theory.large_category C]
[category_theory.preadditive C]
[category_theory.limits.has_finite_biproducts 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
- category_theory.Mat_.equivalence_self_of_has_finite_biproducts C = category_theory.equivalence.mk (category_theory.Mat_.lift (𝟭 C)) (category_theory.Mat_.embedding C) (category_theory.Mat_.ext category_theory.Mat_.equivalence_self_of_has_finite_biproducts_aux) (category_theory.Mat_.embedding_lift_iso (𝟭 C))
@[simp]
@[simp]
@[nolint]
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 category_theory.Mat
@[protected, instance]
@[protected, instance]
def
category_theory.Mat.has_coe_to_sort
(R : Type u) :
has_coe_to_sort (category_theory.Mat R) (Type u)
@[protected, instance]
Equations
- category_theory.Mat.category R = {to_category_struct := {to_quiver := {hom := λ (X Y : category_theory.Mat R), matrix ↥X ↥Y R}, id := λ (X : category_theory.Mat R), 1, comp := λ (X Y Z : category_theory.Mat R) (f : X ⟶ Y) (g : Y ⟶ Z), matrix.mul f g}, id_comp' := _, comp_id' := _, assoc' := _}
@[simp]
theorem
category_theory.Mat.id_apply_self
(R : Type u)
[semiring R]
(M : category_theory.Mat R)
(i : ↥M) :
@[simp]
theorem
category_theory.Mat.id_apply_of_ne
(R : Type u)
[semiring R]
(M : category_theory.Mat R)
(i j : ↥M)
(h : i ≠ j) :
theorem
category_theory.Mat.comp_def
(R : Type u)
[semiring R]
{M N K : category_theory.Mat R}
(f : M ⟶ N)
(g : N ⟶ K) :
@[simp]
theorem
category_theory.Mat.comp_apply
(R : Type u)
[semiring R]
{M N K : category_theory.Mat R}
(f : M ⟶ N)
(g : N ⟶ K)
(i : ↥M)
(k : ↥K) :
@[protected, instance]
def
category_theory.Mat.quiver.hom.inhabited
(R : Type u)
[semiring R]
(M N : category_theory.Mat R) :
Auxiliary definition for category_theory.Mat.equivalence_single_obj.
Equations
- category_theory.Mat.equivalence_single_obj_inverse R = {obj := λ (X : category_theory.Mat_ (category_theory.single_obj Rᵐᵒᵖ)), Fintype.of X.ι, map := λ (X Y : category_theory.Mat_ (category_theory.single_obj Rᵐᵒᵖ)) (f : X ⟶ Y) (i : ↥(Fintype.of X.ι)) (j : ↥(Fintype.of Y.ι)), mul_opposite.unop (f i j), map_id' := _, map_comp' := _}
Instances for category_theory.Mat.equivalence_single_obj_inverse
@[simp]
theorem
category_theory.Mat.equivalence_single_obj_inverse_obj
(R : Type)
[ring R]
(X : category_theory.Mat_ (category_theory.single_obj Rᵐᵒᵖ)) :
@[simp]
theorem
category_theory.Mat.equivalence_single_obj_inverse_map
(R : Type)
[ring R]
(X Y : category_theory.Mat_ (category_theory.single_obj Rᵐᵒᵖ))
(f : X ⟶ Y)
(i : ↥(Fintype.of X.ι))
(j : ↥(Fintype.of Y.ι)) :
(category_theory.Mat.equivalence_single_obj_inverse R).map f i j = mul_opposite.unop (f i j)
@[protected, instance]
@[protected, instance]
Equations
- category_theory.Mat.equivalence_single_obj_inverse.category_theory.full R = {preimage := λ (X Y : category_theory.Mat_ (category_theory.single_obj Rᵐᵒᵖ)) (f : (category_theory.Mat.equivalence_single_obj_inverse R).obj X ⟶ (category_theory.Mat.equivalence_single_obj_inverse R).obj Y) (i : X.ι) (j : Y.ι), mul_opposite.op (f i j), witness' := _}
@[protected, instance]
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.
@[protected, instance]
Equations
- category_theory.Mat.category_theory.preadditive R = {hom_group := λ (P Q : category_theory.Mat R), matrix.add_comm_group, add_comp' := _, comp_add' := _}