mathlib documentation

order.category.Frame

The category of frames #

This file defines Frame, the category of frames.

References #

@[protected, instance]
Equations
def Frame.of (α : Type u_1) [order.frame α] :

Construct a bundled Frame from a frame.

Equations
@[simp]
theorem Frame.coe_of (α : Type u_1) [order.frame α] :
(Frame.of α) = α
@[reducible]
def Frame.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]
Equations
def Frame.iso.mk {α β : Frame} (e : α ≃o β) :
α β

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

Equations
@[simp]
theorem Frame.iso.mk_hom {α β : Frame} (e : α ≃o β) :
@[simp]
theorem Frame.iso.mk_inv {α β : Frame} (e : α ≃o β) :

The forgetful functor from Topᵒᵖ to Frame.

Equations