doc-next-gen

Mathlib.RingTheory.SimpleModule.Basic

Module docstring

{"# 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

"}

IsSimpleModule abbrev
Full source 
/-- A module is simple when it has only two submodules, `⊥` and `⊤`. -/
abbrev IsSimpleModule :=
  IsSimpleOrder (Submodule R M)
Definition of Simple Module
Informal description
A module $M$ over a ring $R$ is called *simple* if it has exactly two submodules: the zero submodule $\{0\}$ and $M$ itself.
IsSemisimpleModule abbrev
Full source 
/-- 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)
Definition of Semisimple Module
Informal description
A module $M$ over a ring $R$ is called *semisimple* if every submodule of $M$ has a complement (i.e., for every submodule $N \subseteq M$, there exists another submodule $N' \subseteq M$ such that $M = N \oplus N'$), or equivalently, if $M$ is a direct sum of simple submodules (modules with no proper nonzero submodules).
IsSemisimpleRing abbrev
Full source 
/-- A ring is semisimple if it is semisimple as a module over itself. -/
abbrev IsSemisimpleRing := IsSemisimpleModule R R
Semisimple Ring via Semisimple Module Over Itself
Informal description
A ring $R$ is called *semisimple* if it is semisimple as a module over itself, meaning that every left ideal of $R$ has a complement (i.e., $R$ is a direct sum of simple left ideals).
RingEquiv.isSemisimpleRing_iff theorem
(e : R ≃+* S) : IsSemisimpleRing R ↔ IsSemisimpleRing S
Full source 
theorem RingEquiv.isSemisimpleRing_iff (e : R ≃+* S) : IsSemisimpleRingIsSemisimpleRing R ↔ IsSemisimpleRing S :=
  ⟨fun _ ↦ e.isSemisimpleRing, fun _ ↦ e.symm.isSemisimpleRing⟩
Semisimplicity is Preserved Under Ring Isomorphism
Informal description
Let $R$ and $S$ be rings with a ring isomorphism $e \colon R \simeq S$. Then $R$ is a semisimple ring if and only if $S$ is a semisimple ring.
LinearMap.isSimpleModule_iff_of_bijective theorem
[Module S N] {σ : R →+* S} [RingHomSurjective σ] (l : M →ₛₗ[σ] N) (hl : Function.Bijective l) : IsSimpleModule R M ↔ IsSimpleModule S N
Full source 
theorem LinearMap.isSimpleModule_iff_of_bijective [Module S N] {σ : R →+* S} [RingHomSurjective σ]
    (l : M →ₛₗ[σ] N) (hl : Function.Bijective l) : IsSimpleModuleIsSimpleModule R M ↔ IsSimpleModule S N :=
  (Submodule.orderIsoMapComapOfBijective l hl).isSimpleOrder_iff
Bijective Linear Map Preserves Simplicity of Modules
Informal description
Let $R$ and $S$ be rings, and let $M$ be an $R$-module and $N$ an $S$-module. Given a ring homomorphism $\sigma: R \to S$ that is surjective, and a bijective $\sigma$-linear map $l: M \to N$, then $M$ is a simple $R$-module if and only if $N$ is a simple $S$-module.
isSimpleModule_iff_isAtom theorem
: IsSimpleModule R m ↔ IsAtom m
Full source 
theorem isSimpleModule_iff_isAtom : IsSimpleModuleIsSimpleModule R m ↔ IsAtom m := by
  rw [← Set.isSimpleOrder_Iic_iff_isAtom]
  exact m.mapIic.isSimpleOrder_iff
Simple Module Characterization via Atomicity in Submodule Lattice
Informal description
A module $M$ over a ring $R$ is simple if and only if $M$ is an atom in the lattice of submodules of $M$, meaning $M$ is nonzero and there are no proper nonzero submodules strictly contained in $M$.
isSimpleModule_iff_isCoatom theorem
: IsSimpleModule R (M ⧸ m) ↔ IsCoatom m
Full source 
theorem isSimpleModule_iff_isCoatom : IsSimpleModuleIsSimpleModule R (M ⧸ m) ↔ IsCoatom m := by
  rw [← Set.isSimpleOrder_Ici_iff_isCoatom]
  apply OrderIso.isSimpleOrder_iff
  exact Submodule.comapMkQRelIso m
