mathlib3 documentation

order.category.FinPartOrd

The category of finite partial orders #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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)

to_PartOrd : PartOrd
is_fintype : fintype ↥(self.to_PartOrd)

The category of finite partial orders with monotone functions.

Instances for FinPartOrd

@[protected, instance]

def FinPartOrd.has_coe_to_sort :

has_coe_to_sort FinPartOrd (Type u_1)

Equations

FinPartOrd.has_coe_to_sort = {coe := λ (X : FinPartOrd), ↥(X.to_PartOrd)}

@[protected, instance]

def FinPartOrd.partial_order (X : FinPartOrd) :

partial_order ↥X

Equations

X.partial_order = X.to_PartOrd.str

@[simp]

theorem FinPartOrd.coe_to_PartOrd (X : FinPartOrd) :

↥(X.to_PartOrd) = ↥X

def FinPartOrd.of (α : Type u_1) [partial_order α] [fintype α] :

Construct a bundled FinPartOrd from fintype + partial_order.

Equations

FinPartOrd.of α = FinPartOrd.mk {α := α, str := _inst_1}

@[simp]

theorem FinPartOrd.coe_of (α : Type u_1) [partial_order α] [fintype α] :

↥(FinPartOrd.of α) = α

@[protected, instance]

def FinPartOrd.inhabited :

inhabited FinPartOrd

Equations

FinPartOrd.inhabited = {default := FinPartOrd.of punit punit.fintype}

@[protected, instance]

def FinPartOrd.large_category :

category_theory.large_category FinPartOrd

Equations

FinPartOrd.large_category = category_theory.induced_category.category FinPartOrd.to_PartOrd

@[protected, instance]

def FinPartOrd.concrete_category :

category_theory.concrete_category FinPartOrd

Equations

FinPartOrd.concrete_category = category_theory.induced_category.concrete_category FinPartOrd.to_PartOrd

@[protected, instance]

def FinPartOrd.has_forget_to_PartOrd :

category_theory.has_forget₂ FinPartOrd PartOrd

Equations

FinPartOrd.has_forget_to_PartOrd = category_theory.induced_category.has_forget₂ FinPartOrd.to_PartOrd

@[protected, instance]

def FinPartOrd.has_forget_to_Fintype :

category_theory.has_forget₂ FinPartOrd Fintype

Equations

FinPartOrd.has_forget_to_Fintype = {forget₂ := {obj := λ (X : FinPartOrd), {α := ↥X, str := X.is_fintype}, map := λ (X Y : FinPartOrd), coe_fn, map_id' := FinPartOrd.has_forget_to_Fintype._proof_1, map_comp' := FinPartOrd.has_forget_to_Fintype._proof_2}, forget_comp := FinPartOrd.has_forget_to_Fintype._proof_3}

@[simp]

theorem FinPartOrd.iso.mk_hom {α β : FinPartOrd} (e : ↥α ≃o ↥β) :

(FinPartOrd.iso.mk e).hom = ↑e

@[simp]

theorem FinPartOrd.iso.mk_inv {α β : FinPartOrd} (e : ↥α ≃o ↥β) :

(FinPartOrd.iso.mk e).inv = ↑(e.symm)

def FinPartOrd.iso.mk {α β : FinPartOrd} (e : ↥α ≃o ↥β) :

α ≅ β

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.dual_map (X Y : FinPartOrd) (ᾰ : ↥(X.to_PartOrd) →o ↥(Y.to_PartOrd)) :

FinPartOrd.dual.map ᾰ = ⇑order_hom.dual ᾰ

@[simp]

theorem FinPartOrd.dual_obj (X : FinPartOrd) :

FinPartOrd.dual.obj X = FinPartOrd.of (↥X)ᵒᵈ

def FinPartOrd.dual :

FinPartOrd ⥤ FinPartOrd

order_dual as a functor.

Equations

FinPartOrd.dual = {obj := λ (X : FinPartOrd), FinPartOrd.of (↥X)ᵒᵈ, map := λ (X Y : FinPartOrd), ⇑order_hom.dual, map_id' := FinPartOrd.dual._proof_1, map_comp' := FinPartOrd.dual._proof_2}

def FinPartOrd.dual_equiv :

FinPartOrd ≌ FinPartOrd

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

Equations

FinPartOrd.dual_equiv = category_theory.equivalence.mk FinPartOrd.dual FinPartOrd.dual (category_theory.nat_iso.of_components (λ (X : FinPartOrd), FinPartOrd.iso.mk (order_iso.dual_dual ↥X)) FinPartOrd.dual_equiv._proof_1) (category_theory.nat_iso.of_components (λ (X : FinPartOrd), FinPartOrd.iso.mk (order_iso.dual_dual ↥X)) FinPartOrd.dual_equiv._proof_2)

@[simp]

theorem FinPartOrd.dual_equiv_inverse :

FinPartOrd.dual_equiv.inverse = FinPartOrd.dual

@[simp]

theorem FinPartOrd.dual_equiv_functor :

FinPartOrd.dual_equiv.functor = FinPartOrd.dual

theorem FinPartOrd_dual_comp_forget_to_PartOrd :

FinPartOrd.dual ⋙ category_theory.forget₂ FinPartOrd PartOrd = category_theory.forget₂ FinPartOrd PartOrd ⋙ PartOrd.dual