set F = Yoneda A;
for c, c9 being Object of A st Hom ((Yoneda A) . c9),((Yoneda A) . c) <> {} holds
for g being Morphism of (Yoneda A) . c9,(Yoneda A) . c holds
( Hom c,c9 <> {} & ex f being Morphism of c,c9 st g = (Yoneda A) . f )
proof
let c,
c9 be
Object of
A;
( Hom ((Yoneda A) . c9),((Yoneda A) . c) <> {} implies for g being Morphism of (Yoneda A) . c9,(Yoneda A) . c holds
( Hom c,c9 <> {} & ex f being Morphism of c,c9 st g = (Yoneda A) . f ) )
assume A1:
Hom ((Yoneda A) . c9),
((Yoneda A) . c) <> {}
;
for g being Morphism of (Yoneda A) . c9,(Yoneda A) . c holds
( Hom c,c9 <> {} & ex f being Morphism of c,c9 st g = (Yoneda A) . f )
A2:
<|c9,?> . c9 =
(hom?- (Hom A),c9) . c9
by ENS_1:def 26
.=
(Obj (hom?- (Hom A),c9)) . c9
by CAT_1:def 20
.=
Hom c9,
c9
by ENS_1:60
;
let g be
Morphism of
(Yoneda A) . c9,
(Yoneda A) . c;
( Hom c,c9 <> {} & ex f being Morphism of c,c9 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;
<|c9,?> in Funct A,
(EnsHom A)
by CAT_2:def 2;
then reconsider d1 =
<|c9,?> as
Object of
(Functors A,(EnsHom A)) by NATTRA_1:def 18;
<|c,?> in Funct A,
(EnsHom A)
by CAT_2:def 2;
then reconsider d =
<|c,?> as
Object of
(Functors A,(EnsHom A)) 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
A 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 c9) = id d1
proof
set X =
dom <|(id c9),?>;
A13:
for
y being
set st
y in dom <|(id c9),?> holds
<|(id c9),?> . y = (id <|c9,?>) . y
proof
let y be
set ;
( y in dom <|(id c9),?> implies <|(id c9),?> . y = (id <|c9,?>) . y )
assume
y in dom <|(id c9),?>
;
<|(id c9),?> . y = (id <|c9,?>) . y
then reconsider z =
y as
Object of
A by FUNCT_2:def 1;
reconsider zz =
id z as
Morphism of
z,
z ;
A14:
Hom z,
z <> {}
by CAT_1:56;
<|(cod (id c9)),?> is_transformable_to <|c9,?>
by CAT_1:44;
then A15:
<|(cod (id c9)),?> is_transformable_to <|(dom (id c9)),?>
by CAT_1:44;
<|(id c9),?> . z =
[[(Hom (cod (id c9)),z),(Hom (dom (id c9)),z)],(hom (id c9),(id z))]
by Def3
.=
[[(Hom c9,z),(Hom (dom (id c9)),z)],(hom (id c9),(id z))]
by CAT_1:44
.=
[[(Hom c9,z),(Hom c9,z)],(hom (id c9),(id z))]
by CAT_1:44
.=
[[(Hom c9,z),(Hom c9,z)],(hom c9,(id z))]
by ENS_1:53
.=
[[(Hom c9,z),(Hom c9,(cod (id z)))],(hom c9,(id z))]
by CAT_1:44
.=
[[(Hom c9,(dom (id z))),(Hom c9,(cod (id z)))],(hom c9,(id z))]
by CAT_1:44
.=
<|c9,?> . (id z)
by ENS_1:def 22
.=
<|c9,?> . zz
by A14, NATTRA_1:def 1
.=
id (<|c9,?> . z)
by NATTRA_1:15
.=
(id <|c9,?>) . z
by NATTRA_1:21
.=
(id <|c9,?>) . z
by NATTRA_1:def 5
;
hence
<|(id c9),?> . y = (id <|c9,?>) . y
by A15, NATTRA_1:def 5;
verum
end;
dom <|(id c9),?> =
the
carrier of
A
by FUNCT_2:def 1
.=
dom (id <|c9,?>)
by FUNCT_2:def 1
;
then A16:
<|(id c9),?> = id <|c9,?>
by A13, FUNCT_1:9;
(Yoneda A) . (id c9) =
[[<|(cod (id c9)),?>,<|(dom (id c9)),?>],<|(id c9),?>]
by Def4
.=
[[<|c9,?>,<|(dom (id c9)),?>],<|(id c9),?>]
by CAT_1:44
.=
[[<|c9,?>,<|c9,?>],(id <|c9,?>)]
by A16, CAT_1:44
.=
id d1
by NATTRA_1:def 18
;
hence
(Yoneda A) . (id c9) = id d1
;
verum
end;
then A17:
(Obj (Yoneda A)) . c9 = 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) . c9 = d1
by A12, OPPCAT_1:31;
A21:
<|c,?> . c9 =
(hom?- (Hom A),c) . c9
by ENS_1:def 26
.=
(Obj (hom?- (Hom A),c)) . c9
by CAT_1:def 20
.=
Hom c,
c9
by ENS_1:60
;
A22:
(
dom g = (Yoneda A) . c9 &
cod g = (Yoneda A) . c )
by A1, CAT_1:23;
then reconsider t =
t as
natural_transformation of
<|c9,?>,
<|c,?> by A5, A18, A12, A11, OPPCAT_1:31;
(Obj (Yoneda A)) . c = d
by A6, OPPCAT_1:31;
then
<|c9,?> is_transformable_to <|c,?>
by A4, A5, A18, A22, A20, NATTRA_1:def 7;
then
Hom (<|c9,?> . c9),
(<|c,?> . c9) <> {}
by NATTRA_1:def 2;
then A23:
t . c9 in Hom (<|c9,?> . c9),
(<|c,?> . c9)
by CAT_1:def 7;
then A24:
cod (t . c9) = <|c,?> . c9
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 . c9 as
Element of
Maps (Hom A) ;
A26:
cod (t . c9) =
(fCod (Hom A)) . (t . c9)
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 . c9) = <|c9,?> . c9
by A23, CAT_1:18;
then
the
Source of
(EnsHom A) . (t . c9) <> {}
by A2, CAT_1:56;
then
dom t1 <> {}
by A25, ENS_1:def 10;
then A29:
cod t1 <> {}
by A27;
then A30:
cod (t . c9) <> {}
by A25, ENS_1:def 11;
hence
Hom c,
c9 <> {}
by A21, A23, CAT_1:18;
ex f being Morphism of c,c9 st g = (Yoneda A) . f
dom (t . c9) =
(fDom (Hom A)) . (t . c9)
by A25
.=
dom t1
by ENS_1:def 10
;
then A31:
t1 `2 is
Function of
(<|c9,?> . c9),
(<|c,?> . c9)
by A28, A24, A27, A26, FUNCT_2:121;
then A32:
dom (t1 `2 ) = Hom c9,
c9
by A2, A24, A30, FUNCT_2:def 1;
then
id c9 in dom (t1 `2 )
by CAT_1:55;
then A33:
(t1 `2 ) . (id c9) in rng (t1 `2 )
by FUNCT_1:def 5;
rng (t1 `2 ) c= Hom c,
c9
by A21, A31, RELAT_1:def 19;
then
(t1 `2 ) . (id c9) in Hom c,
c9
by A33;
then reconsider f =
(t1 `2 ) . (id c9) as
Morphism of
c,
c9 by CAT_1:def 7;
A34:
<|c,?> . c9 <> {}
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 = c9
by A21, A34, CAT_1:23;
A37:
F1 = (Yoneda A) . c9
by A1, A5, CAT_1:23;
then A38:
<|c9,?> is_transformable_to <|c,?>
by A4, A19, A17, A11, NATTRA_1:def 7;
for
a being
Object of
A holds
<|f,?> . a = t . a
proof
let a be
Object of
A;
<|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:
<|c9,?> . a =
(hom?- (Hom A),c9) . a
by ENS_1:def 26
.=
(Obj (hom?- (Hom A),c9)) . a
by CAT_1:def 20
.=
Hom c9,
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 (<|c9,?> . a),
(<|c,?> . a) <> {}
by A38, NATTRA_1:def 2;
then A45:
dom (t . a) = <|c9,?> . 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 = [[(<|c9,?> . 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 c9,
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 . c9 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
c9,
a by A21, A24, A30, CAT_1:23;
A54:
dom h = c9
by A50, A53, CAT_1:23;
reconsider tc9 =
<|c9,?> . 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 c9,(dom h)),(Hom c9,(cod h))],(hom c9,h)] =
<|c9,?> . h
by ENS_1:def 22
.=
<|c9,?> . h
by A50, A53, NATTRA_1:def 1
;
A58:
cod (<|c9,?> . h) =
(fCod (Hom A)) . (<|c9,?> . h)
by A25
.=
cod tc9
by ENS_1:def 11
;
then A59:
cod (<|c9,?> . h) =
(tc9 `1 ) `2
by ENS_1:def 5
.=
[(Hom c9,(dom h)),(Hom c9,(cod h))] `2
by A57, MCART_1:7
.=
Hom c9,
(cod h)
by MCART_1:7
;
then A60:
[(t . a),(<|c9,?> . h)] in dom the
Comp of
(EnsHom A)
by A45, A40, A55, CAT_1:40;
tc9 in Maps (dom tc9),
(cod tc9)
by ENS_1:19;
then A61:
tc9 `2 in Funcs (dom tc9),
(cod tc9)
by ENS_1:20;
A62:
dom (<|c9,?> . h) =
(fDom (Hom A)) . (<|c9,?> . h)
by A25
.=
dom tc9
by ENS_1:def 10
;
then dom (<|c9,?> . h) =
(tc9 `1 ) `1
by ENS_1:def 4
.=
[(Hom c9,(dom h)),(Hom c9,(cod h))] `1
by A57, MCART_1:7
.=
Hom c9,
(dom h)
by MCART_1:7
;
then
tc9 `2 is
Function of
(Hom c9,(dom h)),
(Hom c9,(cod h))
by A62, A58, A59, A61, FUNCT_2:121;
then A63:
dom (tc9 `2 ) = Hom c9,
c9
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;
tc9 = [[(dom tc9),(cod tc9)],(tc9 `2 )]
by ENS_1:8;
then
[(dom tc9),(cod tc9),(tc9 `2 )] = [[(Hom c9,(dom h)),(Hom c9,(cod h))],(hom c9,h)]
by A57, MCART_1:def 3;
then
[(dom tc9),(cod tc9),(tc9 `2 )] = [(Hom c9,(dom h)),(Hom c9,(cod h)),(hom c9,h)]
by MCART_1:def 3;
then A66:
tc9 `2 = hom c9,
h
by MCART_1:28;
A67:
Hom (<|c9,?> . c9),
(<|c,?> . c9) <> {}
by A38, NATTRA_1:def 2;
then
t . c9 in Hom (<|c9,?> . c9),
(<|c,?> . c9)
by CAT_1:def 7;
then A68:
cod (t . c9) = <|c,?> . c9
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 . c9)] in dom the
Comp of
(EnsHom A)
by A21, A54, A68, CAT_1:40;
cod (t . c9) =
(fCod (Hom A)) . (t . c9)
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,?> . c9),
(<|c,?> . a) <> {}
by A50, A53, CAT_1:126;
then A71:
(<|c,?> . h) * (t . c9) =
(<|c,?> . h) * (t . c9)
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 tc9 =
(tc9 `1 ) `2
by ENS_1:def 5
.=
[(Hom c9,(dom h)),(Hom c9,(cod h))] `2
by A57, MCART_1:7
.=
dom ta1
by A45, A43, A40, A55, MCART_1:7
;
Hom (<|c9,?> . c9),
(<|c9,?> . a) <> {}
by A50, A53, CAT_1:126;
then A73:
(t . a) * (<|c9,?> . h) =
(t . a) * (<|c9,?> . h)
by A44, CAT_1:def 13
.=
(fComp (Hom A)) . ta1,
tc9
by A25, A60, CAT_1:def 4
.=
ta1 * tc9
by A72, ENS_1:def 12
.=
[[(dom tc9),(cod ta1)],((ta1 `2 ) * (tc9 `2 ))]
by A72, ENS_1:def 7
;
(t . a) * (<|c9,?> . h) = (<|c,?> . h) * (t . c9)
by A4, A37, A19, A17, A11, A50, A53, NATTRA_1:def 8;
then
[(dom tc9),(cod ta1),((ta1 `2 ) * (tc9 `2 ))] = [[(dom t1),(cod tch)],((tch `2 ) * (t1 `2 ))]
by A73, A71, MCART_1:def 3;
then
[(dom tc9),(cod ta1),((ta1 `2 ) * (tc9 `2 ))] = [(dom t1),(cod tch),((tch `2 ) * (t1 `2 ))]
by MCART_1:def 3;
then A74:
(ta1 `2 ) * (tc9 `2 ) = (tch `2 ) * (t1 `2 )
by MCART_1:28;
A75:
id c9 in Hom c9,
(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 c9))
by A64, A65, A52, ENS_1:def 20
.=
((ta1 `2 ) * (tc9 `2 )) . (id c9)
by A32, A74, CAT_1:55, FUNCT_1:23
.=
(ta1 `2 ) . ((hom c9,h) . (id c9))
by A66, A63, CAT_1:55, FUNCT_1:23
.=
(ta1 `2 ) . (y * (id c9))
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