gc_map_comap

Mathlib.Algebra.Ring.Subring.Basic

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

English

The pair (map f, comap f) forms a Galois connection.

Русский

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

LaTeX

$$$\\text{GaloisConnection} (\\mathrm{map}\\,f) (\\mathrm{comap}\\,f). $$$

Lean4

theorem gc_map_comap (f : R →+* S) : GaloisConnection (map f) (comap f) := fun _ _ => map_le_iff_le_comap

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

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

Разделы

Аффилиация

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