English
For A ≤ B, A covers B (A ⋖ B) if and only if the quotient B / (comap B.subtype A) is a simple R-module.
Русский
Для подмодулов A ≤ B равносильно тому, что A покрывает B (A ⋖ B) тогда и только тогда, когда тождественный до B: B / (comap B.subtype A) прост как R-модуль.
LaTeX
$$$A \\le B \\;\\Rightarrow\\; A \\ covby B \\;\\iff\\; IsSimpleModule\\; R\\; (B / Submodule.comap B.subtype A)$$$
Lean4
theorem covBy_iff_quot_is_simple {A B : Submodule R M} (hAB : A ≤ B) :
A ⋖ B ↔ IsSimpleModule R (B ⧸ Submodule.comap B.subtype A) :=
by
set f : Submodule R B ≃o Set.Iic B := B.mapIic with hf
rw [covBy_iff_coatom_Iic hAB, isSimpleModule_iff_isCoatom, ← OrderIso.isCoatom_iff f, hf]
simp [-OrderIso.isCoatom_iff, Submodule.map_comap_subtype, inf_eq_right.2 hAB]
