gc_map_comap

Mathlib.Algebra.Algebra.Subalgebra.Basic

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

English

The pair (map f, comap f) forms a Galois connection between Subalgebras of A and B.

Русский

Пара (map f, comap f) образует Галуа-связь между подалгебрами A и B.

LaTeX

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

Lean4

theorem gc_map_comap (f : A →ₐ[R] B) : GaloisConnection (map f) (comap f) := fun _S _U => map_le

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

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

Разделы

Аффилиация

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