Category of partial orders, with order embeddings as morphisms

This defines PartOrdEmb, the category of partial orders with order embeddings as morphisms. We also show that PartOrdEmb has filtered colimits.

structure PartOrdEmb : Type (u_1 + 1)

The category of partial orders.

• of :: (
• carrier : Type u_1

  The underlying partially ordered type.

• str : PartialOrder ↑self
• )

@[implicit_reducible]

instance PartOrdEmb.instCoeSortType : CoeSort PartOrdEmb (Type u_1)

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

The type of morphisms in PartOrdEmb R.

• hom' : ↑X ↪o ↑Y

  The underlying OrderEmbedding.

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

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

@[implicit_reducible]

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

@[implicit_reducible]

instance PartOrdEmb.instConcreteCategoryOrderEmbeddingCarrier : CategoryTheory.ConcreteCategory PartOrdEmb fun (x1 x2 : PartOrdEmb) => ↑x1 ↪o ↑x2

@[reducible, inline]

abbrev PartOrdEmb.Hom.hom {X Y : PartOrdEmb} (f : X.Hom Y) : ↑X ↪o ↑Y

Turn a morphism in PartOrdEmb back into a OrderEmbedding.

@[reducible, inline]

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

Typecheck a OrderEmbedding as a morphism in PartOrdEmb.

def PartOrdEmb.Hom.Simps.hom (X Y : PartOrdEmb) (f : X.Hom Y) : ↑X ↪o ↑Y

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

theorem PartOrdEmb.hom_id {X : PartOrdEmb} : Hom.hom (CategoryTheory.CategoryStruct.id X) = RelEmbedding.refl fun (x1 x2 : ↑X) => x1 ≤ x2

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

@[simp]

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

theorem PartOrdEmb.comp_apply {X Y Z : PartOrdEmb} (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 PartOrdEmb.Hom.injective {X Y : PartOrdEmb} (f : X ⟶ Y) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f)

theorem PartOrdEmb.Hom.le_iff_le {X Y : PartOrdEmb} (f : X ⟶ Y) (x₁ x₂ : ↑X) : (CategoryTheory.ConcreteCategory.hom f) x₁ ≤ (CategoryTheory.ConcreteCategory.hom f) x₂ ↔ x₁ ≤ x₂

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem PartOrdEmb.ofHom_id {X : Type u} [PartialOrder X] : ofHom (RelEmbedding.refl fun (x1 x2 : X) => x1 ≤ x2) = CategoryTheory.CategoryStruct.id { carrier := X, str := inst✝ }

@[simp]

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

theorem PartOrdEmb.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 PartOrdEmb.inv_hom_apply {X Y : PartOrdEmb} (e : X ≅ Y) (x : ↑X) : (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x

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

@[implicit_reducible]

instance PartOrdEmb.hasForgetToPartOrd : CategoryTheory.HasForget₂ PartOrdEmb PartOrd

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

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

@[simp]

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

@[simp]

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

def PartOrdEmb.dual : CategoryTheory.Functor PartOrdEmb PartOrdEmb

OrderDual as a functor.

@[simp]

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

def PartOrdEmb.dualEquiv : PartOrdEmb ≌ PartOrdEmb

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

@[simp]

theorem PartOrdEmb.dualEquiv_inverse : dualEquiv.inverse = dual

@[simp]

theorem PartOrdEmb.dualEquiv_functor : dualEquiv.functor = dual

theorem partOrdEmb_dual_comp_forget_to_pardOrd : PartOrdEmb.dual.comp (CategoryTheory.forget₂ PartOrdEmb PartOrd) = (CategoryTheory.forget₂ PartOrdEmb PartOrd).comp PartOrd.dual

def PartOrdEmb.Limits.CoconePt {J : Type u} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J PartOrdEmb} {c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget PartOrdEmb))} : CategoryTheory.Limits.IsColimit c → Type u

