Category of partial orders

This defines PartOrd, the category of partial orders with monotone maps.

def PartOrd : Type (u_1 + 1)

The category of partially ordered types.

Equations

• PartOrd = CategoryTheory.Bundled PartialOrder

instance PartOrd.instParentProjectionPreorderPartialOrderToPreorder : CategoryTheory.BundledHom.ParentProjection @PartialOrder.toPreorder

instance instPartOrdLargeCategory : CategoryTheory.LargeCategory PartOrd

Equations

• instPartOrdLargeCategory = CategoryTheory.BundledHom.category (CategoryTheory.BundledHom.MapHom OrderHom @PartialOrder.toPreorder)

instance PartOrd.instConcreteCategory : CategoryTheory.ConcreteCategory PartOrd

Equations

• PartOrd.instConcreteCategory = CategoryTheory.BundledHom.concreteCategory (CategoryTheory.BundledHom.MapHom OrderHom @PartialOrder.toPreorder)

instance PartOrd.instCoeSortType : CoeSort PartOrd (Type u_1)

Equations

• PartOrd.instCoeSortType = CategoryTheory.Bundled.coeSort

def PartOrd.of (α : Type u_1) [PartialOrder α] : PartOrd

Construct a bundled PartOrd from the underlying type and typeclass.

Equations

• PartOrd.of α = CategoryTheory.Bundled.of α

@[simp]

theorem PartOrd.coe_of (α : Type u_1) [PartialOrder α] : ↑(PartOrd.of α) = α

instance PartOrd.instInhabited : Inhabited PartOrd

Equations

• PartOrd.instInhabited = { default := PartOrd.of PUnit.{?u.3 + 1} }

instance PartOrd.instPartialOrderα (α : PartOrd) : PartialOrder ↑α

Equations

• α.instPartialOrderα = α.str

instance PartOrd.hasForgetToPreord : CategoryTheory.HasForget₂ PartOrd Preord

Equations

• PartOrd.hasForgetToPreord = CategoryTheory.BundledHom.forget₂ OrderHom @PartialOrder.toPreorder

def PartOrd.Iso.mk {α β : PartOrd} (e : ↑α ≃o ↑β) : α ≅ β

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 := ⋯ }

@[simp]

theorem PartOrd.Iso.mk_inv {α β : PartOrd} (e : ↑α ≃o ↑β) : (PartOrd.Iso.mk e).inv = ↑e.symm

@[simp]

theorem PartOrd.Iso.mk_hom {α β : PartOrd} (e : ↑α ≃o ↑β) : (PartOrd.Iso.mk e).hom = ↑e

def PartOrd.dual : CategoryTheory.Functor PartOrd PartOrd

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 }

@[simp]

theorem PartOrd.dual_obj (X : PartOrd) : PartOrd.dual.obj X = PartOrd.of (↑X)ᵒᵈ

@[simp]

theorem PartOrd.dual_map {X✝ Y✝ : PartOrd} (a : ↑X✝ →o ↑Y✝) : PartOrd.dual.map a = OrderHom.dual a

def PartOrd.dualEquiv : PartOrd ≌ PartOrd

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem PartOrd.dualEquiv_inverse : PartOrd.dualEquiv.inverse = PartOrd.dual

@[simp]

theorem PartOrd.dualEquiv_functor : PartOrd.dualEquiv.functor = PartOrd.dual

theorem partOrd_dual_comp_forget_to_preord : PartOrd.dual.comp (CategoryTheory.forget₂ PartOrd Preord) = (CategoryTheory.forget₂ PartOrd Preord).comp Preord.dual

def preordToPartOrd : CategoryTheory.Functor Preord PartOrd

Antisymmetrization as a functor. It is the free functor.

Equations

• One or more equations did not get rendered due to their size.

def preordToPartOrdForgetAdjunction : preordToPartOrd ⊣ CategoryTheory.forget₂ PartOrd Preord

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.

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.

@[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