Documentation

Mathlib.Order.Category.PartOrd

Category of partial orders #

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

source
def PartOrd :
Type (u_1 + 1)

The category of partially ordered types.

Equations
source
instance PartOrd.instParentProjectionPreorderPartialOrderToPreorder :
CategoryTheory.BundledHom.ParentProjection @PartialOrder.toPreorder
Equations
source
instance instPartOrdLargeCategory :
CategoryTheory.LargeCategory PartOrd
Equations
source
instance PartOrd.instConcreteCategory :
CategoryTheory.ConcreteCategory PartOrd
Equations
source
instance PartOrd.instCoeSortType :
CoeSort PartOrd (Type u_1)
Equations
source
def PartOrd.of (α : Type u_1) [PartialOrder α] :
PartOrd

Construct a bundled PartOrd from the underlying type and typeclass.

Equations
source
@[simp]
theorem PartOrd.coe_of (α : Type u_1) [PartialOrder α] :
↑(PartOrd.of α) = α
source
instance PartOrd.instInhabited :
Inhabited PartOrd
Equations
source
instance PartOrd.instPartialOrderα (α : PartOrd) :
PartialOrder ↑α
Equations
  • α.instPartialOrderα = α.str
source
instance PartOrd.hasForgetToPreord :
CategoryTheory.HasForget₂ PartOrd Preord
Equations
source
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 := ⋯ }
source
@[simp]
theorem PartOrd.Iso.mk_inv {α β : PartOrd} (e : ↑α ≃o ↑β) :
(PartOrd.Iso.mk e).inv = ↑e.symm
source
@[simp]
theorem PartOrd.Iso.mk_hom {α β : PartOrd} (e : ↑α ≃o ↑β) :
(PartOrd.Iso.mk e).hom = ↑e
source
def PartOrd.dual :
CategoryTheory.Functor PartOrd PartOrd

OrderDual as a functor.

Equations
source
@[simp]
theorem PartOrd.dual_obj (X : PartOrd) :
PartOrd.dual.obj X = PartOrd.of (↑X)ᵒᵈ
source
@[simp]
theorem PartOrd.dual_map {X✝ Y✝ : PartOrd} (a : ↑X✝ →o ↑Y✝) :
PartOrd.dual.map a = OrderHom.dual a
source
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.
source
@[simp]
theorem PartOrd.dualEquiv_inverse :
PartOrd.dualEquiv.inverse = PartOrd.dual
source
@[simp]
theorem PartOrd.dualEquiv_functor :
PartOrd.dualEquiv.functor = PartOrd.dual
source
theorem partOrd_dual_comp_forget_to_preord :
PartOrd.dual.comp (CategoryTheory.forget₂ PartOrd Preord) = (CategoryTheory.forget₂ PartOrd Preord).comp Preord.dual
source
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.
source
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.
source
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.
source
@[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
source
theorem preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_hom_app_coe (X : Preord) (a : ↑((preordToPartOrd.comp PartOrd.dual).obj X)) :
(preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd.hom.app X) a = (OrderIso.dualAntisymmetrization ↑X) a