isSemisimpleModule_of_isSemisimpleModule_submodule

English

A submodule of a semisimple module is semisimple.

Русский

Подмодуль полупрямого модуля является полупрямым.

LaTeX

$$IsSemisimpleModule R (Subtype fun x => x ∈ m)$$

Lean4

/-- A module generated by semisimple submodules is itself semisimple. -/
theorem 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
  simp_rw [isSemisimpleModule_iff] at hp ⊢
  refine complementedLattice_of_complementedLattice_Iic (fun i hi ↦ ?_) hp'
  simpa only [← (p i).mapIic.complementedLattice_iff] using hp i hi

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