# Documentation

Mathlib.Algebra.Category.FGModuleCat.Basic

# The category of finitely generated modules over a ring #

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

When K is a field, FGModuleCatCat 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 FGModuleCat R is abelian when R is (left)-noetherian.
def FGModuleCat (R : Type u) [Ring R] :
Type (u + 1)

Define FGModuleCat as the subtype of ModuleCat.{u} R of finitely generated modules.

Instances For
def FGModuleCat.carrier {R : Type u} [Ring R] (M : ) :

A synonym for M.obj.carrier, which we can mark with @[coe].

Instances For
@[simp]
theorem obj_carrier {R : Type u} [Ring R] (M : ) :
M.obj = M
instance instAddCommGroupCarrier {R : Type u} [Ring R] (M : ) :
instance FGModuleCat.finite (R : Type u) [Ring R] (V : ) :
def FGModuleCat.of (R : Type u) [Ring R] (V : Type u) [] [Module R V] [] :

Lift an unbundled finitely generated module to FGModuleCat R.

Instances For
def FGModuleCat.isoToLinearEquiv {R : Type u} [Ring R] {V : } {W : } (i : V W) :
V ≃ₗ[R] W

Converts and isomorphism in the category FGModuleCat R to a LinearEquiv between the underlying modules.

Instances For
@[simp]
theorem LinearEquiv.toFGModuleCatIso_inv {R : Type u} [Ring R] {V : Type u} {W : Type u} [] [Module R V] [] [] [Module R W] [] (e : V ≃ₗ[R] W) :
().inv = ↑()
@[simp]
theorem LinearEquiv.toFGModuleCatIso_hom {R : Type u} [Ring R] {V : Type u} {W : Type u} [] [Module R V] [] [] [Module R W] [] (e : V ≃ₗ[R] W) :
().hom = e
def LinearEquiv.toFGModuleCatIso {R : Type u} [Ring R] {V : Type u} {W : Type u} [] [Module R V] [] [] [Module R W] [] (e : V ≃ₗ[R] W) :

Converts a LinearEquiv to an isomorphism in the category FGModuleCat R.

Instances For
@[simp]
theorem FGModuleCat.tensorUnit_obj (R : Type u) [] :
@[simp]
theorem FGModuleCat.tensorObj_obj (R : Type u) [] (M : ) (N : ) :
=

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

Instances For
instance FGModuleCat.forget₂Monoidal_faithful (R : Type u) [] :
CategoryTheory.Faithful ().toLaxMonoidalFunctor.toFunctor
instance FGModuleCat.forget₂Monoidal_additive (R : Type u) [] :
instance FGModuleCat.forget₂Monoidal_linear (R : Type u) [] :
CategoryTheory.Functor.Linear R ().toLaxMonoidalFunctor.toFunctor
theorem FGModuleCat.Iso.conj_eq_conj (R : Type u) [] {V : } {W : } (i : V W) (f : ) :
↑() f =
@[simp]
theorem FGModuleCat.ihom_obj (K : Type u) [] (V : ) (W : ) :
().obj W = FGModuleCat.of K (V →ₗ[K] W)
def FGModuleCat.FGModuleCatDual (K : Type u) [] (V : ) :

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

Instances For
@[simp]
theorem FGModuleCat.FGModuleCatDual_obj (K : Type u) [] (V : ) :
().obj = ModuleCat.of K (Module.Dual K V)
@[simp]
theorem FGModuleCat.FGModuleCatDual_coe (K : Type u) [] (V : ) :
↑() = Module.Dual K V

The coevaluation map is defined in LinearAlgebra.coevaluation.

Instances For
theorem FGModuleCat.FGModuleCatCoevaluation_apply_one (K : Type u) [] (V : ) :
= Finset.sum Finset.univ fun i => ↑() i ⊗ₜ[K] Basis.coord () i

The evaluation morphism is given by the contraction map.

Instances For
@[simp]
theorem FGModuleCat.FGModuleCatEvaluation_apply (K : Type u) [] (V : ) (f : ↑()) (x : V) :