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

PartOrd = CategoryTheory.Bundled PartialOrder

Instances For

source

instance PartOrd.instParentProjectionPreorderPartialOrderToPreorder :

CategoryTheory.BundledHom.ParentProjection @PartialOrder.toPreorder

source

instance instPartOrdLargeCategory :

CategoryTheory.LargeCategory PartOrd

Equations

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

source

instance PartOrd.instHasForget :

CategoryTheory.HasForget PartOrd

Equations

PartOrd.instHasForget = CategoryTheory.BundledHom.hasForget (CategoryTheory.BundledHom.MapHom OrderHom @PartialOrder.toPreorder)

source

instance PartOrd.instCoeSortType :

CoeSort PartOrd (Type u_1)

Equations

PartOrd.instCoeSortType = CategoryTheory.Bundled.coeSort

source

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

PartOrd

Construct a bundled PartOrd from the underlying type and typeclass.

Equations

PartOrd.of α = CategoryTheory.Bundled.of α

Instances For

source

@[simp]

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

↑(of α) = α

source

instance PartOrd.instInhabited :

Inhabited PartOrd

Equations

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

source

instance PartOrd.instPartialOrderα (α : PartOrd) :

PartialOrder ↑α

Equations

α.instPartialOrderα = α.str

source

instance PartOrd.hasForgetToPreord :

CategoryTheory.HasForget₂ PartOrd Preord

Equations

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

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

Instances For

source

@[simp]

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

(mk e).inv = ↑e.symm

source

@[simp]

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

(mk e).hom = ↑e

source

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 }

Instances For

source

@[simp]

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

dual.map a = OrderHom.dual a

source

@[simp]

theorem PartOrd.dual_obj (X : PartOrd) :

dual.obj X = of (↑X)ᵒᵈ

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.

Instances For

source

@[simp]

theorem PartOrd.dualEquiv_functor :

dualEquiv.functor = dual

source

@[simp]

theorem PartOrd.dualEquiv_inverse :

dualEquiv.inverse = 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.

Instances For

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.

Instances For

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.

Instances For

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

Documentation

Mathlib.Order.Category.PartOrd

Category of partial orders #