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.instCoeSortType : CoeSort Locale (Type u_1)

Equations

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

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

Equations

• X.instFrameαUnopFrm = (Opposite.unop X).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 α] : ↑(Opposite.unop (Locale.of α)) = α

instance Locale.instInhabited : Inhabited Locale

Equations

• Locale.instInhabited = { 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 = Quiver.Hom.op (TopologicalSpace.Opens.comap f)

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 : (compHausToTop.comp topToLocale).Faithful

Equations

• CompHausToLocale.faithful = ⋯