Nonempty finite linear orders #
This defines NonemptyFinLinOrd
, the category of nonempty finite linear orders with monotone maps.
This is the index category for simplicial objects.
@[class]
- to_fintype : fintype α
- to_linear_order : linear_order α
- nonempty : nonempty α . "apply_instance"
A typeclass for nonempty finite linear orders.
@[protected, instance]
Equations
@[protected, instance]
Equations
- punit.nonempty_fin_lin_ord = {to_fintype := {elems := fintype.elems punit punit.fintype, complete := _}, to_linear_order := {le := linear_ordered_cancel_add_comm_monoid.le punit.linear_ordered_cancel_add_comm_monoid, lt := linear_ordered_cancel_add_comm_monoid.lt punit.linear_ordered_cancel_add_comm_monoid, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := linear_ordered_cancel_add_comm_monoid.decidable_le punit.linear_ordered_cancel_add_comm_monoid, decidable_eq := linear_ordered_cancel_add_comm_monoid.decidable_eq punit.linear_ordered_cancel_add_comm_monoid, decidable_lt := linear_ordered_cancel_add_comm_monoid.decidable_lt punit.linear_ordered_cancel_add_comm_monoid, max := linear_ordered_cancel_add_comm_monoid.max punit.linear_ordered_cancel_add_comm_monoid, max_def := _, min := linear_ordered_cancel_add_comm_monoid.min punit.linear_ordered_cancel_add_comm_monoid, min_def := _}, nonempty := _}
@[protected, instance]
Equations
- fin.nonempty_fin_lin_ord n = {to_fintype := {elems := fintype.elems (fin (n + 1)) (fin.fintype (n + 1)), complete := _}, to_linear_order := {le := linear_order.le fin.linear_order, lt := linear_order.lt fin.linear_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := linear_order.decidable_le fin.linear_order, decidable_eq := linear_order.decidable_eq fin.linear_order, decidable_lt := linear_order.decidable_lt fin.linear_order, max := max fin.linear_order, max_def := _, min := min fin.linear_order, min_def := _}, nonempty := _}
@[protected, instance]
Equations
- ulift.nonempty_fin_lin_ord α = {to_fintype := {elems := fintype.elems (ulift α) (ulift.fintype α), complete := _}, to_linear_order := {le := linear_order.le (linear_order.lift ⇑equiv.ulift _), lt := linear_order.lt (linear_order.lift ⇑equiv.ulift _), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := linear_order.decidable_le (linear_order.lift ⇑equiv.ulift _), decidable_eq := linear_order.decidable_eq (linear_order.lift ⇑equiv.ulift _), decidable_lt := linear_order.decidable_lt (linear_order.lift ⇑equiv.ulift _), max := max (linear_order.lift ⇑equiv.ulift _), max_def := _, min := min (linear_order.lift ⇑equiv.ulift _), min_def := _}, nonempty := _}
@[protected, instance]
Equations
- order_dual.nonempty_fin_lin_ord α = {to_fintype := {elems := fintype.elems (order_dual α) (order_dual.fintype α), complete := _}, to_linear_order := order_dual.linear_order α nonempty_fin_lin_ord.to_linear_order, nonempty := _}
The category of nonempty finite linear orders.
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
Construct a bundled NonemptyFinLinOrd
from the underlying type and typeclass.
Equations
@[protected, instance]
@[protected, instance]
Equations
- α.nonempty_fin_lin_ord = α.str
@[protected, instance]
@[simp]
theorem
NonemptyFinLinOrd.iso.mk_inv
{α β : NonemptyFinLinOrd}
(e : ↥α ≃o ↥β) :
(NonemptyFinLinOrd.iso.mk e).inv = ↑(e.symm)
Constructs an equivalence between nonempty finite linear orders from an order isomorphism between them.
Equations
- NonemptyFinLinOrd.iso.mk e = {hom := ↑e, inv := ↑(e.symm), hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
NonemptyFinLinOrd.iso.mk_hom
{α β : NonemptyFinLinOrd}
(e : ↥α ≃o ↥β) :
(NonemptyFinLinOrd.iso.mk e).hom = ↑e
@[simp]
@[simp]
order_dual
as a functor.
Equations
- NonemptyFinLinOrd.to_dual = {obj := λ (X : NonemptyFinLinOrd), NonemptyFinLinOrd.of (order_dual ↥X), map := λ (X Y : NonemptyFinLinOrd), ⇑order_hom.dual, map_id' := NonemptyFinLinOrd.to_dual._proof_1, map_comp' := NonemptyFinLinOrd.to_dual._proof_2}
The equivalence between FinPartialOrder
and itself induced by order_dual
both ways.
Equations
- NonemptyFinLinOrd.dual_equiv = category_theory.equivalence.mk NonemptyFinLinOrd.to_dual NonemptyFinLinOrd.to_dual (category_theory.nat_iso.of_components (λ (X : NonemptyFinLinOrd), NonemptyFinLinOrd.iso.mk (order_iso.dual_dual ↥X)) NonemptyFinLinOrd.dual_equiv._proof_1) (category_theory.nat_iso.of_components (λ (X : NonemptyFinLinOrd), NonemptyFinLinOrd.iso.mk (order_iso.dual_dual ↥X)) NonemptyFinLinOrd.dual_equiv._proof_2)