Simple Quotient Module Characterization via Maximal Submodules
Informal description
A quotient module $M/m$ is simple if and only if the submodule $m$ is a coatom in the lattice of submodules of $M$, meaning $m$ is a maximal proper submodule of $M$.
covBy_iff_quot_is_simple theorem
{A B : Submodule R M} (hAB : A ≤ B) : A ⋖ B ↔ IsSimpleModule R (B ⧸ Submodule.comap B.subtype A)
Full source 
theorem covBy_iff_quot_is_simple {A B : Submodule R M} (hAB : A ≤ B) :
    A ⋖ BA ⋖ 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]
Covering Relation in Submodule Lattice via Simple Quotient
Informal description
Let $A$ and $B$ be submodules of a module $M$ over a ring $R$ with $A \leq B$. Then $A$ is covered by $B$ (denoted $A \lessdot B$) if and only if the quotient module $B/(A \cap B)$ is simple.
IsSimpleModule.isAtom theorem
[IsSimpleModule R m] : IsAtom m
Full source 
@[simp]
theorem isAtom [IsSimpleModule R m] : IsAtom m :=
  isSimpleModule_iff_isAtom.1 ‹_›
Simple Modules are Atoms in the Submodule Lattice
Informal description
If $M$ is a simple module over a ring $R$, then $M$ is an atom in the lattice of submodules of $M$, meaning $M$ is nonzero and there are no proper nonzero submodules strictly contained in $M$.
IsSimpleModule.span_singleton_eq_top theorem
{m : M} (hm : m ≠ 0) : Submodule.span R { m } = ⊤
Full source 
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)
Span of Nonzero Element in Simple Module is Entire Module
Informal description
For any nonzero element $m$ in a simple module $M$ over a ring $R$, the submodule generated by $m$ is the entire module $M$, i.e., $\text{span}_R\{m\} = M$.
IsSimpleModule.instIsPrincipal instance
(S : Submodule R M) : S.IsPrincipal
Full source 
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⟩
Submodules of Simple Modules are Principal
Informal description
For any submodule $S$ of a simple module $M$ over a ring $R$, $S$ is a principal submodule, meaning it is generated by a single element.
IsSimpleModule.toSpanSingleton_surjective theorem
{m : M} (hm : m ≠ 0) : Function.Surjective (toSpanSingleton R M m)
Full source 
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]
Surjectivity of Span Singleton Map in Simple Module
Informal description
For any nonzero element $m$ in a simple module $M$ over a ring $R$, the linear map $\text{toSpanSingleton}_R(M, m) : R \to M$ defined by $r \mapsto r \cdot m$ is surjective.
IsSimpleModule.ker_toSpanSingleton_isMaximal theorem
{m : M} (hm : m ≠ 0) : Ideal.IsMaximal (ker (toSpanSingleton R M m))
Full source 
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)
Maximality of Kernel in Simple Module's Span Singleton Map
Informal description
For any nonzero element $m$ in a simple module $M$ over a ring $R$, the kernel of the linear map $\text{toSpanSingleton}_R(M, m) : R \to M$ defined by $r \mapsto r \cdot m$ is a maximal ideal of $R$.
isSimpleModule_iff_quot_maximal theorem
: IsSimpleModule R M ↔ ∃ I : Ideal R, I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I)
Full source 
/-- 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 :
    IsSimpleModuleIsSimpleModule 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]
