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

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

Equations

• instModuleCarrier M = id inferInstance

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

Equations

• instLargeCategoryFGModuleCat = id inferInstance

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

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

Equations

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

@[reducible, inline]

abbrev 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 := ⋯ }

@[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) : FGModuleCat.of R V ⟶ FGModuleCat.of R W

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

Equations

• FGModuleCat.ofHom f = ModuleCat.ofHom f

theorem FGModuleCat.hom_ext {R : Type u} [Ring R] {V W : FGModuleCat R} {f g : V ⟶ W} (h : f.hom = g.hom) : f = g

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

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

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

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

def LinearEquiv.toFGModuleCatIso {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] (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 := ModuleCat.ofHom ↑e, inv := ModuleCat.ofHom ↑e.symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem LinearEquiv.toFGModuleCatIso_hom_hom {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] (e : V ≃ₗ[R] W) : e.toFGModuleCatIso.hom.hom = ↑e

@[simp]

theorem LinearEquiv.toFGModuleCatIso_inv_hom {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] (e : V ≃ₗ[R] W) : e.toFGModuleCatIso.inv.hom = ↑e.symm

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

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 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)

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

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

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

Equations

• FGModuleCat.instMonoidalModuleCatForget₂ R = CategoryTheory.MonoidalCategory.fullSubcategoryInclusionMonoidal fun (V : ModuleCat R) => Module.Finite R ↑V

instance FGModuleCat.instAdditiveModuleCatForget₂ (R : Type u) [CommRing R] : (CategoryTheory.forget₂ (FGModuleCat R) (ModuleCat R)).Additive

instance FGModuleCat.instLinearModuleCatForget₂ (R : Type u) [CommRing R] : CategoryTheory.Functor.Linear R (CategoryTheory.forget₂ (FGModuleCat R) (ModuleCat R))

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

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

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

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

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 W : FGModuleCat K) : (CategoryTheory.ihom V).obj W = FGModuleCat.of K (V ⟶ 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 = ModuleCat.ofHom (coevaluation K ↑V)

theorem FGModuleCat.FGModuleCatCoevaluation_apply_one (K : Type u) [Field K] (V : FGModuleCat K) : (FGModuleCat.FGModuleCatCoevaluation K V).hom 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 = ModuleCat.ofHom (contractLeft K ↑V)

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

@[simp]

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

@[simp]-normal form of FGModuleCatEvaluation_apply, where the carriers have been unfolded.

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).hom = 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).hom ∘ₗ f = f