adjunction — Mathlib

English

An inducing map f yields an adjunction between Opens Y and Opens X with map on opens and a functor.

Русский

Индукцирующее отображение f даёт adjunction между Opens Y и Opens X с отображением на открытые множества и функтором.

LaTeX

$$$ \text{adjunction}(hf): Opens(map f) \dashv hf.functor$$$

Lean4

/-- An inducing map `f : X ⟶ Y` induces an adjunction between `Opens Y` and `Opens X`. -/
def adjunction {X Y : TopCat} {f : X ⟶ Y} (hf : IsInducing f) : Opens.map f ⊣ hf.functor :=
  hf.opensGI.gc.adjunction

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