mathlib3 documentation

topology.category.Locale

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.

def Locale  :
Type (u_1+1)

The category of locales.

Equations
Instances for Locale
@[protected, instance]
Equations
@[protected, instance]
Equations
def Locale.of (α : Type u_1) [order.frame α] :

Construct a bundled Locale from a frame.

Equations
@[simp]
theorem Locale.coe_of (α : Type u_1) [order.frame α] :
(Locale.of α) = α

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

Equations