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.

Equations

• Locale = Frmᵒᵖ

instance Locale.instCoeSortLocaleType : CoeSort Locale (Type u_1)

Equations

• Locale.instCoeSortLocaleType = { coe := fun (X : Locale) => ↑X.unop }

instance Locale.instFrameαUnopFrm (X : Locale) : Order.Frame ↑X.unop

Equations

• Locale.instFrameαUnopFrm X = X.unop.str

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

Construct a bundled Locale from a Frame.

Equations

• Locale.of α = Opposite.op (Frm.of α)

@[simp]

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

instance Locale.instInhabitedLocale : Inhabited Locale

Equations

• Locale.instInhabitedLocale = { default := Locale.of PUnit.{u_1 + 1} }

@[simp]

theorem topToLocale_obj (X : TopCat) : topToLocale.obj X = Opposite.op (Frm.of (TopologicalSpace.Opens ↑X))

@[simp]

theorem topToLocale_map : ∀ {X Y : TopCat} (f : X ⟶ Y), topToLocale.map f = (TopologicalSpace.Opens.comap f).op

def topToLocale : CategoryTheory.Functor TopCat Locale

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

Equations

• topToLocale = topCatOpToFrm.rightOp

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

Equations

• CompHausToLocale.faithful = ⋯