Simple Module Characterization via Quotient by Maximal Ideal
Informal description
A module $M$ over a ring $R$ is simple if and only if there exists a maximal ideal $I$ of $R$ such that $M$ is isomorphic as an $R$-module to the quotient ring $R/I$.
IsSimpleModule.annihilator_isMaximal theorem
{R} [CommRing R] [Module R M] [simple : IsSimpleModule R M] : (Module.annihilator R M).IsMaximal
Full source 
/-- 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]
Maximality of Annihilator for Simple Modules over Commutative Rings
Informal description
For a commutative ring $R$ and a simple $R$-module $M$, the annihilator of $M$ is a maximal ideal of $R$.
isSimpleModule_iff_toSpanSingleton_surjective theorem
: IsSimpleModule R M ↔ Nontrivial M ∧ ∀ x : M, x ≠ 0 → Function.Surjective (LinearMap.toSpanSingleton R M x)
Full source 
theorem isSimpleModule_iff_toSpanSingleton_surjective : IsSimpleModuleIsSimpleModule 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⟩⟩
Characterization of Simple Modules via Surjective Span Maps
Informal description
A module $M$ over a ring $R$ is simple if and only if $M$ is nontrivial and for every nonzero element $x \in M$, the linear map $R \to M$ defined by $r \mapsto r \cdot x$ is surjective.
isSimpleModule_self_iff_isUnit theorem
: IsSimpleModule R R ↔ Nontrivial R ∧ ∀ x : R, x ≠ 0 → IsUnit x
Full source 
/-- A ring is a simple module over itself iff it is a division ring. -/
theorem isSimpleModule_self_iff_isUnit :
    IsSimpleModuleIsSimpleModule 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⟩
Simple Module Characterization for Division Rings
Informal description
A ring $R$ is a simple module over itself if and only if $R$ is nontrivial and every nonzero element $x \in R$ is a unit (i.e., $R$ is a division ring).
IsSemisimpleModule.of_sSup_simples_eq_top theorem
(h : sSup {m : Submodule R M | IsSimpleModule R m} = ⊤) : IsSemisimpleModule R M
Full source 
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])
Semisimplicity Criterion via Supremum of Simple Submodules
Informal description
Let $M$ be a module over a ring $R$. If the supremum of all simple submodules of $M$ equals the entire module (i.e., $\bigvee \{ N \subseteq M \mid \text{$N$ is simple} \} = M$), then $M$ is a semisimple module.
IsSemisimpleModule.sSup_simples_le theorem
(N : Submodule R M) : sSup {m : Submodule R M | IsSimpleModule R m ∧ m ≤ N} = N
Full source 
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 _
Supremum of Simple Submodules in a Semisimple Module Equals the Submodule
Informal description
For any submodule $N$ of a semisimple module $M$ over a ring $R$, the supremum of all simple submodules of $M$ contained in $N$ is equal to $N$ itself. In other words, $N$ is generated by the simple submodules it contains.
IsSemisimpleModule.exists_simple_submodule theorem
[Nontrivial M] : ∃ m : Submodule R M, IsSimpleModule R m
Full source 
theorem exists_simple_submodule [Nontrivial M] : ∃ m : Submodule R M, IsSimpleModule R m := by
  simpa only [isSimpleModule_iff_isAtom] using IsAtomic.exists_atom _
Existence of Simple Submodule in Nontrivial Module
Informal description
For any nontrivial module $M$ over a ring $R$, there exists a simple submodule $m$ of $M$, i.e., a submodule with no proper nonzero submodules.
IsSemisimpleModule.sSup_simples_eq_top theorem
: sSup {m : Submodule R M | IsSimpleModule R m} = ⊤
Full source 
theorem sSup_simples_eq_top : sSup { m : Submodule R M | IsSimpleModule R m } = ⊤ := by
  simpa only [isSimpleModule_iff_isAtom] using sSup_atoms_eq_top
Semisimple Module is Generated by its Simple Submodules
Informal description
The supremum of all simple submodules of a semisimple module $M$ over a ring $R$ is equal to the top submodule (i.e., $M$ itself). In other words, $M$ is generated by its simple submodules.
IsSemisimpleModule.exists_sSupIndep_sSup_simples_eq_top theorem
: ∃ s : Set (Submodule R M), sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R m
Full source 
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
Decomposition of Semisimple Module into Independent Simple Submodules
Informal description
For a semisimple module $M$ over a ring $R$, there exists a set $s$ of submodules of $M$ such that: 1. The supremum of $s$ is independent (i.e., the submodules in $s$ are pairwise independent), 2. The supremum of $s$ equals the top submodule $M$, 3. Every submodule in $s$ is simple. In other words, $M$ can be decomposed as a direct sum of simple submodules.
IsSemisimpleModule.annihilator_isRadical theorem
(R) [CommRing R] [Module R M] [IsSemisimpleModule R M] : (Module.annihilator R M).IsRadical
Full source 
/-- 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
Annihilator of a Semisimple Module is Radical
Informal description
For a commutative ring $R$ and a semisimple $R$-module $M$, the annihilator $\mathrm{ann}_R(M)$ is a radical ideal of $R$.
IsSemisimpleModule.congr theorem
(e : N ≃ₗ[R] M) : IsSemisimpleModule R N
Full source 
theorem congr (e : N ≃ₗ[R] M) : IsSemisimpleModule R N :=
  (Submodule.orderIsoMapComap e.symm).complementedLattice
