Morita Equivalece between R and Mₙ(R)

Main definitions

• ModuleCat.toMatrixModCat: The functor from Mod-R to Mod-Mₙ(R) induced by LinearMap.mapMatrixModule and Matrix.Module.matrixModule.

TODO (Edison)

• Prove R and Mₙ(R) are morita-equivalent.

def ModuleCat.toMatrixModCat (R : Type u_1) (ι : Type u_2) [Ring R] [Fintype ι] [DecidableEq ι] : CategoryTheory.Functor (ModuleCat R) (ModuleCat (Matrix ι ι R))

The functor from Mod-R to Mod-Mₙ(R) induced by LinearMap.mapModule and Matrix.matrixModule.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ModuleCat.toMatrixModCat_map (R : Type u_1) (ι : Type u_2) [Ring R] [Fintype ι] [DecidableEq ι] {X✝ Y✝ : ModuleCat R} (f : X✝ ⟶ Y✝) : (toMatrixModCat R ι).map f = ofHom (LinearMap.mapMatrixModule ι (Hom.hom f))

@[simp]

theorem ModuleCat.toMatrixModCat_obj_isAddCommGroup (R : Type u_1) (ι : Type u_2) [Ring R] [Fintype ι] [DecidableEq ι] (M : ModuleCat R) : ((toMatrixModCat R ι).obj M).isAddCommGroup = Pi.addCommGroup

@[simp]

theorem ModuleCat.toMatrixModCat_obj_carrier (R : Type u_1) (ι : Type u_2) [Ring R] [Fintype ι] [DecidableEq ι] (M : ModuleCat R) : ↑((toMatrixModCat R ι).obj M) = (ι → ↑M)

@[simp]

theorem ModuleCat.toMatrixModCat_obj_isModule (R : Type u_1) (ι : Type u_2) [Ring R] [Fintype ι] [DecidableEq ι] (M : ModuleCat R) : ((toMatrixModCat R ι).obj M).isModule = Matrix.Module.matrixModule