[Merged by Bors] - feat(RingTheory): isotypic API and simple Wedderburn–Artin existence

Mathlib.lean

@@ -5207,6 +5207,7 @@ import Mathlib.RingTheory.RootsOfUnity.Minpoly
 import Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
 import Mathlib.RingTheory.SimpleModule.Basic
 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/Algebra/Equiv/TransferInstance.lean

@@ -461,11 +461,6 @@ protected abbrev commRing [CommRing β] : CommRing α := by
 noncomputable instance [Small.{v} α] [CommRing α] : CommRing (Shrink.{v} α) :=
   (equivShrink α).symm.commRing
 
-include e in
-/-- Transfer `Nontrivial` across an `Equiv` -/
-protected theorem nontrivial [Nontrivial β] : Nontrivial α :=
-  e.surjective.nontrivial
-
 noncomputable instance [Small.{v} α] [Nontrivial α] : Nontrivial (Shrink.{v} α) :=
   (equivShrink α).symm.nontrivial
 

Mathlib/Algebra/Module/Equiv/Basic.lean

@@ -9,6 +9,7 @@ import Mathlib.Algebra.GroupWithZero.Action.Basic
 import Mathlib.Algebra.GroupWithZero.Action.Units
 import Mathlib.Algebra.Module.Equiv.Defs
 import Mathlib.Algebra.Module.Hom
+import Mathlib.Algebra.Module.LinearMap.Basic
 import Mathlib.Algebra.Module.LinearMap.End
 import Mathlib.Algebra.Module.Pi
 import Mathlib.Algebra.Module.Prod
@@ -487,11 +488,11 @@ open LinearMap
 variable {M₂₁ M₂₂ : Type*} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂]
   [AddCommMonoid M₂₁] [AddCommMonoid M₂₂] [Module R M₁] [Module R M₂] [Module R M₂₁] [Module R M₂₂]
 
-/-- A linear isomorphism between the domains and codomains of two spaces of linear maps gives a
+/-- A linear isomorphism between the domains and codomains of two spaces of linear maps gives an
 additive isomorphism between the two function spaces.
 
 See also `LinearEquiv.arrowCongr` for the linear version of this isomorphism. -/
-def arrowCongrAddEquiv (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : M₂₁ ≃ₗ[R] M₂₂) :
+@[simps] def arrowCongrAddEquiv (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : M₂₁ ≃ₗ[R] M₂₂) :
     (M₁ →ₗ[R] M₂₁) ≃+ (M₂ →ₗ[R] M₂₂) where
   toFun f := e₂.comp (f.comp e₁.symm.toLinearMap)
   invFun f := e₂.symm.comp (f.comp e₁.toLinearMap)
