English
If N ≤ M is simple and sSup s = ⊤ for some set s of submodules, then there exist S ∈ s and a linear equivalence N ≃ₗ[R] S with S ≤ m.
Русский
Если N прост и существует множество подмодулей s, такое что sSup s = ⊤, то существует S ∈ s и линейное эквив N ≃ₗ[R] S с S ≤ m.
LaTeX
$$$Eq (sSup s) \top → ∃ S ∈ s, Nonempty (N \cong_{R} S)$$$
Lean4
theorem linearEquiv_of_sSup_eq_top [h : ∀ m : s, IsSimpleModule R m] (hs : sSup s = ⊤) :
∃ S ∈ s, Nonempty (N ≃ₗ[R] S) :=
have := isSemisimpleModule_of_isSemisimpleModule_submodule' (fun _ ↦ inferInstance) (sSup_eq_iSup' s ▸ hs)
have ⟨m, hm, _S, le, ⟨e⟩⟩ := N.le_linearEquiv_of_sSup_eq_top _ hs
have := isSimpleModule_iff_isAtom.mp (IsSimpleModule.congr e.symm)
have := ((isSimpleModule_iff_isAtom.mp <| h ⟨m, hm⟩).le_iff_eq this.1).mp le
⟨m, hm, ⟨e.trans (.ofEq _ _ this)⟩⟩
