mathlib documentation

algebra.category.Module.basic

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

The category of R-modules and their morphisms.

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

Equations
@[instance]

Equations
@[instance]

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
@[instance]
def Module.inhabited (R : Type u) [ring R] :

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

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

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

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
@[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₂} :
(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} :
(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 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} :
(X Y)(X ≃ₗ[R] 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} [add_comm_group X] [add_comm_group Y] [module R X] [module R Y] (i : Module.of R X Module.of R Y) :

@[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) :

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.ker_eq_bot_of_mono {R : Type u} [ring R] {M N : Module R} (f : M N) [category_theory.mono f] :

theorem Module.range_eq_top_of_epi {R : Type u} [ring R] {M N : Module R} (f : M N) [category_theory.epi f] :

theorem Module.mono_of_ker_eq_bot {R : Type u} [ring R] {M N : Module R} (f : M N) :

theorem Module.epi_of_range_eq_top {R : Type u} [ring R] {M N : Module R} (f : M N) :

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

Equations