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)

Equations

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

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

Equations

• X.instPartialOrderCarrier = X.str

@[reducible, inline]

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

Construct a bundled FinPartOrd from PartialOrder + Fintype.

Equations

• FinPartOrd.of α = { carrier := α, str := inst✝¹, isFintype := inst✝ }

instance FinPartOrd.instInhabited : Inhabited FinPartOrd

Equations

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

instance FinPartOrd.largeCategory : CategoryTheory.LargeCategory FinPartOrd

Equations

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

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

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.

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

Equations

• FinPartOrd.ofHom f = CategoryTheory.ConcreteCategory.ofHom f

@[simp]

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

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

@[simp]

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

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 = PartOrd.Hom.hom g) : f = g

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

@[simp]

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) = f

@[simp]

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

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

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

Equations

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

@[simp]

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

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_unitIso : dualEquiv.unitIso = CategoryTheory.NatIso.ofComponents (fun (X : FinPartOrd) => Iso.mk (OrderIso.dualDual ↑X.toPartOrd)) @dualEquiv._proof_10

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

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