Wedderburn-Artin theorem

Stream: Is there code for X?

[Stepan Nesterov]

The following is the mathlib proof of the Wedderburn-Artin theorem in mathlib:

/-- The **Wedderburn–Artin Theorem**: an Artinian simple ring is isomorphic to a matrix
ring over the opposite of the endomorphism ring of its simple module. -/
theorem exists_ringEquiv_matrix_end_mulOpposite :
    ∃ (n : ℕ) (_ : NeZero n) (I : Ideal R) (_ : IsSimpleModule R I),
      Nonempty (R ≃+* Matrix (Fin n) (Fin n) (Module.End R I)ᵐᵒᵖ) := by
  have ⟨n, hn, S, hS, ⟨e⟩⟩ := (isIsotypic R R).linearEquiv_fun
  refine ⟨n, hn, S, hS, ⟨.trans (.opOp R) <| .trans (.op ?_) (.symm .mopMatrix)⟩⟩
  exact .trans (.moduleEndSelf R) <| .trans e.conjRingEquiv (endVecRingEquivMatrixEnd ..)

Is there a way to extract the fact that specifically the map $R \to M_n(\mathrm{End}_R(I))$, which sends $r$ to $m \mapsto rm$, is an isomorphism? The reason I need this is to prove that a group representation is absolutely irreducible iff its base change to the algebraic closure is absolutely irreducible. The informal proof runs as follows: if $V$ is an irreducible representation of $G$ over $k$, then by Schur's lemma we have $\mathrm{End}_{\overline{k}[G]}(V) = \overline{k}$. Then the natural map $\overline{k}[G] \to M_n(\overline{k})$ is surjective by the claim above. Hence for any field extension $F$ of $\overline{k}$, the map $F[G] \to M_n(F)$ is surjective, hence $V_F$ is irreducible.

[Junyan Xu]

Your outline seems to be missing the MulOpposite.
I think absolute irreducibility is equivalent to $k\to\mathrm{End}_R(I)$ being bijective?

[Stepan Nesterov]

Junyan Xu said:

Your outline seems to be missing the MulOpposite.
I think absolute irreducibility is equivalent to $k\to\mathrm{End}_R(I)$ being bijective?

Yes and the harder direction boils down to exactly this explicit form of Artin-Wedderburn

[Stepan Nesterov]

Oh wait I think I see what you're saying.
An alternative proof could be "If endomorphisms of the representation are more than $k$, then after base change to $\overline{k}$, there is an idempotent endomorphism, hence, a subrepresentation"

[Junyan Xu]

Lorenz invokes the Jacobson density theorem (should be easy from mathlib):
image.png
image.png

[Kevin Buzzard]

You can't extract the fact that you state from the theorem/proof as it stands (the proof is forgotten), but the proof is giving you an explicit isomorphism so you could rewrite everything as a def and get some kind of map, e.g.

noncomputable def AW_n : ℕ := (isIsotypic R R).linearEquiv_fun.choose

instance AW_n_neZero : NeZero (AW_n R) := (isIsotypic R R).linearEquiv_fun.choose_spec.1

etc etc; you'll finish with