Semisimplicity is Preserved under Linear Isomorphism
Informal description
Let $R$ be a ring and let $M$ and $N$ be $R$-modules. If there exists a linear isomorphism $e \colon N \simeq M$ and $M$ is a semisimple $R$-module, then $N$ is also a semisimple $R$-module.
IsSemisimpleModule.of_injective theorem
(f : N →ₗ[R] M) (hf : Function.Injective f) : IsSemisimpleModule R N
Full source 
theorem of_injective (f : N →ₗ[R] M) (hf : Function.Injective f) : IsSemisimpleModule R N :=
  congr (Submodule.topEquiv.symm.trans <| Submodule.equivMapOfInjective f hf _)
Semisimplicity via Injective Linear Maps
Informal description
Let $R$ be a ring and let $M$ and $N$ be $R$-modules. If there exists an injective linear map $f \colon N \to M$ and $M$ is a semisimple $R$-module, then $N$ is also a semisimple $R$-module.
IsSemisimpleModule.quotient instance
: IsSemisimpleModule R (M ⧸ m)
Full source 
instance quotient : IsSemisimpleModule R (M ⧸ m) :=
  have ⟨P, compl⟩ := exists_isCompl m
  .congr (m.quotientEquivOfIsCompl P compl)
Quotients of Semisimple Modules are Semisimple
Informal description
For any semisimple module $M$ over a ring $R$ and any submodule $m$ of $M$, the quotient module $M / m$ is also semisimple.
IsSemisimpleModule.range theorem
(f : M →ₗ[R] N) : IsSemisimpleModule R (range f)
Full source 
protected theorem range (f : M →ₗ[R] N) : IsSemisimpleModule R (range f) :=
  congr (quotKerEquivRange _).symm
Range of a Linear Map from a Semisimple Module is Semisimple
Informal description
For any linear map \( f \colon M \to N \) between modules over a ring \( R \), if \( M \) is a semisimple \( R \)-module, then the range of \( f \) is also a semisimple \( R \)-module.
IsSemisimpleModule.of_surjective theorem
(f : M →ₗ[R] N) (hf : Function.Surjective f) : IsSemisimpleModule R N
Full source 
theorem of_surjective (f : M →ₗ[R] N) (hf : Function.Surjective f) : IsSemisimpleModule R N :=
  congr (f.quotKerEquivOfSurjective hf).symm
Semisimplicity is Preserved under Surjective Linear Maps
Informal description
Let $R$ be a ring and let $M$ and $N$ be $R$-modules. If there exists a surjective linear map $f \colon M \to N$ and $M$ is a semisimple $R$-module, then $N$ is also a semisimple $R$-module.
LinearMap.isSemisimpleModule_iff_of_bijective theorem
[RingHomSurjective σ] (hl : Function.Bijective l) : IsSemisimpleModule R M' ↔ IsSemisimpleModule S N'
Full source 
theorem _root_.LinearMap.isSemisimpleModule_iff_of_bijective
    [RingHomSurjective σ] (hl : Function.Bijective l) :
    IsSemisimpleModuleIsSemisimpleModule R M' ↔ IsSemisimpleModule S N' :=
  (Submodule.orderIsoMapComapOfBijective l hl).complementedLattice_iff
