Category of linear orders #
This defines LinearOrder
, the category of linear orders with monotone maps.
The category of linear orders.
Equations
@[protected, instance]
Equations
- LinearOrder.linear_order.to_partial_order.category_theory.bundled_hom.parent_projection = category_theory.bundled_hom.parent_projection.mk
@[protected, instance]
@[protected, instance]
@[protected, instance]
Construct a bundled LinearOrder
from the underlying type and typeclass.
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
- α.linear_order = α.str
@[protected, instance]
Equations
- LinearOrder.has_forget_to_Lattice = {forget₂ := {obj := λ (X : LinearOrder), Lattice.of ↥X, map := λ (X Y : LinearOrder) (f : X ⟶ Y), order_hom_class.to_lattice_hom ↥X ↥Y f, map_id' := LinearOrder.has_forget_to_Lattice._proof_1, map_comp' := LinearOrder.has_forget_to_Lattice._proof_2}, forget_comp := LinearOrder.has_forget_to_Lattice._proof_3}
Constructs an equivalence between linear orders from an order isomorphism between them.
Equations
- LinearOrder.iso.mk e = {hom := ↑e, inv := ↑(e.symm), hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
LinearOrder.iso.mk_inv
{α β : LinearOrder}
(e : ↥α ≃o ↥β) :
(LinearOrder.iso.mk e).inv = ↑(e.symm)
@[simp]
@[simp]
@[simp]
order_dual
as a functor.
Equations
- LinearOrder.dual = {obj := λ (X : LinearOrder), LinearOrder.of (↥X)ᵒᵈ, map := λ (X Y : LinearOrder), ⇑order_hom.dual, map_id' := LinearOrder.dual._proof_1, map_comp' := LinearOrder.dual._proof_2}
@[simp]
@[simp]
The equivalence between LinearOrder
and itself induced by order_dual
both ways.
Equations
- LinearOrder.dual_equiv = category_theory.equivalence.mk LinearOrder.dual LinearOrder.dual (category_theory.nat_iso.of_components (λ (X : LinearOrder), LinearOrder.iso.mk (order_iso.dual_dual ↥X)) LinearOrder.dual_equiv._proof_1) (category_theory.nat_iso.of_components (λ (X : LinearOrder), LinearOrder.iso.mk (order_iso.dual_dual ↥X)) LinearOrder.dual_equiv._proof_2)