# 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.str
def Frm.of (α : Type u_1) [] :

Construct a bundled Frm from a Frame.

Equations
Instances For
@[simp]
theorem Frm.coe_of (α : Type u_1) [] :
() = α
Equations
@[inline, reducible]
abbrev Frm.Hom (α : Type u_1) (β : Type u_2) [] [] :
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 : β) :
().inv a = () a
@[simp]
theorem Frm.Iso.mk_hom_toFun {α : Frm} {β : Frm} (e : α ≃o β) (a : α) :
().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]
@[simp]
theorem topCatOpToFrm_map :
∀ {X Y : } (f : X Y), topCatOpToFrm.map f =

The forgetful functor from TopCatᵒᵖ to Frm.

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