Documentation

Mathlib.Topology.Category.Locale

The category of locales #

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

source
def Locale :
Type (u_1 + 1)

The category of locales.

Instances For
    source
    instance Locale.instCoeSortLocaleType :
    CoeSort Locale (Type u_1)
    source
    instance Locale.instFrameαUnopFrmCat (X : Locale) :
    Order.Frame ↑X.unop
    source
    def Locale.of (α : Type u_1) [Order.Frame α] :
    Locale

    Construct a bundled Locale from a Frame.

    Instances For
      source
      @[simp]
      theorem Locale.coe_of (α : Type u_1) [Order.Frame α] :
      ↑(Locale.of α).unop = α
      source
      instance Locale.instInhabitedLocale :
      Inhabited Locale
      source
      @[simp]
      theorem topToLocale_obj (X : TopCat) :
      topToLocale.obj X = Opposite.op (FrmCat.of (TopologicalSpace.Opens ↑X))
      source
      @[simp]
      theorem topToLocale_map :
      ∀ {X Y : TopCat} (f : X ⟶ Y), topToLocale.map f = (TopologicalSpace.Opens.comap f).op
      source
      def topToLocale :
      CategoryTheory.Functor TopCat Locale

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

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