Subobjects in the category of R-modules #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We construct an explicit order isomorphism between the categorical subobjects of an R-module M
and its submodules. This immediately implies that the category of R-modules is well-powered.
The categorical subobjects of a module M are in one-to-one correspondence with its
submodules.
Equations
- M.subobject_Module = order_iso.symm {to_equiv := {to_fun := λ (N : submodule R ↥M), category_theory.subobject.mk (Module.as_hom_right N.subtype), inv_fun := λ (S : category_theory.subobject M), linear_map.range S.arrow, left_inv := _, right_inv := _}, map_rel_iff' := _}
@[protected, instance]
Bundle an element m : M such that f m = 0 as a term of kernel_subobject f.
@[simp]
theorem
Module.to_kernel_subobject_arrow
{R : Type u}
[ring R]
{M N : Module R}
{f : M ⟶ N}
(x : ↥(linear_map.ker f)) :
@[ext]
theorem
Module.cokernel_π_image_subobject_ext
{R : Type u}
[ring R]
{L M N : Module R}
(f : L ⟶ M)
[category_theory.limits.has_image f]
(g : ↑(category_theory.limits.image_subobject f) ⟶ N)
[category_theory.limits.has_cokernel g]
{x y : ↥N}
(l : ↥L)
(w : x = y + ⇑g (⇑(category_theory.limits.factor_thru_image_subobject f) l)) :
An extensionality lemma showing that two elements of a cokernel by an image are equal if they differ by an element of the image.
The application is for homology: two elements in homology are equal if they differ by a boundary.