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
.=
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
object st
y in dom <|(id c),?> holds
<|(id c),?> . y = (id <|c,?>) . y
proof
let y be
object ;
( 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)
<> {}
;
<|(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)))]
.=
[[(Hom (c,z)),(Hom (c,z))],(hom ((id c),(id z)))]
.=
[[(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)))]
.=
[[(Hom (c,(dom (id z)))),(Hom (c,(cod (id z))))],(hom (c,(id z)))]
.=
<|c,?> . (id z)
by ENS_1:def 21
.=
<|c,?> /. zz
by A8, CAT_3:def 10
.=
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 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 A9:
<|(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),?>]
.=
[[<|c,?>,<|c,?>],(id <|c,?>)]
by A9
.=
id d
by NATTRA_1:def 17
;
hence
(Yoneda A) . (id c) = id d
;
verum
end;
then A10:
(Yoneda A) . c = d
by OPPCAT_1:30;
A11:
(Yoneda A) . (id c9) = id d1
proof
set X =
dom <|(id c9),?>;
A12:
for
y being
object st
y in dom <|(id c9),?> holds
<|(id c9),?> . y = (id <|c9,?>) . y
proof
let y be
object ;
( 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 ;
A13:
Hom (
z,
z)
<> {}
;
<|(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)))]
.=
[[(Hom (c9,z)),(Hom (c9,z))],(hom ((id c9),(id z)))]
.=
[[(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)))]
.=
[[(Hom (c9,(dom (id z)))),(Hom (c9,(cod (id z))))],(hom (c9,(id z)))]
.=
<|c9,?> . (id z)
by ENS_1:def 21
.=
<|c9,?> /. zz
by A13, CAT_3:def 10
.=
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 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 A14:
<|(id c9),?> = id <|c9,?>
by A12, FUNCT_1:2;
(Yoneda A) . (id c9) =
[[<|(cod (id c9)),?>,<|(dom (id c9)),?>],<|(id c9),?>]
by Def4
.=
[[<|c9,?>,<|(dom (id c9)),?>],<|(id c9),?>]
.=
[[<|c9,?>,<|c9,?>],(id <|c9,?>)]
by A14
.=
id d1
by NATTRA_1:def 17
;
hence
(Yoneda A) . (id c9) = id d1
;
verum
end;
then A15:
(Obj (Yoneda A)) . c9 = d1
by OPPCAT_1:30;
A16:
cod g = F2
by A3, NATTRA_1:33;
then A17:
F2 = (Yoneda A) . c
by A1, CAT_1:5;
A18:
(Yoneda A) . c9 = d1
by A11, OPPCAT_1:30;
A19:
<|c,?> . c9 =
(hom?- ((Hom A),c)) . c9
by ENS_1:def 25
.=
(Obj (hom?- ((Hom A),c))) . c9
.=
Hom (
c,
c9)
by ENS_1:60
;
A20:
(
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, A16, A11, A10, OPPCAT_1:30;
(Obj (Yoneda A)) . c = d
by A6, OPPCAT_1:30;
then
<|c9,?> is_transformable_to <|c,?>
by A4, A5, A16, A20, A18, NATTRA_1:def 7;
then
Hom (
(<|c9,?> . c9),
(<|c,?> . c9))
<> {}
by NATTRA_1:def 2;
then A21:
t . c9 in Hom (
(<|c9,?> . c9),
(<|c,?> . c9))
by CAT_1:def 5;
then A22:
cod (t . c9) = <|c,?> . c9
by CAT_1:1;
A23:
EnsHom A = CatStr(#
(Hom A),
(Maps (Hom A)),
(fDom (Hom A)),
(fCod (Hom A)),
(fComp (Hom A)) #)
by ENS_1:def 13;
then reconsider t1 =
t . c9 as
Element of
Maps (Hom A) ;
A24:
cod (t . c9) =
(fCod (Hom A)) . (t . c9)
by A23
.=
cod t1
by ENS_1:def 10
;
t1 in Maps (
(dom t1),
(cod t1))
by ENS_1:19;
then A25:
t1 `2 in Funcs (
(dom t1),
(cod t1))
by ENS_1:20;
A26:
dom (t . c9) = <|c9,?> . c9
by A21, CAT_1:1;
then
the
Source of
(EnsHom A) . (t . c9) <> {}
by A2;
then
dom t1 <> {}
by A23, ENS_1:def 9;
then A27:
cod t1 <> {}
by A25;
then A28:
cod (t . c9) <> {}
by A23, ENS_1:def 10;
hence
Hom (
c,
c9)
<> {}
by A19, A21, CAT_1:1;
ex f being Morphism of c,c9 st g = (Yoneda A) . f
dom (t . c9) =
(fDom (Hom A)) . (t . c9)
by A23
.=
dom t1
by ENS_1:def 9
;
then A29:
t1 `2 is
Function of
(<|c9,?> . c9),
(<|c,?> . c9)
by A26, A22, A25, A24, FUNCT_2:66;
then A30:
dom (t1 `2) = Hom (
c9,
c9)
by A2, A22, A28, FUNCT_2:def 1;
then
id c9 in dom (t1 `2)
by CAT_1:27;
then A31:
(t1 `2) . (id c9) in rng (t1 `2)
by FUNCT_1:def 3;
rng (t1 `2) c= Hom (
c,
c9)
by A19, A29, RELAT_1:def 19;
then
(t1 `2) . (id c9) in Hom (
c,
c9)
by A31;
then reconsider f =
(t1 `2) . (id c9) as
Morphism of
c,
c9 by CAT_1:def 5;
A32:
<|c,?> . c9 <> {}
by A22, A23, A27, ENS_1:def 10;
then A33:
dom f = c
by A19, CAT_1:5;
take
f
;
g = (Yoneda A) . f
A34:
cod f = c9
by A19, A32, CAT_1:5;
A35:
F1 = (Yoneda A) . c9
by A1, A5, CAT_1:5;
then A36:
<|c9,?> is_transformable_to <|c,?>
by A4, A17, A15, A10, 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
A37:
<|c,?> . a =
(hom?- ((Hom A),c)) . a
by ENS_1:def 25
.=
(Obj (hom?- ((Hom A),c))) . a
.=
Hom (
c,
a)
by ENS_1:60
;
reconsider ta1 =
t . a as
Element of
Maps (Hom A) by A23;
A38:
<|c9,?> . a =
(hom?- ((Hom A),c9)) . a
by ENS_1:def 25
.=
(Obj (hom?- ((Hom A),c9))) . a
.=
Hom (
c9,
a)
by ENS_1:60
;
ta1 in Maps (
(dom ta1),
(cod ta1))
by ENS_1:19;
then A39:
ta1 `2 in Funcs (
(dom ta1),
(cod ta1))
by ENS_1:20;
then A40:
ta1 `2 is
Function of
(dom ta1),
(cod ta1)
by FUNCT_2:66;
set X =
dom (ta1 `2);
A41:
dom (t . a) =
(fDom (Hom A)) . (t . a)
by A23
.=
dom ta1
by ENS_1:def 9
;
A42:
Hom (
(<|c9,?> . a),
(<|c,?> . a))
<> {}
by A36, NATTRA_1:def 2;
then A43:
dom (t . a) = <|c9,?> . a
by CAT_1:5;
A44:
cod (t . a) = <|c,?> . a
by A42, CAT_1:5;
A45:
cod (t . a) =
(fCod (Hom A)) . (t . a)
by A23
.=
cod ta1
by ENS_1:def 10
;
then A46:
ta1 = [[(<|c9,?> . a),(<|c,?> . a)],(ta1 `2)]
by A43, A44, A41, ENS_1:8;
A47:
ta1 `2 is
Function of
(dom (t . a)),
(cod (t . a))
by A41, A45, A39, FUNCT_2:66;
A48:
dom (ta1 `2) = Hom (
c9,
a)
A49:
for
x being
object 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 A23;
let x be
object ;
( x in dom (ta1 `2) implies (hom (f,(id a))) . x = (ta1 `2) . x )
A50:
f in Hom (
c,
(cod f))
by A33;
assume A51:
x in dom (ta1 `2)
;
(hom (f,(id a))) . x = (ta1 `2) . x
then reconsider y =
x as
Morphism of
cod f,
a by A34, A48, CAT_1:def 5;
reconsider h =
y as
Morphism of
c9,
a by A19, A22, A28, CAT_1:5;
A52:
dom h = c9
by A48, A51, CAT_1:5;
reconsider tc9 =
<|c9,?> . h as
Element of
Maps (Hom A) by A23;
A53:
cod h = a
by A48, A51, CAT_1:5;
reconsider tch =
<|c,?> . h as
Element of
Maps (Hom A) by A23;
A54:
[[(Hom (c,(dom h))),(Hom (c,(cod h)))],(hom (c,h))] =
<|c,?> . h
by ENS_1:def 21
.=
<|c,?> . h
;
A55:
[[(Hom (c9,(dom h))),(Hom (c9,(cod h)))],(hom (c9,h))] =
<|c9,?> . h
by ENS_1:def 21
.=
<|c9,?> . h
;
A56:
cod (<|c9,?> . h) =
(fCod (Hom A)) . (<|c9,?> . h)
by A23
.=
cod tc9
by ENS_1:def 10
;
then A57:
cod (<|c9,?> . h) =
(tc9 `1) `2
by ENS_1:def 4
.=
[(Hom (c9,(dom h))),(Hom (c9,(cod h)))] `2
by A55
.=
Hom (
c9,
(cod h))
;
then A58:
[(t . a),(<|c9,?> . h)] in dom the
Comp of
(EnsHom A)
by A43, A38, A53, CAT_1:15;
tc9 in Maps (
(dom tc9),
(cod tc9))
by ENS_1:19;
then A59:
tc9 `2 in Funcs (
(dom tc9),
(cod tc9))
by ENS_1:20;
A60:
dom (<|c9,?> . h) =
(fDom (Hom A)) . (<|c9,?> . h)
by A23
.=
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 A55
.=
Hom (
c9,
(dom h))
;
then
tc9 `2 is
Function of
(Hom (c9,(dom h))),
(Hom (c9,(cod h)))
by A60, A56, A57, A59, FUNCT_2:66;
then A61:
dom (tc9 `2) = Hom (
c9,
c9)
by A48, A51, A52, A53, FUNCT_2:def 1;
A62:
dom y = cod f
by A34, A48, A51, 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 A54;
then
[(Hom (c,(dom h))),(Hom (c,(cod h))),(hom (c,h))] = [(dom tch),(cod tch),(tch `2)]
;
then A63:
hom (
c,
h)
= tch `2
by XTUPLE_0:3;
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 A55;
then
[(dom tc9),(cod tc9),(tc9 `2)] = [(Hom (c9,(dom h))),(Hom (c9,(cod h))),(hom (c9,h))]
;
then A64:
tc9 `2 = hom (
c9,
h)
by XTUPLE_0:3;
A65:
Hom (
(<|c9,?> . c9),
(<|c,?> . c9))
<> {}
by A36, NATTRA_1:def 2;
then
t . c9 in Hom (
(<|c9,?> . c9),
(<|c,?> . c9))
by CAT_1:def 5;
then A66:
cod (t . c9) = <|c,?> . c9
by CAT_1:1;
dom (<|c,?> . h) =
(fDom (Hom A)) . (<|c,?> . h)
by A23
.=
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 A54
.=
Hom (
c,
(dom h))
;
then A67:
[(<|c,?> . h),(t . c9)] in dom the
Comp of
(EnsHom A)
by A19, A52, A66, CAT_1:15;
cod (t . c9) =
(fCod (Hom A)) . (t . c9)
by A23
.=
cod t1
by ENS_1:def 10
;
then A68:
cod t1 =
[(Hom (c,(dom h))),(Hom (c,(cod h)))] `1
by A19, A52, A66
.=
(tch `1) `1
by A54
.=
dom tch
by ENS_1:def 3
;
A69:
h in Hom (
c9,
a)
by A48, A51;
then A70:
<|c,?> /. h = <|c,?> . h
by CAT_3:def 10;
Hom (
(<|c,?> . c9),
(<|c,?> . a))
<> {}
by A48, A51, CAT_1:84;
then A71:
(<|c,?> /. h) * (t . c9) =
(<|c,?> . h) (*) (t . c9)
by A65, A70, CAT_1:def 13
.=
(fComp (Hom A)) . (
tch,
t1)
by A23, A67, CAT_1:def 1
.=
tch * t1
by A68, ENS_1:def 11
.=
[[(dom t1),(cod tch)],((tch `2) * (t1 `2))]
by A68, 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 A55
.=
dom ta1
by A43, A41, A38, A53
;
A73:
<|c9,?> /. h = <|c9,?> . h
by A69, CAT_3:def 10;
Hom (
(<|c9,?> . c9),
(<|c9,?> . a))
<> {}
by A48, A51, CAT_1:84;
then A74:
(t . a) * (<|c9,?> /. h) =
(t . a) (*) (<|c9,?> . h)
by A42, A73, CAT_1:def 13
.=
(fComp (Hom A)) . (
ta1,
tc9)
by A23, A58, 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, A35, A17, A15, A10, A48, A51, NATTRA_1:def 8;
then
[(dom tc9),(cod ta1),((ta1 `2) * (tc9 `2))] = [[(dom t1),(cod tch)],((tch `2) * (t1 `2))]
by A74, A71;
then
[(dom tc9),(cod ta1),((ta1 `2) * (tc9 `2))] = [(dom t1),(cod tch),((tch `2) * (t1 `2))]
;
then A75:
(ta1 `2) * (tc9 `2) = (tch `2) * (t1 `2)
by XTUPLE_0:3;
A76:
id c9 in Hom (
c9,
(cod f))
by A34, CAT_1:27;
(hom (f,(id a))) . x =
(hom (f,a)) . y
by ENS_1:53
.=
y (*) f
by A34, A48, A51, ENS_1:def 20
.=
(tch `2) . ((t1 `2) . (id c9))
by A62, A63, A50, ENS_1:def 19
.=
((ta1 `2) * (tc9 `2)) . (id c9)
by A30, A75, CAT_1:27, FUNCT_1:13
.=
(ta1 `2) . ((hom (c9,h)) . (id c9))
by A64, A61, CAT_1:27, FUNCT_1:13
.=
(ta1 `2) . (y (*) (id c9))
by A62, A76, ENS_1:def 19
.=
(ta1 `2) . x
by A34, A62, 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 A34, A48, ENS_1:53;
then
hom (
f,
(id a))
= ta1 `2
by A49, FUNCT_1:2;
hence
<|f,?> . a = t . a
by A33, A34, A38, A37, A46, Def3;
verum
end;
then
<|f,?> = t
by A4, A35, A17, A15, A10, A33, A34, ISOCAT_1:26;
hence
g = (Yoneda A) . f
by A3, A5, A16, A20, A15, A10, A33, A34, Def4;
verum
end;
hence
Yoneda A is full
; verum