English
Equivalence: IsSimpleModule R M holds exactly when M is nontrivial and every nonzero element x yields a surjective toSpanSingleton map.
Русский
Эквивалентность: IsSimpleModule R M выполняется тогда и только тогда, когда M непустой и для каждого ненулевого x отображение toSpanSingleton сюръективно.
LaTeX
$$IsSimpleModule R M \\iff (Nontrivial M ∧ ∀ x : M, x ≠ 0 → Function.Surjective (toSpanSingleton R M x))$$
Lean4
theorem isSimpleModule_iff_toSpanSingleton_surjective :
IsSimpleModule R M ↔ Nontrivial M ∧ ∀ x : M, x ≠ 0 → Function.Surjective (LinearMap.toSpanSingleton R M x)
where
mp h := ⟨h.nontrivial, fun _ ↦ h.toSpanSingleton_surjective⟩
mpr := fun ⟨_, h⟩ ↦
(isSimpleModule_iff R M).mpr
⟨fun m ↦
or_iff_not_imp_left.mpr fun ne_bot ↦
have ⟨x, hxm, hx0⟩ := m.ne_bot_iff.mp ne_bot
top_unique <| fun z _ ↦ by obtain ⟨y, rfl⟩ := h x hx0 z; exact m.smul_mem _ hxm⟩
