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.

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

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

instance instCoeSortFGModuleCatType {R : Type u} [Ring R] : CoeSort (FGModuleCat R) (Type u)

@[simp]

theorem obj_carrier {R : Type u} [Ring R] (M : FGModuleCat R) : ↑M.obj = ↑M

instance instAddCommGroupCarrier {R : Type u} [Ring R] (M : FGModuleCat R) : AddCommGroup ↑M

instance instModuleCarrierToSemiringToAddCommMonoidInstAddCommGroupCarrier {R : Type u} [Ring R] (M : FGModuleCat R) : Module R ↑M

instance instLargeCategoryFGModuleCat {R : Type u} [Ring R] : CategoryTheory.LargeCategory (FGModuleCat R)

instance instLinearMapClassHomFGModuleCatToQuiverToCategoryStructInstLargeCategoryFGModuleCatCarrierToSemiringToAddCommMonoidInstAddCommGroupCarrierInstModuleCarrierToSemiringToAddCommMonoidInstAddCommGroupCarrier {R : Type u} [Ring R] {M : FGModuleCat R} {N : FGModuleCat R} : LinearMapClass (M ⟶ N) R ↑M ↑N

instance instConcreteCategoryFGModuleCatInstLargeCategoryFGModuleCat {R : Type u} [Ring R] : CategoryTheory.ConcreteCategory (FGModuleCat R)

instance instPreadditiveFGModuleCatInstLargeCategoryFGModuleCat {R : Type u} [Ring R] : CategoryTheory.Preadditive (FGModuleCat R)

instance FGModuleCat.finite (R : Type u) [Ring R] (V : FGModuleCat R) : Module.Finite R ↑V

instance FGModuleCat.instInhabitedFGModuleCat (R : Type u) [Ring R] : Inhabited (FGModuleCat R)

def FGModuleCat.of (R : Type u) [Ring R] (V : Type u) [AddCommGroup V] [Module R V] [Module.Finite R V] : FGModuleCat R

Lift an unbundled finitely generated module to FGModuleCat R.

instance FGModuleCat.instFiniteCarrierToSemiringToAddCommMonoidInstAddCommGroupCarrierInstModuleCarrierToSemiringToAddCommMonoidInstAddCommGroupCarrier (R : Type u) [Ring R] (V : FGModuleCat R) : Module.Finite R ↑V

instance FGModuleCat.instHasForget₂FGModuleCatModuleCatInstLargeCategoryFGModuleCatInstConcreteCategoryFGModuleCatInstLargeCategoryFGModuleCatModuleCategoryModuleConcreteCategory (R : Type u) [Ring R] : CategoryTheory.HasForget₂ (FGModuleCat R) (ModuleCat R)

instance FGModuleCat.instFullFGModuleCatInstLargeCategoryFGModuleCatModuleCatModuleCategoryForget₂InstConcreteCategoryFGModuleCatInstLargeCategoryFGModuleCatModuleConcreteCategoryInstHasForget₂FGModuleCatModuleCatInstLargeCategoryFGModuleCatInstConcreteCategoryFGModuleCatInstLargeCategoryFGModuleCatModuleCategoryModuleConcreteCategory (R : Type u) [Ring R] : CategoryTheory.Full (CategoryTheory.forget₂ (FGModuleCat R) (ModuleCat R))

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

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

@[simp]

theorem LinearEquiv.toFGModuleCatIso_inv {R : Type u} [Ring R] {V : Type u} {W : Type u} [AddCommGroup V] [Module R V] [Module.Finite R V] [AddCommGroup W] [Module R W] [Module.Finite R W] (e : V ≃ₗ[R] W) : (LinearEquiv.toFGModuleCatIso e).inv = ↑(LinearEquiv.symm e)

@[simp]

theorem LinearEquiv.toFGModuleCatIso_hom {R : Type u} [Ring R] {V : Type u} {W : Type u} [AddCommGroup V] [Module R V] [Module.Finite R V] [AddCommGroup W] [Module R W] [Module.Finite R W] (e : V ≃ₗ[R] W) : (LinearEquiv.toFGModuleCatIso e).hom = ↑e

