feat(RingTheory): isotypic API and simple Wedderburn–Artin existence (#23963)

A replacement of #23583 with more meaningful intermediate results.

Co-authored-by: Edison Xie @Whysoserioushah 
Co-authored-by: Jujian Zhang [jujian.zhang19@imperial.ac.uk](mailto:jujian.zhang19@imperial.ac.uk)

Author: alreadydone

Mathlib.lean

@@ -5347,7 +5347,10 @@ import Mathlib.RingTheory.RootsOfUnity.Lemmas
 import Mathlib.RingTheory.RootsOfUnity.Minpoly
 import Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
 import Mathlib.RingTheory.SimpleModule.Basic
+import Mathlib.RingTheory.SimpleModule.IsAlgClosed
+import Mathlib.RingTheory.SimpleModule.Isotypic
 import Mathlib.RingTheory.SimpleModule.Rank
+import Mathlib.RingTheory.SimpleModule.WedderburnArtin
 import Mathlib.RingTheory.SimpleRing.Basic
 import Mathlib.RingTheory.SimpleRing.Congr
 import Mathlib.RingTheory.SimpleRing.Defs

Mathlib/RingTheory/SimpleModule/Basic.lean

@@ -3,8 +3,10 @@ Copyright (c) 2020 Aaron Anderson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson
 -/
-import Mathlib.LinearAlgebra.DFinsupp
+import Mathlib.Algebra.DirectSum.Module
+import Mathlib.Data.Finite.Card
 import Mathlib.Data.Matrix.Mul
+import Mathlib.LinearAlgebra.DFinsupp
 import Mathlib.LinearAlgebra.Finsupp.Span
 import Mathlib.LinearAlgebra.Isomorphisms
 import Mathlib.LinearAlgebra.Projection
@@ -70,7 +72,6 @@ variable {R S} in
 theorem RingEquiv.isSemisimpleRing_iff (e : R ≃+* S) : IsSemisimpleRing R ↔ IsSemisimpleRing S :=
   ⟨fun _ ↦ e.isSemisimpleRing, fun _ ↦ e.symm.isSemisimpleRing⟩
 
--- Making this an instance causes the linter to complain of "dangerous instances"
 theorem IsSimpleModule.nontrivial [IsSimpleModule R M] : Nontrivial M :=
   ⟨⟨0, by
       have h : (⊥ : Submodule R M) ≠ ⊤ := bot_ne_top
@@ -86,8 +87,11 @@ theorem LinearMap.isSimpleModule_iff_of_bijective [Module S N] {σ : R →+* S}
 
 variable [Module R N]
 
-theorem IsSimpleModule.congr (l : M ≃ₗ[R] N) [IsSimpleModule R N] : IsSimpleModule R M :=
-  (Submodule.orderIsoMapComap l).isSimpleOrder
+theorem IsSimpleModule.congr (e : M ≃ₗ[R] N) [IsSimpleModule R N] : IsSimpleModule R M :=
+  (Submodule.orderIsoMapComap e).isSimpleOrder
+
+theorem LinearEquiv.isSimpleModule_iff (e : M ≃ₗ[R] N) : IsSimpleModule R M ↔ IsSimpleModule R N :=
+  ⟨(·.congr e.symm), (·.congr e)⟩
 
 theorem isSimpleModule_iff_isAtom : IsSimpleModule R m ↔ IsAtom m := by
   rw [← Set.isSimpleOrder_Iic_iff_isAtom]
@@ -182,6 +186,12 @@ namespace IsSemisimpleModule
 
 variable [IsSemisimpleModule R M]
 
+theorem extension_property {P} [AddCommGroup P] [Module R P] (f : N →ₗ[R] M)
+    (hf : Function.Injective f) (g : N →ₗ[R] P) :
+    ∃ h : M →ₗ[R] P, h ∘ₗ f = g :=
+  have ⟨m, compl⟩ := exists_isCompl (LinearMap.range f)
+  ⟨g ∘ₗ LinearMap.linearProjOfIsCompl _ f hf compl, by ext; simp⟩
+
 theorem eq_bot_or_exists_simple_le (N : Submodule R M) : N = ⊥ ∨ ∃ m ≤ N, IsSimpleModule R m := by
   simpa only [isSimpleModule_iff_isAtom, and_comm] using eq_bot_or_exists_atom_le _
 
@@ -261,6 +271,10 @@ end
 
 end IsSemisimpleModule
 
+theorem LinearEquiv.isSemisimpleModule_iff (e : M ≃ₗ[R] N) :
+    IsSemisimpleModule R M ↔ IsSemisimpleModule R N :=
+  ⟨(·.congr e.symm), (·.congr e)⟩
+
 /-- A module is semisimple iff it is generated by its simple submodules. -/
 theorem sSup_simples_eq_top_iff_isSemisimpleModule :
     sSup { m : Submodule R M | IsSimpleModule R m } = ⊤ ↔ IsSemisimpleModule R M :=
@@ -273,21 +287,14 @@ lemma isSemisimpleModule_of_isSemisimpleModule_submodule {s : Set ι} {p : ι 
   refine complementedLattice_of_complementedLattice_Iic (fun i hi ↦ ?_) hp'
   simpa only [← (p i).mapIic.complementedLattice_iff] using hp i hi
 
+open Submodule in
 lemma isSemisimpleModule_biSup_of_isSemisimpleModule_submodule {s : Set ι} {p : ι → Submodule R M}
     (hp : ∀ i ∈ s, IsSemisimpleModule R (p i)) :
     IsSemisimpleModule R ↥(⨆ i ∈ s, p i) := by
-  let q := ⨆ i ∈ s, p i
-  let p' : ι → Submodule R q := fun i ↦ (p i).comap q.subtype
-  have hp₀ : ∀ i ∈ s, p i ≤ LinearMap.range q.subtype := fun i hi ↦ by
-    simpa only [Submodule.range_subtype] using le_biSup _ hi
-  have hp₁ : ∀ i ∈ s, IsSemisimpleModule R (p' i) := fun i hi ↦ by
-    let e : p' i ≃ₗ[R] p i := (p i).comap_equiv_self_of_inj_of_le q.injective_subtype (hp₀ i hi)
-    exact (Submodule.orderIsoMapComap e).complementedLattice_iff.mpr <| hp i hi
-  have hp₂ : ⨆ i ∈ s, p' i = ⊤ := by
-    apply Submodule.map_injective_of_injective q.injective_subtype
-    simp_rw [Submodule.map_top, Submodule.range_subtype, Submodule.map_iSup]
-    exact biSup_congr fun i hi ↦ Submodule.map_comap_eq_of_le (hp₀ i hi)
-  exact isSemisimpleModule_of_isSemisimpleModule_submodule hp₁ hp₂
+  refine isSemisimpleModule_of_isSemisimpleModule_submodule
+    ((comap_equiv_self_of_inj_of_le (injective_subtype _) ?_).isSemisimpleModule_iff.mpr <| hp · ·)
+    (biSup_comap_subtype_eq_top ..)
+  simp_rw [range_subtype, le_biSup p ‹_›]
 
 lemma isSemisimpleModule_of_isSemisimpleModule_submodule' {p : ι → Submodule R M}
     (hp : ∀ i, IsSemisimpleModule R (p i)) (hp' : ⨆ i, p i = ⊤) :
@@ -300,16 +307,32 @@ instance {ι} (M : ι → Type*) [∀ i, AddCommGroup (M i)] [∀ i, Module R (M
   exact isSemisimpleModule_of_isSemisimpleModule_submodule'
     (fun _ ↦ .range _) DFinsupp.iSup_range_lsingle
 
-theorem isSemisimpleModule_iff_exists_linearEquiv_dfinsupp : IsSemisimpleModule R M ↔
-    ∃ (s : Set (Submodule R M)) (_ : M ≃ₗ[R] Π₀ m : s, m.1), ∀ m : s, IsSimpleModule R m.1 := by
-  refine ⟨fun _ ↦ ?_, fun ⟨s, e, h⟩ ↦ .congr e⟩
+variable (R M) in
+theorem IsSemisimpleModule.exists_linearEquiv_dfinsupp [IsSemisimpleModule R M] :
+    ∃ (s : Set (Submodule R M)) (_ : M ≃ₗ[R] Π₀ m : s, m.1),
+      sSupIndep s ∧ ∀ m : s, IsSimpleModule R m.1 := by
   have ⟨s, ind, sSup, simple⟩ := IsSemisimpleModule.exists_sSupIndep_sSup_simples_eq_top R M
+  refine ⟨s, ?_, ind, SetCoe.forall.mpr simple⟩
   rw [sSupIndep_iff] at ind
-  refine ⟨s, ?_, SetCoe.forall.mpr simple⟩
   classical
   exact .symm <| .trans (.ofInjective _ ind.dfinsupp_lsum_injective) <| .trans (.ofEq _ ⊤ <|
     by rw [← Submodule.iSup_eq_range_dfinsupp_lsum, ← sSup, sSup_eq_iSup']) Submodule.topEquiv
 
+theorem isSemisimpleModule_iff_exists_linearEquiv_dfinsupp : IsSemisimpleModule R M ↔
+    ∃ (s : Set (Submodule R M)) (_ : M ≃ₗ[R] Π₀ m : s, m.1), ∀ m : s, IsSimpleModule R m.1 := by
+  refine ⟨fun _ ↦ ?_, fun ⟨s, e, h⟩ ↦ .congr e⟩
+  have ⟨s, e, h⟩ := IsSemisimpleModule.exists_linearEquiv_dfinsupp R M
+  exact ⟨s, e, h.2⟩
+
+variable (R M) in
+theorem IsSemisimpleModule.exists_linearEquiv_fin_dfinsupp [IsSemisimpleModule R M]
+    [Module.Finite R M] : ∃ (n : ℕ) (S : Fin n → Submodule R M)
+      (_ : M ≃ₗ[R] Π₀ i : Fin n, S i), ∀ i, IsSimpleModule R (S i) :=
+  have ⟨s, e, h, simple⟩ := IsSemisimpleModule.exists_linearEquiv_dfinsupp R M
+  have := WellFoundedGT.finite_of_iSupIndep ((sSupIndep_iff _).mp h)
+    fun S ↦ (S.1.nontrivial_iff_ne_bot).mp <| IsSimpleModule.nontrivial R S
+  ⟨_, _, e.trans <| DirectSum.lequivCongrLeft R (Finite.equivFin s), fun _ ↦ simple _⟩
+
 open LinearMap in
 instance {ι} [Finite ι] (M : ι → Type*) [∀ i, AddCommGroup (M i)] [∀ i, Module R (M i)]
     [∀ i, IsSemisimpleModule R (M i)] : IsSemisimpleModule R (Π i, M i) := by
@@ -429,6 +452,12 @@ theorem isCoatom_ker_of_surjective [IsSimpleModule R N] {f : M →ₗ[R] N}
   rw [← isSimpleModule_iff_isCoatom]
   exact IsSimpleModule.congr (f.quotKerEquivOfSurjective hf)
 
+theorem linearEquiv_of_ne_zero [IsSemisimpleModule R M] [IsSimpleModule R N]
+    {f : M →ₗ[R] N} (h : f ≠ 0) : ∃ S : Submodule R M, Nonempty (N ≃ₗ[R] S) :=
+  have ⟨m, (_ : IsSimpleModule R m), ne⟩ :=
+    exists_ne_zero_of_sSup_eq_top h _ (IsSemisimpleModule.sSup_simples_eq_top ..)
+  ⟨m, ⟨.symm <| .ofBijective _ ((bijective_or_eq_zero _).resolve_right ne)⟩⟩
+
 /-- Schur's Lemma makes the endomorphism ring of a simple module a division ring. -/
 noncomputable instance _root_.Module.End.instDivisionRing
     [DecidableEq (Module.End R M)] [IsSimpleModule R M] : DivisionRing (Module.End R M) where

Mathlib/RingTheory/SimpleModule/IsAlgClosed.lean

@@ -0,0 +1,19 @@
+/-
+Copyright (c) 2025 Junyan Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Junyan Xu
+-/
+import Mathlib.FieldTheory.IsAlgClosed.Basic
+import Mathlib.RingTheory.SimpleModule.WedderburnArtin
+
+/-!
+# Wedderburn-Artin Theorem over an algebraically closed field
+-/
+
+theorem IsSimpleRing.exists_algEquiv_matrix_of_isAlgClosed (F R) [Field F] [IsAlgClosed F]
+    [Ring R] [IsSimpleRing R] [Algebra F R] [FiniteDimensional F R] :
+    ∃ (n : ℕ) (_ : NeZero n), Nonempty (R ≃ₐ[F] Matrix (Fin n) (Fin n) F) :=
+  have := IsArtinianRing.of_finite F R
+  have ⟨n, hn, D, _, _, _, ⟨e⟩⟩ := exists_algEquiv_matrix_divisionRing_finite F R
+  ⟨n, hn, ⟨e.trans <| .mapMatrix <| .symm <| .ofBijective (Algebra.ofId F D)
+    IsAlgClosed.algebraMap_bijective_of_isIntegral⟩⟩