isSimpleModule_iff_isCoatom — Mathlib

English

The quotient M/m is simple as an R-module if and only if m is a coatom in the lattice of submodules of M.

Русский

Квадрат М/м прост как R-модуль тогда и только тогда, когда m является коатомом в решетке подмодулей M.

LaTeX

$$$\\text{IsSimpleModule } R (M / m) \\iff \\text{IsCoatom } m$$$

Lean4

theorem isSimpleModule_iff_isCoatom : IsSimpleModule R (M ⧸ m) ↔ IsCoatom m :=
  by
  rw [← Set.isSimpleOrder_Ici_iff_isCoatom, isSimpleModule_iff]
  exact (Submodule.comapMkQRelIso m).isSimpleOrder_iff

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