map_comap_le

Mathlib.Algebra.Module.Submodule.Map

URI: https://scilib.ai/kg/mathlib#Submodule.map_comap_le

English

For surjective f, map f (comap f q) is contained in q: map f (comap f q) ≤ q.

Русский

При сюръективности f образ предобраза подмодуля q лежит внутри q: map f (comap f q) ≤ q.

LaTeX

$$$\operatorname{map} f (\operatorname{comap} f q) \le q$$$

Lean4

theorem map_comap_le [RingHomSurjective σ₁₂] (f : F) (q : Submodule R₂ M₂) : map f (comap f q) ≤ q :=
  (gc_map_comap f).l_u_le _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru