set F = Yoneda A;
for o1, o2 being Object of A st Hom (o1,o2) <> {} holds
for x1, x2 being Morphism of o1,o2 st (Yoneda A) . x1 = (Yoneda A) . x2 holds
x1 = x2
proof
let o1,
o2 be
Object of
A;
( Hom (o1,o2) <> {} implies for x1, x2 being Morphism of o1,o2 st (Yoneda A) . x1 = (Yoneda A) . x2 holds
x1 = x2 )
assume A1:
Hom (
o1,
o2)
<> {}
;
for x1, x2 being Morphism of o1,o2 st (Yoneda A) . x1 = (Yoneda A) . x2 holds
x1 = x2
let x1,
x2 be
Morphism of
o1,
o2;
( (Yoneda A) . x1 = (Yoneda A) . x2 implies x1 = x2 )
A2:
x2 in Hom (
o1,
o2)
by A1, CAT_1:def 5;
assume
(Yoneda A) . x1 = (Yoneda A) . x2
;
x1 = x2
then
[[<|(cod x1),?>,<|(dom x1),?>],<|x1,?>] = (Yoneda A) . x2
by Def4;
then
[[<|(cod x1),?>,<|(dom x1),?>],<|x1,?>] = [[<|(cod x2),?>,<|(dom x2),?>],<|x2,?>]
by Def4;
then
[<|(cod x1),?>,<|(dom x1),?>,<|x1,?>] = [[<|(cod x2),?>,<|(dom x2),?>],<|x2,?>]
;
then
[<|(cod x1),?>,<|(dom x1),?>,<|x1,?>] = [<|(cod x2),?>,<|(dom x2),?>,<|x2,?>]
;
then A3:
<|x1,?> = <|x2,?>
by XTUPLE_0:3;
A4:
x1 in Hom (
o1,
o2)
by A1, CAT_1:def 5;
then A5:
dom x1 =
o1
by CAT_1:1
.=
dom x2
by A2, CAT_1:1
;
cod x1 =
o2
by A4, CAT_1:1
.=
cod x2
by A2, CAT_1:1
;
then
[[(Hom ((cod x1),o2)),(Hom ((dom x1),o2))],(hom (x1,(id o2)))] = <|x2,?> . o2
by A5, A3, Def3;
then
[[(Hom ((cod x1),o2)),(Hom ((dom x1),o2))],(hom (x1,(id o2)))] = [[(Hom ((cod x2),o2)),(Hom ((dom x2),o2))],(hom (x2,(id o2)))]
by Def3;
then
[[(Hom (o2,o2)),(Hom ((dom x1),o2))],(hom (x1,(id o2)))] = [[(Hom ((cod x2),o2)),(Hom ((dom x2),o2))],(hom (x2,(id o2)))]
by A4, CAT_1:1;
then
[[(Hom (o2,o2)),(Hom (o1,o2))],(hom (x1,(id o2)))] = [[(Hom ((cod x2),o2)),(Hom ((dom x2),o2))],(hom (x2,(id o2)))]
by A4, CAT_1:1;
then
[[(Hom (o2,o2)),(Hom (o1,o2))],(hom (x1,(id o2)))] = [[(Hom (o2,o2)),(Hom ((dom x2),o2))],(hom (x2,(id o2)))]
by A2, CAT_1:1;
then
[[(Hom (o2,o2)),(Hom (o1,o2))],(hom (x1,(id o2)))] = [[(Hom (o2,o2)),(Hom (o1,o2))],(hom (x2,(id o2)))]
by A2, CAT_1:1;
then
[[(Hom (o2,o2)),(Hom (o1,o2))],(hom (x1,(id o2)))] = [(Hom (o2,o2)),(Hom (o1,o2)),(hom (x2,(id o2)))]
;
then A6:
[(Hom (o2,o2)),(Hom (o1,o2)),(hom (x1,(id o2)))] = [(Hom (o2,o2)),(Hom (o1,o2)),(hom (x2,(id o2)))]
;
reconsider dd =
id o2 as
Morphism of
A ;
A7:
Hom (
o2,
o2)
<> {}
;
then A8:
(id o2) (*) dd = (id o2) * (id o2)
by CAT_1:def 13;
id o2 in Hom (
o2,
o2)
by CAT_1:27;
then
id o2 in Hom (
(cod x2),
o2)
by A2, CAT_1:1;
then
id o2 in Hom (
(cod x2),
(dom (id o2)))
;
then A9:
(hom (x2,(id o2))) . dd =
((id o2) * (id o2)) (*) x2
by A8, ENS_1:def 23
.=
(id o2) (*) x2
.=
(id o2) * x2
by A1, A7, CAT_1:def 13
.=
x2
by A1, CAT_1:28
;
id o2 in Hom (
o2,
o2)
by CAT_1:27;
then
id o2 in Hom (
(cod x1),
o2)
by A4, CAT_1:1;
then
id o2 in Hom (
(cod x1),
(dom (id o2)))
;
then (hom (x1,(id o2))) . dd =
((id o2) * (id o2)) (*) x1
by A8, ENS_1:def 23
.=
(id o2) (*) x1
.=
(id o2) * x1
by A1, A7, CAT_1:def 13
.=
x1
by A1, CAT_1:28
;
hence
x1 = x2
by A9, A6, XTUPLE_0:3;
verum
end;
hence
Yoneda A is faithful
; verum