The category of bounded orders #
This defines BoundedOrder
, the category of bounded orders.
- to_PartialOrder : PartialOrder
- is_bounded_order : bounded_order ↥(self.to_PartialOrder)
The category of bounded orders with monotone functions.
Instances for BoundedOrder
@[protected, instance]
@[protected, instance]
Equations
Construct a bundled BoundedOrder
from a fintype
partial_order
.
Equations
- BoundedOrder.of α = BoundedOrder.mk {α := α, str := _inst_1}
@[simp]
theorem
BoundedOrder.coe_of
(α : Type u_1)
[partial_order α]
[bounded_order α] :
↥(BoundedOrder.of α) = α
@[protected, instance]
@[protected, instance]
Equations
- BoundedOrder.large_category = {to_category_struct := {to_quiver := {hom := λ (X Y : BoundedOrder), bounded_order_hom ↥X ↥Y}, id := λ (X : BoundedOrder), bounded_order_hom.id ↥X, comp := λ (X Y Z : BoundedOrder) (f : X ⟶ Y) (g : Y ⟶ Z), bounded_order_hom.comp g f}, id_comp' := BoundedOrder.large_category._proof_1, comp_id' := BoundedOrder.large_category._proof_2, assoc' := BoundedOrder.large_category._proof_3}
@[protected, instance]
Equations
- BoundedOrder.concrete_category = category_theory.concrete_category.mk {obj := coe_sort BoundedOrder.has_coe_to_sort, map := λ (X Y : BoundedOrder), coe_fn, map_id' := BoundedOrder.concrete_category._proof_1, map_comp' := BoundedOrder.concrete_category._proof_2}
@[protected, instance]
Equations
- BoundedOrder.has_forget_to_PartialOrder = {forget₂ := {obj := λ (X : BoundedOrder), X.to_PartialOrder, map := λ (X Y : BoundedOrder), bounded_order_hom.to_order_hom, map_id' := BoundedOrder.has_forget_to_PartialOrder._proof_1, map_comp' := BoundedOrder.has_forget_to_PartialOrder._proof_2}, forget_comp := BoundedOrder.has_forget_to_PartialOrder._proof_3}
@[protected, instance]
Equations
- BoundedOrder.has_forget_to_Bipointed = {forget₂ := {obj := λ (X : BoundedOrder), {X := ↥X, to_prod := (⊥, ⊤)}, map := λ (X Y : BoundedOrder) (f : X ⟶ Y), {to_fun := ⇑f, map_fst := _, map_snd := _}, map_id' := BoundedOrder.has_forget_to_Bipointed._proof_3, map_comp' := BoundedOrder.has_forget_to_Bipointed._proof_4}, forget_comp := BoundedOrder.has_forget_to_Bipointed._proof_5}
order_dual
as a functor.
Equations
- BoundedOrder.dual = {obj := λ (X : BoundedOrder), BoundedOrder.of (↥X)ᵒᵈ, map := λ (X Y : BoundedOrder), ⇑bounded_order_hom.dual, map_id' := BoundedOrder.dual._proof_1, map_comp' := BoundedOrder.dual._proof_2}
@[simp]
@[simp]
Constructs an equivalence between bounded orders from an order isomorphism between them.
Equations
- BoundedOrder.iso.mk e = {hom := ↑e, inv := ↑(e.symm), hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
BoundedOrder.iso.mk_inv
{α β : BoundedOrder}
(e : ↥α ≃o ↥β) :
(BoundedOrder.iso.mk e).inv = ↑(e.symm)
@[simp]
theorem
BoundedOrder.iso.mk_hom
{α β : BoundedOrder}
(e : ↥α ≃o ↥β) :
(BoundedOrder.iso.mk e).hom = ↑e
@[simp]
@[simp]
The equivalence between BoundedOrder
and itself induced by order_dual
both ways.
Equations
- BoundedOrder.dual_equiv = category_theory.equivalence.mk BoundedOrder.dual BoundedOrder.dual (category_theory.nat_iso.of_components (λ (X : BoundedOrder), BoundedOrder.iso.mk (order_iso.dual_dual ↥X)) BoundedOrder.dual_equiv._proof_1) (category_theory.nat_iso.of_components (λ (X : BoundedOrder), BoundedOrder.iso.mk (order_iso.dual_dual ↥X)) BoundedOrder.dual_equiv._proof_2)