The category of finite partial orders #
This defines FinPartOrd
, the category of finite partial orders.
Note: FinPartOrd
is not a subcategory of BddOrd
because finite orders are not necessarily
bounded.
TODO #
FinPartOrd
is equivalent to a small category.
The category of finite partial orders with monotone functions.
Instances For
Construct a bundled FinPartOrd
from PartialOrder
+ Fintype
.
Instances For
@[simp]
theorem
FinPartOrd.coe_of
(α : Type u_1)
[PartialOrder α]
[Fintype α]
:
↑(FinPartOrd.of α).toPartOrd = α
@[simp]
theorem
FinPartOrd.Iso.mk_inv
{α : FinPartOrd}
{β : FinPartOrd}
(e : ↑α.toPartOrd ≃o ↑β.toPartOrd)
:
(FinPartOrd.Iso.mk e).inv = ↑(OrderIso.symm e)
@[simp]
theorem
FinPartOrd.Iso.mk_hom
{α : FinPartOrd}
{β : FinPartOrd}
(e : ↑α.toPartOrd ≃o ↑β.toPartOrd)
:
(FinPartOrd.Iso.mk e).hom = ↑e
Constructs an isomorphism of finite partial orders from an order isomorphism between them.
Instances For
@[simp]
theorem
FinPartOrd.dual_map
{X : FinPartOrd}
{Y : FinPartOrd}
(a : ↑X.toPartOrd →o ↑Y.toPartOrd)
:
FinPartOrd.dual.map a = ↑OrderHom.dual a
@[simp]
theorem
FinPartOrd.dual_obj
(X : FinPartOrd)
:
FinPartOrd.dual.obj X = FinPartOrd.of (↑X.toPartOrd)ᵒᵈ
OrderDual
as a functor.
Instances For
The equivalence between FinPartOrd
and itself induced by OrderDual
both ways.