Metamath Proof Explorer

Definition df-up

Description: Definition of the class of universal properties.

Given categories D and E , if F : D --> E is a functor and W an object of E , a universal pair from W to F is a pair <. X , M >. consisting of an object X of D and a morphism M : W --> F X of E , such that to every pair <. y , g >. with y an object of D and g : W --> F y a morphism of E , there is a unique morphism k : X --> y of D with F k .o. M = g . Such property is commonly referred to as a universal property. In our definition, it is denoted as X ( F ( D UP E ) W ) M .

Note that the universal pair is termed differently as "universal arrow" in p. 55 of Mac Lane, Saunders,Categories for the Working Mathematician, 2nd Edition, Springer Science+Business Media, New York, (1998) [QA169.M33 1998]; available at https://math.mit.edu/~hrm/palestine/maclane-categories.pdf (retrieved 6 Oct 2025). Interestingly, the "universal arrow" is referring to the morphism M instead of the pair near the end of the same piece of the text, causing name collision. The name "universal arrow" is also adopted in papers such as https://arxiv.org/pdf/2212.08981 . Alternatively, the universal pair is called the "universal morphism" in Wikipedia ( https://en.wikipedia.org/wiki/Universal_property ) as well as published works, e.g., https://arxiv.org/pdf/2412.12179 . But the pair <. X , M >. should be named differently as the morphism M , and thus we call X theuniversal object, M theuniversal morphism, and <. X , M >. theuniversal pair.

Given its existence, such universal pair is essentially unique ( upeu3 ), and can be generated from an existing universal pair by isomorphisms ( upeu4 ). See also oppcup for the dual concept.

(Contributed by Zhi Wang, 24-Sep-2025)

Ref Expression
Assertion df-up 
|- UP = ( d e. _V , e e. _V |-> [_ ( Base ` d ) / b ]_ [_ ( Base ` e ) / c ]_ [_ ( Hom ` d ) / h ]_ [_ ( Hom ` e ) / j ]_ [_ ( comp ` e ) / o ]_ ( f e. ( d Func e ) , w e. c |-> { <. x , m >. | ( ( x e. b /\ m e. ( w j ( ( 1st ` f ) ` x ) ) ) /\ A. y e. b A. g e. ( w j ( ( 1st ` f ) ` y ) ) E! k e. ( x h y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. o ( ( 1st ` f ) ` y ) ) m ) ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cup 
 |-  UP
1 vd 
 |-  d
2 cvv 
 |-  _V
3 ve 
 |-  e
4 cbs 
 |-  Base
5 1 cv 
 |-  d
6 5 4 cfv 
 |-  ( Base ` d )
7 vb 
 |-  b
8 3 cv 
 |-  e
9 8 4 cfv 
 |-  ( Base ` e )
10 vc 
 |-  c
11 chom 
 |-  Hom
12 5 11 cfv 
 |-  ( Hom ` d )
13 vh 
 |-  h
14 8 11 cfv 
 |-  ( Hom ` e )
15 vj 
 |-  j
16 cco 
 |-  comp
17 8 16 cfv 
 |-  ( comp ` e )
18 vo 
 |-  o
19 vf 
 |-  f
20 cfunc 
 |-  Func
21 5 8 20 co 
 |-  ( d Func e )
22 vw 
 |-  w
23 10 cv 
 |-  c
24 vx 
 |-  x
25 vm 
 |-  m
26 24 cv 
 |-  x
27 7 cv 
 |-  b
28 26 27 wcel 
 |-  x e. b
29 25 cv 
 |-  m
30 22 cv 
 |-  w
31 15 cv 
 |-  j
32 c1st 
 |-  1st
33 19 cv 
 |-  f
34 33 32 cfv 
 |-  ( 1st ` f )
35 26 34 cfv 
 |-  ( ( 1st ` f ) ` x )
36 30 35 31 co 
 |-  ( w j ( ( 1st ` f ) ` x ) )
37 29 36 wcel 
 |-  m e. ( w j ( ( 1st ` f ) ` x ) )
38 28 37 wa 
 |-  ( x e. b /\ m e. ( w j ( ( 1st ` f ) ` x ) ) )
39 vy 
 |-  y
40 vg 
 |-  g
41 39 cv 
 |-  y
42 41 34 cfv 
 |-  ( ( 1st ` f ) ` y )
43 30 42 31 co 
 |-  ( w j ( ( 1st ` f ) ` y ) )
44 vk 
 |-  k
45 13 cv 
 |-  h
46 26 41 45 co 
 |-  ( x h y )
47 40 cv 
 |-  g
48 c2nd 
 |-  2nd
49 33 48 cfv 
 |-  ( 2nd ` f )
