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.

Equations

• FGModuleCat R = CategoryTheory.FullSubcategory fun (V : ModuleCat R) => Module.Finite R ↑V

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].

Equations

• ↑M = ↑M.obj

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

Equations

• instCoeSortFGModuleCatType = { coe := FGModuleCat.carrier }

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

Equations

• instAddCommGroupCarrier M = let_fun this := inferInstance; this

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

Equations

• instModuleCarrierToSemiringToAddCommMonoidInstAddCommGroupCarrier M = let_fun this := inferInstance; this

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

Equations

• instLargeCategoryFGModuleCat = id inferInstance

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

Equations

• instFunLikeHomFGModuleCatToQuiverToCategoryStructInstLargeCategoryFGModuleCatCarrier = LinearMap.instFunLike

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

Equations

• ⋯ = ⋯

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

Equations

• instConcreteCategoryFGModuleCatInstLargeCategoryFGModuleCat = id inferInstance

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

Equations

• instPreadditiveFGModuleCatInstLargeCategoryFGModuleCat = id inferInstance

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

Equations

• ⋯ = ⋯

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

Equations

• FGModuleCat.instInhabitedFGModuleCat R = { default := { obj := ModuleCat.of R R, property := ⋯ } }

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.

Equations

• FGModuleCat.of R V = { obj := ModuleCat.of R V, property := ⋯ }

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

Equations

• ⋯ = ⋯

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

Equations

• FGModuleCat.instHasForget₂FGModuleCatModuleCatInstLargeCategoryFGModuleCatInstConcreteCategoryFGModuleCatInstLargeCategoryFGModuleCatModuleCategoryModuleConcreteCategory R = id inferInstance

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• FGModuleCat.isoToLinearEquiv i = CategoryTheory.Iso.toLinearEquiv ((CategoryTheory.forget₂ (FGModuleCat R) (ModuleCat R)).mapIso i)

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

Equations

• LinearEquiv.toFGModuleCatIso e = { hom := ↑e, inv := ↑(LinearEquiv.symm e), hom_inv_id := ⋯, inv_hom_id := ⋯ }

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

Equations

• FGModuleCat.instLinearToSemiringToCommSemiringFGModuleCatToRingInstLargeCategoryFGModuleCatInstPreadditiveFGModuleCatInstLargeCategoryFGModuleCat R = id inferInstance

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

Equations

• ⋯ = ⋯

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

Equations

• FGModuleCat.instMonoidalCategoryFGModuleCatToRingInstLargeCategoryFGModuleCat R = id inferInstance

@[simp]

theorem FGModuleCat.tensorUnit_obj (R : Type u) [CommRing R] : (𝟙_ (FGModuleCat R)).obj = 𝟙_ (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)

Equations

• FGModuleCat.instSymmetricCategoryFGModuleCatToRingInstLargeCategoryFGModuleCatInstMonoidalCategoryFGModuleCatToRingInstLargeCategoryFGModuleCat R = id inferInstance

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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.

Equations

• FGModuleCat.forget₂Monoidal R = CategoryTheory.MonoidalCategory.fullMonoidalSubcategoryInclusion fun (V : ModuleCat R) => Module.Finite R ↑V

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• FGModuleCat.FGModuleCatDual K V = { obj := ModuleCat.of K (Module.Dual K ↑V), property := ⋯ }

@[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) : 𝟙_ (FGModuleCat K) ⟶ CategoryTheory.MonoidalCategory.tensorObj V (FGModuleCat.FGModuleCatDual K V)

The coevaluation map is defined in LinearAlgebra.coevaluation.

Equations

• FGModuleCat.FGModuleCatCoevaluation K V = coevaluation K ↑V

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.ofVectorSpaceIndex K ↑V)) => (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 ⟶ 𝟙_ (FGModuleCat K)

The evaluation morphism is given by the contraction map.

Equations

• FGModuleCat.FGModuleCatEvaluation K V = contractLeft K ↑V

@[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) = f.toFun x

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• FGModuleCat.rightDual K V = CategoryTheory.HasRightDual.mk (FGModuleCat.FGModuleCatDual K V)

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

Equations

• FGModuleCat.rightRigidCategory K = CategoryTheory.RightRigidCategory.mk