Category of partial orders #
This defines PartOrd
, the category of partial orders with monotone maps.
The category of partially ordered types.
Equations
Instances For
Equations
- PartOrd.instCoeSortType = CategoryTheory.Bundled.coeSort
Construct a bundled PartOrd from the underlying type and typeclass.
Equations
Instances For
Equations
- PartOrd.instInhabited = { default := PartOrd.of PUnit.{?u.3 + 1} }
Equations
- α.instPartialOrderα = α.str
@[simp]
@[simp]
theorem
PartOrd.Iso.mk_inv
{α : PartOrd}
{β : PartOrd}
(e : ↑α ≃o ↑β)
:
(PartOrd.Iso.mk e).inv = ↑e.symm
Constructs an equivalence between partial orders from an order isomorphism between them.
Equations
- PartOrd.Iso.mk e = { hom := ↑e, inv := ↑e.symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
@[simp]
OrderDual
as a functor.
Equations
- PartOrd.dual = { obj := fun (X : PartOrd) => PartOrd.of (↑X)ᵒᵈ, map := fun {X Y : PartOrd} => ⇑OrderHom.dual, map_id := PartOrd.dual.proof_1, map_comp := @PartOrd.dual.proof_2 }
Instances For
Antisymmetrization
as a functor. It is the free functor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
preordToPartOrd
is left adjoint to the forgetful functor, meaning it is the free
functor from Preord
to PartOrd
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_coe
(X : Preord)
(a : ↑((Preord.dual.comp preordToPartOrd).obj X))
:
(preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd.inv.app X) a = (OrderIso.dualAntisymmetrization ↑X).symm a
theorem
preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_hom_app_coe
(X : Preord)
(a : ↑((preordToPartOrd.comp PartOrd.dual).obj X))
:
(preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd.hom.app X) a = (OrderIso.dualAntisymmetrization ↑X) a
def
preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd :
preordToPartOrd.comp PartOrd.dual ≅ Preord.dual.comp preordToPartOrd
PreordToPartOrd
and OrderDual
commute.
Equations
- One or more equations did not get rendered due to their size.