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
• )

instance PartOrdEmb.instCoeSortType : CoeSort PartOrdEmb (Type u_1)

Equations

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

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 {X Y : PartOrdEmb} {x y : X.Hom Y} (hom' : x.hom' = y.hom') : x = y

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

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

Equations

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

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

Equations

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

@[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.

Equations

• f.hom = CategoryTheory.ConcreteCategory.hom f

@[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.

Equations

• PartOrdEmb.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

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

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

Equations

• PartOrdEmb.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 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

instance PartOrdEmb.hasForgetToPartOrd : CategoryTheory.HasForget₂ PartOrdEmb PartOrd

Equations

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

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

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

Equations

• PartOrdEmb.Iso.mk e = { hom := PartOrdEmb.ofHom (RelIso.toRelEmbedding e), inv := PartOrdEmb.ofHom (RelIso.toRelEmbedding e.symm), hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

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

@[simp]

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

def PartOrdEmb.dual : CategoryTheory.Functor PartOrdEmb PartOrdEmb

OrderDual as a functor.

Equations

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

@[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.

Equations

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

@[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.

Equations

• PartOrdEmb.Limits.CoconePt x✝ = c.pt

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)

Equations

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

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

Equations

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

@[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

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

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.

Equations

• PartOrdEmb.Limits.CoconePt.desc hc s = { toFun := hc.desc ((CategoryTheory.forget PartOrdEmb).mapCocone s), inj' := ⋯, map_rel_iff' := ⋯ }

@[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 _.

Equations

• PartOrdEmb.Limits.isColimitCocone hc = { desc := fun (s : CategoryTheory.Limits.Cocone F) => PartOrdEmb.ofHom (PartOrdEmb.Limits.CoconePt.desc hc s), fac := ⋯, uniq := ⋯ }

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.instPreservesColimitForget {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.instPreservesColimitsOfShapeForget {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.instPreservesFilteredColimitsOfSizeForget : CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{u, u, u, u, u + 1, u + 1} (CategoryTheory.forget PartOrdEmb)