Metamath Proof Explorer

Theorem yoneda

Description: The Yoneda Lemma. There is a natural isomorphism between the functors Z and E , where Z ( F , X ) is the natural transformations from Yon ( X ) = Hom ( - , X ) to F , and E ( F , X ) = F ( X ) is the evaluation functor. Here we need two universes to state the claim: the smaller universe U is used for forming the functor category Q = C op -> SetCat ( U ) , which itself does not (necessarily) live in U but instead is an element of the larger universe V . (If U is a Grothendieck universe, then it will be closed under this "presheaf" operation, and so we can set U = V in this case.) (Contributed by Mario Carneiro, 29-Jan-2017)

Ref Expression
Hypotheses yoneda.y 
|- Y = ( Yon ` C )
yoneda.b 
|- B = ( Base ` C )
yoneda.1 
|- .1. = ( Id ` C )
yoneda.o 
|- O = ( oppCat ` C )
yoneda.s 
|- S = ( SetCat ` U )
yoneda.t 
|- T = ( SetCat ` V )
yoneda.q 
|- Q = ( O FuncCat S )
yoneda.h 
|- H = ( HomF ` Q )
yoneda.r 
|- R = ( ( Q Xc. O ) FuncCat T )
yoneda.e 
|- E = ( O evalF S )
yoneda.z 
|- Z = ( H o.func ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) )
yoneda.c 
|- ( ph -> C e. Cat )
yoneda.w 
|- ( ph -> V e. W )
yoneda.u 
|- ( ph -> ran ( Homf ` C ) C_ U )
yoneda.v 
|- ( ph -> ( ran ( Homf ` Q ) u. U ) C_ V )
yoneda.m 
|- M = ( f e. ( O Func S ) , x e. B |-> ( a e. ( ( ( 1st ` Y ) ` x ) ( O Nat S ) f ) |-> ( ( a ` x ) ` ( .1. ` x ) ) ) )
yoneda.i 
|- I = ( Iso ` R )
Assertion yoneda 
|- ( ph -> M e. ( Z I E ) )

Proof

Step Hyp Ref Expression
1 yoneda.y 
 |-  Y = ( Yon ` C )
2 yoneda.b 
 |-  B = ( Base ` C )
3 yoneda.1 
 |-  .1. = ( Id ` C )
4 yoneda.o 
 |-  O = ( oppCat ` C )
5 yoneda.s 
 |-  S = ( SetCat ` U )
6 yoneda.t 
 |-  T = ( SetCat ` V )
7 yoneda.q 
 |-  Q = ( O FuncCat S )
8 yoneda.h 
 |-  H = ( HomF ` Q )
9 yoneda.r 
 |-  R = ( ( Q Xc. O ) FuncCat T )
10 yoneda.e 
 |-  E = ( O evalF S )
11 yoneda.z 
 |-  Z = ( H o.func ( ( <. ( 1st ` Y ) , tpos ( 2nd ` Y ) >. o.func ( Q 2ndF O ) ) pairF ( Q 1stF O ) ) )
12 yoneda.c 
 |-  ( ph -> C e. Cat )
13 yoneda.w 
 |-  ( ph -> V e. W )
14 yoneda.u 
 |-  ( ph -> ran ( Homf ` C ) C_ U )
15 yoneda.v 
 |-  ( ph -> ( ran ( Homf ` Q ) u. U ) C_ V )
16 yoneda.m 
 |-  M = ( f e. ( O Func S ) , x e. B |-> ( a e. ( ( ( 1st ` Y ) ` x ) ( O Nat S ) f ) |-> ( ( a ` x ) ` ( .1. ` x ) ) ) )
17 yoneda.i 
 |-  I = ( Iso ` R )
18 9 fucbas 
 |-  ( ( Q Xc. O ) Func T ) = ( Base ` R )
19 eqid 
 |-  ( Inv ` R ) = ( Inv ` R )
20 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 yonedalem1 
 |-  ( ph -> ( Z e. ( ( Q Xc. O ) Func T ) /\ E e. ( ( Q Xc. O ) Func T ) ) )
21 20 simpld 
 |-  ( ph -> Z e. ( ( Q Xc. O ) Func T ) )
22 funcrcl 
 |-  ( Z e. ( ( Q Xc. O ) Func T ) -> ( ( Q Xc. O ) e. Cat /\ T e. Cat ) )
23 21 22 syl 
 |-  ( ph -> ( ( Q Xc. O ) e. Cat /\ T e. Cat ) )
24 23 simpld 
 |-  ( ph -> ( Q Xc. O ) e. Cat )
25 23 simprd 
 |-  ( ph -> T e. Cat )
26 9 24 25 fuccat 
 |-  ( ph -> R e. Cat )
27 20 simprd 
 |-  ( ph -> E e. ( ( Q Xc. O ) Func T ) )
28 eqid 
 |-  ( f e. ( O Func S ) , x e. B |-> ( u e. ( ( 1st ` f ) ` x ) |-> ( y e. B |-> ( g e. ( y ( Hom ` C ) x ) |-> ( ( ( x ( 2nd ` f ) y ) ` g ) ` u ) ) ) ) ) = ( f e. ( O Func S ) , x e. B |-> ( u e. ( ( 1st ` f ) ` x ) |-> ( y e. B |-> ( g e. ( y ( Hom ` C ) x ) |-> ( ( ( x ( 2nd ` f ) y ) ` g ) ` u ) ) ) ) )
29 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 19 28 yonedainv 
 |-  ( ph -> M ( Z ( Inv ` R ) E ) ( f e. ( O Func S ) , x e. B |-> ( u e. ( ( 1st ` f ) ` x ) |-> ( y e. B |-> ( g e. ( y ( Hom ` C ) x ) |-> ( ( ( x ( 2nd ` f ) y ) ` g ) ` u ) ) ) ) ) )
30 18 19 26 21 27 17 29 inviso1 
 |-  ( ph -> M e. ( Z I E ) )