ker_toSpanSingleton_isMaximal — Mathlib

English

A simple module M is equivalent to being nontrivial and every nonzero element generates M via SpanSingleton surjectivity.

Русский

Простой модуль M эквивалентен не тривиальности и тому, что каждый ненулевой элемент порождает M через сюръективность SpanSingleton.

LaTeX

$$IsSimpleModule R M ↔ Nontrivial M ∧ ∀ x : M, x ≠ 0 → Surjective (toSpanSingleton R M x)$$

Lean4

theorem ker_toSpanSingleton_isMaximal {m : M} (hm : m ≠ 0) : Ideal.IsMaximal (ker (toSpanSingleton R M m)) :=
  by
  rw [Ideal.isMaximal_def, ← isSimpleModule_iff_isCoatom]
  exact congr (quotKerEquivOfSurjective _ <| toSpanSingleton_surjective R hm)

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