def LinearEquiv.toFGModuleCatIso {R : Type u} [Ring R] {V : Type u} {W : Type u} [AddCommGroup V] [Module R V] [Module.Finite R V] [AddCommGroup W] [Module R W] [Module.Finite R W] (e : V ≃ₗ[R] W) : FGModuleCat.of R V ≅ FGModuleCat.of R W

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

instance FGModuleCat.instLinearToSemiringToCommSemiringFGModuleCatToRingInstLargeCategoryFGModuleCatInstPreadditiveFGModuleCatInstLargeCategoryFGModuleCat (R : Type u) [CommRing R] : CategoryTheory.Linear R (FGModuleCat R)

instance FGModuleCat.monoidalPredicate_module_finite (R : Type u) [CommRing R] : CategoryTheory.MonoidalCategory.MonoidalPredicate fun V => Module.Finite R ↑V

instance FGModuleCat.instMonoidalCategoryFGModuleCatToRingInstLargeCategoryFGModuleCat (R : Type u) [CommRing R] : CategoryTheory.MonoidalCategory (FGModuleCat R)

@[simp]

theorem FGModuleCat.tensorUnit_obj (R : Type u) [CommRing R] : (CategoryTheory.MonoidalCategory.tensorUnit (FGModuleCat R)).obj = CategoryTheory.MonoidalCategory.tensorUnit (ModuleCat R)

@[simp]

theorem FGModuleCat.tensorObj_obj (R : Type u) [CommRing R] (M : FGModuleCat R) (N : FGModuleCat R) : (CategoryTheory.MonoidalCategory.tensorObj M N).obj = CategoryTheory.MonoidalCategory.tensorObj M.obj N.obj

instance FGModuleCat.instSymmetricCategoryFGModuleCatToRingInstLargeCategoryFGModuleCatInstMonoidalCategoryFGModuleCatToRingInstLargeCategoryFGModuleCat (R : Type u) [CommRing R] : CategoryTheory.SymmetricCategory (FGModuleCat R)

instance FGModuleCat.instMonoidalPreadditiveFGModuleCatToRingInstLargeCategoryFGModuleCatInstPreadditiveFGModuleCatInstLargeCategoryFGModuleCatInstMonoidalCategoryFGModuleCatToRingInstLargeCategoryFGModuleCat (R : Type u) [CommRing R] : CategoryTheory.MonoidalPreadditive (FGModuleCat R)

instance FGModuleCat.instMonoidalLinearToSemiringToCommSemiringFGModuleCatToRingInstLargeCategoryFGModuleCatInstPreadditiveFGModuleCatInstLargeCategoryFGModuleCatInstLinearToSemiringToCommSemiringFGModuleCatToRingInstLargeCategoryFGModuleCatInstPreadditiveFGModuleCatInstLargeCategoryFGModuleCatInstMonoidalCategoryFGModuleCatToRingInstLargeCategoryFGModuleCatInstMonoidalPreadditiveFGModuleCatToRingInstLargeCategoryFGModuleCatInstPreadditiveFGModuleCatInstLargeCategoryFGModuleCatInstMonoidalCategoryFGModuleCatToRingInstLargeCategoryFGModuleCat (R : Type u) [CommRing R] : CategoryTheory.MonoidalLinear R (FGModuleCat R)

def FGModuleCat.forget₂Monoidal (R : Type u) [CommRing R] : CategoryTheory.MonoidalFunctor (FGModuleCat R) (ModuleCat R)

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

instance FGModuleCat.forget₂Monoidal_faithful (R : Type u) [CommRing R] : CategoryTheory.Faithful (FGModuleCat.forget₂Monoidal R).toLaxMonoidalFunctor.toFunctor

instance FGModuleCat.forget₂Monoidal_additive (R : Type u) [CommRing R] : CategoryTheory.Functor.Additive (FGModuleCat.forget₂Monoidal R).toLaxMonoidalFunctor.toFunctor

instance FGModuleCat.forget₂Monoidal_linear (R : Type u) [CommRing R] : CategoryTheory.Functor.Linear R (FGModuleCat.forget₂Monoidal R).toLaxMonoidalFunctor.toFunctor

