Category of partial orders

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

structure PartOrd : Type (u_1 + 1)

The category of partial orders.

• of :: (
• carrier : Type u_1

  The underlying partially ordered type.

• str : PartialOrder ↑self
• )

instance PartOrd.instCoeSortType : CoeSort PartOrd (Type u_1)

Equations

• PartOrd.instCoeSortType = { coe := PartOrd.carrier }

structure PartOrd.Hom (X Y : PartOrd) : Type u

The type of morphisms in PartOrd R.

• hom' : ↑X →o ↑Y

  The underlying OrderHom.

theorem PartOrd.Hom.ext_iff {X Y : PartOrd} {x y : X.Hom Y} : x = y ↔ x.hom' = y.hom'

theorem PartOrd.Hom.ext {X Y : PartOrd} {x y : X.Hom Y} (hom' : x.hom' = y.hom') : x = y

instance PartOrd.instCategory : CategoryTheory.Category.{u, u + 1} PartOrd

Equations

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

instance PartOrd.instConcreteCategoryOrderHomCarrier : CategoryTheory.ConcreteCategory PartOrd fun (x1 x2 : PartOrd) => ↑x1 →o ↑x2

Equations

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

@[reducible, inline]

abbrev PartOrd.Hom.hom {X Y : PartOrd} (f : X.Hom Y) : ↑X →o ↑Y

Turn a morphism in PartOrd back into a OrderHom.

Equations

• f.hom = CategoryTheory.ConcreteCategory.hom f

@[reducible, inline]

abbrev PartOrd.ofHom {X Y : Type u} [PartialOrder X] [PartialOrder Y] (f : X →o Y) : { carrier := X, str := inst✝ } ⟶ { carrier := Y, str := inst✝¹ }

Typecheck a OrderHom as a morphism in PartOrd.

Equations

• PartOrd.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

def PartOrd.Hom.Simps.hom (X Y : PartOrd) (f : X.Hom Y) : ↑X →o ↑Y

Use the ConcreteCategory.hom projection for @[simps] lemmas.

Equations

• PartOrd.Hom.Simps.hom X Y f = f.hom

The results below duplicate the ConcreteCategory simp lemmas, but we can keep them for dsimp.

@[simp]

theorem PartOrd.coe_id {X : PartOrd} : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id

@[simp]

theorem PartOrd.coe_comp {X Y Z : PartOrd} {f : X ⟶ Y} {g : Y ⟶ Z} : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) = ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)

@[simp]

theorem PartOrd.forget_map {X Y : PartOrd} (f : X ⟶ Y) : (CategoryTheory.forget PartOrd).map f = ⇑(CategoryTheory.ConcreteCategory.hom f)

theorem PartOrd.ext {X Y : PartOrd} {f g : X ⟶ Y} (w : ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) : f = g

theorem PartOrd.ext_iff {X Y : PartOrd} {f g : X ⟶ Y} : f = g ↔ ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x

theorem PartOrd.coe_of (X : Type u) [PartialOrder X] : ↑{ carrier := X, str := inst✝ } = X

@[simp]

theorem PartOrd.hom_id {X : PartOrd} : Hom.hom (CategoryTheory.CategoryStruct.id X) = OrderHom.id

theorem PartOrd.id_apply (X : PartOrd) (x : ↑X) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x

@[simp]

theorem PartOrd.hom_comp {X Y Z : PartOrd} (f : X ⟶ Y) (g : Y ⟶ Z) : Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (Hom.hom g).comp (Hom.hom f)

theorem PartOrd.comp_apply {X Y Z : PartOrd} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑X) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x = (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)

theorem PartOrd.hom_ext {X Y : PartOrd} {f g : X ⟶ Y} (hf : Hom.hom f = Hom.hom g) : f = g

theorem PartOrd.hom_ext_iff {X Y : PartOrd} {f g : X ⟶ Y} : f = g ↔ Hom.hom f = Hom.hom g

@[simp]

theorem PartOrd.hom_ofHom {X Y : Type u} [PartialOrder X] [PartialOrder Y] (f : X →o Y) : Hom.hom (ofHom f) = f

@[simp]

theorem PartOrd.ofHom_hom {X Y : PartOrd} (f : X ⟶ Y) : ofHom (Hom.hom f) = f

@[simp]

theorem PartOrd.ofHom_id {X : Type u} [PartialOrder X] : ofHom OrderHom.id = CategoryTheory.CategoryStruct.id { carrier := X, str := inst✝ }

@[simp]

theorem PartOrd.ofHom_comp {X Y Z : Type u} [PartialOrder X] [PartialOrder Y] [PartialOrder Z] (f : X →o Y) (g : Y →o Z) : ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (ofHom f) (ofHom g)

theorem PartOrd.ofHom_apply {X Y : Type u} [PartialOrder X] [PartialOrder Y] (f : X →o Y) (x : X) : (CategoryTheory.ConcreteCategory.hom (ofHom f)) x = f x

theorem PartOrd.inv_hom_apply {X Y : PartOrd} (e : X ≅ Y) (x : ↑X) : (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x

theorem PartOrd.hom_inv_apply {X Y : PartOrd} (e : X ≅ Y) (s : ↑Y) : (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s

instance PartOrd.hasForgetToPreord : CategoryTheory.HasForget₂ PartOrd Preord

Equations

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

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 := PartOrd.ofHom ↑e, inv := PartOrd.ofHom ↑e.symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

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

@[simp]

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

def PartOrd.dual : CategoryTheory.Functor PartOrd PartOrd

OrderDual as a functor.

Equations

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

@[simp]

theorem PartOrd.dual_map {X✝ Y✝ : PartOrd} (f : X✝ ⟶ Y✝) : dual.map f = ofHom (OrderHom.dual (Hom.hom f))

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

@[simp]

theorem PartOrd.dualEquiv_functor : dualEquiv.functor = 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.

theorem preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_hom_app_hom_coe (X : Preord) (a : ↑((preordToPartOrd.comp PartOrd.dual).obj X)) : (PartOrd.Hom.hom (preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd.hom.app X)) a = (OrderIso.dualAntisymmetrization ↑X) a

theorem preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe (X : Preord) (a : ↑((Preord.dual.comp preordToPartOrd).obj X)) : (PartOrd.Hom.hom (preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd.inv.app X)) a = (OrderIso.dualAntisymmetrization ↑X).symm a

@[simp]

theorem preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe' (X : Preord) (a : ↑(preordToPartOrd.obj (Preord.dual.obj X))) : (PartOrd.Hom.hom (preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd.inv.app X)) a = (OrderIso.dualAntisymmetrization ↑X).symm a