Matrices form a semisimple ring

Stream: Is there code for X?

[亚历山大大帝]

Is there a theorem in Mathlib that derives Matrix (Fin n) (Fin n) R is a semisimple ring from R being a semisimple ring?

[Yury G. Kudryashov]

Does docs#IsSemisimpleRing.isSemisimpleModule work for you?

[Notification Bot]

This topic was moved here from #lean4 > 半单环 by Yury G. Kudryashov.

[Yury G. Kudryashov]

Sorry, it doesn't.

[Yury G. Kudryashov]

(deleted)

[Junyan Xu]

Nope, this was left as proof_wanted

[Junyan Xu]

I wonder whether @Edison Xie et al. have anything in the Brauer group repo. If not here's a proof outline: we want to show MnR := Matrix (Fin n) (Fin n) R can be written as a sum of simple modules, i.e. minimal left ideals (IsAtom). We know that R can be written as a sum of minimal left ideals I. For each i : Fin n, we construct the left ideal of MnR consisting of matrices whose entries in the ith column lie in I and whose entries in the other columns are 0, and show this is a minimal left ideal. Finally show MnR is the supremum of all such left ideals.

[Edison Xie]

Junyan Xu said:

I wonder whether Edison Xie et al. have anything in the Brauer group repo

Sadly I don't work under semi-simplicity condition but only simple ones however morita-equivalence between R and Matrix n n R should send simple modules over R to simple modules over Matrix n n R and sends R to Rⁿ, together with

abbrev e (n R : Type*) [Ring R] [Fintype n] [DecidableEq n]:
    Matrix n n R ≃ₗ[Matrix n n R] n → (n → R) :=
  {
  __ := Matrix.ofLinearEquiv R|>.symm
  map_smul' M N := funext fun i ↦ funext fun j ↦ by
    simp [Matrix.of_symm_apply, matrix_smul_vec_def, Matrix.mul_apply]
  }

should give you semi-simplicity?

[Junyan Xu]

failed to synthesize
  Module (Matrix n n R) (n → n → R)

in web editor (import Mathlib). Is the instance in the Brauer group repo and would you PR it? I think [Module R M] : Module (Matrix n n R) (n → M) is a reasonable instance and would be helpful if we want to deal with a semisimple module over a ring that is not necessarily semisimple. If we only deal with semisimple rings, my outline above would not require introducing an additional instance.
P.S. I don't think we need/should use Morita theory (or category theory in general) here (to deal with the case of matrix rings).

[Edison Xie]

Junyan Xu said:

failed to synthesize
  Module (Matrix n n R) (n → n → R)

Oh yes sorry this is in brauer group repo and yes I will PR this but seems like you already have a solution for this!

[Edison Xie]

Junyan Xu said:

I don't think we need/should use Morita theory (or category theory in general) here (to deal with the case of matrix rings).

Yeah we could do it constructively :)

[Edison Xie]

@Junyan Xu the instance is :

import Mathlib

variable (R ι : Type*) [Ring R] [Fintype ι] [DecidableEq ι]

open Matrix in
instance (M : Type*) [AddCommGroup M] [Module R M] : Module (Matrix ι ι R) (ι → M) where
  smul N v i := ∑ j : ι, N i j • v j
  one_smul v := funext fun i => show ∑ _, _ = _ by simp [one_apply]
  mul_smul N₁ N₂ v := funext fun i => show ∑ _, _ = ∑ _, _ • (∑ _, _) by
    simp_rw [mul_apply, Finset.smul_sum, Finset.sum_smul, MulAction.mul_smul]
    rw [Finset.sum_comm]
  smul_zero v := funext fun i => show ∑ _, _ = _ by simp
  smul_add N v₁ v₂ := funext fun i => show ∑ j : ι, N i j • (v₁ + v₂) j = (∑ _, _) + (∑ _, _) by
    simp [Finset.sum_add_distrib]
  add_smul N₁ N₂ v := funext fun i => show ∑ j : ι, (N₁ + N₂) i j • v j = (∑ _, _) + (∑ _, _) by
    simp [add_smul, Finset.sum_add_distrib]
  zero_smul v := funext fun i => show ∑ _, _ = _ by simp

lemma matrix_smul_vec_def {M : Type*} [AddCommGroup M] [Module R M] (N : Matrix ι ι R) (v : ι → M) :
    N • v = fun i => ∑ j : ι, N i j • v j := rfl

abbrev e (n R : Type*) [Ring R] [Fintype n] [DecidableEq n]:
    Matrix n n R ≃ₗ[Matrix n n R] n → (n → R) :=
  {
  __ := Matrix.ofLinearEquiv R|>.symm
  map_smul' M N := funext fun i ↦ funext fun j ↦ by
    simp [matrix_smul_vec_def, Matrix.mul_apply]
  }

[Eric Wieser]

This creates an instance diamond when M := I -> N

[Eric Wieser]

Which is precisely the case you care about with Module (Matrix n n R) (n → n → R)

[Junyan Xu]

Indeed, acting on columns vs. on rows ...

[Junyan Xu]

I think we need a type synonym, maybe MatrixModule ι M := ι → M.

[Edison Xie]

Eric Wieser said:

Which is precisely the case you care about with Module (Matrix n n R) (n → n → R)

I care about ModuleCat R ⥤ ModuleCat (Matrix n n R)

[Junyan Xu]

A different approach using Wedderburn--Artin (semisimple case): a semisimple ring is a finite product of simple Artinian rings, and the matrix ring over the product is a product of matrix rings (missing in mathlib). Matrix rings over a simple ring is still simple, and matrix rings over an Artinian ring is Artinian by IsArtinianRing.of_finite. Therefore matrix rings over a simple Artinian ring is simple Artinian, therefore semisimple. Now conclude using instIsSemisimpleRingForallOfFinite.

[Junyan Xu]

I've killed all the four proof_wanted related to Wedderburn--Artin in this commit.