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 #

Finitely generated modules, as a property of objects of ModuleCat R.

Equations
theorem ModuleCat.isFG_iff {R : Type u} [Ring R] (V : ModuleCat R) :
@[reducible, inline]
abbrev FGModuleCat (R : Type u) [Ring R] :
Type (u + 1)

The category of finitely generated modules.

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

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

Equations
@[simp]
theorem FGModuleCat.obj_carrier {R : Type u} [Ring R] (M : FGModuleCat R) :
M.obj = M
instance instModuleCarrier {R : Type u} [Ring R] (M : FGModuleCat R) :
Module R M
Equations
instance FGModuleCat.finite (R : Type u) [Ring R] (V : FGModuleCat R) :
Equations
@[reducible, inline]
abbrev FGModuleCat.of (R : Type u) [Ring R] (V : Type u) [AddCommGroup V] [Module R V] [Module.Finite R V] :

Lift an unbundled finitely generated module to FGModuleCat R.

Equations
@[simp]
theorem FGModuleCat.of_carrier (R : Type u) [Ring R] (V : Type u) [AddCommGroup V] [Module R V] [Module.Finite R V] :
(of R V) = V
@[reducible, inline]
abbrev FGModuleCat.ofHom {R : Type u} [Ring R] {V W : Type u} [AddCommGroup V] [Module R V] [Module.Finite R V] [AddCommGroup W] [Module R W] [Module.Finite R W] (f : V →ₗ[R] W) :
of R V of R W

Lift a linear map between finitely generated modules to FGModuleCat R.

Equations
theorem FGModuleCat.hom_ext {R : Type u} [Ring R] {V W : FGModuleCat R} {f g : V W} (h : ModuleCat.Hom.hom f = ModuleCat.Hom.hom g) :
f = g
theorem FGModuleCat.hom_ext_iff {R : Type u} [Ring R] {V W : FGModuleCat R} {f g : V W} :
def FGModuleCat.isoToLinearEquiv {R : Type u} [Ring R] {V W : FGModuleCat R} (i : V W) :
V ≃ₗ[R] W

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

Equations

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

Equations
instance FGModuleCat.instFiniteHom (K : Type u) [Field K] (V W : FGModuleCat K) :
@[simp]
theorem FGModuleCat.ihom_obj (K : Type u) [Field K] (V W : FGModuleCat K) :

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

Equations
@[simp]
@[simp]

@[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.

@[simp] lemmas for LinearMap.comp and categorical identities.