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.
Instances of this typeclass
Instances of other typeclasses for nonempty_fin_lin_ord
- nonempty_fin_lin_ord.has_sizeof_inst
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
- fin.nonempty_fin_lin_ord n = {to_fintype := fin.fintype (n + 1), to_linear_order := fin.linear_order (n + 1), nonempty := _}
@[protected, instance]
Equations
- ulift.nonempty_fin_lin_ord α = {to_fintype := ulift.fintype α nonempty_fin_lin_ord.to_fintype, 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 := linear_order.max (linear_order.lift' ⇑equiv.ulift _), max_def := _, min := linear_order.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.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]
def
NonemptyFinLinOrd.nonempty_fin_lin_ord.to_linear_order.category_theory.bundled_hom.parent_projection
:
Equations
- NonemptyFinLinOrd.nonempty_fin_lin_ord.to_linear_order.category_theory.bundled_hom.parent_projection = category_theory.bundled_hom.parent_projection.mk
@[protected, instance]
@[protected, instance]
@[protected, instance]
Construct a bundled NonemptyFinLinOrd
from the underlying type and typeclass.
Equations
@[simp]
theorem
NonemptyFinLinOrd.coe_of
(α : Type u_1)
[nonempty_fin_lin_ord α] :
↥(NonemptyFinLinOrd.of α) = α
@[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.dual = {obj := λ (X : NonemptyFinLinOrd), NonemptyFinLinOrd.of (↥X)ᵒᵈ, map := λ (X Y : NonemptyFinLinOrd), ⇑order_hom.dual, map_id' := NonemptyFinLinOrd.dual._proof_1, map_comp' := NonemptyFinLinOrd.dual._proof_2}
The equivalence between FinPartialOrder
and itself induced by order_dual
both ways.
Equations
- NonemptyFinLinOrd.dual_equiv = category_theory.equivalence.mk NonemptyFinLinOrd.dual NonemptyFinLinOrd.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)