Documentation

Mathlib.Order.Category.Frm

The category of frames #

This file defines Frm, the category of frames.

References #

source
def Frm :
Type (u_1 + 1)

The category of frames.

Equations
Instances For
    source
    instance Frm.instCoeSortFrmType :
    CoeSort Frm (Type u_1)
    Equations
    source
    instance Frm.instFrameα (X : Frm) :
    Order.Frame ↑X
    Equations
    source
    def Frm.of (α : Type u_1) [Order.Frame α] :
    Frm

    Construct a bundled Frm from a Frame.

    Equations
    Instances For
      source
      @[simp]
      theorem Frm.coe_of (α : Type u_1) [Order.Frame α] :
      ↑(Frm.of α) = α
      source
      instance Frm.instInhabitedFrm :
      Inhabited Frm
      Equations
      source
      @[inline, reducible]
      abbrev Frm.Hom (α : Type u_1) (β : Type u_2) [Order.Frame α] [Order.Frame β] :
      Type (max u_1 u_2)

      An abbreviation of FrameHom that assumes Frame instead of the weaker CompleteLattice. Necessary for the category theory machinery.

      Equations
      Instances For
        source
        instance Frm.bundledHom :
        CategoryTheory.BundledHom Frm.Hom
        Equations
        • One or more equations did not get rendered due to their size.
        source
        instance Frm.instConcreteCategoryFrmInstFrmCategory :
        CategoryTheory.ConcreteCategory Frm
        Equations
        source
        instance Frm.hasForgetToLat :
        CategoryTheory.HasForget₂ Frm Lat
        Equations
        • One or more equations did not get rendered due to their size.
        source
        @[simp]
        theorem Frm.Iso.mk_inv_toFun {α : Frm} {β : Frm} (e : ↑α ≃o ↑β) (a : ↑β) :
        (Frm.Iso.mk e).inv a = (OrderIso.symm e) a
        source
        @[simp]
        theorem Frm.Iso.mk_hom_toFun {α : Frm} {β : Frm} (e : ↑α ≃o ↑β) (a : ↑α) :
        (Frm.Iso.mk e).hom a = e a
        source
        def Frm.Iso.mk {α : Frm} {β : Frm} (e : ↑α ≃o ↑β) :
        α ≅ β

        Constructs an isomorphism of frames from an order isomorphism between them.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem topCatOpToFrm_obj (X : TopCatᵒᵖ) :
          topCatOpToFrm.toPrefunctor.obj X = Frm.of (TopologicalSpace.Opens ↑X.unop)
          source
          @[simp]
          theorem topCatOpToFrm_map :
          ∀ {X Y : TopCatᵒᵖ} (f : X ⟶ Y), topCatOpToFrm.toPrefunctor.map f = TopologicalSpace.Opens.comap f.unop
          source
          def topCatOpToFrm :
          CategoryTheory.Functor TopCatᵒᵖ Frm

          The forgetful functor from TopCatᵒᵖ to Frm.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            instance CompHausOpToFrame.faithful :
            CategoryTheory.Faithful (CategoryTheory.Functor.comp compHausToTop.op topCatOpToFrm)
            Equations