theorem FGModuleCat.Iso.conj_eq_conj (R : Type u) [CommRing R] {V : FGModuleCat R} {W : FGModuleCat R} (i : V ≅ W) (f : CategoryTheory.End V) : ↑(CategoryTheory.Iso.conj i) f = ↑(LinearEquiv.conj (FGModuleCat.isoToLinearEquiv i)) f

instance FGModuleCat.instFiniteHomFGModuleCatToRingToDivisionRingToQuiverToCategoryStructInstLargeCategoryFGModuleCatToSemiringToDivisionSemiringToSemifieldToAddCommMonoidHomGroupInstPreadditiveFGModuleCatInstLargeCategoryFGModuleCatHomModuleInstLinearToSemiringToCommSemiringFGModuleCatToRingInstLargeCategoryFGModuleCatInstPreadditiveFGModuleCatInstLargeCategoryFGModuleCatToCommRingToEuclideanDomain (K : Type u) [Field K] (V : FGModuleCat K) (W : FGModuleCat K) : Module.Finite K (V ⟶ W)

instance FGModuleCat.closedPredicateModuleFinite (K : Type u) [Field K] : CategoryTheory.MonoidalCategory.ClosedPredicate fun V => Module.Finite K ↑V

instance FGModuleCat.instMonoidalClosedFGModuleCatToRingToDivisionRingInstLargeCategoryFGModuleCatInstMonoidalCategoryFGModuleCatToRingInstLargeCategoryFGModuleCatToCommRingToEuclideanDomain (K : Type u) [Field K] : CategoryTheory.MonoidalClosed (FGModuleCat K)

@[simp]

theorem FGModuleCat.ihom_obj (K : Type u) [Field K] (V : FGModuleCat K) (W : FGModuleCat K) : (CategoryTheory.ihom V).obj W = FGModuleCat.of K (↑V →ₗ[K] ↑W)

def FGModuleCat.FGModuleCatDual (K : Type u) [Field K] (V : FGModuleCat K) : FGModuleCat K

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

@[simp]

theorem FGModuleCat.FGModuleCatDual_obj (K : Type u) [Field K] (V : FGModuleCat K) : (FGModuleCat.FGModuleCatDual K V).obj = ModuleCat.of K (Module.Dual K ↑V)

@[simp]

theorem FGModuleCat.FGModuleCatDual_coe (K : Type u) [Field K] (V : FGModuleCat K) : ↑(FGModuleCat.FGModuleCatDual K V) = Module.Dual K ↑V

def FGModuleCat.FGModuleCatCoevaluation (K : Type u) [Field K] (V : FGModuleCat K) : CategoryTheory.MonoidalCategory.tensorUnit (FGModuleCat K) ⟶ CategoryTheory.MonoidalCategory.tensorObj V (FGModuleCat.FGModuleCatDual K V)

The coevaluation map is defined in LinearAlgebra.coevaluation.

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

def FGModuleCat.FGModuleCatEvaluation (K : Type u) [Field K] (V : FGModuleCat K) : CategoryTheory.MonoidalCategory.tensorObj (FGModuleCat.FGModuleCatDual K V) V ⟶ CategoryTheory.MonoidalCategory.tensorUnit (FGModuleCat K)

The evaluation morphism is given by the contraction map.

@[simp]

theorem FGModuleCat.FGModuleCatEvaluation_apply (K : Type u) [Field K] (V : FGModuleCat K) (f : ↑(FGModuleCat.FGModuleCatDual K V)) (x : ↑V) : ↑(FGModuleCat.FGModuleCatEvaluation K V) (f ⊗ₜ[K] x) = AddHom.toFun f.toAddHom x

instance FGModuleCat.exactPairing (K : Type u) [Field K] (V : FGModuleCat K) : CategoryTheory.ExactPairing V (FGModuleCat.FGModuleCatDual K V)

instance FGModuleCat.rightDual (K : Type u) [Field K] (V : FGModuleCat K) : CategoryTheory.HasRightDual V

instance FGModuleCat.rightRigidCategory (K : Type u) [Field K] : CategoryTheory.RightRigidCategory (FGModuleCat K)