Morita Equivalence 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.
• MatrixModCat.toModuleCat: The functor from Mod-Mₙ(R) to Mod-R induced by sending M to the image of Eᵢᵢ • · where Eᵢᵢ is the elementary matrix.
• ModuleCat.matrixEquivalence: An equivalence of categories composed by ModuleCat.toMatrixModCat R ι. and MatrixModCat.toModuleCat R i.
• moritaEquivalentToMatrix: moritaEquivalentToMatrix is a MoritaEquivalence.

Main results

• IsMoritaEquivalent.matrix: R and Mₙ(R) are Morita equivalent.

def ModuleCat.toMatrixModCat (R : Type u) (ι : Type v) [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_obj_isAddCommGroup (R : Type u) (ι : Type v) [Ring R] [Fintype ι] [DecidableEq ι] (M : ModuleCat R) : ((toMatrixModCat R ι).obj M).isAddCommGroup = Pi.addCommGroup

@[simp]

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

@[simp]

theorem ModuleCat.toMatrixModCat_map (R : Type u) (ι : Type v) [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_isModule (R : Type u) (ι : Type v) [Ring R] [Fintype ι] [DecidableEq ι] (M : ModuleCat R) : ((toMatrixModCat R ι).obj M).isModule = Matrix.Module.matrixModule

def MatrixModCat.toModuleCatObj (R : Type u) {ι : Type v} [Ring R] [Fintype ι] [DecidableEq ι] (M : Type u_1) [AddCommGroup M] [Module (Matrix ι ι R) M] [Module R M] [IsScalarTower R (Matrix ι ι R) M] (i : ι) : Submodule R M

The image of Eᵢᵢ (the elementary matrix) acting on all elements in M.

Equations

• MatrixModCat.toModuleCatObj R M i = (let __spread.0 := DistribSMul.toAddMonoidHom M (Matrix.single i i 1); { toFun := (↑__spread.0).toFun, map_add' := ⋯, map_smul' := ⋯ }).range

@[simp]

theorem MatrixModCat.mem_toModuleCatObj {R : Type u} {ι : Type v} [Ring R] [Fintype ι] [DecidableEq ι] {M : Type u_1} [AddCommGroup M] [Module (Matrix ι ι R) M] [Module R M] [IsScalarTower R (Matrix ι ι R) M] (i : ι) {x : M} : x ∈ toModuleCatObj R M i ↔ ∃ (y : M), Matrix.single i i 1 • y = x

def MatrixModCat.fromMatrixLinear {R : Type u} {ι : Type v} [Ring R] [Fintype ι] [DecidableEq ι] {M : Type u_1} [AddCommGroup M] [Module (Matrix ι ι R) M] {N : Type u_2} [AddCommGroup N] [Module (Matrix ι ι R) N] (i : ι) [Module R N] [IsScalarTower R (Matrix ι ι R) N] [Module R M] [IsScalarTower R (Matrix ι ι R) M] (f : M →ₗ[Matrix ι ι R] N) : ↥(toModuleCatObj R M i) →ₗ[R] ↥(toModuleCatObj R N i)

An R-linear map between Eᵢᵢ • M and Eᵢᵢ • N induced by an Mₙ(R)-linear map from M to N.

Equations

• MatrixModCat.fromMatrixLinear i f = (↑R f).restrict ⋯

@[simp]

theorem MatrixModCat.fromMatrixLinear_apply_coe {R : Type u} {ι : Type v} [Ring R] [Fintype ι] [DecidableEq ι] {M : Type u_1} [AddCommGroup M] [Module (Matrix ι ι R) M] {N : Type u_2} [AddCommGroup N] [Module (Matrix ι ι R) N] (i : ι) [Module R N] [IsScalarTower R (Matrix ι ι R) N] [Module R M] [IsScalarTower R (Matrix ι ι R) M] (f : M →ₗ[Matrix ι ι R] N) (c : ↥(toModuleCatObj R M i)) : ↑((fromMatrixLinear i f) c) = f ↑c

theorem MatrixModCat.isScalarTower_toModuleCat (R : Type u) {ι : Type v} [Ring R] [Fintype ι] [DecidableEq ι] (M : ModuleCat (Matrix ι ι R)) : IsScalarTower R (Matrix ι ι R) ↑M

def MatrixModCat.toModuleCat (R : Type u) {ι : Type v} [Ring R] [Fintype ι] [DecidableEq ι] (i : ι) : CategoryTheory.Functor (ModuleCat (Matrix ι ι R)) (ModuleCat R)

The functor from the category of modules over Mₙ(R) to the category of modules over R induced by sending M to the image of Eᵢᵢ • · where Eᵢᵢ is the elementary matrix.

Equations

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

@[simp]

theorem MatrixModCat.toModuleCat_obj_isAddCommGroup (R : Type u) {ι : Type v} [Ring R] [Fintype ι] [DecidableEq ι] (i : ι) (M : ModuleCat (Matrix ι ι R)) : ((toModuleCat R i).obj M).isAddCommGroup = (toModuleCatObj R (↑M) i).addCommGroup

@[simp]

theorem MatrixModCat.toModuleCat_obj_isModule (R : Type u) {ι : Type v} [Ring R] [Fintype ι] [DecidableEq ι] (i : ι) (M : ModuleCat (Matrix ι ι R)) : ((toModuleCat R i).obj M).isModule = (toModuleCatObj R (↑M) i).module

@[simp]

theorem MatrixModCat.toModuleCat_obj_carrier (R : Type u) {ι : Type v} [Ring R] [Fintype ι] [DecidableEq ι] (i : ι) (M : ModuleCat (Matrix ι ι R)) : ↑((toModuleCat R i).obj M) = ↥(toModuleCatObj R (↑M) i)

@[simp]

theorem MatrixModCat.toModuleCat_map (R : Type u) {ι : Type v} [Ring R] [Fintype ι] [DecidableEq ι] (i : ι) {X✝ Y✝ : ModuleCat (Matrix ι ι R)} (f : X✝ ⟶ Y✝) : (toModuleCat R i).map f = ModuleCat.ofHom (fromMatrixLinear i (ModuleCat.Hom.hom f))

def fromModuleCatToModuleCatLinearEquivtoModuleCatObj (R : Type u) {ι : Type v} [Ring R] [Fintype ι] [DecidableEq ι] (M : Type u_1) [AddCommGroup M] [Module R M] (i : ι) : ↑(((ModuleCat.toMatrixModCat R ι).comp (MatrixModCat.toModuleCat R i)).obj (ModuleCat.of R M)) ≃ₗ[R] ↥(MatrixModCat.toModuleCatObj R (ι → M) i)

The linear equiv induced by the equality toModuleCat (toMatrixModCat M) = Eᵢᵢ • Mⁿ.

Equations

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

def fromModuleCatToModuleCatLinearEquiv (R : Type u) {ι : Type v} [Ring R] [Fintype ι] [DecidableEq ι] (M : Type u_1) [AddCommGroup M] [Module R M] (i : ι) : ↥(MatrixModCat.toModuleCatObj R (ι → M) i) ≃ₗ[R] M

Auxiliary isomorphism showing that compose two functors gives id on objects.

Equations

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

@[simp]

theorem fromModuleCatToModuleCatLinearEquiv_symm_apply_coe (R : Type u) {ι : Type v} [Ring R] [Fintype ι] [DecidableEq ι] (M : Type u_1) [AddCommGroup M] [Module R M] (i : ι) (x : M) (j : ι) : ↑((fromModuleCatToModuleCatLinearEquiv R M i).symm x) j = Pi.single i x j

@[simp]

theorem fromModuleCatToModuleCatLinearEquiv_apply (R : Type u) {ι : Type v} [Ring R] [Fintype ι] [DecidableEq ι] (M : Type u_1) [AddCommGroup M] [Module R M] (i : ι) (x : ↥(MatrixModCat.toModuleCatObj R (ι → M) i)) : (fromModuleCatToModuleCatLinearEquiv R M i) x = ∑ i_1 : ι, ↑x i_1

def MatrixModCat.unitIso (R : Type u) {ι : Type v} [Ring R] [Fintype ι] [DecidableEq ι] (i : ι) : (ModuleCat.toMatrixModCat R ι).comp (toModuleCat R i) ≅ CategoryTheory.Functor.id (ModuleCat R)

The natural isomorphism showing that toModuleCat is the left inverse of toMatrixModCat.

Equations

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

def toModuleCatFromModuleCatLinearEquiv (R : Type u) {ι : Type v} [Ring R] [Fintype ι] [DecidableEq ι] (M : ModuleCat (Matrix ι ι R)) (j : ι) : ↑M ≃ₗ[Matrix ι ι R] ι → ↥(MatrixModCat.toModuleCatObj R (↑M) j)

The linear equiv induced by the equality toMatrixModCat (toModuleCat M) = Mⁿ

Equations

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

def MatrixModCat.counitIso (R : Type u) {ι : Type v} [Ring R] [Fintype ι] [DecidableEq ι] (i : ι) : (toModuleCat R i).comp (ModuleCat.toMatrixModCat R ι) ≅ CategoryTheory.Functor.id (ModuleCat (Matrix ι ι R))

The natural isomorphism showing that toMatrixModCat is the right inverse of toModuleCat.

Equations

• MatrixModCat.counitIso R i = CategoryTheory.NatIso.ofComponents (fun (X : ModuleCat (Matrix ι ι R)) => (toModuleCatFromModuleCatLinearEquiv R X i).symm.toModuleIso) ⋯

def ModuleCat.matrixEquivalence (R : Type u) {ι : Type v} [Ring R] [Fintype ι] [DecidableEq ι] (i : ι) : ModuleCat R ≌ ModuleCat (Matrix ι ι R)

ModuleCat.toMatrixModCat R ι and MatrixModCat.toModuleCat R i together form an equivalence of categories.

Equations

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

@[simp]

theorem ModuleCat.matrixEquivalence_inverse (R : Type u) {ι : Type v} [Ring R] [Fintype ι] [DecidableEq ι] (i : ι) : (matrixEquivalence R i).inverse = MatrixModCat.toModuleCat R i

@[simp]

theorem ModuleCat.matrixEquivalence_functor (R : Type u) {ι : Type v} [Ring R] [Fintype ι] [DecidableEq ι] (i : ι) : (matrixEquivalence R i).functor = toMatrixModCat R ι

@[simp]

theorem ModuleCat.matrixEquivalence_counitIso (R : Type u) {ι : Type v} [Ring R] [Fintype ι] [DecidableEq ι] (i : ι) : (matrixEquivalence R i).counitIso = MatrixModCat.counitIso R i

@[simp]

theorem ModuleCat.matrixEquivalence_unitIso (R : Type u) {ι : Type v} [Ring R] [Fintype ι] [DecidableEq ι] (i : ι) : (matrixEquivalence R i).unitIso = (MatrixModCat.unitIso R i).symm

def moritaEquivalenceMatrix (R : Type u) {ι : Type v} [Ring R] [Fintype ι] [DecidableEq ι] (R₀ : Type u_1) [CommRing R₀] [Algebra R₀ R] (i : ι) : MoritaEquivalence R₀ R (Matrix ι ι R)

Moreover ModuleCat.matrixEquivalence is a MoritaEquivalence.

Equations

• moritaEquivalenceMatrix R R₀ i = { eqv := ModuleCat.matrixEquivalence R i, linear := ⋯ }

@[simp]

theorem moritaEquivalenceMatrix_eqv (R : Type u) {ι : Type v} [Ring R] [Fintype ι] [DecidableEq ι] (R₀ : Type u_1) [CommRing R₀] [Algebra R₀ R] (i : ι) : (moritaEquivalenceMatrix R R₀ i).eqv = ModuleCat.matrixEquivalence R i

theorem IsMoritaEquivalent.matrix (R : Type u) {ι : Type v} [Ring R] [Fintype ι] [DecidableEq ι] (R₀ : Type u_1) [CommRing R₀] [Algebra R₀ R] [Nonempty ι] : IsMoritaEquivalent R₀ R (Matrix ι ι R)