Semisimplicity Invariance Under Bijective Linear Maps: $M'$ semisimple $\leftrightarrow$ $N'$ semisimple
Informal description
Let $R$ and $S$ be rings, and let $M'$ be an $R$-module and $N'$ an $S$-module. Given a bijective linear map $l \colon M' \to N'$ (with respect to a ring homomorphism $\sigma \colon R \to S$ that is surjective), then $M'$ is a semisimple $R$-module if and only if $N'$ is a semisimple $S$-module.
sSup_simples_eq_top_iff_isSemisimpleModule theorem
: sSup {m : Submodule R M | IsSimpleModule R m} = ⊤ ↔ IsSemisimpleModule R M
Full source 
/-- A module is semisimple iff it is generated by its simple submodules. -/
theorem sSup_simples_eq_top_iff_isSemisimpleModule :
    sSupsSup { m : Submodule R M | IsSimpleModule R m } = ⊤ ↔ IsSemisimpleModule R M :=
  ⟨.of_sSup_simples_eq_top, fun _ ↦ IsSemisimpleModule.sSup_simples_eq_top _ _⟩
Semisimplicity Criterion via Simple Submodule Generation
Informal description
A module $M$ over a ring $R$ is semisimple if and only if the supremum of all its simple submodules equals $M$ itself, i.e., $\bigvee \{ N \subseteq M \mid \text{$N$ is simple} \} = M$.
isSemisimpleModule_of_isSemisimpleModule_submodule theorem
{s : Set ι} {p : ι → Submodule R M} (hp : ∀ i ∈ s, IsSemisimpleModule R (p i)) (hp' : ⨆ i ∈ s, p i = ⊤) : IsSemisimpleModule R M
Full source 
/-- 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
Semisimplicity of a Module Generated by Semisimple Submodules
Informal description
Let $M$ be a module over a ring $R$, and let $\{p_i\}_{i \in s}$ be a family of submodules of $M$ indexed by a set $s$. If each $p_i$ is a semisimple module and the supremum of the family $\{p_i\}_{i \in s}$ is the entire module $M$ (i.e., $\bigvee_{i \in s} p_i = M$), then $M$ itself is a semisimple module.
isSemisimpleModule_biSup_of_isSemisimpleModule_submodule theorem
{s : Set ι} {p : ι → Submodule R M} (hp : ∀ i ∈ s, IsSemisimpleModule R (p i)) : IsSemisimpleModule R ↥(⨆ i ∈ s, p i)
Full source 
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₂
Semisimplicity of the Supremum of Semisimple Submodules
Informal description
Let $M$ be a module over a ring $R$, and let $\{p_i\}_{i \in s}$ be a family of submodules of $M$ indexed by a set $s$. If each $p_i$ is a semisimple module, then the supremum $\bigvee_{i \in s} p_i$ is also a semisimple module.
isSemisimpleModule_of_isSemisimpleModule_submodule' theorem
{p : ι → Submodule R M} (hp : ∀ i, IsSemisimpleModule R (p i)) (hp' : ⨆ i, p i = ⊤) : IsSemisimpleModule R M
Full source 
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)
Semisimplicity of a Module Generated by a Family of Semisimple Submodules
Informal description
Let $M$ be a module over a ring $R$ and let $\{p_i\}_{i \in \iota}$ be a family of submodules of $M$. If each $p_i$ is a semisimple module and the supremum of the family $\{p_i\}_{i \in \iota}$ is the entire module $M$ (i.e., $\bigvee_{i \in \iota} p_i = M$), then $M$ itself is a semisimple module.
instIsSemisimpleModuleDFinsupp instance
{ι} (M : ι → Type*) [∀ i, AddCommGroup (M i)] [∀ i, Module R (M i)] [∀ i, IsSemisimpleModule R (M i)] : IsSemisimpleModule R (Π₀ i, M i)
Full source 
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
Direct Sum of Semisimple Modules is Semisimple
Informal description
For any family of semisimple modules $(M_i)_{i \in \iota}$ over a ring $R$, the direct sum $\bigoplus_{i \in \iota} M_i$ is also a semisimple module.
isSemisimpleModule_iff_exists_linearEquiv_dfinsupp theorem
: IsSemisimpleModule R M ↔ ∃ (s : Set (Submodule R M)) (_ : M ≃ₗ[R] Π₀ m : s, m.1), ∀ m : s, IsSimpleModule R m.1
Full source 
theorem isSemisimpleModule_iff_exists_linearEquiv_dfinsupp : IsSemisimpleModuleIsSemisimpleModule 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, ind, sSup, simple⟩ := IsSemisimpleModule.exists_sSupIndep_sSup_simples_eq_top R M
  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
Characterization of Semisimple Modules as Direct Sums of Simple Submodules
Informal description
A module $M$ over a ring $R$ is semisimple if and only if there exists a set $s$ of submodules of $M$ and a linear isomorphism $M \cong \bigoplus_{m \in s} m$ (where $\bigoplus$ denotes the direct sum of modules), such that every submodule $m \in s$ is simple.
instIsSemisimpleModuleForallOfFinite instance
{ι} [Finite ι] (M : ι → Type*) [∀ i, AddCommGroup (M i)] [∀ i, Module R (M i)] [∀ i, IsSemisimpleModule R (M i)] : IsSemisimpleModule R (Π i, M i)
Full source 
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])
Direct Product of Semisimple Modules is Semisimple for Finite Index Sets
Informal description
For any finite index type $\iota$ and a family of $R$-modules $(M_i)_{i \in \iota}$, if each $M_i$ is a semisimple $R$-module, then the direct product $\prod_{i \in \iota} M_i$ is also a semisimple $R$-module.
IsSemisimpleModule.sup theorem
{p q : Submodule R M} (_ : IsSemisimpleModule R p) (_ : IsSemisimpleModule R q) : IsSemisimpleModule R ↥(p ⊔ q)
Full source 
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)
Supremum of Semisimple Submodules is Semisimple
Informal description
Let $M$ be a module over a ring $R$, and let $p$ and $q$ be submodules of $M$. If both $p$ and $q$ are semisimple modules, then their supremum $p \sqcup q$ is also a semisimple module.
IsSemisimpleRing.isSemisimpleModule instance
[IsSemisimpleRing R] : IsSemisimpleModule R M
Full source 
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
Modules over Semisimple Rings are Semisimple
Informal description
Every module $M$ over a semisimple ring $R$ is semisimple.
IsSemisimpleModule.isCoatomic_submodule instance
[IsSemisimpleModule R M] : IsCoatomic (Submodule R M)
Full source 
instance IsSemisimpleModule.isCoatomic_submodule [IsSemisimpleModule R M] :
    IsCoatomic (Submodule R M) :=
  isCoatomic_of_isAtomic_of_complementedLattice_of_isModular
