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 = inferInstance

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

Equations

• instModuleCarrier M = inferInstance

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

Equations

• instLargeCategoryFGModuleCat = id inferInstance

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

Equations

• instFunLikeHomFGModuleCatCarrier = LinearMap.instFunLike

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

Equations

• ⋯ = ⋯

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

Equations

• instConcreteCategoryFGModuleCat = id inferInstance

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

Equations

• instPreadditiveFGModuleCat = id inferInstance

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

Equations

• ⋯ = ⋯

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

Equations

• FGModuleCat.instInhabited 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.instFiniteCarrier (R : Type u) [Ring R] (V : FGModuleCat R) : Module.Finite R ↑V

Equations

• ⋯ = ⋯

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

Equations

• FGModuleCat.instHasForget₂ModuleCat R = id inferInstance

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

Equations

• ⋯ = ⋯

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.forget₂ (FGModuleCat R) (ModuleCat R)).mapIso i).toLinearEquiv

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

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

@[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) : e.toFGModuleCatIso.inv = ↑e.symm

@[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) : e.toFGModuleCatIso.hom = ↑e

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

Equations

• FGModuleCat.instLinear 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.instMonoidalCategory (R : Type u) [CommRing R] : CategoryTheory.MonoidalCategory (FGModuleCat R)

Equations

• FGModuleCat.instMonoidalCategory 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.instSymmetricCategory (R : Type u) [CommRing R] : CategoryTheory.SymmetricCategory (FGModuleCat R)

Equations

• FGModuleCat.instSymmetricCategory R = id inferInstance

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

Equations

• ⋯ = ⋯

instance FGModuleCat.instMonoidalLinear (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] : (FGModuleCat.forget₂Monoidal R).Faithful

Equations

• ⋯ = ⋯

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

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) : i.conj f = (FGModuleCat.isoToLinearEquiv i).conj f

instance FGModuleCat.instFiniteHom (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.instMonoidalClosed (K : Type u) [Field K] : CategoryTheory.MonoidalClosed (FGModuleCat K)

Equations

• FGModuleCat.instMonoidalClosed K = id (CategoryTheory.MonoidalCategory.fullMonoidalClosedSubcategory fun (V : ModuleCat K) => Module.Finite K ↑V)

@[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 = ∑ i : ↑(Basis.ofVectorSpaceIndex K ↑V), (Basis.ofVectorSpace K ↑V) i ⊗ₜ[K] (Basis.ofVectorSpace K ↑V).coord 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

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

@[simp]

theorem LinearMap.comp_id_fgModuleCat {R : Type u} [Ring R] {G : FGModuleCat R} {H : Type u} [AddCommGroup H] [Module R H] (f : ↑G →ₗ[R] H) : f ∘ₗ CategoryTheory.CategoryStruct.id G = f

@[simp]

theorem LinearMap.id_fgModuleCat_comp {R : Type u} [Ring R] {G : Type u} [AddCommGroup G] [Module R G] {H : FGModuleCat R} (f : G →ₗ[R] ↑H) : CategoryTheory.CategoryStruct.id H ∘ₗ f = f