galoisConnection_map_comap — Mathlib

English

The pair map and comap forms a Galois connection between Subgroupoids: map is left adjoint to comap.

Русский

Пара функций map и comap образуют Галуа-соединение между подгруппоидами: map — левый сопряжённый к comap.

LaTeX

$$$\forall S,T,\ map\ φ hφ S \le T \iff S \le comap\ φ T$$$

Lean4

theorem galoisConnection_map_comap (hφ : Function.Injective φ.obj) : GaloisConnection (map φ hφ) (comap φ) :=
  by
  rintro S T; simp_rw [le_iff]; constructor
  · exact fun h c d f fS => h (Map.Arrows.im f fS)
  · rintro h _ _ g ⟨a, gφS⟩
    exact h gφS

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