Coatomicity of Submodule Lattice in Semisimple Modules
Informal description
For any semisimple module $M$ over a ring $R$, the lattice of submodules of $M$ is coatomic, meaning that every proper submodule is contained in a maximal submodule.
instIsSemisimpleRingForallOfFinite instance
{ι} [Finite ι] (R : ι → Type*) [Π i, Ring (R i)] [∀ i, IsSemisimpleRing (R i)] : IsSemisimpleRing (Π i, R i)
Full source 
/-- 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
Finite Product of Semisimple Rings is Semisimple
Informal description
For any finite index type $\iota$ and a family of rings $(R_i)_{i \in \iota}$, if each $R_i$ is a semisimple ring, then the direct product $\prod_{i \in \iota} R_i$ is also a semisimple ring.
instIsSemisimpleRingProd instance
[hR : IsSemisimpleRing R] [hS : IsSemisimpleRing S] : IsSemisimpleRing (R × S)
Full source 
/-- 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 _)
Direct Product of Semisimple Rings is Semisimple
Informal description
For any two semisimple rings $R$ and $S$, their direct product $R \times S$ is also a semisimple ring.
RingHom.isSemisimpleRing_of_surjective theorem
(f : R →+* S) (hf : Function.Surjective f) [IsSemisimpleRing R] : IsSemisimpleRing S
Full source 
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
Semisimplicity of Quotient Rings via Surjective Homomorphisms
Informal description
Let $f \colon R \to S$ be a surjective ring homomorphism. If $R$ is a semisimple ring, then $S$ is also a semisimple ring.
IsSemisimpleRing.ideal_eq_span_idempotent theorem
[IsSemisimpleRing R] (I : Ideal R) : ∃ e : R, IsIdempotentElem e ∧ I = .span { e }
Full source 
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]⟩
Existence of Idempotent Generators for Ideals in Semisimple Rings
Informal description
Let $R$ be a semisimple ring. For any ideal $I$ of $R$, there exists an idempotent element $e \in R$ (i.e., $e^2 = e$) such that $I$ is equal to the ideal generated by $e$, i.e., $I = \langle e \rangle$.
LinearMap.injective_or_eq_zero theorem
[IsSimpleModule R M] (f : M →ₗ[R] N) : Function.Injective f ∨ f = 0
Full source 
theorem injective_or_eq_zero [IsSimpleModule R M] (f : M →ₗ[R] N) :
    Function.InjectiveFunction.Injective f ∨ f = 0 := by
  rw [← ker_eq_bot, ← ker_eq_top]
  apply eq_bot_or_eq_top
