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, FGModuleCat 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 ModuleCat.isFG (R : Type u) [Ring R] : CategoryTheory.ObjectProperty (ModuleCat R)

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

theorem ModuleCat.isFG_iff {R : Type u} [Ring R] (V : ModuleCat R) : isFG R V ↔ Module.Finite R ↑V

@[reducible, inline]

abbrev FGModuleCat (R : Type u) [Ring R] : Type (max u (v + 1))

The category of finitely generated modules.

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

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

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

@[simp]

theorem FGModuleCat.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 instModuleCarrier {R : Type u} [Ring R] (M : FGModuleCat R) : Module R ↑M

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

instance instFiniteCarrierObjModuleCatIsFG {R : Type u} [Ring R] (M : FGModuleCat R) : Module.Finite R ↑M.obj

@[simp]

theorem FGModuleCat.hom_comp (R : Type u) [Ring R] (A B C : FGModuleCat R) (f : A ⟶ B) (g : B ⟶ C) : ModuleCat.Hom.hom (CategoryTheory.CategoryStruct.comp f g) = ModuleCat.Hom.hom g ∘ₗ ModuleCat.Hom.hom f

@[simp]

theorem FGModuleCat.hom_id (R : Type u) [Ring R] (A : FGModuleCat R) : ModuleCat.Hom.hom (CategoryTheory.CategoryStruct.id A) = LinearMap.id

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

@[reducible, inline]

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

Lift an unbundled finitely generated module to FGModuleCat R.

@[simp]

theorem FGModuleCat.of_carrier (R : Type u) [Ring R] (V : Type v) [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 v} [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.

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} : f = g ↔ ModuleCat.Hom.hom f = ModuleCat.Hom.hom g

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

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 an isomorphism in the category FGModuleCat R to a LinearEquiv between the underlying modules.

def LinearEquiv.toFGModuleCatIso {R : Type u} [Ring R] {V W : Type v} [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.

@[simp]

theorem LinearEquiv.toFGModuleCatIso_inv {R : Type u} [Ring R] {V W : Type v} [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 = ModuleCat.ofHom ↑e.symm

@[simp]

theorem LinearEquiv.toFGModuleCatIso_hom {R : Type u} [Ring R] {V W : Type v} [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 = ModuleCat.ofHom ↑e

def FGModuleCat.ulift (R : Type u) [Ring R] : CategoryTheory.Functor (FGModuleCat R) (FGModuleCat R)

Universe lifting as a functor on FGModuleCat.

def FGModuleCat.fullyFaithfulULift (R : Type u) [Ring R] : (ulift R).FullyFaithful

Universe lifting is fully faithful.

instance FGModuleCat.instFaithfulUlift (R : Type u) [Ring R] : (ulift R).Faithful

instance FGModuleCat.instFullUlift (R : Type u) [Ring R] : (ulift R).Full

instance FGModuleCat.instIsMonoidalModuleCatIsFG (R : Type u) [CommRing R] : (ModuleCat.isFG R).IsMonoidal

@[simp]

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

@[simp]

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

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 = ofHom ((isoToLinearEquiv i).conj (ModuleCat.Hom.hom f))

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

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

instance FGModuleCat.instIsMonoidalClosedModuleCatIsFG (K : Type u) [Field K] : (ModuleCat.isFG K).IsMonoidalClosed

@[simp]

theorem FGModuleCat.ihom_obj (K : Type u) [Field K] (V W : FGModuleCat K) : (CategoryTheory.ihom V).obj W = 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.

@[simp]

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

@[simp]

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

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

The coevaluation map is defined in LinearAlgebra.coevaluation.

theorem FGModuleCat.FGModuleCatCoevaluation_apply_one (K : Type u) [Field K] (V : FGModuleCat K) : (ModuleCat.Hom.hom (FGModuleCatCoevaluation K V)) 1 = ∑ i : ↑(Module.Basis.ofVectorSpaceIndex K ↑V), (Module.Basis.ofVectorSpace K ↑V) i ⊗ₜ[K] (Module.Basis.ofVectorSpace K ↑V).coord i

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

The evaluation morphism is given by the contraction map.

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

@[simp]

theorem FGModuleCat.FGModuleCatEvaluation_apply' (K : Type u) [Field K] (V : FGModuleCat K) (f : ↑(FGModuleCatDual K V)) (x : ↑V) : (ModuleCat.Hom.hom (FGModuleCatEvaluation K V)) (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 (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)

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

@[simp]

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

@[simp]

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