gc_map_comap

Mathlib.Algebra.Module.Submodule.Map

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

English

The pair (map f, comap f) forms a Galois connection: map f is left adjoint to comap f.

Русский

Пара (map f, comap f) образует Галуа связь: image слева, preimage справа.

LaTeX

$$GaloisConnection (map f) (comap f)$$

Lean4

theorem gc_map_comap (f : F) : GaloisConnection (map f) (comap f)
  | _, _ => map_le_iff_le_comap

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

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

Разделы

Аффилиация

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