Finite generation and projectivity along an equivalence of module categories

Let e : ModuleCat A ≌ ModuleCat B be an equivalence of categories between the module categories of two rings, for instance a Morita equivalence. Finite generation of a module is a property of its submodule lattice: M is finitely generated exactly when ⊤ is a compact element of Submodule A M. Since e induces an order isomorphism between subobject lattices, and the subobjects of a module are its submodules, e preserves and reflects finite generation. Projectivity is a categorical property, so it is preserved and reflected as well.

The results are stated for arbitrary equivalences of module categories, with the two rings and the two module universes independent.

Main definitions

• CategoryTheory.Equivalence.submoduleOrderIso: the order isomorphism Submodule A M ≃o Submodule B (e.functor.obj M) induced by e.

Main results

• CategoryTheory.Equivalence.submoduleOrderIso_apply: it sends a submodule to the image of its inclusion under e.functor.
• CategoryTheory.Equivalence.finite_functor_obj_iff: e.functor.obj M is finitely generated if and only if M is.
• CategoryTheory.Equivalence.isFG_inverseImage: e.functor pulls the finitely generated B-modules back to the finitely generated A-modules.
• CategoryTheory.Equivalence.projective_functor_obj_iff: e.functor.obj M is projective if and only if M is.

noncomputable def CategoryTheory.Equivalence.submoduleOrderIso {A : Type u} [Ring A] {B : Type u'} [Ring B] (e : ModuleCat A ≌ ModuleCat B) (M : ModuleCat A) : Submodule A ↑M ≃o Submodule B ↑(e.functor.obj M)

Submodules along an equivalence of module categories. The order isomorphism from the submodules of M to the submodules of e.functor.obj M, obtained by identifying submodules with categorical subobjects on both sides.

Equations

• e.submoduleOrderIso M = M.subobjectModule.symm.trans ((e.subobjectOrderIso M).trans (e.functor.obj M).subobjectModule)

@[simp]

theorem CategoryTheory.Equivalence.submoduleOrderIso_apply {A : Type u} [Ring A] {B : Type u'} [Ring B] (e : ModuleCat A ≌ ModuleCat B) (M : ModuleCat A) (N : Submodule A ↑M) : (e.submoduleOrderIso M) N = (ModuleCat.Hom.hom (e.functor.map (ModuleCat.ofHom N.subtype))).range

The induced order isomorphism of submodule lattices sends a submodule N of M to the image of e.functor.obj N under the map induced by the inclusion N ⟶ M.

@[simp]

theorem CategoryTheory.Equivalence.finite_functor_obj_iff {A : Type u} [Ring A] {B : Type u'} [Ring B] (e : ModuleCat A ≌ ModuleCat B) (M : ModuleCat A) : Module.Finite B ↑(e.functor.obj M) ↔ Module.Finite A ↑M

An equivalence of module categories preserves and reflects finite generation.

@[simp]

theorem CategoryTheory.Equivalence.isFG_inverseImage {A : Type u} [Ring A] {B : Type u'} [Ring B] (e : ModuleCat A ≌ ModuleCat B) : (ModuleCat.isFG B).inverseImage e.functor = ModuleCat.isFG A

An equivalence of module categories pulls the finitely generated B-modules back to the finitely generated A-modules.

@[simp]

theorem CategoryTheory.Equivalence.projective_functor_obj_iff {A : Type u} [Ring A] {B : Type u'} [Ring B] (e : ModuleCat A ≌ ModuleCat B) [Small.{v, u} A] [Small.{v', u'} B] (M : ModuleCat A) : Module.Projective B ↑(e.functor.obj M) ↔ Module.Projective A ↑M

An equivalence of module categories preserves and reflects projectivity.