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 25
.=
(Obj (hom?- ((Hom A),c9))) . c9
by CAT_1:def 17
.=
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 17;
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:33;
<|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 17;
<|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 17;
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:27;
<|(cod (id c)),?> is_transformable_to <|c,?>
by CAT_1:19;
then A9:
<|(cod (id c)),?> is_transformable_to <|(dom (id c)),?>
by CAT_1:19;
<|(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:19
.=
[[(Hom (c,z)),(Hom (c,z))],(hom ((id c),(id z)))]
by CAT_1:19
.=
[[(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:19
.=
[[(Hom (c,(dom (id z)))),(Hom (c,(cod (id z))))],(hom (c,(id z)))]
by CAT_1:19
.=
<|c,?> . (id z)
by ENS_1:def 21
.=
<|c,?> . zz
by A8, NATTRA_1:def 1
.=
id (<|c,?> . z)
by NATTRA_1:15
.=
(id <|c,?>) . z
by NATTRA_1:20
.=
(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:2;
(Yoneda A) . (id c) =
[[<|(cod (id c)),?>,<|(dom (id c)),?>],<|(id c),?>]
by Def4
.=
[[<|c,?>,<|(dom (id c)),?>],<|(id c),?>]
by CAT_1:19
.=
[[<|c,?>,<|c,?>],(id <|c,?>)]
by A10, CAT_1:19
.=
id d
by NATTRA_1:def 17
;
hence
(Yoneda A) . (id c) = id d
;
verum
end;
then A11:
(Yoneda A) . c = d
by OPPCAT_1:30;
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:27;
<|(cod (id c9)),?> is_transformable_to <|c9,?>
by CAT_1:19;
then A15:
<|(cod (id c9)),?> is_transformable_to <|(dom (id c9)),?>
by CAT_1:19;
<|(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:19
.=
[[(Hom (c9,z)),(Hom (c9,z))],(hom ((id c9),(id z)))]
by CAT_1:19
.=
[[(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:19
.=
[[(Hom (c9,(dom (id z)))),(Hom (c9,(cod (id z))))],(hom (c9,(id z)))]
by CAT_1:19
.=
<|c9,?> . (id z)
by ENS_1:def 21
.=
<|c9,?> . zz
by A14, NATTRA_1:def 1
.=
id (<|c9,?> . z)
by NATTRA_1:15
.=
(id <|c9,?>) . z
by NATTRA_1:20
.=
(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:2;
(Yoneda A) . (id c9) =
[[<|(cod (id c9)),?>,<|(dom (id c9)),?>],<|(id c9),?>]
by Def4
.=
[[<|c9,?>,<|(dom (id c9)),?>],<|(id c9),?>]
by CAT_1:19
.=
[[<|c9,?>,<|c9,?>],(id <|c9,?>)]
by A16, CAT_1:19
.=
id d1
by NATTRA_1:def 17
;
hence
(Yoneda A) . (id c9) = id d1
;
verum
end;
then A17:
(Obj (Yoneda A)) . c9 = d1
by OPPCAT_1:30;
A18:
cod g = F2
by A3, NATTRA_1:33;
then A19:
F2 = (Yoneda A) . c
by A1, CAT_1:5;
A20:
(Yoneda A) . c9 = d1
by A12, OPPCAT_1:30;
A21:
<|c,?> . c9 =
(hom?- ((Hom A),c)) . c9
by ENS_1:def 25
.=
(Obj (hom?- ((Hom A),c))) . c9
by CAT_1:def 17
.=
Hom (
c,
c9)
by ENS_1:60
;
A22:
(
dom g = (Yoneda A) . c9 &
cod g = (Yoneda A) . c )
by A1, CAT_1:5;
then reconsider t =
t as
natural_transformation of
<|c9,?>,
<|c,?> by A5, A18, A12, A11, OPPCAT_1:30;
(Obj (Yoneda A)) . c = d
by A6, OPPCAT_1:30;
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 4;
then A24:
cod (t . c9) = <|c,?> . c9
by CAT_1:1;
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 13;
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 10
;
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:1;
then
the
Source of
(EnsHom A) . (t . c9) <> {}
by A2, CAT_1:27;
then
dom t1 <> {}
by A25, ENS_1:def 9;
then A29:
cod t1 <> {}
by A27;
then A30:
cod (t . c9) <> {}
by A25, ENS_1:def 10;
hence
Hom (
c,
c9)
<> {}
by A21, A23, CAT_1:1;
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 9
;
then A31:
t1 `2 is
Function of
(<|c9,?> . c9),
(<|c,?> . c9)
by A28, A24, A27, A26, FUNCT_2:66;
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:26;
then A33:
(t1 `2) . (id c9) in rng (t1 `2)
by FUNCT_1:def 3;
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 4;
A34:
<|c,?> . c9 <> {}
by A24, A25, A29, ENS_1:def 10;
then A35:
dom f = c
by A21, CAT_1:5;
take
f
;
g = (Yoneda A) . f
A36:
cod f = c9
by A21, A34, CAT_1:5;
A37:
F1 = (Yoneda A) . c9
by A1, A5, CAT_1:5;
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 25
.=
(Obj (hom?- ((Hom A),c))) . a
by CAT_1:def 17
.=
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 25
.=
(Obj (hom?- ((Hom A),c9))) . a
by CAT_1:def 17
.=
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:66;
set X =
dom (ta1 `2);
A43:
dom (t . a) =
(fDom (Hom A)) . (t . a)
by A25
.=
dom ta1
by ENS_1:def 9
;
A44:
Hom (
(<|c9,?> . a),
(<|c,?> . a))
<> {}
by A38, NATTRA_1:def 2;
then A45:
dom (t . a) = <|c9,?> . a
by CAT_1:5;
A46:
cod (t . a) = <|c,?> . a
by A44, CAT_1:5;
A47:
cod (t . a) =
(fCod (Hom A)) . (t . a)
by A25
.=
cod ta1
by ENS_1:def 10
;
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:66;
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:1;
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 4;
reconsider h =
y as
Morphism of
c9,
a by A21, A24, A30, CAT_1:5;
A54:
dom h = c9
by A50, A53, CAT_1:5;
reconsider tc9 =
<|c9,?> . h as
Element of
Maps (Hom A) by A25;
A55:
cod h = a
by A50, A53, CAT_1:5;
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 21
.=
<|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 21
.=
<|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 10
;
then A59:
cod (<|c9,?> . h) =
(tc9 `1) `2
by ENS_1:def 4
.=
[(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:15;
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 9
;
then dom (<|c9,?> . h) =
(tc9 `1) `1
by ENS_1:def 3
.=
[(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:66;
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:5;
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:25;
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:25;
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 4;
then A68:
cod (t . c9) = <|c,?> . c9
by CAT_1:1;
dom (<|c,?> . h) =
(fDom (Hom A)) . (<|c,?> . h)
by A25
.=
dom tch
by ENS_1:def 9
;
then dom (<|c,?> . h) =
(tch `1) `1
by ENS_1:def 3
.=
[(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:15;
cod (t . c9) =
(fCod (Hom A)) . (t . c9)
by A25
.=
cod t1
by ENS_1:def 10
;
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 3
;
Hom (
(<|c,?> . c9),
(<|c,?> . a))
<> {}
by A50, A53, CAT_1:84;
then A71:
(<|c,?> . h) * (t . c9) =
(<|c,?> . h) * (t . c9)
by A67, CAT_1:def 10
.=
(fComp (Hom A)) . (
tch,
t1)
by A25, A69, CAT_1:def 1
.=
tch * t1
by A70, ENS_1:def 11
.=
[[(dom t1),(cod tch)],((tch `2) * (t1 `2))]
by A70, ENS_1:def 6
;
A72:
cod tc9 =
(tc9 `1) `2
by ENS_1:def 4
.=
[(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:84;
then A73:
(t . a) * (<|c9,?> . h) =
(t . a) * (<|c9,?> . h)
by A44, CAT_1:def 10
.=
(fComp (Hom A)) . (
ta1,
tc9)
by A25, A60, CAT_1:def 1
.=
ta1 * tc9
by A72, ENS_1:def 11
.=
[[(dom tc9),(cod ta1)],((ta1 `2) * (tc9 `2))]
by A72, ENS_1:def 6
;
(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:25;
A75:
id c9 in Hom (
c9,
(cod f))
by A36, CAT_1:26;
(hom (f,(id a))) . x =
(hom (f,a)) . y
by ENS_1:53
.=
y * f
by A36, A50, A53, ENS_1:def 20
.=
(tch `2) . ((t1 `2) . (id c9))
by A64, A65, A52, ENS_1:def 19
.=
((ta1 `2) * (tc9 `2)) . (id c9)
by A32, A74, CAT_1:26, FUNCT_1:13
.=
(ta1 `2) . ((hom (c9,h)) . (id c9))
by A66, A63, CAT_1:26, FUNCT_1:13
.=
(ta1 `2) . (y * (id c9))
by A64, A75, ENS_1:def 19
.=
(ta1 `2) . x
by A36, A64, CAT_1:22
;
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:2;
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:26;
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