mathlib documentation

order.category.FinPartialOrder

The category of finite partial orders #

This defines FinPartialOrder, the category of finite partial orders.

Note: FinPartialOrder is NOT a subcategory of BoundedOrder because its morphisms do not preserve ⊥ and ⊤.

TODO #

FinPartialOrder is equivalent to a small category.

source
structure FinPartialOrder  :
Type (u_1+1)

The category of finite partial orders with monotone functions.

Instances for FinPartialOrder
source
@[protected, instance]
def FinPartialOrder.has_coe_to_sort  :
has_coe_to_sort FinPartialOrder (Type u_1)
Equations
source
@[protected, instance]
def FinPartialOrder.partial_order (X : FinPartialOrder) :
partial_order ↥X
Equations
source
@[simp]
theorem FinPartialOrder.coe_to_PartialOrder (X : FinPartialOrder) :
↥(X.to_PartialOrder) = ↥X
source
def FinPartialOrder.of (α : Type u_1) [partial_order α] [fintype α] :
FinPartialOrder

Construct a bundled FinPartialOrder from fintype + partial_order.

Equations
source
@[simp]
theorem FinPartialOrder.coe_of (α : Type u_1) [partial_order α] [fintype α] :
↥(FinPartialOrder.of α) = α
source
@[protected, instance]
def FinPartialOrder.inhabited  :
inhabited FinPartialOrder
Equations
source
@[protected, instance]
def FinPartialOrder.large_category  :
category_theory.large_category FinPartialOrder
Equations
source
@[protected, instance]
def FinPartialOrder.concrete_category  :
category_theory.concrete_category FinPartialOrder
Equations
source
@[protected, instance]
def FinPartialOrder.has_forget_to_PartialOrder  :
category_theory.has_forget₂ FinPartialOrder PartialOrder
Equations
source
@[protected, instance]
def FinPartialOrder.has_forget_to_Fintype  :
category_theory.has_forget₂ FinPartialOrder Fintype
Equations
source
@[simp]
theorem FinPartialOrder.iso.mk_hom {α β : FinPartialOrder} (e : ↥α ≃o ↥β) :
(FinPartialOrder.iso.mk e).hom = ↑e
source
@[simp]
theorem FinPartialOrder.iso.mk_inv {α β : FinPartialOrder} (e : ↥α ≃o ↥β) :
(FinPartialOrder.iso.mk e).inv = ↑(e.symm)
source
def FinPartialOrder.iso.mk {α β : FinPartialOrder} (e : ↥α ≃o ↥β) :
α ≅ β

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

Equations
source
def FinPartialOrder.dual  :
FinPartialOrder ⥤ FinPartialOrder

order_dual as a functor.

Equations
source
@[simp]
theorem FinPartialOrder.dual_map (X Y : FinPartialOrder) (ᾰ : ↥(X.to_PartialOrder) →o ↥(Y.to_PartialOrder)) :
FinPartialOrder.dual.map ᾰ = ⇑order_hom.dual ᾰ
source
@[simp]
theorem FinPartialOrder.dual_obj (X : FinPartialOrder) :
FinPartialOrder.dual.obj X = FinPartialOrder.of (↥X)ᵒᵈ
source
def FinPartialOrder.dual_equiv  :
FinPartialOrder ≌ FinPartialOrder

The equivalence between FinPartialOrder and itself induced by order_dual both ways.

Equations
source
@[simp]
theorem FinPartialOrder.dual_equiv_functor  :
FinPartialOrder.dual_equiv.functor = FinPartialOrder.dual
source
@[simp]
theorem FinPartialOrder.dual_equiv_inverse  :
FinPartialOrder.dual_equiv.inverse = FinPartialOrder.dual
source
theorem FinPartialOrder_dual_comp_forget_to_PartialOrder  :
FinPartialOrder.dual ⋙ category_theory.forget₂ FinPartialOrder PartialOrder = category_theory.forget₂ FinPartialOrder PartialOrder ⋙ PartialOrder.dual