# The category of bounded orders #

This defines BddOrd, the category of bounded orders.

structure BddOrd :
Type (u_1 + 1)

The category of bounded orders with monotone functions.

• toPartOrd : PartOrd

The underlying object in the category of partial orders.

• isBoundedOrder : BoundedOrder self.toPartOrd
Instances For
Equations
• X.instPartialOrderαToPartOrd = X.toPartOrd.str
def BddOrd.of (α : Type u_1) [] [] :

Construct a bundled BddOrd from a Fintype PartialOrder.

Equations
Instances For
@[simp]
theorem BddOrd.coe_of (α : Type u_1) [] [] :
().toPartOrd = α
Equations
instance BddOrd.instFunLike (X : BddOrd) (Y : BddOrd) :
FunLike (X Y) X.toPartOrd Y.toPartOrd
Equations
• X.instFunLike Y = let_fun this := inferInstance; this
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.
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem BddOrd.dual_map {X : BddOrd} {Y : BddOrd} (a : BoundedOrderHom X.toPartOrd Y.toPartOrd) :
BddOrd.dual.map a = BoundedOrderHom.dual a
@[simp]
theorem BddOrd.dual_obj (X : BddOrd) :
BddOrd.dual.obj X = BddOrd.of (X.toPartOrd)ᵒᵈ

OrderDual as a functor.

Equations
Instances For
@[simp]
theorem BddOrd.Iso.mk_hom {α : BddOrd} {β : BddOrd} (e : α.toPartOrd ≃o β.toPartOrd) :
().hom = e
@[simp]
theorem BddOrd.Iso.mk_inv {α : BddOrd} {β : BddOrd} (e : α.toPartOrd ≃o β.toPartOrd) :
().inv = e.symm
def BddOrd.Iso.mk {α : BddOrd} {β : BddOrd} (e : α.toPartOrd ≃o β.toPartOrd) :
α β

Constructs an equivalence between bounded orders from an order isomorphism between them.

Equations
• = { hom := e, inv := e.symm, hom_inv_id := , inv_hom_id := }
Instances For

The equivalence between BddOrd and itself induced by OrderDual both ways.

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