# mathlib3documentation

order.category.Frm

# The category of frames #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines Frm, the category of frames.

## References #

def Frm  :
Type (u_1+1)

The category of frames.

Equations
Instances for Frm
@[protected, instance]
def Frm.has_coe_to_sort  :
(Type u_1)
Equations
@[protected, instance]
def Frm.order.frame (X : Frm) :
Equations
def Frm.of (α : Type u_1) [order.frame α] :

Construct a bundled Frm from a frame.

Equations
@[simp]
theorem Frm.coe_of (α : Type u_1) [order.frame α] :
(Frm.of α) = α
@[protected, instance]
Equations
@[reducible]
def Frm.hom (α : Type u_1) (β : Type u_2) [order.frame α] [order.frame β] :
Type (max u_1 u_2)

An abbreviation of frame_hom that assumes frame instead of the weaker complete_lattice. Necessary for the category theory machinery.

@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
@[simp]
theorem Frm.iso.mk_inv {α β : Frm} (e : α ≃o β) :
@[simp]
theorem Frm.iso.mk_hom {α β : Frm} (e : α ≃o β) :
def Frm.iso.mk {α β : Frm} (e : α ≃o β) :
α β

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

Equations
@[simp]
theorem Top_op_to_Frame_obj (X : Topᵒᵖ) :
@[simp]
theorem Top_op_to_Frame_map (X Y : Topᵒᵖ) (f : X Y) :
def Top_op_to_Frame  :

The forgetful functor from Topᵒᵖ to Frm.

Equations
@[protected, instance]