50 26 41 49 co 
 |-  ( x ( 2nd ` f ) y )
51 44 cv 
 |-  k
52 51 50 cfv 
 |-  ( ( x ( 2nd ` f ) y ) ` k )
53 30 35 cop 
 |-  <. w , ( ( 1st ` f ) ` x ) >.
54 18 cv 
 |-  o
55 53 42 54 co 
 |-  ( <. w , ( ( 1st ` f ) ` x ) >. o ( ( 1st ` f ) ` y ) )
56 52 29 55 co 
 |-  ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. o ( ( 1st ` f ) ` y ) ) m )
57 47 56 wceq 
 |-  g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. o ( ( 1st ` f ) ` y ) ) m )
58 57 44 46 wreu 
 |-  E! k e. ( x h y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. o ( ( 1st ` f ) ` y ) ) m )
59 58 40 43 wral 
 |-  A. g e. ( w j ( ( 1st ` f ) ` y ) ) E! k e. ( x h y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. o ( ( 1st ` f ) ` y ) ) m )
60 59 39 27 wral 
 |-  A. y e. b A. g e. ( w j ( ( 1st ` f ) ` y ) ) E! k e. ( x h y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. o ( ( 1st ` f ) ` y ) ) m )
61 38 60 wa 
 |-  ( ( x e. b /\ m e. ( w j ( ( 1st ` f ) ` x ) ) ) /\ A. y e. b A. g e. ( w j ( ( 1st ` f ) ` y ) ) E! k e. ( x h y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. o ( ( 1st ` f ) ` y ) ) m ) )
62 61 24 25 copab 
 |-  { <. x , m >. | ( ( x e. b /\ m e. ( w j ( ( 1st ` f ) ` x ) ) ) /\ A. y e. b A. g e. ( w j ( ( 1st ` f ) ` y ) ) E! k e. ( x h y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. o ( ( 1st ` f ) ` y ) ) m ) ) }
63 19 22 21 23 62 cmpo 
 |-  ( f e. ( d Func e ) , w e. c |-> { <. x , m >. | ( ( x e. b /\ m e. ( w j ( ( 1st ` f ) ` x ) ) ) /\ A. y e. b A. g e. ( w j ( ( 1st ` f ) ` y ) ) E! k e. ( x h y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. o ( ( 1st ` f ) ` y ) ) m ) ) } )
64 18 17 63 csb 
 |-  [_ ( comp ` e ) / o ]_ ( f e. ( d Func e ) , w e. c |-> { <. x , m >. | ( ( x e. b /\ m e. ( w j ( ( 1st ` f ) ` x ) ) ) /\ A. y e. b A. g e. ( w j ( ( 1st ` f ) ` y ) ) E! k e. ( x h y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. o ( ( 1st ` f ) ` y ) ) m ) ) } )
65 15 14 64 csb 
 |-  [_ ( Hom ` e ) / j ]_ [_ ( comp ` e ) / o ]_ ( f e. ( d Func e ) , w e. c |-> { <. x , m >. | ( ( x e. b /\ m e. ( w j ( ( 1st ` f ) ` x ) ) ) /\ A. y e. b A. g e. ( w j ( ( 1st ` f ) ` y ) ) E! k e. ( x h y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. o ( ( 1st ` f ) ` y ) ) m ) ) } )
66 13 12 65 csb 
 |-  [_ ( Hom ` d ) / h ]_ [_ ( Hom ` e ) / j ]_ [_ ( comp ` e ) / o ]_ ( f e. ( d Func e ) , w e. c |-> { <. x , m >. | ( ( x e. b /\ m e. ( w j ( ( 1st ` f ) ` x ) ) ) /\ A. y e. b A. g e. ( w j ( ( 1st ` f ) ` y ) ) E! k e. ( x h y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. o ( ( 1st ` f ) ` y ) ) m ) ) } )
67 10 9 66 csb 
 |-  [_ ( Base ` e ) / c ]_ [_ ( Hom ` d ) / h ]_ [_ ( Hom ` e ) / j ]_ [_ ( comp ` e ) / o ]_ ( f e. ( d Func e ) , w e. c |-> { <. x , m >. | ( ( x e. b /\ m e. ( w j ( ( 1st ` f ) ` x ) ) ) /\ A. y e. b A. g e. ( w j ( ( 1st ` f ) ` y ) ) E! k e. ( x h y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. o ( ( 1st ` f ) ` y ) ) m ) ) } )
68 7 6 67 csb 
 |-  [_ ( Base ` d ) / b ]_ [_ ( Base ` e ) / c ]_ [_ ( Hom ` d ) / h ]_ [_ ( Hom ` e ) / j ]_ [_ ( comp ` e ) / o ]_ ( f e. ( d Func e ) , w e. c |-> { <. x , m >. | ( ( x e. b /\ m e. ( w j ( ( 1st ` f ) ` x ) ) ) /\ A. y e. b A. g e. ( w j ( ( 1st ` f ) ` y ) ) E! k e. ( x h y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. o ( ( 1st ` f ) ` y ) ) m ) ) } )
69 1 3 2 2 68 cmpo 
 |-  ( d e. _V , e e. _V |-> [_ ( Base ` d ) / b ]_ [_ ( Base ` e ) / c ]_ [_ ( Hom ` d ) / h ]_ [_ ( Hom ` e ) / j ]_ [_ ( comp ` e ) / o ]_ ( f e. ( d Func e ) , w e. c |-> { <. x , m >. | ( ( x e. b /\ m e. ( w j ( ( 1st ` f ) ` x ) ) ) /\ A. y e. b A. g e. ( w j ( ( 1st ` f ) ` y ) ) E! k e. ( x h y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. o ( ( 1st ` f ) ` y ) ) m ) ) } ) )
70 0 69 wceq 
 |-  UP = ( d e. _V , e e. _V |-> [_ ( Base ` d ) / b ]_ [_ ( Base ` e ) / c ]_ [_ ( Hom ` d ) / h ]_ [_ ( Hom ` e ) / j ]_ [_ ( comp ` e ) / o ]_ ( f e. ( d Func e ) , w e. c |-> { <. x , m >. | ( ( x e. b /\ m e. ( w j ( ( 1st ` f ) ` x ) ) ) /\ A. y e. b A. g e. ( w j ( ( 1st ` f ) ` y ) ) E! k e. ( x h y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. o ( ( 1st ` f ) ` y ) ) m ) ) } ) )