# mathlibdocumentation

algebra.category.Module.basic

# 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.

structure Module (R : Type u) [ring R] :
Type (max u (v+1))
• carrier : Type ?
• is_module : self.carrier

The category of R-modules and their morphisms.

Note that in the case of R = ℤ, we can not impose here that the ℤ-multiplication field from the module structure is defeq to the one coming from the is_add_comm_group structure (contrary to what we do for all module structures in mathlib), which creates some difficulties down the road.

Instances for Module
@[protected, instance]
def Module.has_coe_to_sort (R : Type u) [ring R] :
(Type v)
Equations
@[protected, instance]
def Module.Module_category (R : Type u) [ring R] :
Equations
@[protected, instance]
def Module.Module_concrete_category (R : Type u) [ring R] :
Equations
@[protected, instance]
def Module.has_forget_to_AddCommGroup (R : Type u) [ring R] :
Equations
@[protected, instance]
def Module.linear_map_class (R : Type u) [ring R] (M N : Module R) :
Equations
def Module.of (R : Type u) [ring R] (X : Type v) [ X] :

The object in the category of R-modules associated to an R-module

Equations
• X =
Instances for Module.of
Instances for ↥Module.of
@[simp]
theorem Module.forget₂_obj (R : Type u) [ring R] (X : Module R) :
@[simp]
theorem Module.forget₂_obj_Module_of (R : Type u) [ring R] (X : Type v) [ X] :
X) =
@[simp]
theorem Module.forget₂_map (R : Type u) [ring R] (X Y : Module R) (f : X Y) :
def Module.of_hom {R : Type u} [ring R] {X Y : Type v} [ X] [ Y] (f : X →ₗ[R] Y) :
X Y

Typecheck a linear_map as a morphism in Module R.

Equations
@[simp]
theorem Module.of_hom_apply {R : Type u} [ring R] {X Y : Type v} [ X] [ Y] (f : X →ₗ[R] Y) (x : X) :
x = f x
@[protected, instance]
def Module.inhabited (R : Type u) [ring R] :
Equations
@[protected, instance]
def Module.of_unique (R : Type u) [ring R] {X : Type v} [ X] [i : unique X] :
Equations
@[simp]
theorem Module.coe_of (R : Type u) [ring R] (X : Type v) [ X] :
X) = X
def Module.of_self_iso {R : Type u} [ring R] (M : Module R) :
M M

Forgetting to the underlying type and then building the bundled object returns the original module.

Equations
@[simp]
theorem Module.of_self_iso_hom {R : Type u} [ring R] (M : Module R) :
@[simp]
theorem Module.of_self_iso_inv {R : Type u} [ring R] (M : Module R) :
theorem Module.is_zero_of_subsingleton {R : Type u} [ring R] (M : Module R)  :
@[protected, instance]
@[simp]
theorem Module.id_apply {R : Type u} [ring R] {M : Module R} (m : M) :
(𝟙 M) m = m
@[simp]
theorem Module.coe_comp {R : Type u} [ring R] {M N U : Module R} (f : M N) (g : N U) :
(f g) = g f
theorem Module.comp_def {R : Type u} [ring R] {M N U : Module R} (f : M N) (g : N U) :
f g =
def Module.as_hom {R : Type u} [ring R] {X₁ X₂ : Type v} [add_comm_group X₁] [ X₁] [add_comm_group X₂] [ X₂] :
(X₁ →ₗ[R] X₂) X₁ X₂)

Reinterpreting a linear map in the category of R-modules.

Equations
def Module.as_hom_right {R : Type u} [ring R] {X₁ : Type v} [add_comm_group X₁] [ X₁] {X₂ : Module R} :
(X₁ →ₗ[R] X₂) X₁ X₂)

Reinterpreting a linear map in the category of R-modules.

Equations
Instances for Module.as_hom_right
def Module.as_hom_left {R : Type u} [ring R] {X₂ : Type v} {X₁ : Module R} [add_comm_group X₂] [ X₂] :
(X₁ →ₗ[R] X₂)(X₁ X₂)

Reinterpreting a linear map in the category of R-modules.

Equations
Instances for Module.as_hom_left
@[simp]
theorem linear_equiv.to_Module_iso_hom {R : Type u} [ring R] {X₁ X₂ : Type v} {g₁ : add_comm_group X₁} {g₂ : add_comm_group X₂} {m₁ : X₁} {m₂ : X₂} (e : X₁ ≃ₗ[R] X₂) :
def linear_equiv.to_Module_iso {R : Type u} [ring R] {X₁ X₂ : Type v} {g₁ : add_comm_group X₁} {g₂ : add_comm_group X₂} {m₁ : X₁} {m₂ : X₂} (e : X₁ ≃ₗ[R] X₂) :
X₁ X₂

Build an isomorphism in the category Module R from a linear_equiv between modules.

