Subobjects in the category of R
-modules #
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 ↾(N.subtype), inv_fun := λ (S : category_theory.subobject M), linear_map.range S.arrow, left_inv := _, right_inv := _}, map_rel_iff' := _}
@[protected, instance]