mathlib 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,

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_add_comm_group : add_comm_group self.carrier
is_module : module R 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] :

has_coe_to_sort (Module R) (Type v)

Equations

Module.has_coe_to_sort R = {coe := Module.carrier _inst_1}

@[protected, instance]

def Module.Module_category (R : Type u) [ring R] :

category_theory.category (Module R)

Equations

Module.Module_category R = {to_category_struct := {to_quiver := {hom := λ (M N : Module R), ↥M →ₗ[R] ↥N}, id := λ (M : Module R), 1, comp := λ (A B C : Module R) (f : A ⟶ B) (g : B ⟶ C), linear_map.comp g f}, id_comp' := _, comp_id' := _, assoc' := _}

@[protected, instance]

def Module.Module_concrete_category (R : Type u) [ring R] :

category_theory.concrete_category (Module R)

Equations

Module.Module_concrete_category R = category_theory.concrete_category.mk {obj := λ (R_1 : Module R), ↥R_1, map := λ (R_1 S : Module R) (f : R_1 ⟶ S), ⇑f, map_id' := _, map_comp' := _}

@[protected, instance]

def Module.has_forget_to_AddCommGroup (R : Type u) [ring R] :

category_theory.has_forget₂ (Module R) AddCommGroup

Equations

Module.has_forget_to_AddCommGroup R = {forget₂ := {obj := λ (M : Module R), AddCommGroup.of ↥M, map := λ (M₁ M₂ : Module R) (f : M₁ ⟶ M₂), linear_map.to_add_monoid_hom f, map_id' := _, map_comp' := _}, forget_comp := _}

@[protected, instance]

def Module.linear_map_class (R : Type u) [ring R] (M N : Module R) :

linear_map_class (M ⟶ N) R ↥M ↥N

Equations

Module.linear_map_class R M N = {coe := λ (f : M ⟶ N), ⇑f, coe_injective' := _, map_add := _, map_smulₛₗ := _}

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

Module.of R X = Module.mk X

Instances for Module.of

simple_of_is_simple_module

Instances for ↥Module.of

Module.of_unique

@[simp]

theorem Module.forget₂_obj (R : Type u) [ring R] (X : Module R) :

(category_theory.forget₂ (Module R) AddCommGroup).obj X = AddCommGroup.of ↥X

@[simp]

theorem Module.forget₂_obj_Module_of (R : Type u) [ring R] (X : Type v) [add_comm_group X] [module R X] :

(category_theory.forget₂ (Module R) AddCommGroup).obj (Module.of R X) = AddCommGroup.of X

@[simp]

theorem Module.forget₂_map (R : Type u) [ring R] (X Y : Module R) (f : X ⟶ Y) :

(category_theory.forget₂ (Module R) AddCommGroup).map f = linear_map.to_add_monoid_hom f

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

Module.of R X ⟶ Module.of R Y

Typecheck a linear_map as a morphism in Module R.

Equations

Module.of_hom f = f

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

⇑(Module.of_hom f) x = ⇑f x

@[protected, instance]

def Module.inhabited (R : Type u) [ring R] :

inhabited (Module R)

Equations

Module.inhabited R = {default := Module.of R punit punit.module}

@[protected, instance]

def Module.of_unique (R : Type u) [ring R] {X : Type v} [add_comm_group X] [module R X] [i : unique X] :

unique ↥(Module.of R X)

Equations

Module.of_unique R = i

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

Module.of R ↥M ≅ M

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

Equations

M.of_self_iso = {hom := 𝟙 M, inv := 𝟙 M, hom_inv_id' := _, inv_hom_id' := _}

@[simp]

theorem Module.of_self_iso_hom {R : Type u} [ring R] (M : Module R) :

M.of_self_iso.hom = 𝟙 M

@[simp]

theorem Module.of_self_iso_inv {R : Type u} [ring R] (M : Module R) :

M.of_self_iso.inv = 𝟙 M

theorem Module.is_zero_of_subsingleton {R : Type u} [ring R] (M : Module R) [subsingleton ↥M] :

category_theory.limits.is_zero M

@[protected, instance]

def Module.category_theory.limits.has_zero_object {R : Type u} [ring R] :

category_theory.limits.has_zero_object (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) :

f ≫ g = linear_map.comp 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

Module.as_hom = id

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

Module.as_hom_right = id

Instances for Module.as_hom_right

Module.mono_as_hom'_subtype

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

Module.as_hom_left = id

Instances for Module.as_hom_left

Module.epi_as_hom''_mkq

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

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

e.to_Module_iso = {hom := ↑e, inv := ↑(e.symm), hom_inv_id' := _, inv_hom_id' := _}

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

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

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

i.to_Module_iso' = {hom := ↑i, inv := ↑(i.symm), hom_inv_id' := _, inv_hom_id' := _}

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

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

e.to_Module_iso'_left.inv = ↑(e.symm)

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

e.to_Module_iso'_left = {hom := ↑e, inv := ↑(e.symm), hom_inv_id' := _, inv_hom_id' := _}

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

e.to_Module_iso'_left.hom = ↑e

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

e.to_Module_iso'_right.hom = ↑e

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

e.to_Module_iso'_right.inv = ↑(e.symm)

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

e.to_Module_iso'_right = {hom := ↑e, inv := ↑(e.symm), hom_inv_id' := _, inv_hom_id' := _}

@[simp]

theorem category_theory.iso.to_linear_equiv_symm_apply {R : Type u} [ring R] {X Y : Module R} (i : X ≅ Y) (ᾰ : ↥Y) :

⇑(i.to_linear_equiv.symm) ᾰ = ⇑(i.inv) ᾰ

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

↥X ≃ₗ[R] ↥Y

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

Equations

i.to_linear_equiv = {to_fun := ⇑(i.hom), map_add' := _, map_smul' := _, inv_fun := ⇑(i.inv), left_inv := _, right_inv := _}

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

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

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

linear_equiv_iso_Module_iso = {hom := λ (e : X ≃ₗ[R] Y), e.to_Module_iso, inv := λ (i : Module.of R X ≅ Module.of R Y), i.to_linear_equiv, hom_inv_id' := _, inv_hom_id' := _}

@[protected, instance]

def Module.category_theory.preadditive {R : Type u} [ring R] :

category_theory.preadditive (Module R)

Equations

Module.category_theory.preadditive = {hom_group := λ (P Q : Module R), linear_map.add_comm_group, add_comp' := _, comp_add' := _}

@[protected, instance]

def Module.forget₂_AddCommGroup_additive {R : Type u} [ring R] :

(category_theory.forget₂ (Module R) AddCommGroup).additive

@[protected, instance]

def Module.category_theory.linear {S : Type u} [comm_ring S] :

category_theory.linear S (Module S)

Equations

Module.category_theory.linear = {hom_module := λ (X Y : Module S), linear_map.module, smul_comp' := _, comp_smul' := _}

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 = ⇑(i.to_linear_equiv.arrow_congr j.to_linear_equiv) 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) :

⇑(i.conj) f = ⇑(i.to_linear_equiv.conj) f

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

Module.has_coe M = {coe := λ (N : submodule R M), Module.of R ↥N}