Morita equivalences on finitely generated modules

A linear equivalence between the categories of all modules over two finite-dimensional algebras preserves finite-length objects. Over an Artinian ring these are exactly the finitely generated modules, so a Mathlib MoritaEquivalence restricts to the finitely generated module categories.

theorem MagnitudeConjecture.MoritaEquivalence.moduleFinite_functor_obj {k A B : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [Ring B] [Algebra k B] [FiniteDimensional k B] (e : MoritaEquivalence k A B) (M : ModuleCat A) [Module.Finite A ↑M] : Module.Finite B ↑(e.eqv.functor.obj M)

A categorical equivalence carries a finite-length module over one finite-dimensional algebra to a finite-length module over the other.

def MagnitudeConjecture.MoritaEquivalence.fgModuleEquivalence {k A B : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [Ring B] [Algebra k B] [FiniteDimensional k B] (e : MoritaEquivalence k A B) : FGModuleCat A ≌ FGModuleCat B

A Morita equivalence between finite-dimensional algebras restricts to an equivalence of their finitely generated left-module categories.

instance MagnitudeConjecture.MoritaEquivalence.fgModuleEquivalence_functor_additive {k A B : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [Ring B] [Algebra k B] [FiniteDimensional k B] (e : MoritaEquivalence k A B) : (fgModuleEquivalence e).functor.Additive

instance MagnitudeConjecture.MoritaEquivalence.fgModuleEquivalence_inverse_additive {k A B : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [Ring B] [Algebra k B] [FiniteDimensional k B] (e : MoritaEquivalence k A B) : (fgModuleEquivalence e).inverse.Additive

instance MagnitudeConjecture.MoritaEquivalence.fgModuleEquivalence_functor_linear {k A B : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [Ring B] [Algebra k B] [FiniteDimensional k B] (e : MoritaEquivalence k A B) : CategoryTheory.Functor.Linear k (fgModuleEquivalence e).functor

instance MagnitudeConjecture.MoritaEquivalence.fgModuleEquivalence_inverse_linear {k A B : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [Ring B] [Algebra k B] [FiniteDimensional k B] (e : MoritaEquivalence k A B) : CategoryTheory.Functor.Linear k (fgModuleEquivalence e).inverse

noncomputable def MagnitudeConjecture.MoritaEquivalence.fgRightModuleEquivalence {k A B : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [Ring B] [Algebra k B] [FiniteDimensional k B] (e : MoritaEquivalence k A B) : FGModuleCat Aᵐᵒᵖ ≌ FGModuleCat Bᵐᵒᵖ

A Morita equivalence of finite-dimensional algebras also induces a linear equivalence between their finitely generated right-module categories. Contragredient duality changes right modules to the opposites of the corresponding left-module categories, where the supplied Morita equivalence applies.

instance MagnitudeConjecture.MoritaEquivalence.fgRightModuleEquivalence_functor_additive {k A B : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [Ring B] [Algebra k B] [FiniteDimensional k B] (e : MoritaEquivalence k A B) : (fgRightModuleEquivalence e).functor.Additive

instance MagnitudeConjecture.MoritaEquivalence.fgRightModuleEquivalence_functor_linear {k A B : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [Ring B] [Algebra k B] [FiniteDimensional k B] (e : MoritaEquivalence k A B) : CategoryTheory.Functor.Linear k (fgRightModuleEquivalence e).functor

instance MagnitudeConjecture.MoritaEquivalence.fgRightModuleEquivalence_inverse_additive {k A B : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [Ring B] [Algebra k B] [FiniteDimensional k B] (e : MoritaEquivalence k A B) : (fgRightModuleEquivalence e).inverse.Additive

instance MagnitudeConjecture.MoritaEquivalence.fgRightModuleEquivalence_inverse_linear {k A B : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [Ring B] [Algebra k B] [FiniteDimensional k B] (e : MoritaEquivalence k A B) : CategoryTheory.Functor.Linear k (fgRightModuleEquivalence e).inverse