Definition df-prstc

Description: Definition of the function converting a preordered set to a category. Justified by prsthinc .

This definition is somewhat arbitrary. Example 3.3(4.d) of Adamek p. 24 demonstrates an alternate definition with pairwise disjoint hom-sets. The behavior of the function is defined entirely, up to isomorphism, by prstcnid , prstchom , and prstcthin . Other important properties include prstcbas , prstcleval , prstcle , prstcocval , prstcoc , prstchom2 , and prstcprs . Use those instead.

Note that the defining property prstchom is equivalent to prstchom2 given prstcthin . See thincn0eu for justification.

"ProsetToCat" was taken instead of "ProsetCat" because the latter might mean the category of preordered sets (classes). However, "ProsetToCat" seems too long. (Contributed by Zhi Wang, 20-Sep-2024) (New usage is discouraged.)

	Ref	Expression
Assertion	df-prstc	⊢ ProsetToCat = ( 𝑘 ∈ Proset ↦ ( ( 𝑘 sSet ⟨ ( Hom ‘ ndx ) , ( ( le ‘ 𝑘 ) × { 1o } ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ∅ ⟩ ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cprstc	⊢ ProsetToCat
1		vk	⊢ 𝑘
2		cproset	⊢ Proset
3	1	cv	⊢ 𝑘
4		csts	⊢ sSet
5		chom	⊢ Hom
6		cnx	⊢ ndx
7	6 5	cfv	⊢ ( Hom ‘ ndx )
8		cple	⊢ le
9	3 8	cfv	⊢ ( le ‘ 𝑘 )
10		c1o	⊢ 1o
11	10	csn	⊢ { 1o }
12	9 11	cxp	⊢ ( ( le ‘ 𝑘 ) × { 1o } )
13	7 12	cop	⊢ ⟨ ( Hom ‘ ndx ) , ( ( le ‘ 𝑘 ) × { 1o } ) ⟩
14	3 13 4	co	⊢ ( 𝑘 sSet ⟨ ( Hom ‘ ndx ) , ( ( le ‘ 𝑘 ) × { 1o } ) ⟩ )
15		cco	⊢ comp
16	6 15	cfv	⊢ ( comp ‘ ndx )
17		c0	⊢ ∅
18	16 17	cop	⊢ ⟨ ( comp ‘ ndx ) , ∅ ⟩
19	14 18 4	co	⊢ ( ( 𝑘 sSet ⟨ ( Hom ‘ ndx ) , ( ( le ‘ 𝑘 ) × { 1o } ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ∅ ⟩ )
20	1 2 19	cmpt	⊢ ( 𝑘 ∈ Proset ↦ ( ( 𝑘 sSet ⟨ ( Hom ‘ ndx ) , ( ( le ‘ 𝑘 ) × { 1o } ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ∅ ⟩ ) )
21	0 20	wceq	⊢ ProsetToCat = ( 𝑘 ∈ Proset ↦ ( ( 𝑘 sSet ⟨ ( Hom ‘ ndx ) , ( ( le ‘ 𝑘 ) × { 1o } ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ∅ ⟩ ) )