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 α] : ↑(FinPartOrd.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.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.

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

@[simp]

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

@[simp]

theorem FinPartOrd.Iso.mk_hom {α : FinPartOrd} {β : FinPartOrd} (e : ↑α.toPartOrd ≃o ↑β.toPartOrd) : (FinPartOrd.Iso.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) : FinPartOrd.dual.obj X = FinPartOrd.of (↑X.toPartOrd)ᵒᵈ

@[simp]

theorem FinPartOrd.dual_map : ∀ {x x_1 : FinPartOrd} (a : ↑x.toPartOrd →o ↑x_1.toPartOrd), FinPartOrd.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 : FinPartOrd.dualEquiv.inverse = FinPartOrd.dual

@[simp]

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

@[simp]

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

@[simp]

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

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