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 #

@[protected, instance]
@[protected, instance]
@[protected, instance]
def fgModule.finite (R : Type u) [ring R] (V : fgModule R) :
@[protected, instance]
def fgModule.inhabited (R : Type u) [ring R] :
Equations
def fgModule.of (R : Type u) [ring R] (V : Type u) [add_comm_group V] [module R V] [module.finite R V] :

Lift an unbundled finitely generated module to fgModule R.

Equations
@[protected, instance]
def fgModule.iso_to_linear_equiv {R : Type u} [ring R] {V W : fgModule R} (i : V W) :

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

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

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

Equations
@[simp]
@[protected, instance]
def fgModule.quiver.hom.module.finite (K : Type u) [field K] (V W : fgModule K) :
@[simp]
theorem fgModule.ihom_obj (K : Type u) [field K] (V W : fgModule K) :
def fgModule.fgModule_dual (K : Type u) [field K] (V : fgModule K) :

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

Equations
Instances for fgModule.fgModule_dual
noncomputable def fgModule.fgModule_coevaluation (K : Type u) [field K] (V : fgModule K) :

The coevaluation map is defined in linear_algebra.coevaluation.

Equations

The evaluation morphism is given by the contraction map.

Equations
@[simp]