linearEquiv_of_le_sSup — Mathlib

English

If a submodule N is contained in the sum of a family s of submodules, where every member is simple, then N is isomorphic to one of the summands in s.

Русский

Если подмодуль N содержится в сумме семейства s подподмодулей, каждый из которых прост, то N изоморфен одному из слагаемых в s.

LaTeX

$$$$ \\exists S \\in s,\\; N \\cong_R S. $$$$

Lean4

theorem linearEquiv_of_le_sSup [simple : ∀ m : s, IsSimpleModule R m] (hs : N ≤ sSup s) :
    ∃ S ∈ s, Nonempty (N ≃ₗ[R] S) :=
  have ⟨m, hm, _S, le, ⟨e⟩⟩ := N.le_linearEquiv_of_le_sSup _ hs
  have := isSimpleModule_iff_isAtom.mp (.congr e.symm)
  have := ((isSimpleModule_iff_isAtom.mp <| simple ⟨m, hm⟩).le_iff_eq this.1).mp le
  ⟨m, hm, ⟨e.trans (.ofEq _ _ this)⟩⟩

Похожие утверждения