Documentation

Mathlib.Order.Category.Frm

The category of frames #

This file defines Frm, the category of frames.

References #

def Frm :
Type (u_1 + 1)

The category of frames.

Equations
Instances For
    Equations
    instance Frm.instFrameα (X : Frm) :
    Equations
    • X.instFrameα = X.str
    def Frm.of (α : Type u_1) [Order.Frame α] :

    Construct a bundled Frm from a Frame.

    Equations
    Instances For
      @[simp]
      theorem Frm.coe_of (α : Type u_1) [Order.Frame α] :
      (Frm.of α) = α
      @[reducible, inline]
      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
        Equations
        • One or more equations did not get rendered due to their size.
        Equations
        • One or more equations did not get rendered due to their size.
        @[simp]
        theorem Frm.Iso.mk_inv_toFun {α : Frm} {β : Frm} (e : α ≃o β) (a : β) :
        (Frm.Iso.mk e).inv a = e.symm a
        @[simp]
        theorem Frm.Iso.mk_hom_toFun {α : Frm} {β : Frm} (e : α ≃o β) (a : α) :
        (Frm.Iso.mk e).hom a = e a
        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
          @[simp]
          theorem topCatOpToFrm_map :
          ∀ {X Y : TopCatᵒᵖ} (f : X Y), topCatOpToFrm.map f = TopologicalSpace.Opens.comap f.unop

          The forgetful functor from TopCatᵒᵖ to Frm.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For