The category of finite partial orders

This defines FinPartOrd, the category of finite partial orders.

Note: FinPartOrd is not a subcategory of BddOrd because finite orders are not necessarily bounded.

TODO

FinPartOrd is equivalent to a small category.

structure FinPartOrd : Type (u_1 + 1)

The category of finite partial orders with monotone functions.

• toPartOrd : PartOrd
• isFintype : Fintype ↑self.toPartOrd

instance FinPartOrd.instCoeSortFinPartOrdType : CoeSort FinPartOrd (Type u_1)

Equations

• FinPartOrd.instCoeSortFinPartOrdType = { coe := fun (X : FinPartOrd) => ↑X.toPartOrd }

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

Equations

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

def FinPartOrd.of (α : Type u_1) [PartialOrder α] [Fintype α] : FinPartOrd

Construct a bundled FinPartOrd from PartialOrder + Fintype.

Equations

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

@[simp]

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

instance FinPartOrd.instInhabitedFinPartOrd : Inhabited FinPartOrd

Equations

• FinPartOrd.instInhabitedFinPartOrd = { default := FinPartOrd.of PUnit.{u_1 + 1} }

instance FinPartOrd.largeCategory : CategoryTheory.LargeCategory FinPartOrd

Equations

• FinPartOrd.largeCategory = CategoryTheory.InducedCategory.category FinPartOrd.toPartOrd

instance FinPartOrd.concreteCategory : CategoryTheory.ConcreteCategory FinPartOrd

Equations

• FinPartOrd.concreteCategory = CategoryTheory.InducedCategory.concreteCategory FinPartOrd.toPartOrd

instance FinPartOrd.hasForgetToPartOrd : CategoryTheory.HasForget₂ FinPartOrd PartOrd

Equations

• FinPartOrd.hasForgetToPartOrd = CategoryTheory.InducedCategory.hasForget₂ FinPartOrd.toPartOrd

instance FinPartOrd.hasForgetToFintype : CategoryTheory.HasForget₂ FinPartOrd FintypeCat

Equations

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

@[simp]

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

@[simp]

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

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

Constructs an isomorphism of finite partial orders from an order isomorphism between them.

Equations

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

@[simp]

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

@[simp]

theorem FinPartOrd.dual_map {X : FinPartOrd} {Y : FinPartOrd} (a : ↑X.toPartOrd →o ↑Y.toPartOrd) : FinPartOrd.dual.toPrefunctor.map a = OrderHom.dual a

def FinPartOrd.dual : CategoryTheory.Functor FinPartOrd FinPartOrd

OrderDual as a functor.

Equations

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

@[simp]

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

@[simp]

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

def FinPartOrd.dualEquiv : FinPartOrd ≌ FinPartOrd

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

Equations

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

theorem FinPartOrd_dual_comp_forget_to_partOrd : CategoryTheory.Functor.comp FinPartOrd.dual (CategoryTheory.forget₂ FinPartOrd PartOrd) = CategoryTheory.Functor.comp (CategoryTheory.forget₂ FinPartOrd PartOrd) PartOrd.dual