Category of partial orders, with order embeddings as morphisms

This defines PartOrdEmb, the category of partial orders with order embeddings as morphisms.

structure PartOrdEmb : Type (u_1 + 1)

The category of partial orders.

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

@[reducible, inline]

abbrev PartOrdEmb.of (X : Type u_1) [PartialOrder X] : PartOrdEmb

Construct a bundled PartOrdEmb from the underlying type and typeclass.

Equations

• PartOrdEmb.of X = { carrier := X, str := inst✝ }

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) : of X ⟶ of Y

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] : ↑(of X) = 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_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 (of X)

@[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_functor : dualEquiv.functor = dual

@[simp]

theorem PartOrdEmb.dualEquiv_inverse : dualEquiv.inverse = dual

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