gc_map_comap — Mathlib

English

Let f be a multiplicative homomorphism. The map and comap operations on subsemigroups form a Galois connection: map f is left adjoint to comap f.

Русский

Пусть f — мультипликативный гомоморфизм. Операции образа и обратного образа на подполугруппах образуют галуа-связь: образ через f является левой дугой к обратному образу относительно f.

LaTeX

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

Lean4

@[to_additive]
theorem gc_map_comap (f : M →ₙ* N) : GaloisConnection (map f) (comap f) := fun _ _ => map_le_iff_le_comap

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