The category of R-modules #

Module.{v} R is the category of bundled R-modules with carrier in the universe v. We show that it is preadditive and show that being an isomorphism, monomorphism and epimorphism is equivalent to being a linear equivalence, an injective linear map and a surjective linear map, respectively.

Implementation details #

To construct an object in the category of R-modules from a type M with an instance of the module typeclass, write of R M. There is a coercion in the other direction.

Similarly, there is a coercion from morphisms in Module R to linear maps.

Unfortunately, Lean is not smart enough to see that, given an object M : Module R, the expression of R M, where we coerce M to the carrier type, is definitionally equal to M itself. This means that to go the other direction, i.e., from linear maps/equivalences to (iso)morphisms in the category of R-modules, we have to take care not to inadvertently end up with an of R M where M is already an object. Hence, given f : M →ₗ[R] N,

• if M N : Module R, simply use f;
• if M : Module R and N is an unbundled R-module, use ↿f or as_hom_left f;
• if M is an unbundled R-module and N : Module R, use ↾f or as_hom_right f;
• if M and N are unbundled R-modules, use ↟f or as_hom f.

Similarly, given f : M ≃ₗ[R] N, use to_Module_iso, to_Module_iso'_left, to_Module_iso'_right or to_Module_iso', respectively.

The arrow notations are localized, so you may have to open_locale Module to use them. Note that the notation for as_hom_left clashes with the notation used to promote functions between types to morphisms in the category Type, so to avoid confusion, it is probably a good idea to avoid having the locales Module and category_theory.Type open at the same time.

If you get an error when trying to apply a theorem and the convert tactic produces goals of the form M = of R M, then you probably used an incorrect variant of as_hom or to_Module_iso.