Basic.lean

/-
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.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
import Mathlib.Order.Atoms.Finite
import Mathlib.Order.CompactlyGenerated.Intervals
import Mathlib.Order.JordanHolder
import Mathlib.RingTheory.Ideal.Colon
import Mathlib.RingTheory.Noetherian.Defs

/-!
# Simple Modules

## Main Definitions
  * `IsSimpleModule` indicates that a module has no proper submodules
  (the only submodules are `⊥` and `⊤`).
  * `IsSemisimpleModule` indicates that every submodule has a complement, or equivalently,
    the module is a direct sum of simple modules.
  * A `DivisionRing` structure on the endomorphism ring of a simple module.

## Main Results
  * Schur's Lemma: `bijective_or_eq_zero` shows that a linear map between simple modules
    is either bijective or 0, leading to a `DivisionRing` structure on the endomorphism ring.
  * `isSimpleModule_iff_quot_maximal`:
    a module is simple iff it's isomorphic to the quotient of the ring by a maximal left ideal.
  * `sSup_simples_eq_top_iff_isSemisimpleModule`:
    a module is semisimple iff it is generated by its simple submodules.
  * `IsSemisimpleModule.annihilator_isRadical`:
    the annihilator of a semisimple module over a commutative ring is a radical ideal.
  * `IsSemisimpleModule.submodule`, `IsSemisimpleModule.quotient`:
    any submodule or quotient module of a semisimple module is semisimple.
  * `isSemisimpleModule_of_isSemisimpleModule_submodule`:
    a module generated by semisimple submodules is itself semisimple.
  * `IsSemisimpleRing.isSemisimpleModule`: every module over a semisimple ring is semisimple.
  * `instIsSemisimpleRingForAllRing`: a finite product of semisimple rings is semisimple.
  * `RingHom.isSemisimpleRing_of_surjective`: any quotient of a semisimple ring is semisimple.

## TODO
  * Artin-Wedderburn Theory
  * Unify with the work on Schur's Lemma in a category theory context

-/


variable {ι : Type*} (R S : Type*) [Ring R] [Ring S] (M : Type*) [AddCommGroup M] [Module R M]

/-- A module is simple when it has only two submodules, `⊥` and `⊤`. -/
abbrev IsSimpleModule :=
  IsSimpleOrder (Submodule R M)

/-- A module is semisimple when every submodule has a complement, or equivalently, the module
  is a direct sum of simple modules. -/
abbrev IsSemisimpleModule :=
  ComplementedLattice (Submodule R M)

/-- A ring is semisimple if it is semisimple as a module over itself. -/
abbrev IsSemisimpleRing := IsSemisimpleModule R R

variable {R S} in
theorem RingEquiv.isSemisimpleRing (e : R ≃+* S) [IsSemisimpleRing R] : IsSemisimpleRing S :=
  (Submodule.orderIsoMapComap e.toSemilinearEquiv).complementedLattice

variable {R S} in
theorem RingEquiv.isSemisimpleRing_iff (e : R ≃+* S) : IsSemisimpleRing R ↔ IsSemisimpleRing S :=
  ⟨fun _ ↦ e.isSemisimpleRing, fun _ ↦ e.symm.isSemisimpleRing⟩

theorem IsSimpleModule.nontrivial [IsSimpleModule R M] : Nontrivial M :=
  ⟨⟨0, by
      have h : (⊥ : Submodule R M) ≠ ⊤ := bot_ne_top
      contrapose! h
      ext x
      simp [Submodule.mem_bot, Submodule.mem_top, h x]⟩⟩

variable {m : Submodule R M} {N : Type*} [AddCommGroup N] {R S M}

theorem LinearMap.isSimpleModule_iff_of_bijective [Module S N] {σ : R →+* S} [RingHomSurjective σ]
    (l : M →ₛₗ[σ] N) (hl : Function.Bijective l) : IsSimpleModule R M ↔ IsSimpleModule S N :=
  (Submodule.orderIsoMapComapOfBijective l hl).isSimpleOrder_iff

variable [Module R N]

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]
  exact m.mapIic.isSimpleOrder_iff

theorem isSimpleModule_iff_isCoatom : IsSimpleModule R (M ⧸ m) ↔ IsCoatom m := by
  rw [← Set.isSimpleOrder_Ici_iff_isCoatom]
  apply OrderIso.isSimpleOrder_iff
  exact Submodule.comapMkQRelIso m

