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.

Equations
    Instances For
      source
      instance instLocaleLargeCategory :
      CategoryTheory.LargeCategory Locale
      Equations
        source
        instance Locale.instCoeSortType :
        CoeSort Locale (Type u_1)
        Equations
          source
          instance Locale.instFrameCarrierUnopFrm (X : Locale) :
          Order.Frame ↑(Opposite.unop X)
          Equations
            source
            def Locale.of (α : Type u_1) [Order.Frame α] :
            Locale

            Construct a bundled Locale from a Frame.

            Equations
              Instances For
                source
                @[simp]
                theorem Locale.coe_of (α : Type u_1) [Order.Frame α] :
                ↑(Opposite.unop (of α)) = α
                source
                instance Locale.instInhabited :
                Inhabited Locale
                Equations
                  source
                  def topToLocale :
                  CategoryTheory.Functor TopCat Locale

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

                  Equations
                    Instances For
                      source
                      @[simp]
                      theorem topToLocale_obj (X : TopCat) :
                      topToLocale.obj X = Opposite.op (topCatOpToFrm.obj (Opposite.op X))
                      source
                      @[simp]
                      theorem topToLocale_map {X✝ Y✝ : TopCat} (f : X✝ ⟶ Y✝) :
                      topToLocale.map f = (Frm.ofHom (TopologicalSpace.Opens.comap (TopCat.Hom.hom f))).op
                      source
                      instance CompHausToLocale.faithful :
                      (compHausToTop.comp topToLocale).Faithful