Documentation

Mathlib.Order.Category.NonemptyFinLinOrd

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.

Note: NonemptyFinLinOrd is not a subcategory of FinBddDistLat because its morphisms do not preserve and .

structure NonemptyFinLinOrdextends LinOrd :
Type (u_1 + 1)

The category of nonempty finite linear orders.

@[reducible, inline]

Construct a bundled NonemptyFinLinOrd from the underlying type and typeclass.

Equations
theorem NonemptyFinLinOrd.coe_of (α : Type u_1) [Nonempty α] [Fintype α] [LinearOrder α] :
(of α).toLinOrd = α
@[reducible, inline]
abbrev NonemptyFinLinOrd.ofHom {X Y : Type u} [Nonempty X] [LinearOrder X] [Fintype X] [Nonempty Y] [LinearOrder Y] [Fintype Y] (f : X →o Y) :
of X of Y

Typecheck a OrderHom as a morphism in NonemptyFinLinOrd.

Equations
@[simp]
Equations
  • One or more equations did not get rendered due to their size.
def NonemptyFinLinOrd.Iso.mk {α β : NonemptyFinLinOrd} (e : α.toLinOrd ≃o β.toLinOrd) :
α β

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

Equations
@[simp]
theorem NonemptyFinLinOrd.Iso.mk_hom {α β : NonemptyFinLinOrd} (e : α.toLinOrd ≃o β.toLinOrd) :
(mk e).hom = ofHom e
@[simp]
theorem NonemptyFinLinOrd.Iso.mk_inv {α β : NonemptyFinLinOrd} (e : α.toLinOrd ≃o β.toLinOrd) :
(mk e).inv = ofHom e.symm

OrderDual as a functor.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]

The equivalence between NonemptyFinLinOrd and itself induced by OrderDual both ways.

Equations
  • One or more equations did not get rendered due to their size.
def Fin.hom_succ {n : } (i : Fin n) :

The generating arrow i ⟶ i+1 in the category Fin n

Equations