The category of locales

This file defines Locale, the category of locales. This is the opposite of the category of frames.

def Locale : Type (u_1 + 1)

The category of locales.

instance instLargeCategoryLocale : CategoryTheory.LargeCategory Locale

instance Locale.instCoeSortType : CoeSort Locale (Type u_1)

instance Locale.instFrameCarrierUnopFrm (X : Locale) : Order.Frame ↑(Opposite.unop X)

def Locale.of (α : Type u_1) [Order.Frame α] : Locale

Construct a bundled Locale from a Frame.

@[simp]

theorem Locale.coe_of (α : Type u_1) [Order.Frame α] : ↑(Opposite.unop (of α)) = α

instance Locale.instInhabited : Inhabited Locale

def topToLocale : CategoryTheory.Functor TopCat Locale

The forgetful functor from Top to Locale which forgets that the space has "enough points".

@[simp]

theorem topToLocale_map {X✝ Y✝ : TopCat} (f : X✝ ⟶ Y✝) : topToLocale.map f = (Frm.ofHom (TopologicalSpace.Opens.comap (TopCat.Hom.hom f))).op

@[simp]

theorem topToLocale_obj (X : TopCat) : topToLocale.obj X = Opposite.op (topCatOpToFrm.obj (Opposite.op X))

instance CompHausToLocale.faithful : (compHausToTop.comp topToLocale).Faithful