theorem covBy_iff_quot_is_simple {A B : Submodule R M} (hAB : A ≤ B) :
    A ⋖ B ↔ IsSimpleModule R (B ⧸ Submodule.comap B.subtype A) := by
  set f : Submodule R B ≃o Set.Iic B := B.mapIic with hf
  rw [covBy_iff_coatom_Iic hAB, isSimpleModule_iff_isCoatom, ← OrderIso.isCoatom_iff f, hf]
  simp [-OrderIso.isCoatom_iff, Submodule.map_comap_subtype, inf_eq_right.2 hAB]

namespace IsSimpleModule

@[simp]
theorem isAtom [IsSimpleModule R m] : IsAtom m :=
  isSimpleModule_iff_isAtom.1 ‹_›

variable [IsSimpleModule R M] (R)
open LinearMap

theorem span_singleton_eq_top {m : M} (hm : m ≠ 0) : Submodule.span R {m} = ⊤ :=
  (eq_bot_or_eq_top _).resolve_left fun h ↦ hm (h.le <| Submodule.mem_span_singleton_self m)

instance (S : Submodule R M) : S.IsPrincipal where
  principal := by
    obtain rfl | rfl := eq_bot_or_eq_top S
    · exact ⟨0, Submodule.span_zero.symm⟩
    have := IsSimpleModule.nontrivial R M
    have ⟨m, hm⟩ := exists_ne (0 : M)
    exact ⟨m, (span_singleton_eq_top R hm).symm⟩

theorem toSpanSingleton_surjective {m : M} (hm : m ≠ 0) :
    Function.Surjective (toSpanSingleton R M m) := by
  rw [← range_eq_top, ← span_singleton_eq_range, span_singleton_eq_top R hm]

theorem ker_toSpanSingleton_isMaximal {m : M} (hm : m ≠ 0) :
    Ideal.IsMaximal (ker (toSpanSingleton R M m)) := by
  rw [Ideal.isMaximal_def, ← isSimpleModule_iff_isCoatom]
  exact congr (quotKerEquivOfSurjective _ <| toSpanSingleton_surjective R hm)

instance : IsNoetherian R M := isNoetherian_iff'.mpr inferInstance

end IsSimpleModule

open IsSimpleModule in
/-- A module is simple iff it's isomorphic to the quotient of the ring by a maximal left ideal
(not necessarily unique if the ring is not commutative). -/
theorem isSimpleModule_iff_quot_maximal :
    IsSimpleModule R M ↔ ∃ I : Ideal R, I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I) := by
  refine ⟨fun h ↦ ?_, fun ⟨I, ⟨coatom⟩, ⟨equiv⟩⟩ ↦ ?_⟩
  · have := IsSimpleModule.nontrivial R M
    have ⟨m, hm⟩ := exists_ne (0 : M)
    exact ⟨_, ker_toSpanSingleton_isMaximal R hm,
      ⟨(LinearMap.quotKerEquivOfSurjective _ <| toSpanSingleton_surjective R hm).symm⟩⟩
  · convert congr equiv; rwa [isSimpleModule_iff_isCoatom]

/-- In general, the annihilator of a simple module is called a primitive ideal, and it is
always a two-sided prime ideal, but mathlib's `Ideal.IsPrime` is not the correct definition
for noncommutative rings. -/
theorem IsSimpleModule.annihilator_isMaximal {R} [CommRing R] [Module R M]
    [simple : IsSimpleModule R M] : (Module.annihilator R M).IsMaximal := by
  have ⟨I, max, ⟨e⟩⟩ := isSimpleModule_iff_quot_maximal.mp simple
  rwa [e.annihilator_eq, I.annihilator_quotient]

theorem isSimpleModule_iff_toSpanSingleton_surjective : IsSimpleModule R M ↔
    Nontrivial M ∧ ∀ x : M, x ≠ 0 → Function.Surjective (LinearMap.toSpanSingleton R M x) :=
  ⟨fun h ↦ ⟨h.nontrivial, fun _ ↦ h.toSpanSingleton_surjective⟩, fun ⟨_, h⟩ ↦
    ⟨fun m ↦ or_iff_not_imp_left.mpr fun ne_bot ↦
      have ⟨x, hxm, hx0⟩ := m.ne_bot_iff.mp ne_bot
      top_unique <| fun z _ ↦ by obtain ⟨y, rfl⟩ := h x hx0 z; exact m.smul_mem _ hxm⟩⟩

