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.instCoeSortType : CoeSort BddOrd (Type u_1)

Equations

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

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

Equations

• X.instPartialOrderαToPartOrd = 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 { α := α, str := inferInstance }

@[simp]

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

instance BddOrd.instInhabited : Inhabited BddOrd

Equations

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

instance BddOrd.largeCategory : CategoryTheory.LargeCategory BddOrd

Equations

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

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

Equations

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

instance BddOrd.concreteCategory : CategoryTheory.ConcreteCategory BddOrd

Equations

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

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.map a = BoundedOrderHom.dual a

@[simp]

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

def BddOrd.dual : CategoryTheory.Functor BddOrd BddOrd

OrderDual as a functor.

Equations

• BddOrd.dual = { obj := fun (X : BddOrd) => BddOrd.of (↑X.toPartOrd)ᵒᵈ, map := fun {X Y : BddOrd} => ⇑BoundedOrderHom.dual, map_id := BddOrd.dual.proof_1, map_comp := @BddOrd.dual.proof_2 }

@[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 = ↑e.symm

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 = { hom := ↑e, inv := ↑e.symm, hom_inv_id := ⋯, inv_hom_id := ⋯ }

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