Schur's Lemma: Injective or Zero for Linear Maps on Simple Modules
Informal description
Let $M$ be a simple module over a ring $R$ and let $f : M \to N$ be a linear map. Then either $f$ is injective or $f$ is the zero map.
LinearMap.surjective_or_eq_zero theorem
[IsSimpleModule R N] (f : M →ₗ[R] N) : Function.Surjective f ∨ f = 0
Full source 
theorem surjective_or_eq_zero [IsSimpleModule R N] (f : M →ₗ[R] N) :
    Function.SurjectiveFunction.Surjective f ∨ f = 0 := by
  rw [← range_eq_top, ← range_eq_bot, or_comm]
  apply eq_bot_or_eq_top
Surjectivity or Zero Property for Linear Maps on Simple Modules
Informal description
Let $M$ and $N$ be modules over a ring $R$, with $N$ being a simple module. For any linear map $f: M \to N$, either $f$ is surjective or $f$ is the zero map.
LinearMap.bijective_or_eq_zero theorem
[IsSimpleModule R M] [IsSimpleModule R N] (f : M →ₗ[R] N) : Function.Bijective f ∨ f = 0
Full source 
/-- **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.BijectiveFunction.Bijective f ∨ f = 0 :=
  or_iff_not_imp_right.mpr fun h ↦ ⟨injective_of_ne_zero h, surjective_of_ne_zero h⟩
Schur's Lemma: Bijective or Zero for Linear Maps Between Simple Modules
Informal description
Let $M$ and $N$ be simple modules over a ring $R$. For any linear map $f: M \to N$, either $f$ is bijective or $f$ is the zero map.
LinearMap.bijective_of_ne_zero theorem
[IsSimpleModule R M] [IsSimpleModule R N] {f : M →ₗ[R] N} (h : f ≠ 0) : Function.Bijective f
Full source 
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
Schur's Lemma: Nonzero Linear Maps Between Simple Modules are Bijective
Informal description
Let $M$ and $N$ be simple modules over a ring $R$. For any nonzero linear map $f: M \to N$, $f$ is bijective.
LinearMap.isCoatom_ker_of_surjective theorem
[IsSimpleModule R N] {f : M →ₗ[R] N} (hf : Function.Surjective f) : IsCoatom (LinearMap.ker f)
Full source 
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)
Kernel of Surjective Map to Simple Module is Maximal
Informal description
Let $M$ and $N$ be modules over a ring $R$, with $N$ being simple. For any surjective linear map $f: M \to N$, the kernel $\ker f$ is a coatomic submodule of $M$ (i.e., a maximal proper submodule).
Module.End.instDivisionRing instance
[DecidableEq (Module.End R M)] [IsSimpleModule R M] : DivisionRing (Module.End R M)
Full source 
/-- 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
  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