/-- A ring is a simple module over itself iff it is a division ring. -/
theorem isSimpleModule_self_iff_isUnit :
    IsSimpleModule R R ↔ Nontrivial R ∧ ∀ x : R, x ≠ 0 → IsUnit x :=
  isSimpleModule_iff_toSpanSingleton_surjective.trans <| and_congr_right fun _ ↦ by
    refine ⟨fun h x hx ↦ ?_, fun h x hx ↦ (h x hx).unit.mulRight_bijective.surjective⟩
    obtain ⟨y, hyx : y * x = 1⟩ := h x hx 1
    have hy : y ≠ 0 := left_ne_zero_of_mul (hyx.symm ▸ one_ne_zero)
    obtain ⟨z, hzy : z * y = 1⟩ := h y hy 1
    exact ⟨⟨x, y, left_inv_eq_right_inv hzy hyx ▸ hzy, hyx⟩, rfl⟩

theorem IsSemisimpleModule.of_sSup_simples_eq_top
    (h : sSup { m : Submodule R M | IsSimpleModule R m } = ⊤) : IsSemisimpleModule R M :=
  complementedLattice_of_sSup_atoms_eq_top (by simp_rw [← h, isSimpleModule_iff_isAtom])

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 _

theorem sSup_simples_le (N : Submodule R M) :
    sSup { m : Submodule R M | IsSimpleModule R m ∧ m ≤ N } = N := by
  simpa only [isSimpleModule_iff_isAtom] using sSup_atoms_le_eq _

variable (R M)

theorem exists_simple_submodule [Nontrivial M] : ∃ m : Submodule R M, IsSimpleModule R m := by
  simpa only [isSimpleModule_iff_isAtom] using IsAtomic.exists_atom _

theorem sSup_simples_eq_top : sSup { m : Submodule R M | IsSimpleModule R m } = ⊤ := by
  simpa only [isSimpleModule_iff_isAtom] using sSup_atoms_eq_top

theorem exists_sSupIndep_sSup_simples_eq_top :
    ∃ s : Set (Submodule R M), sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R m := by
  have := sSup_simples_eq_top R M
  simp_rw [isSimpleModule_iff_isAtom] at this ⊢
  exact exists_sSupIndep_of_sSup_atoms_eq_top this

@[deprecated (since := "2024-11-24")]
alias exists_setIndependent_sSup_simples_eq_top := exists_sSupIndep_sSup_simples_eq_top

