let A be Category; Yoneda A is full
set F = Yoneda A;
for c, c' being Object of st Hom ((Yoneda A) . c'),((Yoneda A) . c) <> {} holds
for g being Morphism of (Yoneda A) . c',(Yoneda A) . c holds
( Hom c,c' <> {} & ex f being Morphism of c,c' st g = (Yoneda A) . f )
proof
let c,
c' be
Object of ;
( Hom ((Yoneda A) . c'),((Yoneda A) . c) <> {} implies for g being Morphism of (Yoneda A) . c',(Yoneda A) . c holds
( Hom c,c' <> {} & ex f being Morphism of c,c' st g = (Yoneda A) . f ) )
assume A1:
Hom ((Yoneda A) . c'),
((Yoneda A) . c) <> {}
;
for g being Morphism of (Yoneda A) . c',(Yoneda A) . c holds
( Hom c,c' <> {} & ex f being Morphism of c,c' st g = (Yoneda A) . f )
A2:
<|c',?> . c' =
(hom?- (Hom A),c') . c'
by ENS_1:def 26
.=
(Obj (hom?- (Hom A),c')) . c'
by CAT_1:def 20
.=
Hom c',
c'
by ENS_1:60
;
let g be
Morphism of
(Yoneda A) . c',
(Yoneda A) . c;
( Hom c,c' <> {} & ex f being Morphism of c,c' st g = (Yoneda A) . f )
g in the
carrier' of
(Functors A,(EnsHom A))
;
then
g in NatTrans A,
(EnsHom A)
by NATTRA_1:def 18;
then consider F1,
F2 being
Functor of
A,
EnsHom A,
t being
natural_transformation of
F1,
F2 such that A3:
g = [[F1,F2],t]
and A4:
F1 is_naturally_transformable_to F2
by NATTRA_1:def 16;
A5:
dom g = F1
by A3, NATTRA_1:39;
<|c',?> in Funct A,
(EnsHom A)
by CAT_2:def 2;
then reconsider d1 =
<|c',?> as
Object of
by NATTRA_1:def 18;
<|c,?> in Funct A,
(EnsHom A)
by CAT_2:def 2;
then reconsider d =
<|c,?> as
Object of
by NATTRA_1:def 18;
A6:
(Yoneda A) . (id c) = id d
proof
set X =
dom <|(id c),?>;
A7:
for
y being
set st
y in dom <|(id c),?> holds
<|(id c),?> . y = (id <|c,?>) . y
proof
let y be
set ;
( y in dom <|(id c),?> implies <|(id c),?> . y = (id <|c,?>) . y )
assume
y in dom <|(id c),?>
;
<|(id c),?> . y = (id <|c,?>) . y
then reconsider z =
y as
Object of
by FUNCT_2:def 1;
reconsider zz =
id z as
Morphism of
z,
z ;
A8:
Hom z,
z <> {}
by CAT_1:56;
<|(cod (id c)),?> is_transformable_to <|c,?>
by CAT_1:44;
then A9:
<|(cod (id c)),?> is_transformable_to <|(dom (id c)),?>
by CAT_1:44;
<|(id c),?> . z =
[[(Hom (cod (id c)),z),(Hom (dom (id c)),z)],(hom (id c),(id z))]
by Def3
.=
[[(Hom c,z),(Hom (dom (id c)),z)],(hom (id c),(id z))]
by CAT_1:44
.=
[[(Hom c,z),(Hom c,z)],(hom (id c),(id z))]
by CAT_1:44
.=
[[(Hom c,z),(Hom c,z)],(hom c,(id z))]
by ENS_1:53
.=
[[(Hom c,z),(Hom c,(cod (id z)))],(hom c,(id z))]
by CAT_1:44
.=
[[(Hom c,(dom (id z))),(Hom c,(cod (id z)))],(hom c,(id z))]
by CAT_1:44
.=
<|c,?> . (id z)
by ENS_1:def 22
.=
<|c,?> . zz
by A8, NATTRA_1:def 1
.=
id (<|c,?> . z)
by NATTRA_1:15
.=
(id <|c,?>) . z
by NATTRA_1:21
.=
(id <|c,?>) . z
by NATTRA_1:def 5
;
hence
<|(id c),?> . y = (id <|c,?>) . y
by A9, NATTRA_1:def 5;
verum
end;
dom <|(id c),?> =
the
carrier of
A
by FUNCT_2:def 1
.=
dom (id <|c,?>)
by FUNCT_2:def 1
;
then A10:
<|(id c),?> = id <|c,?>
by A7, FUNCT_1:9;
(Yoneda A) . (id c) =
[[<|(cod (id c)),?>,<|(dom (id c)),?>],<|(id c),?>]
by Def4
.=
[[<|c,?>,<|(dom (id c)),?>],<|(id c),?>]
by CAT_1:44
.=
[[<|c,?>,<|c,?>],(id <|c,?>)]
by A10, CAT_1:44
.=
id d
by NATTRA_1:def 18
;
hence
(Yoneda A) . (id c) = id d
;
verum
end;
then A11:
(Yoneda A) . c = d
by OPPCAT_1:31;
A12:
(Yoneda A) . (id c') = id d1
proof
set X =
dom <|(id c'),?>;
A13:
for
y being
set st
y in dom <|(id c'),?> holds
<|(id c'),?> . y = (id <|c',?>) . y
proof
let y be
set ;
( y in dom <|(id c'),?> implies <|(id c'),?> . y = (id <|c',?>) . y )
assume
y in dom <|(id c'),?>
;
<|(id c'),?> . y = (id <|c',?>) . y
then reconsider z =
y as
Object of
by FUNCT_2:def 1;
reconsider zz =
id z as
Morphism of
z,
z ;
A14:
Hom z,
z <> {}
by CAT_1:56;
<|(cod (id c')),?> is_transformable_to <|c',?>
by CAT_1:44;
then A15:
<|(cod (id c')),?> is_transformable_to <|(dom (id c')),?>
by CAT_1:44;
<|(id c'),?> . z =
[[(Hom (cod (id c')),z),(Hom (dom (id c')),z)],(hom (id c'),(id z))]
by Def3
.=
[[(Hom c',z),(Hom (dom (id c')),z)],(hom (id c'),(id z))]
by CAT_1:44
.=
[[(Hom c',z),(Hom c',z)],(hom (id c'),(id z))]
by CAT_1:44
.=
[[(Hom c',z),(Hom c',z)],(hom c',(id z))]
by ENS_1:53
.=
[[(Hom c',z),(Hom c',(cod (id z)))],(hom c',(id z))]
by CAT_1:44
.=
[[(Hom c',(dom (id z))),(Hom c',(cod (id z)))],(hom c',(id z))]
by CAT_1:44
.=
<|c',?> . (id z)
by ENS_1:def 22
.=
<|c',?> . zz
by A14, NATTRA_1:def 1
.=
id (<|c',?> . z)
by NATTRA_1:15
.=
(id <|c',?>) . z
by NATTRA_1:21
.=
(id <|c',?>) . z
by NATTRA_1:def 5
;
hence
<|(id c'),?> . y = (id <|c',?>) . y
by A15, NATTRA_1:def 5;
verum
end;
dom <|(id c'),?> =
the
carrier of
A
by FUNCT_2:def 1
.=
dom (id <|c',?>)
by FUNCT_2:def 1
;
then A16:
<|(id c'),?> = id <|c',?>
by A13, FUNCT_1:9;
(Yoneda A) . (id c') =
[[<|(cod (id c')),?>,<|(dom (id c')),?>],<|(id c'),?>]
by Def4
.=
[[<|c',?>,<|(dom (id c')),?>],<|(id c'),?>]
by CAT_1:44
.=
[[<|c',?>,<|c',?>],(id <|c',?>)]
by A16, CAT_1:44
.=
id d1
by NATTRA_1:def 18
;
hence
(Yoneda A) . (id c') = id d1
;
verum
end;
then A17:
(Obj (Yoneda A)) . c' = d1
by OPPCAT_1:31;
A18:
cod g = F2
by A3, NATTRA_1:39;
then A19:
F2 = (Yoneda A) . c
by A1, CAT_1:23;
A20:
(Yoneda A) . c' = d1
by A12, OPPCAT_1:31;
A21:
<|c,?> . c' =
(hom?- (Hom A),c) . c'
by ENS_1:def 26
.=
(Obj (hom?- (Hom A),c)) . c'
by CAT_1:def 20
.=
Hom c,
c'
by ENS_1:60
;
A22:
(
dom g = (Yoneda A) . c' &
cod g = (Yoneda A) . c )
by A1, CAT_1:23;
then reconsider t =
t as
natural_transformation of
<|c',?>,
<|c,?> by A5, A18, A12, A11, OPPCAT_1:31;
(Obj (Yoneda A)) . c = d
by A6, OPPCAT_1:31;
then
<|c',?> is_transformable_to <|c,?>
by A4, A5, A18, A22, A20, NATTRA_1:def 7;
then
Hom (<|c',?> . c'),
(<|c,?> . c') <> {}
by NATTRA_1:def 2;
then A23:
t . c' in Hom (<|c',?> . c'),
(<|c,?> . c')
by CAT_1:def 7;
then A24:
cod (t . c') = <|c,?> . c'
by CAT_1:18;
A25:
EnsHom A = CatStr(#
(Hom A),
(Maps (Hom A)),
(fDom (Hom A)),
(fCod (Hom A)),
(fComp (Hom A)),
(fId (Hom A)) #)
by ENS_1:def 14;
then reconsider t1 =
t . c' as
Element of
Maps (Hom A) ;
A26:
cod (t . c') =
(fCod (Hom A)) . (t . c')
by A25
.=
cod t1
by ENS_1:def 11
;
t1 in Maps (dom t1),
(cod t1)
by ENS_1:19;
then A27:
t1 `2 in Funcs (dom t1),
(cod t1)
by ENS_1:20;
A28:
dom (t . c') = <|c',?> . c'
by A23, CAT_1:18;
then
the
Source of
(EnsHom A) . (t . c') <> {}
by A2, CAT_1:56;
then
dom t1 <> {}
by A25, ENS_1:def 10;
then A29:
cod t1 <> {}
by A27;
then A30:
cod (t . c') <> {}
by A25, ENS_1:def 11;
hence
Hom c,
c' <> {}
by A21, A23, CAT_1:18;
ex f being Morphism of c,c' st g = (Yoneda A) . f
dom (t . c') =
(fDom (Hom A)) . (t . c')
by A25
.=
dom t1
by ENS_1:def 10
;
then A31:
t1 `2 is
Function of
<|c',?> . c',
<|c,?> . c'
by A28, A24, A27, A26, FUNCT_2:121;
then A32:
dom (t1 `2 ) = Hom c',
c'
by A2, A24, A30, FUNCT_2:def 1;
then
id c' in dom (t1 `2 )
by CAT_1:55;
then A33:
(t1 `2 ) . (id c') in rng (t1 `2 )
by FUNCT_1:def 5;
rng (t1 `2 ) c= Hom c,
c'
by A21, A31, RELAT_1:def 19;
then
(t1 `2 ) . (id c') in Hom c,
c'
by A33;
then reconsider f =
(t1 `2 ) . (id c') as
Morphism of
c,
c' by CAT_1:def 7;
A34:
<|c,?> . c' <> {}
by A24, A25, A29, ENS_1:def 11;
then A35:
dom f = c
by A21, CAT_1:23;
take
f
;
g = (Yoneda A) . f
A36:
cod f = c'
by A21, A34, CAT_1:23;
A37:
F1 = (Yoneda A) . c'
by A1, A5, CAT_1:23;
then A38:
<|c',?> is_transformable_to <|c,?>
by A4, A19, A17, A11, NATTRA_1:def 7;
for
a being
Object of holds
<|f,?> . a = t . a
proof
let a be
Object of ;
<|f,?> . a = t . a
A39:
<|c,?> . a =
(hom?- (Hom A),c) . a
by ENS_1:def 26
.=
(Obj (hom?- (Hom A),c)) . a
by CAT_1:def 20
.=
Hom c,
a
by ENS_1:60
;
reconsider ta1 =
t . a as
Element of
Maps (Hom A) by A25;
A40:
<|c',?> . a =
(hom?- (Hom A),c') . a
by ENS_1:def 26
.=
(Obj (hom?- (Hom A),c')) . a
by CAT_1:def 20
.=
Hom c',
a
by ENS_1:60
;
ta1 in Maps (dom ta1),
(cod ta1)
by ENS_1:19;
then A41:
ta1 `2 in Funcs (dom ta1),
(cod ta1)
by ENS_1:20;
then A42:
ta1 `2 is
Function of
dom ta1,
cod ta1
by FUNCT_2:121;
set X =
dom (ta1 `2 );
A43:
dom (t . a) =
(fDom (Hom A)) . (t . a)
by A25
.=
dom ta1
by ENS_1:def 10
;
A44:
Hom (<|c',?> . a),
(<|c,?> . a) <> {}
by A38, NATTRA_1:def 2;
then A45:
dom (t . a) = <|c',?> . a
by CAT_1:23;
A46:
cod (t . a) = <|c,?> . a
by A44, CAT_1:23;
A47:
cod (t . a) =
(fCod (Hom A)) . (t . a)
by A25
.=
cod ta1
by ENS_1:def 11
;
then A48:
ta1 = [[(<|c',?> . a),(<|c,?> . a)],(ta1 `2 )]
by A45, A46, A43, ENS_1:8;
A49:
ta1 `2 is
Function of
dom (t . a),
cod (t . a)
by A43, A47, A41, FUNCT_2:121;
A50:
dom (ta1 `2 ) = Hom c',
a
A51:
for
x being
set st
x in dom (ta1 `2 ) holds
(hom f,(id a)) . x = (ta1 `2 ) . x
proof
reconsider t1 =
t . c' as
Element of
Maps (Hom A) by A25;
let x be
set ;
( x in dom (ta1 `2 ) implies (hom f,(id a)) . x = (ta1 `2 ) . x )
A52:
f in Hom c,
(cod f)
by A35, CAT_1:18;
assume A53:
x in dom (ta1 `2 )
;
(hom f,(id a)) . x = (ta1 `2 ) . x
then reconsider y =
x as
Morphism of
cod f,
a by A36, A50, CAT_1:def 7;
reconsider h =
y as
Morphism of
c',
a by A21, A24, A30, CAT_1:23;
A54:
dom h = c'
by A50, A53, CAT_1:23;
reconsider tc' =
<|c',?> . h as
Element of
Maps (Hom A) by A25;
A55:
cod h = a
by A50, A53, CAT_1:23;
reconsider tch =
<|c,?> . h as
Element of
Maps (Hom A) by A25;
A56:
[[(Hom c,(dom h)),(Hom c,(cod h))],(hom c,h)] =
<|c,?> . h
by ENS_1:def 22
.=
<|c,?> . h
by A50, A53, NATTRA_1:def 1
;
A57:
[[(Hom c',(dom h)),(Hom c',(cod h))],(hom c',h)] =
<|c',?> . h
by ENS_1:def 22
.=
<|c',?> . h
by A50, A53, NATTRA_1:def 1
;
A58:
cod (<|c',?> . h) =
(fCod (Hom A)) . (<|c',?> . h)
by A25
.=
cod tc'
by ENS_1:def 11
;
then A59:
cod (<|c',?> . h) =
(tc' `1 ) `2
by ENS_1:def 5
.=
[(Hom c',(dom h)),(Hom c',(cod h))] `2
by A57, MCART_1:7
.=
Hom c',
(cod h)
by MCART_1:7
;
then A60:
[(t . a),(<|c',?> . h)] in dom the
Comp of
(EnsHom A)
by A45, A40, A55, CAT_1:40;
tc' in Maps (dom tc'),
(cod tc')
by ENS_1:19;
then A61:
tc' `2 in Funcs (dom tc'),
(cod tc')
by ENS_1:20;
A62:
dom (<|c',?> . h) =
(fDom (Hom A)) . (<|c',?> . h)
by A25
.=
dom tc'
by ENS_1:def 10
;
then dom (<|c',?> . h) =
(tc' `1 ) `1
by ENS_1:def 4
.=
[(Hom c',(dom h)),(Hom c',(cod h))] `1
by A57, MCART_1:7
.=
Hom c',
(dom h)
by MCART_1:7
;
then
tc' `2 is
Function of
Hom c',
(dom h),
Hom c',
(cod h)
by A62, A58, A59, A61, FUNCT_2:121;
then A63:
dom (tc' `2 ) = Hom c',
c'
by A50, A53, A54, A55, FUNCT_2:def 1;
A64:
dom y = cod f
by A36, A50, A53, CAT_1:23;
tch = [[(dom tch),(cod tch)],(tch `2 )]
by ENS_1:8;
then
[(Hom c,(dom h)),(Hom c,(cod h)),(hom c,h)] = [[(dom tch),(cod tch)],(tch `2 )]
by A56, MCART_1:def 3;
then
[(Hom c,(dom h)),(Hom c,(cod h)),(hom c,h)] = [(dom tch),(cod tch),(tch `2 )]
by MCART_1:def 3;
then A65:
hom c,
h = tch `2
by MCART_1:28;
tc' = [[(dom tc'),(cod tc')],(tc' `2 )]
by ENS_1:8;
then
[(dom tc'),(cod tc'),(tc' `2 )] = [[(Hom c',(dom h)),(Hom c',(cod h))],(hom c',h)]
by A57, MCART_1:def 3;
then
[(dom tc'),(cod tc'),(tc' `2 )] = [(Hom c',(dom h)),(Hom c',(cod h)),(hom c',h)]
by MCART_1:def 3;
then A66:
tc' `2 = hom c',
h
by MCART_1:28;
A67:
Hom (<|c',?> . c'),
(<|c,?> . c') <> {}
by A38, NATTRA_1:def 2;
then
t . c' in Hom (<|c',?> . c'),
(<|c,?> . c')
by CAT_1:def 7;
then A68:
cod (t . c') = <|c,?> . c'
by CAT_1:18;
dom (<|c,?> . h) =
(fDom (Hom A)) . (<|c,?> . h)
by A25
.=
dom tch
by ENS_1:def 10
;
then dom (<|c,?> . h) =
(tch `1 ) `1
by ENS_1:def 4
.=
[(Hom c,(dom h)),(Hom c,(cod h))] `1
by A56, MCART_1:7
.=
Hom c,
(dom h)
by MCART_1:7
;
then A69:
[(<|c,?> . h),(t . c')] in dom the
Comp of
(EnsHom A)
by A21, A54, A68, CAT_1:40;
cod (t . c') =
(fCod (Hom A)) . (t . c')
by A25
.=
cod t1
by ENS_1:def 11
;
then A70:
cod t1 =
[(Hom c,(dom h)),(Hom c,(cod h))] `1
by A21, A54, A68, MCART_1:7
.=
(tch `1 ) `1
by A56, MCART_1:7
.=
dom tch
by ENS_1:def 4
;
Hom (<|c,?> . c'),
(<|c,?> . a) <> {}
by A50, A53, CAT_1:126;
then A71:
(<|c,?> . h) * (t . c') =
(<|c,?> . h) * (t . c')
by A67, CAT_1:def 13
.=
(fComp (Hom A)) . tch,
t1
by A25, A69, CAT_1:def 4
.=
tch * t1
by A70, ENS_1:def 12
.=
[[(dom t1),(cod tch)],((tch `2 ) * (t1 `2 ))]
by A70, ENS_1:def 7
;
A72:
cod tc' =
(tc' `1 ) `2
by ENS_1:def 5
.=
[(Hom c',(dom h)),(Hom c',(cod h))] `2
by A57, MCART_1:7
.=
dom ta1
by A45, A43, A40, A55, MCART_1:7
;
Hom (<|c',?> . c'),
(<|c',?> . a) <> {}
by A50, A53, CAT_1:126;
then A73:
(t . a) * (<|c',?> . h) =
(t . a) * (<|c',?> . h)
by A44, CAT_1:def 13
.=
(fComp (Hom A)) . ta1,
tc'
by A25, A60, CAT_1:def 4
.=
ta1 * tc'
by A72, ENS_1:def 12
.=
[[(dom tc'),(cod ta1)],((ta1 `2 ) * (tc' `2 ))]
by A72, ENS_1:def 7
;
(t . a) * (<|c',?> . h) = (<|c,?> . h) * (t . c')
by A4, A37, A19, A17, A11, A50, A53, NATTRA_1:def 8;
then
[(dom tc'),(cod ta1),((ta1 `2 ) * (tc' `2 ))] = [[(dom t1),(cod tch)],((tch `2 ) * (t1 `2 ))]
by A73, A71, MCART_1:def 3;
then
[(dom tc'),(cod ta1),((ta1 `2 ) * (tc' `2 ))] = [(dom t1),(cod tch),((tch `2 ) * (t1 `2 ))]
by MCART_1:def 3;
then A74:
(ta1 `2 ) * (tc' `2 ) = (tch `2 ) * (t1 `2 )
by MCART_1:28;
A75:
id c' in Hom c',
(cod f)
by A36, CAT_1:55;
(hom f,(id a)) . x =
(hom f,a) . y
by ENS_1:53
.=
y * f
by A36, A50, A53, ENS_1:def 21
.=
(tch `2 ) . ((t1 `2 ) . (id c'))
by A64, A65, A52, ENS_1:def 20
.=
((ta1 `2 ) * (tc' `2 )) . (id c')
by A32, A74, CAT_1:55, FUNCT_1:23
.=
(ta1 `2 ) . ((hom c',h) . (id c'))
by A66, A63, CAT_1:55, FUNCT_1:23
.=
(ta1 `2 ) . (y * (id c'))
by A64, A75, ENS_1:def 20
.=
(ta1 `2 ) . x
by A36, A64, CAT_1:47
;
hence
(hom f,(id a)) . x = (ta1 `2 ) . x
;
verum
end;
dom (hom f,a) = Hom (cod f),
a
then
dom (ta1 `2 ) = dom (hom f,(id a))
by A36, A50, ENS_1:53;
then
hom f,
(id a) = ta1 `2
by A51, FUNCT_1:9;
hence
<|f,?> . a = t . a
by A35, A36, A40, A39, A48, Def3;
verum
end;
then
<|f,?> = t
by A4, A37, A19, A17, A11, A35, A36, ISOCAT_1:31;
hence
g = (Yoneda A) . f
by A3, A5, A18, A22, A17, A11, A35, A36, Def4;
verum
end;
hence
Yoneda A is full
by Def7; verum