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.
Equations
- FGModuleCat R = CategoryTheory.FullSubcategory fun (V : ModuleCat R) => Module.Finite R ↑V
Instances For
Equations
- instCoeSortFGModuleCatType = { coe := FGModuleCat.carrier }
Equations
- instAddCommGroupCarrier M = id inferInstance
Equations
- instModuleCarrier M = id inferInstance
Equations
- FGModuleCat.instInhabited R = { default := { obj := ModuleCat.of R R, property := ⋯ } }
Lift an unbundled finitely generated module to FGModuleCat R
.
Equations
- FGModuleCat.of R V = { obj := ModuleCat.of R V, property := ⋯ }
Instances For
Lift a linear map between finitely generated modules to FGModuleCat R
.
Equations
Instances For
Equations
- FGModuleCat.instHasForget₂ModuleCat R = id inferInstance
Converts and isomorphism in the category FGModuleCat R
to
a LinearEquiv
between the underlying modules.
Equations
- FGModuleCat.isoToLinearEquiv i = ((CategoryTheory.forget₂ (FGModuleCat R) (ModuleCat R)).mapIso i).toLinearEquiv
Instances For
Converts a LinearEquiv
to an isomorphism in the category FGModuleCat R
.
Equations
- e.toFGModuleCatIso = { hom := ModuleCat.ofHom ↑e, inv := ModuleCat.ofHom ↑e.symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
Equations
- FGModuleCat.instLinear R = id inferInstance
Equations
- FGModuleCat.instMonoidalCategory R = id inferInstance
Equations
- FGModuleCat.instSymmetricCategory R = id inferInstance
The forgetful functor FGModuleCat R ⥤ Module R
is a monoidal functor.
Equations
Equations
- FGModuleCat.instMonoidalClosed K = id (CategoryTheory.MonoidalCategory.fullMonoidalClosedSubcategory fun (V : ModuleCat K) => Module.Finite K ↑V)
The dual module is the dual in the rigid monoidal category FGModuleCat K
.
Equations
- FGModuleCat.FGModuleCatDual K V = { obj := ModuleCat.of K (Module.Dual K ↑V), property := ⋯ }
Instances For
The coevaluation map is defined in LinearAlgebra.coevaluation
.
Equations
Instances For
The evaluation morphism is given by the contraction map.
Equations
Instances For
@[simp]
-normal form of FGModuleCatEvaluation_apply
, where the carriers have been unfolded.
Equations
- One or more equations did not get rendered due to their size.
Equations
Equations
- FGModuleCat.rightRigidCategory K = CategoryTheory.RightRigidCategory.mk
@[simp]
lemmas for LinearMap.comp
and categorical identities.