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.

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

    Construct a bundled Locale from a Frame.

    Instances For
      theorem Locale.coe_of (α : Type u_1) [Order.Frame α] :
      (Locale.of α).unop = α
      theorem topToLocale_map :
      ∀ {X Y : TopCat} (f : X Y), f = (TopologicalSpace.Opens.comap f).op

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

      Instances For