The category of bounded orders

This defines BddOrd, the category of bounded orders.

structure BddOrdextends PartOrd : Type (u_1 + 1)

The category of bounded orders with monotone functions.

• carrier : Type u_1
• str : PartialOrder ↑self.toPartOrd
• isBoundedOrder : BoundedOrder ↑self.toPartOrd

instance BddOrd.instCoeSortType : CoeSort BddOrd (Type u_1)

Equations

• BddOrd.instCoeSortType = CategoryTheory.InducedCategory.hasCoeToSort BddOrd.toPartOrd

@[reducible, inline]

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

Construct a bundled BddOrd from the underlying type and typeclass.

Equations

• BddOrd.of X = BddOrd.mk (PartOrd.mk X)

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

The type of morphisms in BddOrd R.

• hom' : BoundedOrderHom ↑X.toPartOrd ↑Y.toPartOrd

  The underlying BoundedOrderHom.

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

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

Equations

• BddOrd.instCategory = CategoryTheory.Category.mk @BddOrd.instCategory.proof_1 @BddOrd.instCategory.proof_2 @BddOrd.instCategory.proof_3

instance BddOrd.instConcreteCategoryBoundedOrderHomCarrier : CategoryTheory.ConcreteCategory BddOrd fun (x1 x2 : BddOrd) => BoundedOrderHom ↑x1.toPartOrd ↑x2.toPartOrd

Equations

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

@[reducible, inline]

abbrev BddOrd.Hom.hom {X Y : BddOrd} (f : X.Hom Y) : BoundedOrderHom ↑X.toPartOrd ↑Y.toPartOrd

Turn a morphism in BddOrd back into a BoundedOrderHom.

Equations

• f.hom = CategoryTheory.ConcreteCategory.hom f

@[reducible, inline]

abbrev BddOrd.ofHom {X Y : Type u} [PartialOrder X] [BoundedOrder X] [PartialOrder Y] [BoundedOrder Y] (f : BoundedOrderHom X Y) : of X ⟶ of Y

Typecheck a BoundedOrderHom as a morphism in BddOrd.

Equations

• BddOrd.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

def BddOrd.Hom.Simps.hom (X Y : BddOrd) (f : X.Hom Y) : BoundedOrderHom ↑X.toPartOrd ↑Y.toPartOrd

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

Equations

• BddOrd.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 BddOrd.coe_id {X : BddOrd} : ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id

@[simp]

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

@[simp]

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

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

theorem BddOrd.coe_of (X : Type u) [PartialOrder X] [BoundedOrder X] : ↑(of X).toPartOrd = X

@[simp]

theorem BddOrd.hom_id {X : BddOrd} : Hom.hom (CategoryTheory.CategoryStruct.id X) = BoundedOrderHom.id ↑X.toPartOrd

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

@[simp]

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

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

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

@[simp]

theorem BddOrd.hom_ofHom {X Y : Type u} [PartialOrder X] [BoundedOrder X] [PartialOrder Y] [BoundedOrder Y] (f : BoundedOrderHom X Y) : Hom.hom (ofHom f) = f

@[simp]

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

@[simp]

theorem BddOrd.ofHom_id {X : Type u} [PartialOrder X] [BoundedOrder X] : ofHom (BoundedOrderHom.id X) = CategoryTheory.CategoryStruct.id (of X)

@[simp]

theorem BddOrd.ofHom_comp {X Y Z : Type u} [PartialOrder X] [BoundedOrder X] [PartialOrder Y] [BoundedOrder Y] [PartialOrder Z] [BoundedOrder Z] (f : BoundedOrderHom X Y) (g : BoundedOrderHom Y Z) : ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (ofHom f) (ofHom g)

theorem BddOrd.ofHom_apply {X Y : Type u} [PartialOrder X] [BoundedOrder X] [PartialOrder Y] [BoundedOrder Y] (f : BoundedOrderHom X Y) (x : X) : (CategoryTheory.ConcreteCategory.hom (ofHom f)) x = f x

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

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

instance BddOrd.instInhabited : Inhabited BddOrd

Equations

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

instance BddOrd.hasForgetToPartOrd : CategoryTheory.HasForget₂ BddOrd PartOrd

Equations

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

instance BddOrd.hasForgetToBipointed : CategoryTheory.HasForget₂ BddOrd Bipointed

Equations

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

def BddOrd.dual : CategoryTheory.Functor BddOrd BddOrd

OrderDual as a functor.

Equations

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

@[simp]

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

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

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

Equations

• BddOrd.Iso.mk e = { hom := BddOrd.ofHom ↑e, inv := BddOrd.ofHom ↑e.symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

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

@[simp]

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

def BddOrd.dualEquiv : BddOrd ≌ BddOrd

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

Equations

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

@[simp]

theorem BddOrd.dualEquiv_functor : dualEquiv.functor = dual

@[simp]

theorem BddOrd.dualEquiv_inverse : dualEquiv.inverse = dual

theorem bddOrd_dual_comp_forget_to_partOrd : BddOrd.dual.comp (CategoryTheory.forget₂ BddOrd PartOrd) = (CategoryTheory.forget₂ BddOrd PartOrd).comp PartOrd.dual

theorem bddOrd_dual_comp_forget_to_bipointed : BddOrd.dual.comp (CategoryTheory.forget₂ BddOrd Bipointed) = (CategoryTheory.forget₂ BddOrd Bipointed).comp Bipointed.swap