Given a functor F : J ⥤ PartOrdEmb and a colimit cocone c for F ⋙ forget _, this is the type c.pt on which we define a partial order which makes it the colimit of F.

@[implicit_reducible]

instance PartOrdEmb.Limits.instPartialOrderCoconePt {J : Type u} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] {F : CategoryTheory.Functor J PartOrdEmb} {c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget PartOrdEmb))} (hc : CategoryTheory.Limits.IsColimit c) : PartialOrder (CoconePt hc)

def PartOrdEmb.Limits.cocone {J : Type u} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] {F : CategoryTheory.Functor J PartOrdEmb} {c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget PartOrdEmb))} (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Limits.Cocone F

The colimit cocone for a functor F : J ⥤ PartOrdEmb from a filtered category that is constructed from a colimit cocone for F ⋙ forget _.

@[simp]

theorem PartOrdEmb.Limits.cocone_ι_app {J : Type u} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] {F : CategoryTheory.Functor J PartOrdEmb} {c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget PartOrdEmb))} (hc : CategoryTheory.Limits.IsColimit c) (j : J) : (cocone hc).ι.app j = ofHom { toFun := c.ι.app j, inj' := ⋯, map_rel_iff' := ⋯ }

@[simp]

theorem PartOrdEmb.Limits.cocone_pt_coe {J : Type u} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] {F : CategoryTheory.Functor J PartOrdEmb} {c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget PartOrdEmb))} (hc : CategoryTheory.Limits.IsColimit c) : ↑(cocone hc).pt = CoconePt hc

def PartOrdEmb.Limits.CoconePt.desc {J : Type u} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] {F : CategoryTheory.Functor J PartOrdEmb} {c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget PartOrdEmb))} (hc : CategoryTheory.Limits.IsColimit c) (s : CategoryTheory.Limits.Cocone F) : CoconePt hc ↪o ↑s.pt

Auxiliary definition for isColimitCocone.

@[simp]

theorem PartOrdEmb.Limits.CoconePt.fac_apply {J : Type u} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] {F : CategoryTheory.Functor J PartOrdEmb} {c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget PartOrdEmb))} (hc : CategoryTheory.Limits.IsColimit c) (s : CategoryTheory.Limits.Cocone F) (j : J) (x : ↑(F.obj j)) : (desc hc s) (c.ι.app j x) = (CategoryTheory.ConcreteCategory.hom (s.ι.app j)) x

def PartOrdEmb.Limits.isColimitCocone {J : Type u} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] {F : CategoryTheory.Functor J PartOrdEmb} {c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget PartOrdEmb))} (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Limits.IsColimit (cocone hc)

A colimit cocone for F : J ⥤ PartOrdEmb (with J filtered) can be obtained from a colimit cocone for F ⋙ forget _.

instance PartOrdEmb.Limits.instHasColimit {J : Type u} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] {F : CategoryTheory.Functor J PartOrdEmb} : CategoryTheory.Limits.HasColimit F

instance PartOrdEmb.Limits.instPreservesColimitForgetOrderEmbeddingCarrier {J : Type u} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] {F : CategoryTheory.Functor J PartOrdEmb} : CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget PartOrdEmb)

instance PartOrdEmb.Limits.instHasColimitsOfShape {J : Type u} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] : CategoryTheory.Limits.HasColimitsOfShape J PartOrdEmb

instance PartOrdEmb.Limits.instPreservesColimitsOfShapeForgetOrderEmbeddingCarrier {J : Type u} [CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J] : CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.forget PartOrdEmb)

instance PartOrdEmb.Limits.instHasFilteredColimitsOfSize : CategoryTheory.Limits.HasFilteredColimitsOfSize.{u, u, u, u + 1} PartOrdEmb

instance PartOrdEmb.Limits.instPreservesFilteredColimitsOfSizeForgetOrderEmbeddingCarrier : CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{u, u, u, u, u + 1, u + 1} (CategoryTheory.forget PartOrdEmb)