algebra.category.fgModule.basic - mathlib3 docs

mathlib3 documentation

algebra.category.fgModule.basic

The category of finitely generated modules over a ring #

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

This introduces fgModule R, the category of finitely generated modules over a ring R. It is implemented as a full subcategory on a subtype of Module R.

When K is a field, fgModule K is the category of finite dimensional vector spaces over K.

We first create the instance as a preadditive category. When R is commutative we then give the structure as an R-linear monoidal category. When R is a field we give it the structure of a closed monoidal category and then as a right-rigid monoidal category.

Future work #

  • Show that fgModule R is abelian when R is (left)-noetherian.
source
@[protected, instance]
def fgModule.concrete_category (R : Type u) [ring R] :
category_theory.concrete_category (fgModule R)
source
@[protected, instance]
def fgModule.preadditive (R : Type u) [ring R] :
category_theory.preadditive (fgModule R)
source
@[protected, instance]
def fgModule.large_category (R : Type u) [ring R] :
category_theory.large_category (fgModule R)
source
@[protected, instance]
def fgModule.finite (R : Type u) [ring R] (V : fgModule R) :
module.finite R ↥(V.obj)
source
@[protected, instance]
def fgModule.inhabited (R : Type u) [ring R] :
inhabited (fgModule R)
Equations
source
def fgModule.of (R : Type u) [ring R] (V : Type u) [add_comm_group V] [module R V] [module.finite R V] :
fgModule R

Lift an unbundled finitely generated module to fgModule R.

Equations
source
@[protected, instance]
def fgModule.obj.module.finite (R : Type u) [ring R] (V : fgModule R) :
module.finite R ↥(V.obj)
source
def fgModule.iso_to_linear_equiv {R : Type u} [ring R] {V W : fgModule R} (i : V ≅ W) :
↥(V.obj) ≃ₗ[R] ↥(W.obj)

Converts and isomorphism in the category fgModule R to a linear_equiv between the underlying modules.

Equations
source
def linear_equiv.to_fgModule_iso {R : Type u} [ring R] {V W : Type u} [add_comm_group V] [module R V] [module.finite R V] [add_comm_group W] [module R W] [module.finite R W] (e : V ≃ₗ[R] W) :
fgModule.of R V ≅ fgModule.of R W

Converts a linear_equiv to an isomorphism in the category fgModule R.

Equations
source
@[simp]
theorem linear_equiv.to_fgModule_iso_inv {R : Type u} [ring R] {V W : Type u} [add_comm_group V] [module R V] [module.finite R V] [add_comm_group W] [module R W] [module.finite R W] (e : V ≃ₗ[R] W) :
e.to_fgModule_iso.inv = e.symm.to_linear_map
source
@[simp]
theorem linear_equiv.to_fgModule_iso_hom {R : Type u} [ring R] {V W : Type u} [add_comm_group V] [module R V] [module.finite R V] [add_comm_group W] [module R W] [module.finite R W] (e : V ≃ₗ[R] W) :
e.to_fgModule_iso.hom = e.to_linear_map
source
theorem fgModule.iso.conj_eq_conj (R : Type u) [comm_ring R] {V W : fgModule R} (i : V ≅ W) (f : category_theory.End V) :
⇑(i.conj) f = ⇑((fgModule.iso_to_linear_equiv i).conj) f
source
@[protected, instance]
def fgModule.quiver.hom.module.finite (K : Type u) [field K] (V W : fgModule K) :
module.finite K (V ⟶ W)
source
@[simp]
theorem fgModule.ihom_obj (K : Type u) [field K] (V W : fgModule K) :
(category_theory.ihom V).obj W = fgModule.of K (↥(V.obj) →ₗ[K] ↥(W.obj))
source
def fgModule.fgModule_dual (K : Type u) [field K] (V : fgModule K) :
fgModule K

The dual module is the dual in the rigid monoidal category fgModule K.

Equations
Instances for fgModule.fgModule_dual
source
noncomputable def fgModule.fgModule_coevaluation (K : Type u) [field K] (V : fgModule K) :
𝟙_ (fgModule K) ⟶ V ⊗ fgModule.fgModule_dual K V

The coevaluation map is defined in linear_algebra.coevaluation.

Equations
source
def fgModule.fgModule_evaluation (K : Type u) [field K] (V : fgModule K) :
fgModule.fgModule_dual K V ⊗ V ⟶ 𝟙_ (fgModule K)

The evaluation morphism is given by the contraction map.

Equations
source
@[simp]
theorem fgModule.fgModule_evaluation_apply (K : Type u) [field K] (V : fgModule K) (f : ↥((fgModule.fgModule_dual K V).obj)) (x : ↥(V.obj)) :
⇑(fgModule.fgModule_evaluation K V) (f ⊗ₜ[K] x) = f.to_fun x
source
@[protected, instance]
noncomputable def fgModule.right_dual (K : Type u) [field K] (V : fgModule K) :
category_theory.has_right_dual V
Equations