# mathlib3documentation

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.
@[protected, instance]
def fgModule.concrete_category (R : Type u) [ring R] :
def fgModule (R : Type u) [ring R] :
Type (u+1)

Define fgModule as the subtype of Module.{u} R of finitely generated modules.

Equations
Instances for fgModule
@[protected, instance]
def fgModule.preadditive (R : Type u) [ring R] :
@[protected, instance]
def fgModule.large_category (R : Type u) [ring R] :
@[protected, instance]
def fgModule.finite (R : Type u) [ring R] (V : fgModule R) :
(V.obj)
@[protected, instance]
def fgModule.inhabited (R : Type u) [ring R] :
Equations
def fgModule.of (R : Type u) [ring R] (V : Type u) [ V] [ V] :

Lift an unbundled finitely generated module to fgModule R.

Equations
@[protected, instance]
def fgModule.obj.module.finite (R : Type u) [ring R] (V : fgModule R) :
(V.obj)
@[protected, instance]
Equations
@[protected, instance]
Equations
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} [ V] [ V] [ W] [ W] (e : V ≃ₗ[R] W) :
V W

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

Equations
@[simp]
theorem linear_equiv.to_fgModule_iso_inv {R : Type u} [ring R] {V W : Type u} [ V] [ V] [ W] [ W] (e : V ≃ₗ[R] W) :
@[simp]
theorem linear_equiv.to_fgModule_iso_hom {R : Type u} [ring R] {V W : Type u} [ V] [ V] [ W] [ W] (e : V ≃ₗ[R] W) :
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]

The forgetful functor fgModule R ⥤ Module R as a monoidal functor.

Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
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 =
@[protected, instance]
def fgModule.quiver.hom.module.finite (K : Type u) [field K] (V W : fgModule K) :
(V W)
@[protected, instance]
Equations
@[simp]
theorem fgModule.ihom_obj (K : Type u) [field K] (V W : fgModule K) :
W = ((V.obj) →ₗ[K] (W.obj))
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
theorem fgModule.fgModule_coevaluation_apply_one (K : Type u) [field K] (V : fgModule K) :
= finset.univ.sum (λ (i : (V.obj))), (V.obj)) i ⊗ₜ[K] (V.obj)).coord i)

The evaluation morphism is given by the contraction map.

Equations
@[simp]
theorem fgModule.fgModule_evaluation_apply (K : Type u) [field K] (V : fgModule K) (f : V).obj)) (x : (V.obj)) :
(f ⊗ₜ[K] x) = f.to_fun x
@[protected, instance]
noncomputable def fgModule.exact_pairing (K : Type u) [field K] (V : fgModule K) :
Equations
@[protected, instance]
noncomputable def fgModule.right_dual (K : Type u) [field K] (V : fgModule K) :
Equations
@[protected, instance]
noncomputable def fgModule.right_rigid_category (K : Type u) [field K] :
Equations