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

Equations

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

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

Equations

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

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

Construct a bundled FinPartOrd from PartialOrder + Fintype.

Equations

• FinPartOrd.of α = FinPartOrd.mk { α := α, str := inferInstance }

@[simp]

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

instance FinPartOrd.instInhabited : Inhabited FinPartOrd

Equations

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

instance FinPartOrd.largeCategory : CategoryTheory.LargeCategory FinPartOrd

Equations

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

instance FinPartOrd.hasForget : CategoryTheory.HasForget FinPartOrd

Equations

• FinPartOrd.hasForget = CategoryTheory.InducedCategory.hasForget 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.

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

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

Equations

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

@[simp]

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

@[simp]

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

def FinPartOrd.dual : CategoryTheory.Functor FinPartOrd FinPartOrd

OrderDual as a functor.

Equations

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

@[simp]

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

@[simp]

theorem FinPartOrd.dual_map {x✝ x✝¹ : FinPartOrd} (a : ↑x✝.toPartOrd →o ↑x✝¹.toPartOrd) : dual.map a = OrderHom.dual a

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.

@[simp]

theorem FinPartOrd.dualEquiv_inverse : dualEquiv.inverse = dual

@[simp]

theorem FinPartOrd.dualEquiv_counitIso : dualEquiv.counitIso = CategoryTheory.NatIso.ofComponents (fun (X : FinPartOrd) => Iso.mk (OrderIso.dualDual ↑X.toPartOrd)) @dualEquiv.proof_2

@[simp]

theorem FinPartOrd.dualEquiv_unitIso : dualEquiv.unitIso = CategoryTheory.NatIso.ofComponents (fun (X : FinPartOrd) => Iso.mk (OrderIso.dualDual ↑X.toPartOrd)) @dualEquiv.proof_1

@[simp]

theorem FinPartOrd.dualEquiv_functor : dualEquiv.functor = dual

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