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 FinPartOrdextends PartOrd : Type (u_1 + 1)

The category of finite partial orders with monotone functions.

• carrier : Type u_1
• str : PartialOrder ↑self.toPartOrd
• isFintype : Fintype ↑self.toPartOrd

instance FinPartOrd.instCoeSortType : CoeSort FinPartOrd (Type u_1)

instance FinPartOrd.instPartialOrderCarrier (X : FinPartOrd) : PartialOrder ↑X.toPartOrd

@[reducible, inline]

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

Construct a bundled FinPartOrd from PartialOrder + Fintype.

instance FinPartOrd.instInhabited : Inhabited FinPartOrd

instance FinPartOrd.largeCategory : CategoryTheory.LargeCategory FinPartOrd

instance FinPartOrd.concreteCategory : CategoryTheory.ConcreteCategory FinPartOrd fun (x1 x2 : FinPartOrd) => ↑x1.toPartOrd →o ↑x2.toPartOrd

instance FinPartOrd.hasForgetToPartOrd : CategoryTheory.HasForget₂ FinPartOrd PartOrd

instance FinPartOrd.hasForgetToFintype : CategoryTheory.HasForget₂ FinPartOrd FintypeCat

@[reducible, inline]

abbrev FinPartOrd.ofHom {X Y : Type u} [PartialOrder X] [Fintype X] [PartialOrder Y] [Fintype Y] (f : X →o Y) : of X ⟶ of Y

Typecheck a OrderHom as a morphism in FinPartOrd.

@[simp]

theorem FinPartOrd.hom_hom_id {X : FinPartOrd} : PartOrd.Hom.hom (CategoryTheory.CategoryStruct.id X).hom = OrderHom.id

@[deprecated FinPartOrd.hom_hom_id (since := "2025-12-18")]

theorem FinPartOrd.hom_id {X : FinPartOrd} : PartOrd.Hom.hom (CategoryTheory.CategoryStruct.id X).hom = OrderHom.id

Alias of FinPartOrd.hom_hom_id.

theorem FinPartOrd.id_apply (X : FinPartOrd) (x : ↑X.toPartOrd) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x

@[simp]

theorem FinPartOrd.hom_hom_comp {X Y Z : FinPartOrd} (f : X ⟶ Y) (g : Y ⟶ Z) : PartOrd.Hom.hom (CategoryTheory.CategoryStruct.comp f g).hom = (PartOrd.Hom.hom g.hom).comp (PartOrd.Hom.hom f.hom)

@[deprecated FinPartOrd.hom_hom_comp (since := "2025-12-18")]

theorem FinPartOrd.hom_comp {X Y Z : FinPartOrd} (f : X ⟶ Y) (g : Y ⟶ Z) : PartOrd.Hom.hom (CategoryTheory.CategoryStruct.comp f g).hom = (PartOrd.Hom.hom g.hom).comp (PartOrd.Hom.hom f.hom)

Alias of FinPartOrd.hom_hom_comp.

theorem FinPartOrd.comp_apply {X Y Z : FinPartOrd} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑X.toPartOrd) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x = (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)

theorem FinPartOrd.hom_ext {X Y : FinPartOrd} {f g : X ⟶ Y} (hf : PartOrd.Hom.hom f.hom = PartOrd.Hom.hom g.hom) : f = g

theorem FinPartOrd.hom_ext_iff {X Y : FinPartOrd} {f g : X ⟶ Y} : f = g ↔ PartOrd.Hom.hom f.hom = PartOrd.Hom.hom g.hom

@[simp]

theorem FinPartOrd.hom_hom_ofHom {X Y : Type u} [PartialOrder X] [Fintype X] [PartialOrder Y] [Fintype Y] (f : X →o Y) : PartOrd.Hom.hom (ofHom f).hom = f

@[deprecated FinPartOrd.hom_hom_ofHom (since := "2025-12-18")]

theorem FinPartOrd.hom_ofHom {X Y : Type u} [PartialOrder X] [Fintype X] [PartialOrder Y] [Fintype Y] (f : X →o Y) : PartOrd.Hom.hom (ofHom f).hom = f

Alias of FinPartOrd.hom_hom_ofHom.

@[simp]

theorem FinPartOrd.ofHom_hom_hom {X Y : FinPartOrd} (f : X ⟶ Y) : ofHom (PartOrd.Hom.hom f.hom) = f

@[deprecated FinPartOrd.ofHom_hom_hom (since := "2025-12-18")]

theorem FinPartOrd.ofHom_hom {X Y : FinPartOrd} (f : X ⟶ Y) : ofHom (PartOrd.Hom.hom f.hom) = f

Alias of FinPartOrd.ofHom_hom_hom.

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

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

@[simp]

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

@[simp]

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

def FinPartOrd.dual : CategoryTheory.Functor FinPartOrd FinPartOrd

OrderDual as a functor.

@[simp]

theorem FinPartOrd.dual_map {X✝ Y✝ : FinPartOrd} (f : X✝ ⟶ Y✝) : dual.map f = ofHom (OrderHom.dual (PartOrd.Hom.hom f.hom))

def FinPartOrd.dualEquiv : FinPartOrd ≌ FinPartOrd

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

@[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_functor : dualEquiv.functor = dual

@[simp]

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

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