@@ -505,6 +506,13 @@ def arrowCongrAddEquiv (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : M₂₁ ≃ₗ[R] M
     ext x
     simp only [map_add, add_apply, Function.comp_apply, coe_comp, coe_coe]
 
+/-- A linear isomorphism between the domains an codomains of two spaces of linear maps gives a
+linear isomorphism with respect to an action on the domains. -/
+@[simps] def domMulActCongrRight [Semiring S] [Module S M₁] [SMulCommClass R S M₁]
+    (e₂ : M₂₁ ≃ₗ[R] M₂₂) : (M₁ →ₗ[R] M₂₁) ≃ₗ[Sᵈᵐᵃ] (M₁ →ₗ[R] M₂₂) where
+  __ := arrowCongrAddEquiv (.refl ..) e₂
+  map_smul' := DomMulAct.mk.forall_congr_right.mp fun _ _ ↦ by ext; simp
+
 /-- If `M` and `M₂` are linearly isomorphic then the endomorphism rings of `M` and `M₂`
 are isomorphic.
 

Mathlib/Algebra/Module/LinearMap/Defs.lean

@@ -800,6 +800,15 @@ instance uniqueOfLeft [Subsingleton M] : Unique (M →ₛₗ[σ₁₂] M₂) :=
 instance uniqueOfRight [Subsingleton M₂] : Unique (M →ₛₗ[σ₁₂] M₂) :=
   coe_injective.unique
 
+theorem ne_zero_of_injective [Nontrivial M] {f : M →ₛₗ[σ₁₂] M₂} (hf : Injective f) : f ≠ 0 :=
+  have ⟨x, ne⟩ := exists_ne (0 : M)
+  fun h ↦ hf.ne ne <| by simp [h]
+
+theorem ne_zero_of_surjective [Nontrivial M₂] {f : M →ₛₗ[σ₁₂] M₂} (hf : Surjective f) : f ≠ 0 := by
+  have ⟨y, ne⟩ := exists_ne (0 : M₂)
+  obtain ⟨x, rfl⟩ := hf y
+  exact fun h ↦ ne congr($h x)
+
 /-- The sum of two linear maps is linear. -/
 instance : Add (M →ₛₗ[σ₁₂] M₂) :=
   ⟨fun f g ↦

Mathlib/Algebra/Module/Submodule/Ker.lean

@@ -72,6 +72,10 @@ theorem map_coe_ker (f : F) (x : ker f) : f x = 0 :=
 theorem ker_toAddSubmonoid (f : M →ₛₗ[τ₁₂] M₂) : f.ker.toAddSubmonoid = (AddMonoidHom.mker f) :=
   rfl
 
+theorem le_ker_iff_comp_subtype_eq_zero {N : Submodule R M} {f : M →ₛₗ[τ₁₂] M₂} :
+    N ≤ ker f ↔ f ∘ₛₗ N.subtype = 0 := by
+  rw [SetLike.le_def, LinearMap.ext_iff, Subtype.forall]; rfl
+
 theorem comp_ker_subtype (f : M →ₛₗ[τ₁₂] M₂) : f.comp f.ker.subtype = 0 :=
   LinearMap.ext fun x => mem_ker.1 x.2
 
@@ -126,6 +130,12 @@ theorem ker_zero : ker (0 : M →ₛₗ[τ₁₂] M₂) = ⊤ :=
 theorem ker_eq_top {f : M →ₛₗ[τ₁₂] M₂} : ker f = ⊤ ↔ f = 0 :=
   ⟨fun h => ext fun _ => mem_ker.1 <| h.symm ▸ trivial, fun h => h.symm ▸ ker_zero⟩
 
+theorem exists_ne_zero_of_sSup_eq_top {f : M →ₛₗ[τ₁₂] M₂} (h : f ≠ 0) (s : Set (Submodule R M))
+    (hs : sSup s = ⊤): ∃ m ∈ s, f ∘ₛₗ m.subtype ≠ 0 := by
+  contrapose! h
+  simp_rw [← ker_eq_top, eq_top_iff, ← hs, sSup_le_iff, le_ker_iff_comp_subtype_eq_zero]
+  exact h
+
 @[simp]
 theorem _root_.AddMonoidHom.coe_toIntLinearMap_ker {M M₂ : Type*} [AddCommGroup M] [AddCommGroup M₂]
     (f : M →+ M₂) : LinearMap.ker f.toIntLinearMap = AddSubgroup.toIntSubmodule f.ker := rfl

Mathlib/GroupTheory/GroupAction/DomAct/Basic.lean

@@ -7,7 +7,7 @@ import Mathlib.Algebra.Group.Action.Basic
 import Mathlib.Algebra.Group.Opposite
 import Mathlib.Algebra.Group.Pi.Lemmas
 import Mathlib.Algebra.GroupWithZero.Action.Defs
-import Mathlib.Algebra.Ring.Defs
+import Mathlib.Algebra.Field.Defs
 
 /-!
 # Type tags for right action on the domain of a function
@@ -112,8 +112,8 @@ run_cmd
     `RightCancelSemigroup, `MulOneClass, `Monoid, `CommMonoid, `LeftCancelMonoid,
     `RightCancelMonoid, `CancelMonoid, `CancelCommMonoid, `InvolutiveInv, `DivInvMonoid,
     `InvOneClass, `DivInvOneMonoid, `DivisionMonoid, `DivisionCommMonoid, `Group,
-    `CommGroup, `NonAssocSemiring, `NonUnitalSemiring, `Semiring,
-    `Ring, `CommRing].map Lean.mkIdent do
+    `CommGroup, `NonAssocSemiring, `NonUnitalSemiring, `Semiring, `Ring, `CommSemiring, `CommRing,
+    `Semifield, `Field, `DivisionSemiring, `DivisionRing].map Lean.mkIdent do
   Lean.Elab.Command.elabCommand (← `(
     @[to_additive] instance [$n Mᵐᵒᵖ] : $n Mᵈᵐᵃ := ‹_›
   ))

Mathlib/LinearAlgebra/Projection.lean

@@ -148,6 +148,10 @@ theorem linearProjOfIsCompl_apply_left (h : IsCompl p q) (x : p) :
 theorem linearProjOfIsCompl_range (h : IsCompl p q) : range (linearProjOfIsCompl p q h) = ⊤ :=
   range_eq_of_proj (linearProjOfIsCompl_apply_left h)
 
+theorem linearProjOfIsCompl_surjective (h : IsCompl p q) :
+    Function.Surjective (linearProjOfIsCompl p q h) :=
+  range_eq_top.mp (linearProjOfIsCompl_range h)
+
 @[simp]
 theorem linearProjOfIsCompl_apply_eq_zero_iff (h : IsCompl p q) {x : E} :
     linearProjOfIsCompl p q h x = 0 ↔ x ∈ q := by simp [linearProjOfIsCompl]

Mathlib/LinearAlgebra/Span/Basic.lean

@@ -393,6 +393,26 @@ lemma _root_.LinearMap.BilinMap.apply_apply_mem_of_mem_span {R M N P : Type*} [C
   | smul_left t u v hu hv huv => simpa using Submodule.smul_mem _ _ huv
   | smul_right t u v hu hv huv => simpa using Submodule.smul_mem _ _ huv
 
+@[simp]
+lemma biSup_comap_subtype_eq_top {ι : Type*} (s : Set ι) (p : ι → Submodule R M) :
+    ⨆ i ∈ s, (p i).comap (⨆ i ∈ s, p i).subtype = ⊤ := by
+  refine eq_top_iff.mpr fun ⟨x, hx⟩ _ ↦ ?_
+  suffices x ∈ (⨆ i ∈ s, (p i).comap (⨆ i ∈ s, p i).subtype).map (⨆ i ∈ s, (p i)).subtype by
+    obtain ⟨y, hy, rfl⟩ := Submodule.mem_map.mp this
+    exact hy
+  suffices ∀ i ∈ s, (comap (⨆ i ∈ s, p i).subtype (p i)).map (⨆ i ∈ s, p i).subtype = p i by
+    simpa only [map_iSup, biSup_congr this]
+  intro i hi
+  rw [map_comap_eq, range_subtype, inf_eq_right]
+  exact le_biSup p hi
+
+theorem _root_.LinearMap.exists_ne_zero_of_sSup_eq {N : Submodule R M} {f : N →ₛₗ[σ₁₂] M₂}
+    (h : f ≠ 0) (s : Set (Submodule R M)) (hs : sSup s = N):
+    ∃ m, ∃ h : m ∈ s, f ∘ₛₗ inclusion ((le_sSup h).trans_eq hs) ≠ 0 :=
+  have ⟨_, ⟨m, hm, rfl⟩, ne⟩ := LinearMap.exists_ne_zero_of_sSup_eq_top h (comap N.subtype '' s) <|
+    by rw [sSup_eq_iSup] at hs; rw [sSup_image, ← hs, biSup_comap_subtype_eq_top]
+  ⟨m, hm, fun eq ↦ ne (LinearMap.ext fun x ↦ congr($eq ⟨x, x.2⟩))⟩
+
 end AddCommMonoid
 
 section AddCommGroup
@@ -500,19 +520,6 @@ lemma _root_.LinearMap.range_domRestrict_eq_range_iff {f : M →ₛₗ[τ₁₂]
   rw [← hf]
   exact LinearMap.range_domRestrict_eq_range_iff
 
-@[simp]
-lemma biSup_comap_subtype_eq_top {ι : Type*} (s : Set ι) (p : ι → Submodule R M) :
-    ⨆ i ∈ s, (p i).comap (⨆ i ∈ s, p i).subtype = ⊤ := by
-  refine eq_top_iff.mpr fun ⟨x, hx⟩ _ ↦ ?_
-  suffices x ∈ (⨆ i ∈ s, (p i).comap (⨆ i ∈ s, p i).subtype).map (⨆ i ∈ s, (p i)).subtype by
-    obtain ⟨y, hy, rfl⟩ := Submodule.mem_map.mp this
-    exact hy
-  suffices ∀ i ∈ s, (comap (⨆ i ∈ s, p i).subtype (p i)).map (⨆ i ∈ s, p i).subtype = p i by
-    simpa only [map_iSup, biSup_congr this]
-  intro i hi
-  rw [map_comap_eq, range_subtype, inf_eq_right]
-  exact le_biSup p hi
-
 lemma biSup_comap_eq_top_of_surjective {ι : Type*} (s : Set ι) (hs : s.Nonempty)
     (p : ι → Submodule R₂ M₂) (hp : ⨆ i ∈ s, p i = ⊤)
     (f : M →ₛₗ[τ₁₂] M₂) (hf : Surjective f) :
@@ -524,7 +531,7 @@ lemma biSup_comap_eq_top_of_surjective {ι : Type*} (s : Set ι) (hs : s.Nonempt
   rw [← comap_map_eq, map_iSup_comap_of_sujective hf, hp, comap_top]
 
 lemma biSup_comap_eq_top_of_range_eq_biSup
-    {R R₂ : Type*} [Ring R] [Ring R₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂]
+    {R R₂ : Type*} [Semiring R] [Ring R₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂]
     [Module R M] [Module R₂ M₂] {ι : Type*} (s : Set ι) (hs : s.Nonempty)
     (p : ι → Submodule R₂ M₂) (f : M →ₛₗ[τ₁₂] M₂) (hf : LinearMap.range f = ⨆ i ∈ s, p i) :
     ⨆ i ∈ s, (p i).comap f = ⊤ := by

Mathlib/Logic/Equiv/Defs.lean

@@ -194,6 +194,12 @@ instance permUnique [Subsingleton α] : Unique (Perm α) :=
 theorem Perm.subsingleton_eq_refl [Subsingleton α] (e : Perm α) : e = Equiv.refl α :=
   Subsingleton.elim _ _
 
+protected theorem nontrivial {α β} (e : α ≃ β) [Nontrivial β] : Nontrivial α :=
+  e.surjective.nontrivial
+
+theorem nontrivial_congr {α β} (e : α ≃ β) : Nontrivial α ↔ Nontrivial β :=
+  ⟨fun _ ↦ e.symm.nontrivial, fun _ ↦ e.nontrivial⟩
+
 /-- Transfer `DecidableEq` across an equivalence. -/
 protected def decidableEq (e : α ≃ β) [DecidableEq β] : DecidableEq α :=
   e.injective.decidableEq

Mathlib/Order/Atoms.lean

@@ -698,10 +698,18 @@ protected def IsSimpleOrder.linearOrder [DecidableEq α] : LinearOrder α :=
 theorem isAtom_top : IsAtom (⊤ : α) :=
   ⟨top_ne_bot, fun a ha => Or.resolve_right (eq_bot_or_eq_top a) (ne_of_lt ha)⟩
 
+@[simp]
+theorem isAtom_iff_eq_top {a : α} : IsAtom a ↔ a = ⊤ :=
+  ⟨fun h ↦ (eq_bot_or_eq_top a).resolve_left h.1, (· ▸ isAtom_top)⟩
+
 @[simp]
 theorem isCoatom_bot : IsCoatom (⊥ : α) :=
   isAtom_dual_iff_isCoatom.1 isAtom_top
 
+@[simp]
+theorem isCoatom_iff_eq_bot {a : α} : IsCoatom a ↔ a = ⊥ :=
+  ⟨fun h ↦ (eq_bot_or_eq_top a).resolve_right h.1, (· ▸ isCoatom_bot)⟩
+
 theorem bot_covBy_top : (⊥ : α) ⋖ ⊤ :=
   isAtom_top.bot_covBy
 

Mathlib/RingTheory/Congruence/Basic.lean

@@ -187,6 +187,17 @@ instance [Nontrivial R] : Nontrivial (RingCon R) where
     let ⟨x, y, ne⟩ := exists_pair_ne R
     ⟨⊥, ⊤, ne_of_apply_ne (· x y) <| by simp [ne]⟩
 
+instance [Subsingleton R] : Subsingleton (RingCon R) where
+  allEq c c' := ext fun r r' ↦ by simp_rw [Subsingleton.elim r' r, c.refl, c'.refl]
+
+theorem nontrivial_iff : Nontrivial (RingCon R) ↔ Nontrivial R := by
+  cases subsingleton_or_nontrivial R
+  on_goal 1 => simp_rw [← not_subsingleton_iff_nontrivial, not_iff_not]
+  all_goals exact iff_of_true inferInstance ‹_›
+
+theorem subsingleton_iff : Subsingleton (RingCon R) ↔ Subsingleton R := by
+  simp_rw [← not_nontrivial_iff_subsingleton, nontrivial_iff]
+
 /-- The inductively defined smallest congruence relation containing a binary relation `r` equals
     the infimum of the set of congruence relations containing `r`. -/
 theorem ringConGen_eq (r : R → R → Prop) :

Mathlib/RingTheory/Ideal/Defs.lean

@@ -43,7 +43,7 @@ namespace Ideal
 variable [Semiring α] (I : Ideal α) {a b : α}
 
 /-- A left ideal `I : Ideal R` is two-sided if it is also a right ideal. -/
-class IsTwoSided : Prop where
+@[mk_iff] class IsTwoSided : Prop where
   mul_mem_of_left {a : α} (b : α) : a ∈ I → a * b ∈ I
 
 protected theorem zero_mem : (0 : α) ∈ I :=

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.divisionRing
     [DecidableEq (Module.End R M)] [IsSimpleModule R M] : DivisionRing (Module.End R M) where