mathlib documentation

algebra.category.Module.basic

source
structure Module (R : Type u) [ring R] :
Type (max u (v+1))

The category of R-modules and their morphisms.

source
@[instance]
def Module.has_coe_to_sort (R : Type u) [ring R] :
has_coe_to_sort (Module R)

Equations
source
@[instance]
def Module.category_theory.category (R : Type u) [ring R] :
category_theory.category (Module R)

Equations
source
@[instance]
def Module.category_theory.concrete_category (R : Type u) [ring R] :
category_theory.concrete_category (Module R)

Equations
source
@[instance]
def Module.has_forget_to_AddCommGroup (R : Type u) [ring R] :
category_theory.has_forget₂ (Module R) AddCommGroup

Equations
source
def Module.of (R : Type u) [ring R] (X : Type v) [add_comm_group X] [module R X] :
Module R

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

Equations
source
@[instance]
def Module.inhabited (R : Type u) [ring R] :
inhabited (Module R)

Equations
source
@[simp]
theorem Module.coe_of (R : Type u) [ring R] (X : Type u) [add_comm_group X] [module R X] :
↥(Module.of R X) = X

source
def Module.of_self_iso {R : Type u} [ring R] (M : Module R) :
Module.of R ↥M ≅ M

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

Equations
source
@[simp]
theorem Module.of_self_iso_hom {R : Type u} [ring R] (M : Module R) :
M.of_self_iso.hom = 𝟙 M

source
@[simp]
theorem Module.of_self_iso_inv {R : Type u} [ring R] (M : Module R) :
M.of_self_iso.inv = 𝟙 M

source
@[instance]
def Module.subsingleton {R : Type u} [ring R] :
subsingleton ↥(Module.of R punit)

source
@[instance]
def Module.category_theory.limits.has_zero_object {R : Type u} [ring R] :
category_theory.limits.has_zero_object (Module R)

Equations
source
@[simp]
theorem Module.id_apply {R : Type u} [ring R] {M : Module R} (m : ↥M) :
⇑(𝟙 M) m = m

source
@[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

source
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₂] (a : X₁ →ₗ[R] X₂) :
Module.of R X₁ ⟶ Module.of R X₂

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

Equations
source
@[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₂) :
e.to_Module_iso.hom = ↑e

source
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
source
@[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₂) :
e.to_Module_iso.inv = ↑(e.symm)

source
@[simp]
theorem linear_equiv.to_Module_iso'_inv {R : Type u} [ring R] {M N : Module R} (i : ↥M ≃ₗ[R] ↥N) :
i.to_Module_iso'.inv = ↑(i.symm)

source
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
source
@[simp]
theorem linear_equiv.to_Module_iso'_hom {R : Type u} [ring R] {M N : Module R} (i : ↥M ≃ₗ[R] ↥N) :
i.to_Module_iso'.hom = ↑i

source
@[simp]
theorem category_theory.iso.to_linear_equiv_to_fun {R : Type u} [ring R] {X Y : Module R} (i : X ≅ Y) (a : ↥X) :
⇑(i.to_linear_equiv) a = ⇑(i.hom) a

source
@[simp]
theorem category_theory.iso.to_linear_equiv_inv_fun {R : Type u} [ring R] {X Y : Module R} (i : X ≅ Y) (a : ↥Y) :
i.to_linear_equiv.inv_fun a = ⇑(i.inv) a

source
def category_theory.iso.to_linear_equiv {R : Type u} [ring R] {X Y : Module R} (i : X ≅ Y) :
↥X ≃ₗ[R] ↥Y

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

Equations
source
@[simp]
theorem linear_equiv_iso_Module_iso_inv {R : Type u} [ring R] {X Y : Type u} [add_comm_group X] [add_comm_group Y] [module R X] [module R Y] (i : Module.of R X ≅ Module.of R Y) :
linear_equiv_iso_Module_iso.inv i = i.to_linear_equiv

source
@[simp]
theorem linear_equiv_iso_Module_iso_hom {R : Type u} [ring R] {X Y : Type u} [add_comm_group X] [add_comm_group Y] [module R X] [module R Y] (e : X ≃ₗ[R] Y) :
linear_equiv_iso_Module_iso.hom e = e.to_Module_iso

source
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] :
(X ≃ₗ[R] Y) ≅ Module.of R X ≅ Module.of R Y

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

Equations
source
@[instance]
def Module.category_theory.preadditive {R : Type u} [ring R] :
category_theory.preadditive (Module R)

Equations
source
theorem Module.ker_eq_bot_of_mono {R : Type u} [ring R] {M N : Module R} (f : M ⟶ N) [category_theory.mono f] :
linear_map.ker f = ⊥

source
theorem Module.range_eq_top_of_epi {R : Type u} [ring R] {M N : Module R} (f : M ⟶ N) [category_theory.epi f] :
linear_map.range f = ⊤

source
theorem Module.mono_of_ker_eq_bot {R : Type u} [ring R] {M N : Module R} (f : M ⟶ N) (hf : linear_map.ker f = ⊥) :
category_theory.mono f

source
theorem Module.epi_of_range_eq_top {R : Type u} [ring R] {M N : Module R} (f : M ⟶ N) (hf : linear_map.range f = ⊤) :
category_theory.epi f

source
@[instance]
def Module.has_coe {R : Type u} [ring R] (M : Type u) [add_comm_group M] [module R M] :
has_coe (submodule R M) (Module R)

Equations