mathlib3 documentation

algebra.category.Module.basic

The category of R-modules #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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,

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))

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]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
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) [add_comm_group X] [module R X] :

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

Equations
Instances for Module.of
def Module.of_hom {R : Type u} [ring R] {X Y : Type v} [add_comm_group X] [module R X] [add_comm_group Y] [module R Y] (f : X →ₗ[R] 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} [add_comm_group X] [module R X] [add_comm_group Y] [module R Y] (f : X →ₗ[R] Y) (x : 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} [add_comm_group X] [module R X] [i : unique X] :
Equations
@[simp]
theorem Module.coe_of (R : Type u) [ring R] (X : Type v) [add_comm_group X] [module R X] :
(Module.of R X) = X
def Module.of_self_iso {R : Type u} [ring R] (M : Module R) :

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) :
@[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) :
def Module.as_hom {R : Type u} [ring R] {X₁ X₂ : Type v} [add_comm_group X₁] [module R X₁] [add_comm_group X₂] [module R X₂] :
(X₁ →ₗ[R] X₂) (Module.of R X₁ Module.of R 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₁] [module R X₁] {X₂ : Module R} :
(X₁ →ₗ[R] X₂) (Module.of R X₁ X₂)

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

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

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

Equations
@[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₁ : module R X₁} {m₂ : module R 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₁ : module R X₁} {m₂ : module R X₂} (e : X₁ ≃ₗ[R] X₂) :
Module.of R X₁ Module.of R 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₁ : module R X₁} {m₂ : module R 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₂ : module R 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₂ : module R X₂} (e : X₁ ≃ₗ[R] X₂) :
X₁ Module.of R 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₂ : module R 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₁ : module R 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₁ : module R 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₁ : module R X₁} {X₂ : Module R} (e : X₁ ≃ₗ[R] X₂) :
Module.of R 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
def linear_equiv_iso_Module_iso {R : Type u} [ring R] {X Y : Type u} [add_comm_group X] [add_comm_group Y] [module R X] [module R Y] :

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

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) :
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) [add_comm_group M] [module R M] :
Equations