The category of locales #
This file defines Locale
, the category of locales. This is the opposite of the category of frames.
@[simp]
theorem
topToLocale_obj
(X : TopCat)
:
topToLocale.obj X = Opposite.op (FrmCat.of (TopologicalSpace.Opens ↑X))
@[simp]
theorem
topToLocale_map :
∀ {X Y : TopCat} (f : X ⟶ Y), topToLocale.map f = (TopologicalSpace.Opens.comap f).op