map_le_iff_le_comap — Mathlib

English

For an injective on objects φ, the relation between map φ hφ S and comap φ T is a Galois connection: map φ hφ S ≤ T iff S ≤ comap φ T.

Русский

Для инъективности по объектам φ существует связность Галуа между map φ hφ S и comap φ T: map φ hφ S ≤ T тогда и только тогда S ≤ comap φ T.

LaTeX

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

Lean4

theorem map_le_iff_le_comap (hφ : Function.Injective φ.obj) (S : Subgroupoid C) (T : Subgroupoid D) :
    map φ hφ S ≤ T ↔ S ≤ comap φ T :=
  (galoisConnection_map_comap φ hφ).le_iff_le

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