Morita equivalence for matrix algebras

This file ports the upstream BrauerGroup development proving the Morita equivalence between modules over a ring and over a matrix ring.

@[implicit_reducible]

instance instModuleMatrixForallLeanPool (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [DecidableEq ι] (M : Type u_1) [AddCommGroup M] [Module R M] : Module (Matrix ι ι R) (ι → M)

Equations

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

def toModuleCatOverMatrix (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [DecidableEq ι] : CategoryTheory.Functor (ModuleCat R) (ModuleCat (Matrix ι ι R))

The functor sending an R-module to the coordinatewise module over ι × ι matrices.

Equations

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

@[simp]

theorem toModuleCatOverMatrix_obj_carrier (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [DecidableEq ι] (M : ModuleCat R) : ↑((toModuleCatOverMatrix R ι).obj M) = (ι → ↑M)

@[simp]

theorem toModuleCatOverMatrix_map (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [DecidableEq ι] {X✝ Y✝ : ModuleCat R} (f : X✝ ⟶ Y✝) : (toModuleCatOverMatrix R ι).map f = ModuleCat.ofHom { toFun := fun (v : ι → ↑X✝) (i : ι) => (CategoryTheory.ConcreteCategory.hom f) (v i), map_add' := ⋯, map_smul' := ⋯ }

def fromModuleCatOverMatrix.α (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] (M : Type u_1) [AddCommGroup M] [Module (Matrix ι ι R) M] : AddSubgroup M

The additive subgroup cut out by the default diagonal idempotent.

Equations

• fromModuleCatOverMatrix.α R ι M = { carrier := Set.range fun (x : M) => Matrix.single default default 1 • x, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

@[simp]

theorem fromModuleCatOverMatrix.coe_α (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] (M : Type u_1) [AddCommGroup M] [Module (Matrix ι ι R) M] : ↑(α R ι M) = Set.range fun (x : M) => Matrix.single default default 1 • x

@[implicit_reducible]

instance fromModuleCatOverMatrix.moduleΑ (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] (M : Type u_1) [AddCommGroup M] [Module (Matrix ι ι R) M] : Module R ↥(α R ι M)

Equations

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

def fromModuleCatOverMatrix (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] : CategoryTheory.Functor (ModuleCat (Matrix ι ι R)) (ModuleCat R)

The functor sending a matrix-module to the default diagonal idempotent summand.

Equations

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

@[simp]

theorem fromModuleCatOverMatrix_obj_carrier (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] (M : ModuleCat (Matrix ι ι R)) : ↑((fromModuleCatOverMatrix R ι).obj M) = ↥(fromModuleCatOverMatrix.α R ι ↑M)

@[simp]

theorem fromModuleCatOverMatrix_map (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] {X✝ Y✝ : ModuleCat (Matrix ι ι R)} (f : X✝ ⟶ Y✝) : (fromModuleCatOverMatrix R ι).map f = ModuleCat.ofHom { toFun := fun (x : ↥(fromModuleCatOverMatrix.α R ι ↑X✝)) => ⟨(CategoryTheory.ConcreteCategory.hom f) ↑x, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

def matrix.unitIsoHom (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] : (toModuleCatOverMatrix R ι).comp (fromModuleCatOverMatrix R ι) ⟶ CategoryTheory.Functor.id (ModuleCat R)

The counit of toModuleCatOverMatrix ⋙ fromModuleCatOverMatrix.

Equations

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

@[simp]

theorem matrix.unitIsoHom_app (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] (X : ModuleCat R) : (unitIsoHom R ι).app X = ModuleCat.ofHom { toFun := fun (x : ↥(fromModuleCatOverMatrix.α R ι ↑((toModuleCatOverMatrix R ι).obj X))) => ∑ i : ι, ↑x i, map_add' := ⋯, map_smul' := ⋯ }

def matrix.unitIsoInv (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] : CategoryTheory.Functor.id (ModuleCat R) ⟶ (toModuleCatOverMatrix R ι).comp (fromModuleCatOverMatrix R ι)

The inverse unit map for toModuleCatOverMatrix ⋙ fromModuleCatOverMatrix.

Equations

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

@[simp]

theorem matrix.unitIsoInv_app (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] (X : ModuleCat R) : (unitIsoInv R ι).app X = ModuleCat.ofHom { toFun := fun (x : ↑X) => ⟨Function.update 0 default x, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

def matrix.unitIso (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] : (toModuleCatOverMatrix R ι).comp (fromModuleCatOverMatrix R ι) ≅ CategoryTheory.Functor.id (ModuleCat R)

The natural isomorphism from toModuleCatOverMatrix ⋙ fromModuleCatOverMatrix to the identity.

Equations

• matrix.unitIso R ι = { hom := matrix.unitIsoHom R ι, inv := matrix.unitIsoInv R ι, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem matrix.unitIso_inv (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] : (unitIso R ι).inv = unitIsoInv R ι

@[simp]

theorem matrix.unitIso_hom (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] : (unitIso R ι).hom = unitIsoHom R ι

noncomputable def matrix.counitIsoHomMap (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] (M : ModuleCat (Matrix ι ι R)) : M ≅ ((fromModuleCatOverMatrix R ι).comp (toModuleCatOverMatrix R ι)).obj M

The linear isomorphism comparing a matrix-module with its reconstructed coordinate module.

Equations

• matrix.counitIsoHomMap R ι M = (LinearEquiv.ofBijective { toFun := fun (m : ↑M) (i : ι) => ⟨Matrix.single default i 1 • m, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ } ⋯).toModuleIso

noncomputable def matrix.counitIsoHom (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] : (fromModuleCatOverMatrix R ι).comp (toModuleCatOverMatrix R ι) ⟶ CategoryTheory.Functor.id (ModuleCat (Matrix ι ι R))

The counit map from the reconstructed matrix-module to the original matrix-module.

Equations

• matrix.counitIsoHom R ι = { app := fun (M : ModuleCat (Matrix ι ι R)) => (matrix.counitIsoHomMap R ι M).inv, naturality := ⋯ }

@[simp]

theorem matrix.counitIsoHom_app (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] (M : ModuleCat (Matrix ι ι R)) : (counitIsoHom R ι).app M = (counitIsoHomMap R ι M).inv

noncomputable def matrix.counitIsoInv (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] : CategoryTheory.Functor.id (ModuleCat (Matrix ι ι R)) ⟶ (fromModuleCatOverMatrix R ι).comp (toModuleCatOverMatrix R ι)

The inverse of the matrix-module counit map.

Equations

• matrix.counitIsoInv R ι = { app := fun (M : ModuleCat (Matrix ι ι R)) => (matrix.counitIsoHomMap R ι M).hom, naturality := ⋯ }

@[simp]

theorem matrix.counitIsoInv_app (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] (M : ModuleCat (Matrix ι ι R)) : (counitIsoInv R ι).app M = (counitIsoHomMap R ι M).hom

noncomputable def matrix.counitIso (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] : (fromModuleCatOverMatrix R ι).comp (toModuleCatOverMatrix R ι) ≅ CategoryTheory.Functor.id (ModuleCat (Matrix ι ι R))

The natural isomorphism from fromModuleCatOverMatrix ⋙ toModuleCatOverMatrix to the identity.

Equations

• matrix.counitIso R ι = { hom := matrix.counitIsoHom R ι, inv := matrix.counitIsoInv R ι, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem matrix.counitIso_hom (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] : (counitIso R ι).hom = counitIsoHom R ι

@[simp]

theorem matrix.counitIso_inv (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] : (counitIso R ι).inv = counitIsoInv R ι

noncomputable def moritaEquivalentToMatrix (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] : ModuleCat R ≌ ModuleCat (Matrix ι ι R)

The Morita equivalence between modules over R and modules over Matrix ι ι R.

Equations

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

@[simp]

theorem moritaEquivalentToMatrix_inverse (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] : (moritaEquivalentToMatrix R ι).inverse = fromModuleCatOverMatrix R ι

@[simp]

theorem moritaEquivalentToMatrix_counitIso (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] : (moritaEquivalentToMatrix R ι).counitIso = matrix.counitIso R ι

@[simp]

theorem moritaEquivalentToMatrix_unitIso (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] : (moritaEquivalentToMatrix R ι).unitIso = (matrix.unitIso R ι).symm

@[simp]

theorem moritaEquivalentToMatrix_functor (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [Inhabited ι] [DecidableEq ι] : (moritaEquivalentToMatrix R ι).functor = toModuleCatOverMatrix R ι

theorem IsMoritaEquivalent.division_ring.division_ring_exists_unique_isSimpleModule (S : Type u) [DivisionRing S] (N : Type u_1) [AddCommGroup N] [Module S N] [IsSimpleModule S N] : Nonempty (N ≃ₗ[S] S)

instance IsMoritaEquivalent.division_ring.instAdditiveModuleCatFunctor_leanPool (R S : Type u) [DivisionRing R] [DivisionRing S] (e : ModuleCat R ≌ ModuleCat S) : e.functor.Additive

theorem IsMoritaEquivalent.division_ring.isSimpleModule_iff_injective_or_eq_zero (R : Type u) [Ring R] (M : ModuleCat R) : IsSimpleModule R ↑M ↔ Nontrivial ↑M ∧ ∀ (N : ModuleCat R) (f : M ⟶ N), f = 0 ∨ Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f)

instance CategoryTheory.Equivalence.nontrivial {R S : Type u} [Ring R] [Ring S] (e : ModuleCat R ≌ ModuleCat S) (M : ModuleCat R) [h : Nontrivial ↑M] : Nontrivial ↑(e.functor.obj M)

theorem IsMoritaEquivalent.division_ring.IsSimpleModule.functor (R S : Type u) [Ring R] [Ring S] (e : ModuleCat R ≌ ModuleCat S) (M : ModuleCat R) [simple_module : IsSimpleModule R ↑M] : IsSimpleModule S ↑(e.functor.obj M)

theorem matrix_smul_vec_def (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [DecidableEq ι] {M : Type u_1} [AddCommGroup M] [Module R M] (N : Matrix ι ι R) (v : ι → M) : N • v = fun (i : ι) => ∑ j : ι, N i j • v j

theorem matrix_smul_vec_def' (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [DecidableEq ι] {M : Type u_1} [AddCommGroup M] [Module R M] (N : Matrix ι ι R) (v : ι → M) : N • v = ∑ j : ι, fun (i : ι) => N i j • v j

theorem matrix_smul_vec_apply (R : Type u) [Ring R] (ι : Type w) [Fintype ι] [DecidableEq ι] {M : Type u_1} [AddCommGroup M] [Module R M] (N : Matrix ι ι R) (v : ι → M) (i : ι) : (N • v) i = ∑ j : ι, N i j • v j