gc_map_comap — Mathlib

English

The pair of operations map f and comap f form a Galois connection between subalgebras of A and B: for all S ⊆ A and U ⊆ B, map f S ≤ U iff S ≤ comap f U.

Русский

Пара операций map f и comap f образует гамильоново-связь между подалгебрами A и B: для любых S ⊆ A, U ⊆ B выполняется map f S ≤ U тогда и только тогда S ≤ comap f U.

LaTeX

$$$\\text{GaloisConnection}(\\mathrm{map}\ f, \\mathrm{comap}\ f)$, equivalently, $\\forall S \\ U, \\mathrm{map}\ f\\ S \\le U \\iff S \\le \\mathrm{comap}\ f\\ U$$$

Lean4

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

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