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 whenR
is (left)-noetherian.
Define FGModuleCat
as the subtype of ModuleCat.{u} R
of finitely generated modules.
Instances For
A synonym for M.obj.carrier
, which we can mark with @[coe]
.
Instances For
Lift an unbundled finitely generated module to FGModuleCat R
.
Instances For
Converts and isomorphism in the category FGModuleCat R
to
a LinearEquiv
between the underlying modules.
Instances For
Converts a LinearEquiv
to an isomorphism in the category FGModuleCat R
.
Instances For
The forgetful functor FGModuleCat R ⥤ Module R
as a monoidal functor.
Instances For
The dual module is the dual in the rigid monoidal category FGModuleCat K
.
Instances For
The coevaluation map is defined in LinearAlgebra.coevaluation
.
Instances For
The evaluation morphism is given by the contraction map.