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.instParentProjectionTypePreorderPartialOrderToPreorder : CategoryTheory.BundledHom.ParentProjection @PartialOrder.toPreorder

Equations

• PartOrd.instParentProjectionTypePreorderPartialOrderToPreorder = (_ : CategoryTheory.BundledHom.ParentProjection @PartialOrder.toPreorder)

instance PartOrd.instConcreteCategoryPartOrdInstPartOrdLargeCategory : CategoryTheory.ConcreteCategory PartOrd

Equations

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

instance PartOrd.instCoeSortPartOrdType : CoeSort PartOrd (Type u_1)

Equations

• PartOrd.instCoeSortPartOrdType = 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.instInhabitedPartOrd : Inhabited PartOrd

Equations

• PartOrd.instInhabitedPartOrd = { default := PartOrd.of PUnit.{u_1 + 1} }

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

Equations

• PartOrd.instPartialOrderα α = α.str

instance PartOrd.hasForgetToPreord : CategoryTheory.HasForget₂ PartOrd Preord

Equations

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

@[simp]

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

@[simp]

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

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

Constructs an equivalence between partial orders from an order isomorphism between them.

Equations

• PartOrd.Iso.mk e = CategoryTheory.Iso.mk ↑e ↑(OrderIso.symm e)

@[simp]

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

@[simp]

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

def PartOrd.dual : CategoryTheory.Functor PartOrd PartOrd

OrderDual as a functor.

Equations

• PartOrd.dual = CategoryTheory.Functor.mk { obj := fun (X : PartOrd) => PartOrd.of (↑X)ᵒᵈ, map := fun {X Y : PartOrd} => ⇑OrderHom.dual }

@[simp]

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

@[simp]

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

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.

theorem partOrd_dual_comp_forget_to_preord : CategoryTheory.Functor.comp PartOrd.dual (CategoryTheory.forget₂ PartOrd Preord) = CategoryTheory.Functor.comp (CategoryTheory.forget₂ PartOrd Preord) 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

Preord_to_PartOrd 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.

@[simp]

theorem preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_coe (X : Preord) (a : ↑((CategoryTheory.Functor.comp Preord.dual preordToPartOrd).toPrefunctor.obj X)) : (preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd.inv.app X) a = (OrderIso.symm (OrderIso.dualAntisymmetrization ↑X)) a

theorem preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_hom_app_coe (X : Preord) (a : ↑((CategoryTheory.Functor.comp preordToPartOrd PartOrd.dual).toPrefunctor.obj X)) : (preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd.hom.app X) a = (OrderIso.dualAntisymmetrization ↑X) a

def preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd : CategoryTheory.Functor.comp preordToPartOrd PartOrd.dual ≅ CategoryTheory.Functor.comp Preord.dual preordToPartOrd

PreordToPartOrd and OrderDual commute.

Equations

• preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd = CategoryTheory.NatIso.ofComponents fun (x : Preord) => PartOrd.Iso.mk (OrderIso.dualAntisymmetrization ↑x)