isSemisimpleModule_iff_exists_linearEquiv_dfinsupp

English

A module is semisimple iff there exists a linear equivalence to a DFinsupp presentation with simple components.

Русский

Модуль полупрямой тогда и только тогда, когда существует линейное эквивалентное отображение к DFinsupp-представлению с простыми компонентами.

LaTeX

$$IsSemisimpleModule R M ↔ ∃ s, e, ∀ m : s, IsSimpleModule R m.1$$

Lean4

theorem isSemisimpleModule_iff_exists_linearEquiv_dfinsupp :
    IsSemisimpleModule 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, e, h⟩ := IsSemisimpleModule.exists_linearEquiv_dfinsupp R M
  exact ⟨s, e, h.2⟩

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