def AW_map : R ≃+* Matrix (Fin (AW_n R)) (Fin (AW_n R) (Module.End R (AW_I R)ᵐᵒᵖ := <what it says in the proof>

[Junyan Xu]

The proof of Wedderburn Artin goes like: $R$ is isomorphic to $I^n$ as $R$-modules, so $R^\mathrm{op}\cong \mathrm{End}_R(R)\cong \mathrm{End}_R(I^n)\cong M_n(\mathrm{End}_R(I))$ as rings.

[Stepan Nesterov]

Junyan Xu said:

Lorenz invokes the Jacobson density theorem (should be easy from mathlib):
image.png
image.png

If $V$ is a semisimple $A$-module this implies the map $T : A \to \mathrm{End}_K(V)$ is surjective -- that's exactly my question

[Stepan Nesterov]

I tried searching "Jacobson density" on leansearch.net, but didn't find anything

[Junyan Xu]

You just need to formalize this:
image.png

[Stepan Nesterov]

Junyan Xu said:

The proof of Wedderburn Artin goes like: $R$ is isomorphic to $I^n$ as $R$-modules, so $R^\mathrm{op}\cong \mathrm{End}_R(R)\cong \mathrm{End}_R(I^n)\cong M_n(\mathrm{End}_R(I))$ as rings.

Are you saying that in the mathlib proof of Artin-Wedderburn, the isomorphism constructed is not $r$ to $m \mapsto rm$?

[Kevin Buzzard]

For sure it's .trans (.opOp R) <| .trans (.op (.trans (.moduleEndSelf R) <| .trans e.conjRingEquiv (endVecRingEquivMatrixEnd ..))) (.symm .mopMatrix)

[Kevin Buzzard]

and that seems to be what Junyan wrote. Note that the isomorphism $R\cong I^n$ is unspecified; it's coming from (isIsotypic R R).linearEquiv_fun which again is just an existence statement.

[Junyan Xu]

(deleted)

[Junyan Xu]

Stepan Nesterov said:

Are you saying that in the mathlib proof of Artin-Wedderburn, the isomorphism constructed is not $r$ to $m \mapsto rm$?

$R$ acts on $R$ by right multiplication (the first ring isomorphism), and this action doesn't fix the copies of $I$ s.
There is no map $R\to\mathrm{End}_R(I)$ in general if $R$ is noncommutative, since $m\mapsto rm$ wouldn't be $R$-linear.

[Stepan Nesterov]

Sorry I'm saying nonsense
I think I mean $R \to \mathrm{End}_{\mathrm{End}_R(I)}(I)$

[Stepan Nesterov]

Where $I$ is a right $\mathrm{End}_R(I)$-module

[Junyan Xu]

So this is the setting of Jacobson density instead; the proof of Wedderburn Artin doesn't involve such nested End.

[Stepan Nesterov]

And is Jacobson density not in mathlib?

[Junyan Xu]

not yet

[Junyan Xu]

Would you like me to do it? I'm probably more familiar with the IsSemisimpleModule API.

[Stepan Nesterov]

Can you give me an idiomatic statement and I can try to prove what I want with sorried Jacobson density?

[Stepan Nesterov]

(I might even say that the proof of Jacobson density is knownin1980s if I'm inside FLT :thinking: )

[Junyan Xu]

import Mathlib.RingTheory.SimpleModule.Basic

open Module (End)

variable {A M : Type*} [Ring A] [AddCommGroup M] [Module A M] [IsSemisimpleModule A M]

theorem jacobson_density (f : End (End A M) M) (s : Finset M) :
    ∃ a : A, ∀ m ∈ s, f m = a • m := by
  sorry

theorem Module.Finite.jacobson_density [Module.Finite (End A M) M] :
    Function.Surjective (Module.toModuleEnd A (S := End A M) M) := by
  sorry

[Stepan Nesterov]

Junyan Xu said:

import Mathlib.RingTheory.SimpleModule.Basic

open Module (End)

variable {A M : Type*} [Ring A] [AddCommGroup M] [Module A M] [IsSemisimpleModule A M]

theorem jacobson_density (s : Finset M) :
    letI C := End A M
    ∀ f : End C M, ∃ a : A, ∀ m ∈ s, f m = a • m := by
  sorry

theorem Module.Finite.jacobson_density [Module.Finite (End A M) M] :
    Function.Surjective (Module.toModuleEnd A (S := End A M) M) := by
  sorry

Ok thank you so much!

[Junyan Xu]

changed the statement a bit; it's wasteful to introduce a name for C if it's only used once :)

[Junyan Xu]

#33906

[Junyan Xu]

Correction: Module.toModuleEnd A (S := End A M) M above should be Module.toModuleEnd (End A M) (S := A) M (the original statement is solved by id_surjective)