English
An open map f induces an adjunction between Opens X and Opens Y with unit and counit given by explicit monotone maps.
Русский
Открытое отображение f порождает смыкание (адъюнкцию) между Opens X и Opens Y с единицей и коэффициентами как явные монотонные отображения.
LaTeX
$$$ \text{IsOpenMap adjunction: } \mathrm{Opens}(X) \dashv \mathrm{Opens}(Y) \text{ via } \mathrm{map}(f) \text{ and } hf.functor.$$$
Lean4
/-- An open map `f : X ⟶ Y` induces an adjunction between `Opens X` and `Opens Y`.
-/
def adjunction {X Y : TopCat} {f : X ⟶ Y} (hf : IsOpenMap f) : hf.functor ⊣ Opens.map f
where
unit := { app := fun _ => homOfLE fun x hxU => ⟨x, hxU, rfl⟩ }
counit := { app := fun _ => homOfLE fun _ ⟨_, hfxV, hxy⟩ => hxy ▸ hfxV }
