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
Equations
- FinPartOrd.instCoeSortType = { coe := fun (X : FinPartOrd) => ↑X.toPartOrd }
Equations
- X.instPartialOrderαToPartOrd = X.toPartOrd.str
Construct a bundled FinPartOrd
from PartialOrder
+ Fintype
.
Equations
- FinPartOrd.of α = FinPartOrd.mk { α := α, str := inferInstance }
Instances For
@[simp]
theorem
FinPartOrd.coe_of
(α : Type u_1)
[PartialOrder α]
[Fintype α]
:
↑(FinPartOrd.of α).toPartOrd = α
Equations
- FinPartOrd.instInhabited = { default := FinPartOrd.of PUnit.{?u.3 + 1} }
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
FinPartOrd.Iso.mk_inv
{α : FinPartOrd}
{β : FinPartOrd}
(e : ↑α.toPartOrd ≃o ↑β.toPartOrd)
:
(FinPartOrd.Iso.mk e).inv = ↑e.symm
@[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.
Equations
- FinPartOrd.Iso.mk e = { hom := ↑e, inv := ↑e.symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
@[simp]
theorem
FinPartOrd.dual_obj
(X : FinPartOrd)
:
FinPartOrd.dual.obj X = FinPartOrd.of (↑X.toPartOrd)ᵒᵈ
@[simp]
theorem
FinPartOrd.dual_map
{X : FinPartOrd}
{Y : FinPartOrd}
(a : ↑X.toPartOrd →o ↑Y.toPartOrd)
:
FinPartOrd.dual.map a = OrderHom.dual a
OrderDual
as a functor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
FinPartOrd.dualEquiv_unitIso :
FinPartOrd.dualEquiv.unitIso = CategoryTheory.NatIso.ofComponents (fun (X : FinPartOrd) => FinPartOrd.Iso.mk (OrderIso.dualDual ↑X.toPartOrd))
@FinPartOrd.dualEquiv.proof_1
@[simp]
theorem
FinPartOrd.dualEquiv_counitIso :
FinPartOrd.dualEquiv.counitIso = CategoryTheory.NatIso.ofComponents (fun (X : FinPartOrd) => FinPartOrd.Iso.mk (OrderIso.dualDual ↑X.toPartOrd))
@FinPartOrd.dualEquiv.proof_2
The equivalence between FinPartOrd
and itself induced by OrderDual
both ways.
Equations
- One or more equations did not get rendered due to their size.