mathlib documentation

order.category.LinearOrder

Category of linear orders #

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

source
def LinearOrder  :
Type (u_1+1)

The category of linear orders.

Equations
source
@[protected, instance]
def LinearOrder.linear_order.to_partial_order.category_theory.bundled_hom.parent_projection  :
category_theory.bundled_hom.parent_projection linear_order.to_partial_order
Equations
source
@[protected, instance]
def LinearOrder.concrete_category  :
category_theory.concrete_category LinearOrder
source
@[protected, instance]
def LinearOrder.large_category  :
category_theory.large_category LinearOrder
source
@[protected, instance]
def LinearOrder.has_coe_to_sort  :
has_coe_to_sort LinearOrder (Type u_1)
Equations
source
def LinearOrder.of (α : Type u_1) [linear_order α] :
LinearOrder

Construct a bundled LinearOrder from the underlying type and typeclass.

Equations
source
@[protected, instance]
def LinearOrder.inhabited  :
inhabited LinearOrder
Equations
source
@[protected, instance]
def LinearOrder.linear_order (α : LinearOrder) :
linear_order ↥α
Equations
source
@[protected, instance]
def LinearOrder.has_forget_to_PartialOrder  :
category_theory.has_forget₂ LinearOrder PartialOrder
Equations
source
def LinearOrder.iso.mk {α β : LinearOrder} (e : ↥α ≃o ↥β) :
α ≅ β

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

Equations
source
@[simp]
theorem LinearOrder.iso.mk_inv {α β : LinearOrder} (e : ↥α ≃o ↥β) :
(LinearOrder.iso.mk e).inv = ↑(e.symm)
source
@[simp]
theorem LinearOrder.iso.mk_hom {α β : LinearOrder} (e : ↥α ≃o ↥β) :
(LinearOrder.iso.mk e).hom = ↑e
source
@[simp]
theorem LinearOrder.to_dual_obj (X : LinearOrder) :
LinearOrder.to_dual.obj X = LinearOrder.of (order_dual ↥X)
source
def LinearOrder.to_dual  :
LinearOrder ⥤ LinearOrder

order_dual as a functor.

Equations
source
@[simp]
theorem LinearOrder.to_dual_map (X Y : LinearOrder) (ᾰ : ↥X →o ↥Y) :
LinearOrder.to_dual.map ᾰ = ⇑order_hom.dual ᾰ
source
@[simp]
theorem LinearOrder.dual_equiv_functor  :
LinearOrder.dual_equiv.functor = LinearOrder.to_dual
source
@[simp]
theorem LinearOrder.dual_equiv_inverse  :
LinearOrder.dual_equiv.inverse = LinearOrder.to_dual
source
def LinearOrder.dual_equiv  :
LinearOrder ≌ LinearOrder

The equivalence between PartialOrder and itself induced by order_dual both ways.

Equations
source
theorem LinearOrder_dual_equiv_comp_forget_to_PartialOrder  :
LinearOrder.dual_equiv.functor ⋙ category_theory.forget₂ LinearOrder PartialOrder = category_theory.forget₂ LinearOrder PartialOrder ⋙ PartialOrder.dual_equiv.functor