Division Ring Structure on Endomorphism Ring of a Simple Module (Schur's Lemma)
Informal description
For any simple module $M$ over a ring $R$, the endomorphism ring $\text{End}_R(M)$ is a division ring. This is a consequence of Schur's Lemma, which states that every nonzero endomorphism of $M$ is invertible.
JordanHolderModule.Iso definition
(X Y : Submodule R M × Submodule R M) : Prop
Full source 
/-- An isomorphism `X₂ / X₁ ∩ X₂ ≅ Y₂ / Y₁ ∩ Y₂` of modules for pairs
`(X₁,X₂) (Y₁,Y₂) : Submodule R M` -/
def Iso (X Y : SubmoduleSubmodule R M × Submodule R M) : Prop :=
  Nonempty <| (X.2 ⧸ X.1.comap X.2.subtype) ≃ₗ[R] Y.2 ⧸ Y.1.comap Y.2.subtype
Isomorphism of submodule pairs via quotient modules
Informal description
Given two pairs of submodules $(X_1, X_2)$ and $(Y_1, Y_2)$ of a module $M$ over a ring $R$, we say they are isomorphic (denoted $\text{Iso}(X, Y)$) if there exists a linear isomorphism between the quotient modules $X_2 / (X_1 \cap X_2)$ and $Y_2 / (Y_1 \cap Y_2)$.
JordanHolderModule.iso_symm theorem
{X Y : Submodule R M × Submodule R M} : Iso X Y → Iso Y X
Full source 
theorem iso_symm {X Y : SubmoduleSubmodule R M × Submodule R M} : Iso X Y → Iso Y X :=
  fun ⟨f⟩ => ⟨f.symm⟩
Symmetry of Submodule Quotient Isomorphism
Informal description
Given two pairs of submodules $(X_1, X_2)$ and $(Y_1, Y_2)$ of a module $M$ over a ring $R$, if there exists an isomorphism between the quotient modules $X_2 / (X_1 \cap X_2)$ and $Y_2 / (Y_1 \cap Y_2)$, then there also exists an isomorphism between $Y_2 / (Y_1 \cap Y_2)$ and $X_2 / (X_1 \cap X_2)$.
JordanHolderModule.iso_trans theorem
{X Y Z : Submodule R M × Submodule R M} : Iso X Y → Iso Y Z → Iso X Z
Full source 
theorem iso_trans {X Y Z : SubmoduleSubmodule R M × Submodule R M} : Iso X Y → Iso Y Z → Iso X Z :=
  fun ⟨f⟩ ⟨g⟩ => ⟨f.trans g⟩
Transitivity of Submodule Pair Isomorphism
Informal description
For any three pairs of submodules $(X_1, X_2)$, $(Y_1, Y_2)$, and $(Z_1, Z_2)$ of a module $M$ over a ring $R$, if $(X_1, X_2)$ is isomorphic to $(Y_1, Y_2)$ and $(Y_1, Y_2)$ is isomorphic to $(Z_1, Z_2)$, then $(X_1, X_2)$ is isomorphic to $(Z_1, Z_2)$. Here, isomorphism means there exists a linear isomorphism between the respective quotient modules $X_2 / (X_1 \cap X_2)$ and $Y_2 / (Y_1 \cap Y_2)$, and similarly between $Y_2 / (Y_1 \cap Y_2)$ and $Z_2 / (Z_1 \cap Z_2)$.
JordanHolderModule.second_iso theorem
{X Y : Submodule R M} (_ : X ⋖ X ⊔ Y) : Iso (X, X ⊔ Y) (X ⊓ Y, Y)
Full source 
@[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
Second Isomorphism Theorem for Submodules with Coatoms
Informal description
Let $X$ and $Y$ be submodules of an $R$-module $M$ such that $X$ is a coatom in the lattice of submodules between $X$ and $X \sqcup Y$ (i.e., $X \subsetneq X \sqcup Y$ and there is no proper intermediate submodule). Then there exists an isomorphism between the quotient modules $(X \sqcup Y)/X$ and $Y/(X \sqcap Y)$.
JordanHolderModule.instJordanHolderLattice instance
: JordanHolderLattice (Submodule R M)
Full source 
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
Jordan-Hölder Lattice Structure on Submodules
Informal description
The lattice of submodules of a module $M$ over a ring $R$ forms a Jordan-Hölder lattice. This means that the submodule lattice satisfies the conditions required for the Jordan-Hölder theorem, which guarantees the existence and uniqueness (up to isomorphism and permutation) of composition series for modules of finite length.