CategoryTheory.Mat_.hom_ext
theorem CategoryTheory.Mat_.hom_ext :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
{M N : CategoryTheory.Mat_ C} (f g : M ⟶ N), (∀ (i : M.ι) (j : N.ι), f i j = g i j) → f = g
The theorem `CategoryTheory.Mat_.hom_ext` states that for any type `C` which is endowed with a category structure and a preadditive structure, and for any two objects `M` and `N` in the category of matrices over `C`, if two morphisms `f` and `g` from `M` to `N` agree on all entries (i.e., `f i j = g i j` for all indices `i` and `j`), then `f` and `g` are equal.
More concisely: For any preadditive category `C` with types `M` and `N` as objects, and morphisms `f` and `g` from `M` to `N` of matrices, if their entries are equal for all indices `i` and `j`, then `f` is equal to `g`.
|
CategoryTheory.Mat.hom_ext
theorem CategoryTheory.Mat.hom_ext :
∀ {R : Type u} [inst : Semiring R] {X Y : CategoryTheory.Mat R} (f g : X ⟶ Y),
(∀ (i : ↑X) (j : ↑Y), f i j = g i j) → f = g
This theorem states that for any semiring `R`, and any two objects `X` and `Y` in the category `CategoryTheory.Mat R` (which is equipped with a category structure where the morphisms are matrices with components in `R`), if two morphisms `f` and `g` from `X` to `Y` are such that their corresponding entries are equal for all indices `i` in `X` and `j` in `Y`, then the two morphisms `f` and `g` are equal. In other words, two morphisms in this category are considered equal if and only if their matrix representations are elementwise equal.
More concisely: In the category of matrices over a semiring `R`, two morphisms have equal matrix representations if and only if they are equal as morphisms.
|