English
A homeomorphism H: X ≅ Y induces an equivalence between the categories of open sets of Y and X, given by mapping opens along H and its inverse.
Русский
Гомеоморфизм H: X ≅ Y порождает эквивалентность между категориями открытых множеств Y и X, задаваемую отображением открытых множеств вдоль H и его обратного.
LaTeX
$$$ \text{If } H: X \simeq Y, \ Opens(Y) \simeq Opens(X), \text{ via } map H.hom \text{ and } map H.inv.$$$
Lean4
/-- A homeomorphism of spaces gives an equivalence of categories of open sets.
TODO: define `OrderIso.equivalence`, use it.
-/
@[simps]
def mapMapIso {X Y : TopCat.{u}} (H : X ≅ Y) : Opens Y ≌ Opens X
where
functor := map H.hom
inverse := map H.inv
unitIso := NatIso.ofComponents fun U => eqToIso (by simp [map, Set.preimage_preimage])
counitIso := NatIso.ofComponents fun U => eqToIso (by simp [map, Set.preimage_preimage])
