Documentation

Mathlib.Algebra.Category.FGModuleCat.Basic

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.

Instances For

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.

Instances For

@[reducible]

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

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

Instances For

@[implicit_reducible]

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 instFiniteCarrier {R : Type u} [Ring R] (M : FGModuleCat R) :

Module.Finite R ↑M

@[simp]

theorem FGModuleCat.hom_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).hom = ModuleCat.Hom.hom g.hom ∘ₗ ModuleCat.Hom.hom f.hom

@[simp]

theorem FGModuleCat.hom_hom_id (R : Type u) [Ring R] (A : FGModuleCat R) :

ModuleCat.Hom.hom (CategoryTheory.CategoryStruct.id A).hom = LinearMap.id

@[deprecated FGModuleCat.hom_hom_comp (since := "2025-12-18")]

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

Alias of FGModuleCat.hom_hom_comp.

@[deprecated FGModuleCat.hom_hom_id (since := "2025-12-18")]

theorem FGModuleCat.hom_id (R : Type u) [Ring R] (A : FGModuleCat R) :

ModuleCat.Hom.hom (CategoryTheory.CategoryStruct.id A).hom = LinearMap.id

Alias of FGModuleCat.hom_hom_id.

@[implicit_reducible]

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

Lift an unbundled finitely generated module to FGModuleCat R.

Instances For

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

Instances For

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

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.hom = ModuleCat.Hom.hom g.hom

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

Module.Finite R ↑V

instance FGModuleCat.instFullModuleCatForget₂LinearMapIdCarrierObjIsFG (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.

Instances For

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.

Instances For

@[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 = CategoryTheory.ConcreteCategory.ofHom ↑e

@[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 = CategoryTheory.ConcreteCategory.ofHom ↑e.symm

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

CategoryTheory.Functor (FGModuleCat R) (FGModuleCat R)

Universe lifting as a functor on FGModuleCat.

Instances For

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

(ulift R).FullyFaithful

Universe lifting is fully faithful.

Instances For

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

(ulift R).Faithful

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

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₂LinearMapIdCarrierObjIsFG (R : Type u) [CommRing R] :

(CategoryTheory.forget₂ (FGModuleCat R) (ModuleCat R)).Additive

instance FGModuleCat.instLinearModuleCatForget₂LinearMapIdCarrierObjIsFG (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.hom))

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

instance FGModuleCat.instFiniteHomModuleCatObjIsFG (K : Type u) [Field K] (V W : FGModuleCat K) :

Module.Finite K (V.obj ⟶ W.obj)

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

(V ⟹ W) = of K (V.obj ⟶ W.obj)

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

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

Instances For

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

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

Instances For

theorem FGModuleCat.FGModuleCatCoevaluation_apply_one (K : Type u) [Field K] (V : FGModuleCat K) :

(CategoryTheory.ConcreteCategory.hom (FGModuleCatCoevaluation K V).hom) 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.

Instances For

theorem FGModuleCat.FGModuleCatEvaluation_apply (K : Type u) [Field K] (V : FGModuleCat K) (f : ↑(FGModuleCatDual K V)) (x : ↑V) :

(CategoryTheory.ConcreteCategory.hom (FGModuleCatEvaluation K V).hom) (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).hom) (f ⊗ₜ[K] x) = f.toFun x

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

@[implicit_reducible]

noncomputable instance FGModuleCat.exactPairing (K : Type u) [Field K] (V : FGModuleCat K) :

CategoryTheory.ExactPairing V (FGModuleCatDual K V)

@[implicit_reducible]

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

CategoryTheory.HasRightDual V

@[implicit_reducible]

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

CategoryTheory.RightRigidCategory (FGModuleCat K)

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

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

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