The category of locales #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source

@[protected, instance]

def Locale.large_category :

category_theory.large_category Locale

source

def Locale :

Type (u_1+1)

The category of locales.

Equations

Locale = Frm ᵒᵖ

Instances for Locale

source

@[protected, instance]

def Locale.has_coe_to_sort :

has_coe_to_sort Locale (Type u_1)

Equations

Locale.has_coe_to_sort = {coe := λ (X : Locale), ↥(opposite.unop X)}

source

@[protected, instance]

def Locale.order.frame (X : Locale) :

order.frame ↥X

Equations

Locale.order.frame X = (opposite.unop X).str

source

def Locale.of (α : Type u_1) [order.frame α] :

Locale

Construct a bundled Locale from a frame.

Equations

Locale.of α = opposite.op (Frm.of α)

source

@[simp]

theorem Locale.coe_of (α : Type u_1) [order.frame α] :

↥(Locale.of α) = α

source

@[protected, instance]

def Locale.inhabited :

inhabited Locale

Equations

Locale.inhabited = {default := Locale.of punit (complete_distrib_lattice.to_frame punit)}

source

@[simp]

theorem Top_to_Locale_obj (X : Top) :

Top_to_Locale.obj X = opposite.op (Frm.of (topological_space.opens ↥X))

source

def Top_to_Locale :

Top ⥤ Locale

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

Equations

Top_to_Locale = Top_op_to_Frame.right_op

source

@[simp]

theorem Top_to_Locale_map (X Y : Top) (f : X ⟶ Y) :

Top_to_Locale.map f = quiver.hom.op (topological_space.opens.comap f)

source

@[protected, instance]

def CompHaus_to_Locale.faithful :

category_theory.faithful (CompHaus_to_Top ⋙ Top_to_Locale)