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
🔸 coverage
def Locale :
Type (u_1 + 1)

The category of locales.

Instances For
    source
    🔸 coverage
    @[implicit_reducible]
    instance instLargeCategoryLocale :
    CategoryTheory.LargeCategory Locale
    source
    🔸 coverage
    @[implicit_reducible]
    instance Locale.instCoeSortType :
    CoeSort Locale (Type u_1)
    source
    🔸 coverage
    @[implicit_reducible]
    instance Locale.instFrameCarrierUnopFrm (X : Locale) :
    Order.Frame ↑(Opposite.unop X)
    source
    🔸 coverage
    def Locale.of (α : Type u_1) [Order.Frame α] :
    Locale

    Construct a bundled Locale from a Frame.

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

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

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