The category of bounded orders

This defines BddOrd, the category of bounded orders.

structure BddOrd : Type (u_1 + 1)

The category of bounded orders with monotone functions.

• toPartOrd : PartOrd

  The underlying object in the category of partial orders.

• isBoundedOrder : BoundedOrder ↑self.toPartOrd

instance BddOrd.instCoeSortBddOrdType : CoeSort BddOrd (Type u_1)

Equations

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

instance BddOrd.instPartialOrderαToPartOrd (X : BddOrd) : PartialOrder ↑X.toPartOrd

Equations

• BddOrd.instPartialOrderαToPartOrd X = X.toPartOrd.str

def BddOrd.of (α : Type u_1) [PartialOrder α] [BoundedOrder α] : BddOrd

Construct a bundled BddOrd from a Fintype PartialOrder.

Equations

• BddOrd.of α = BddOrd.mk (CategoryTheory.Bundled.mk α)

@[simp]

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

instance BddOrd.instInhabitedBddOrd : Inhabited BddOrd

Equations

• BddOrd.instInhabitedBddOrd = { default := BddOrd.of PUnit.{u_1 + 1} }

instance BddOrd.largeCategory : CategoryTheory.LargeCategory BddOrd

Equations

• BddOrd.largeCategory = CategoryTheory.Category.mk

instance BddOrd.instFunLike (X : BddOrd) (Y : BddOrd) : FunLike (X ⟶ Y) ↑X.toPartOrd ↑Y.toPartOrd

Equations

• BddOrd.instFunLike X Y = let_fun this := inferInstance; this

instance BddOrd.concreteCategory : CategoryTheory.ConcreteCategory BddOrd

Equations

• BddOrd.concreteCategory = CategoryTheory.ConcreteCategory.mk (CategoryTheory.Functor.mk { obj := fun (x : BddOrd) => ↑x.toPartOrd, map := fun {X Y : BddOrd} => DFunLike.coe })

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.

@[simp]

theorem BddOrd.dual_map {X : BddOrd} {Y : BddOrd} (a : BoundedOrderHom ↑X.toPartOrd ↑Y.toPartOrd) : BddOrd.dual.toPrefunctor.map a = BoundedOrderHom.dual a

@[simp]

theorem BddOrd.dual_obj (X : BddOrd) : BddOrd.dual.toPrefunctor.obj X = BddOrd.of (↑X.toPartOrd)ᵒᵈ

def BddOrd.dual : CategoryTheory.Functor BddOrd BddOrd

OrderDual as a functor.

Equations

• BddOrd.dual = CategoryTheory.Functor.mk { obj := fun (X : BddOrd) => BddOrd.of (↑X.toPartOrd)ᵒᵈ, map := fun {X Y : BddOrd} => ⇑BoundedOrderHom.dual }

@[simp]

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

@[simp]

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

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

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

Equations

• BddOrd.Iso.mk e = CategoryTheory.Iso.mk ↑e ↑(OrderIso.symm e)

@[simp]

theorem BddOrd.dualEquiv_functor : BddOrd.dualEquiv.functor = BddOrd.dual

@[simp]

theorem BddOrd.dualEquiv_inverse : BddOrd.dualEquiv.inverse = BddOrd.dual

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.

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

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