/-- The annihilator of a semisimple module over a commutative ring is a radical ideal. -/
theorem annihilator_isRadical (R) [CommRing R] [Module R M] [IsSemisimpleModule R M] :
    (Module.annihilator R M).IsRadical := by
  rw [← Submodule.annihilator_top, ← sSup_simples_eq_top, sSup_eq_iSup', Submodule.annihilator_iSup]
  exact Ideal.isRadical_iInf _ fun i ↦ (i.2.annihilator_isMaximal).isPrime.isRadical

instance submodule {m : Submodule R M} : IsSemisimpleModule R m :=
  m.mapIic.complementedLattice_iff.2 IsModularLattice.complementedLattice_Iic

variable {R M}
open LinearMap

theorem congr (e : N ≃ₗ[R] M) : IsSemisimpleModule R N :=
  (Submodule.orderIsoMapComap e.symm).complementedLattice

theorem of_injective (f : N →ₗ[R] M) (hf : Function.Injective f) : IsSemisimpleModule R N :=
  congr (Submodule.topEquiv.symm.trans <| Submodule.equivMapOfInjective f hf _)

instance quotient : IsSemisimpleModule R (M ⧸ m) :=
  have ⟨P, compl⟩ := exists_isCompl m
  .congr (m.quotientEquivOfIsCompl P compl)

instance (priority := low) [Module.Finite R M] : IsNoetherian R M where
  noetherian m := have ⟨P, compl⟩ := exists_isCompl m
    Module.Finite.iff_fg.mp (Module.Finite.equiv <| P.quotientEquivOfIsCompl m compl.symm)

-- does not work as an instance, not sure why
protected theorem range (f : M →ₗ[R] N) : IsSemisimpleModule R (range f) :=
  congr (quotKerEquivRange _).symm

theorem of_surjective (f : M →ₗ[R] N) (hf : Function.Surjective f) : IsSemisimpleModule R N :=
  congr (f.quotKerEquivOfSurjective hf).symm

section

variable {M' : Type*} [AddCommGroup M'] [Module R M'] {N'} [AddCommGroup N'] [Module S N']
  {σ : R →+* S} (l : M' →ₛₗ[σ] N')

theorem _root_.LinearMap.isSemisimpleModule_iff_of_bijective
    [RingHomSurjective σ] (hl : Function.Bijective l) :
    IsSemisimpleModule R M' ↔ IsSemisimpleModule S N' :=
  (Submodule.orderIsoMapComapOfBijective l hl).complementedLattice_iff

-- TODO: generalize Submodule.equivMapOfInjective from InvPair to RingHomSurjective
proof_wanted _root_.LinearMap.isSemisimpleModule_of_injective (_ : Function.Injective l)
    [IsSemisimpleModule S N'] : IsSemisimpleModule R M'

--TODO: generalize LinearMap.quotKerEquivOfSurjective to SemilinearMaps + RingHomSurjective
proof_wanted _root_.LinearMap.isSemisimpleModule_of_surjective (_ : Function.Surjective l)
    [IsSemisimpleModule R M'] : IsSemisimpleModule S N'

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 :=
  ⟨.of_sSup_simples_eq_top, fun _ ↦ IsSemisimpleModule.sSup_simples_eq_top _ _⟩

/-- A module generated by semisimple submodules is itself semisimple. -/
lemma isSemisimpleModule_of_isSemisimpleModule_submodule {s : Set ι} {p : ι → Submodule R M}
    (hp : ∀ i ∈ s, IsSemisimpleModule R (p i)) (hp' : ⨆ i ∈ s, p i = ⊤) :
    IsSemisimpleModule R M := by
  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
  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 = ⊤) :
    IsSemisimpleModule R M :=
  isSemisimpleModule_of_isSemisimpleModule_submodule (s := Set.univ) (fun i _ ↦ hp i) (by simpa)

instance {ι} (M : ι → Type*) [∀ i, AddCommGroup (M i)] [∀ i, Module R (M i)]
    [∀ i, IsSemisimpleModule R (M i)] : IsSemisimpleModule R (Π₀ i, M i) := by
  classical
  exact isSemisimpleModule_of_isSemisimpleModule_submodule'
    (fun _ ↦ .range _) DFinsupp.iSup_range_lsingle

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
  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
  classical
  exact isSemisimpleModule_of_isSemisimpleModule_submodule' (p := (range <| single _ _ ·))
    (fun i ↦ .range _) (by simp_rw [range_eq_map, Submodule.iSup_map_single, Submodule.pi_top])

theorem IsSemisimpleModule.sup {p q : Submodule R M}
    (_ : IsSemisimpleModule R p) (_ : IsSemisimpleModule R q) :
    IsSemisimpleModule R ↥(p ⊔ q) := by
  let f : Bool → Submodule R M := Bool.rec q p
  rw [show p ⊔ q = ⨆ i ∈ Set.univ, f i by rw [iSup_univ, iSup_bool_eq]]
  exact isSemisimpleModule_biSup_of_isSemisimpleModule_submodule (by rintro (_|_) _ <;> assumption)

instance IsSemisimpleRing.isSemisimpleModule [IsSemisimpleRing R] : IsSemisimpleModule R M :=
  have : IsSemisimpleModule R (M →₀ R) := isSemisimpleModule_of_isSemisimpleModule_submodule'
    (fun _ ↦ .congr (LinearMap.quotKerEquivRange _).symm) Finsupp.iSup_lsingle_range
  .congr (LinearMap.quotKerEquivOfSurjective _ <| Finsupp.linearCombination_id_surjective R M).symm

instance IsSemisimpleModule.isCoatomic_submodule [IsSemisimpleModule R M] :
    IsCoatomic (Submodule R M) :=
  isCoatomic_of_isAtomic_of_complementedLattice_of_isModular

open LinearMap in
/-- A finite product of semisimple rings is semisimple. -/
instance {ι} [Finite ι] (R : ι → Type*) [Π i, Ring (R i)] [∀ i, IsSemisimpleRing (R i)] :
    IsSemisimpleRing (Π i, R i) := by
  letI (i) : Module (Π i, R i) (R i) := Module.compHom _ (Pi.evalRingHom R i)
  let e (i) : R i →ₛₗ[Pi.evalRingHom R i] R i :=
    { AddMonoidHom.id (R i) with map_smul' := fun _ _ ↦ rfl }
  have (i) : IsSemisimpleModule (Π i, R i) (R i) :=
    ((e i).isSemisimpleModule_iff_of_bijective Function.bijective_id).mpr inferInstance
  infer_instance

/-- A binary product of semisimple rings is semisimple. -/
instance [hR : IsSemisimpleRing R] [hS : IsSemisimpleRing S] : IsSemisimpleRing (R × S) := by
  letI : Module (R × S) R := Module.compHom _ (.fst R S)
  letI : Module (R × S) S := Module.compHom _ (.snd R S)
  -- e₁, e₂ got falsely flagged by the unused argument linter
  let _e₁ : R →ₛₗ[.fst R S] R := { AddMonoidHom.id R with map_smul' := fun _ _ ↦ rfl }
  let _e₂ : S →ₛₗ[.snd R S] S := { AddMonoidHom.id S with map_smul' := fun _ _ ↦ rfl }
  rw [IsSemisimpleRing, ← _e₁.isSemisimpleModule_iff_of_bijective Function.bijective_id] at hR
  rw [IsSemisimpleRing, ← _e₂.isSemisimpleModule_iff_of_bijective Function.bijective_id] at hS
  rw [IsSemisimpleRing, ← Submodule.topEquiv.isSemisimpleModule_iff_of_bijective
    (LinearEquiv.bijective _), ← LinearMap.sup_range_inl_inr]
  exact .sup (.range _) (.range _)

theorem RingHom.isSemisimpleRing_of_surjective (f : R →+* S) (hf : Function.Surjective f)
    [IsSemisimpleRing R] : IsSemisimpleRing S := by
  letI : Module R S := Module.compHom _ f
  haveI : RingHomSurjective f := ⟨hf⟩
  let e : S →ₛₗ[f] S := { AddMonoidHom.id S with map_smul' := fun _ _ ↦ rfl }
  rw [IsSemisimpleRing, ← e.isSemisimpleModule_iff_of_bijective Function.bijective_id]
  infer_instance

theorem IsSemisimpleRing.ideal_eq_span_idempotent [IsSemisimpleRing R] (I : Ideal R) :
    ∃ e : R, IsIdempotentElem e ∧ I = .span {e} := by
  obtain ⟨J, h⟩ := exists_isCompl I
  obtain ⟨f, idem, rfl⟩ := I.isIdempotentElemEquiv.symm (I.isComplEquivProj ⟨J, h⟩)
  exact ⟨f 1, LinearMap.isIdempotentElem_apply_one_iff.mpr idem, by
    rw [LinearMap.range_eq_map, ← Ideal.span_one, ← Ideal.submodule_span_eq, LinearMap.map_span,
      Set.image_one, Ideal.submodule_span_eq]⟩

instance [IsSemisimpleRing R] : IsPrincipalIdealRing R where
  principal I := have ⟨e, _, he⟩ := IsSemisimpleRing.ideal_eq_span_idempotent I; ⟨e, he⟩

variable (ι R)

proof_wanted IsSemisimpleRing.mulOpposite [IsSemisimpleRing R] : IsSemisimpleRing Rᵐᵒᵖ

proof_wanted IsSemisimpleRing.module_end [IsSemisimpleModule R M] [Module.Finite R M] :
    IsSemisimpleRing (Module.End R M)

proof_wanted IsSemisimpleRing.matrix [Fintype ι] [DecidableEq ι] [IsSemisimpleRing R] :
    IsSemisimpleRing (Matrix ι ι R)

universe u in
/-- The existence part of the Artin–Wedderburn theorem. -/
proof_wanted isSemisimpleRing_iff_pi_matrix_divisionRing {R : Type u} [Ring R] :
    IsSemisimpleRing R ↔
    ∃ (n : ℕ) (S : Fin n → Type u) (d : Fin n → ℕ) (_ : Π i, DivisionRing (S i)),
      Nonempty (R ≃+* Π i, Matrix (Fin (d i)) (Fin (d i)) (S i))

variable {ι R}

namespace LinearMap

theorem injective_or_eq_zero [IsSimpleModule R M] (f : M →ₗ[R] N) :
    Function.Injective f ∨ f = 0 := by
  rw [← ker_eq_bot, ← ker_eq_top]
  apply eq_bot_or_eq_top

theorem injective_of_ne_zero [IsSimpleModule R M] {f : M →ₗ[R] N} (h : f ≠ 0) :
    Function.Injective f :=
  f.injective_or_eq_zero.resolve_right h

theorem surjective_or_eq_zero [IsSimpleModule R N] (f : M →ₗ[R] N) :
    Function.Surjective f ∨ f = 0 := by
  rw [← range_eq_top, ← range_eq_bot, or_comm]
  apply eq_bot_or_eq_top

theorem surjective_of_ne_zero [IsSimpleModule R N] {f : M →ₗ[R] N} (h : f ≠ 0) :
    Function.Surjective f :=
  f.surjective_or_eq_zero.resolve_right h

/-- **Schur's Lemma** for linear maps between (possibly distinct) simple modules -/
theorem bijective_or_eq_zero [IsSimpleModule R M] [IsSimpleModule R N] (f : M →ₗ[R] N) :
    Function.Bijective f ∨ f = 0 :=
  or_iff_not_imp_right.mpr fun h ↦ ⟨injective_of_ne_zero h, surjective_of_ne_zero h⟩

theorem bijective_of_ne_zero [IsSimpleModule R M] [IsSimpleModule R N] {f : M →ₗ[R] N} (h : f ≠ 0) :
    Function.Bijective f :=
  f.bijective_or_eq_zero.resolve_right h

theorem isCoatom_ker_of_surjective [IsSimpleModule R N] {f : M →ₗ[R] N}
    (hf : Function.Surjective f) : IsCoatom (LinearMap.ker f) := by
  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
  __ := Module.End.ring
  inv f := if h : f = 0 then 0 else (LinearEquiv.ofBijective _ <| bijective_of_ne_zero h).symm
  exists_pair_ne := ⟨0, 1, have := IsSimpleModule.nontrivial R M; zero_ne_one⟩
  mul_inv_cancel a a0 := by
    simp_rw [dif_neg a0]; ext
    exact (LinearEquiv.ofBijective _ <| bijective_of_ne_zero a0).right_inv _
  inv_zero := dif_pos rfl
  nnqsmul := _
  nnqsmul_def := fun _ _ => rfl
  qsmul := _
  qsmul_def := fun _ _ => rfl

end LinearMap

-- Porting note: adding a namespace with all the new statements; existing result is not used in ML3
namespace JordanHolderModule

-- Porting note: jordanHolderModule was timing out so outlining the fields

/-- An isomorphism `X₂ / X₁ ∩ X₂ ≅ Y₂ / Y₁ ∩ Y₂` of modules for pairs
`(X₁,X₂) (Y₁,Y₂) : Submodule R M` -/
def Iso (X Y : Submodule R M × Submodule R M) : Prop :=
  Nonempty <| (X.2 ⧸ X.1.comap X.2.subtype) ≃ₗ[R] Y.2 ⧸ Y.1.comap Y.2.subtype

theorem iso_symm {X Y : Submodule R M × Submodule R M} : Iso X Y → Iso Y X :=
  fun ⟨f⟩ => ⟨f.symm⟩

theorem iso_trans {X Y Z : Submodule R M × Submodule R M} : Iso X Y → Iso Y Z → Iso X Z :=
  fun ⟨f⟩ ⟨g⟩ => ⟨f.trans g⟩

@[nolint unusedArguments]
theorem second_iso {X Y : Submodule R M} (_ : X ⋖ X ⊔ Y) :
    Iso (X,X ⊔ Y) (X ⊓ Y,Y) := by
  constructor
  rw [sup_comm, inf_comm]
  dsimp
  exact (LinearMap.quotientInfEquivSupQuotient Y X).symm

instance instJordanHolderLattice : JordanHolderLattice (Submodule R M) where
  IsMaximal := (· ⋖ ·)
  lt_of_isMaximal := CovBy.lt
  sup_eq_of_isMaximal hxz hyz := WCovBy.sup_eq hxz.wcovBy hyz.wcovBy
  isMaximal_inf_left_of_isMaximal_sup := inf_covBy_of_covBy_sup_of_covBy_sup_left
  Iso := Iso
  iso_symm := iso_symm
  iso_trans := iso_trans
  second_iso := second_iso

end JordanHolderModule