# Category of linear orders #

This defines LinOrd, the category of linear orders with monotone maps.

def LinOrd :
Type (u_1 + 1)

The category of linear orders.

Equations
Instances For
Equations
• One or more equations did not get rendered due to their size.
Equations
def LinOrd.of (α : Type u_1) [] :

Construct a bundled LinOrd from the underlying type and typeclass.

Equations
Instances For
@[simp]
theorem LinOrd.coe_of (α : Type u_1) [] :
() = α
Equations
Equations
• α.instLinearOrderα = α.str
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem LinOrd.Iso.mk_hom {α : LinOrd} {β : LinOrd} (e : α ≃o β) :
().hom = e
@[simp]
theorem LinOrd.Iso.mk_inv {α : LinOrd} {β : LinOrd} (e : α ≃o β) :
().inv = e.symm
def LinOrd.Iso.mk {α : LinOrd} {β : LinOrd} (e : α ≃o β) :
α β

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

Equations
• = { hom := e, inv := e.symm, hom_inv_id := , inv_hom_id := }
Instances For
@[simp]
theorem LinOrd.dual_map :
∀ {X Y : LinOrd} (a : X →o Y), LinOrd.dual.map a = OrderHom.dual a
@[simp]
theorem LinOrd.dual_obj (X : LinOrd) :

OrderDual as a functor.

Equations
Instances For

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

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