gc_map_comap — Mathlib

English

For a map f, the pair (map f, comap f) forms a Galois connection between the lattices of nonunital subalgebras: map f S ≤ U if and only if S ≤ comap f U.

Русский

Для отображения f пара (образ f, предобраз f) образует галоисову связь между решетками неполных подалгебр: образ f(S) ≤ U тогда и только тогда S ≤ предобраз f(U).

LaTeX

$$$\\text{GaloisConnection}(\\mathrm{map}\,f, \\mathrm{comap}\,f)$ which is equivalent to $\\forall S,U,\\, \\mathrm{map}\,f\,S \\le U \\iff S \\le \\mathrm{comap}\,f\,U$$$

Lean4

theorem gc_map_comap (f : F) : GaloisConnection (map f : NonUnitalSubalgebra R A → NonUnitalSubalgebra R B) (comap f) :=
  fun _ _ => map_le

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