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.instCoeSortType :
    CoeSort Frm (Type u_1)
    Equations
    source
    instance Frm.instFrameα (X : Frm) :
    Order.Frame ↑X
    Equations
    • X.instFrameα = X.str
    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.instInhabited :
      Inhabited Frm
      Equations
      source
      @[reducible, inline]
      abbrev Frm.Hom (α : Type u_1) (β : Type u_2) [Order.Frame α] [Order.Frame β] :
      Type (max u_2 u_1)

      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 instFrmLargeCategory :
        CategoryTheory.LargeCategory Frm
        Equations
        source
        instance instFrmCategory :
        CategoryTheory.Category.{u_1, u_1 + 1} Frm
        Equations
        source
        instance Frm.instConcreteCategory :
        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
        def Frm.Iso.mk {α β : 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 Frm.Iso.mk_hom_toFun {α β : Frm} (e : ↑α ≃o ↑β) (a : ↑α) :
          (Frm.Iso.mk e).hom a = e a
          source
          @[simp]
          theorem Frm.Iso.mk_inv_toFun {α β : Frm} (e : ↑α ≃o ↑β) (a : ↑β) :
          (Frm.Iso.mk e).inv a = e.symm a
          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
            @[simp]
            theorem topCatOpToFrm_obj (X : TopCatᵒᵖ) :
            topCatOpToFrm.obj X = Frm.of (TopologicalSpace.Opens ↑(Opposite.unop X))
            source
            @[simp]
            theorem topCatOpToFrm_map {X✝ Y✝ : TopCatᵒᵖ} (f : X✝ ⟶ Y✝) :
            topCatOpToFrm.map f = TopologicalSpace.Opens.comap f.unop
            source
            instance CompHausOpToFrame.faithful :
            (compHausToTop.op.comp topCatOpToFrm).Faithful
            Equations