Equations
@[simp]
theorem linear_equiv.to_Module_iso_inv {R : Type u} [ring R] {X₁ X₂ : Type v} {g₁ : add_comm_group X₁} {g₂ : add_comm_group X₂} {m₁ : X₁} {m₂ : X₂} (e : X₁ ≃ₗ[R] X₂) :
@[simp]
theorem linear_equiv.to_Module_iso'_inv {R : Type u} [ring R] {M N : Module R} (i : M ≃ₗ[R] N) :
def linear_equiv.to_Module_iso' {R : Type u} [ring R] {M N : Module R} (i : M ≃ₗ[R] N) :
M N

Build an isomorphism in the category Module R from a linear_equiv between modules.

This version is better than linear_equiv_to_Module_iso when applicable, because Lean can't see Module.of R M is defeq to M when M : Module R.

Equations
@[simp]
theorem linear_equiv.to_Module_iso'_hom {R : Type u} [ring R] {M N : Module R} (i : M ≃ₗ[R] N) :
@[simp]
theorem linear_equiv.to_Module_iso'_left_inv {R : Type u} [ring R] {X₂ : Type v} {X₁ : Module R} {g₂ : add_comm_group X₂} {m₂ : X₂} (e : X₁ ≃ₗ[R] X₂) :
def linear_equiv.to_Module_iso'_left {R : Type u} [ring R] {X₂ : Type v} {X₁ : Module R} {g₂ : add_comm_group X₂} {m₂ : X₂} (e : X₁ ≃ₗ[R] X₂) :
X₁ X₂

Build an isomorphism in the category Module R from a linear_equiv between modules.

This version is better than linear_equiv_to_Module_iso when applicable, because Lean can't see Module.of R M is defeq to M when M : Module R.

Equations
@[simp]
theorem linear_equiv.to_Module_iso'_left_hom {R : Type u} [ring R] {X₂ : Type v} {X₁ : Module R} {g₂ : add_comm_group X₂} {m₂ : X₂} (e : X₁ ≃ₗ[R] X₂) :
@[simp]
theorem linear_equiv.to_Module_iso'_right_hom {R : Type u} [ring R] {X₁ : Type v} {g₁ : add_comm_group X₁} {m₁ : X₁} {X₂ : Module R} (e : X₁ ≃ₗ[R] X₂) :
@[simp]
theorem linear_equiv.to_Module_iso'_right_inv {R : Type u} [ring R] {X₁ : Type v} {g₁ : add_comm_group X₁} {m₁ : X₁} {X₂ : Module R} (e : X₁ ≃ₗ[R] X₂) :
def linear_equiv.to_Module_iso'_right {R : Type u} [ring R] {X₁ : Type v} {g₁ : add_comm_group X₁} {m₁ : X₁} {X₂ : Module R} (e : X₁ ≃ₗ[R] X₂) :
X₁ X₂

Build an isomorphism in the category Module R from a linear_equiv between modules.

This version is better than linear_equiv_to_Module_iso when applicable, because Lean can't see Module.of R M is defeq to M when M : Module R.

Equations
@[simp]
theorem category_theory.iso.to_linear_equiv_symm_apply {R : Type u} [ring R] {X Y : Module R} (i : X Y) (ᾰ : Y) :
@[simp]
theorem category_theory.iso.to_linear_equiv_apply {R : Type u} [ring R] {X Y : Module R} (i : X Y) (ᾰ : X) :
(i.to_linear_equiv) ᾰ = (i.hom) ᾰ
def category_theory.iso.to_linear_equiv {R : Type u} [ring R] {X Y : Module R} (i : X Y) :

Build a linear_equiv from an isomorphism in the category Module R.

Equations
@[simp]
theorem linear_equiv_iso_Module_iso_inv {R : Type u} [ring R] {X Y : Type u} [ X] [ Y] (i : X Y) :
@[simp]
theorem linear_equiv_iso_Module_iso_hom {R : Type u} [ring R] {X Y : Type u} [ X] [ Y] (e : X ≃ₗ[R] Y) :
def linear_equiv_iso_Module_iso {R : Type u} [ring R] {X Y : Type u} [ X] [ Y] :
(X ≃ₗ[R] Y) X Y

linear equivalences between modules are the same as (isomorphic to) isomorphisms in Module

Equations
@[protected, instance]
def Module.category_theory.preadditive {R : Type u} [ring R] :
Equations
@[protected, instance]
@[protected, instance]
def Module.category_theory.linear {S : Type u} [comm_ring S] :
Equations
theorem Module.iso.hom_congr_eq_arrow_congr {S : Type u} [comm_ring S] {X Y X' Y' : Module S} (i : X X') (j : Y Y') (f : X Y) :
(i.hom_congr j) f =
theorem Module.iso.conj_eq_conj {S : Type u} [comm_ring S] {X X' : Module S} (i : X X') (f : category_theory.End X) :
@[protected, instance]
def Module.has_coe {R : Type u} [ring R] (M : Type u) [ M] :
Equations