English
Let N be a simple submodule of a module M, and suppose N lies in the sum of a family of semisimple submodules indexed by s. Then N is isomorphic to a submodule of one of the summands; more precisely, there exists m ∈ s and a submodule S ≤ m together with an isomorphism N ≅ S of R-modules.
Русский
Пусть N — простой подмодуль модуля M, и пусть N лежит в сумме семейства подпомодулей, каждая из которых семисимплна. Тогда N изоморфен подмодулю S, вложенному в один из суммантов; существует m ∈ s и S ≤ m с изоморфизмом N ≅ S как R-модули.
LaTeX
$$$$ \\exists m \\in s, \\; \\exists S \\le m,\\; N \\cong_R S. $$$$
Lean4
/-- If a simple module is contained in a sum of semisimple modules, it must be isomorphic
to a submodule of one of the summands. -/
theorem le_linearEquiv_of_le_sSup [hs : ∀ m : s, IsSemisimpleModule R m] (hN : N ≤ sSup s) :
∃ m ∈ s, ∃ S ≤ m, Nonempty (N ≃ₗ[R] S) := by
rw [sSup_eq_iSup] at hN
have e := LinearEquiv.ofInjective _ (inclusion_injective hN)
have := IsSimpleModule.congr e.symm
have := isSemisimpleModule_biSup_of_isSemisimpleModule_submodule fun m hm ↦ hs ⟨m, hm⟩
obtain ⟨_, ⟨m, hm, rfl⟩, S, le, ⟨e'⟩⟩ :=
LinearMap.range (inclusion hN) |>.le_linearEquiv_of_sSup_eq_top (comap (⨆ i ∈ s, i).subtype '' s) <| by
rw [sSup_image, biSup_comap_subtype_eq_top]
exact ⟨m, hm, _, map_le_iff_le_comap.mpr le, ⟨(e.trans e').trans (equivMapOfInjective _ (subtype_injective _) _)⟩⟩
