let A be Category; for F being Functor of A, Functors A,(EnsHom A) st Obj F is one-to-one & F is faithful holds
F is one-to-one
let F be Functor of A, Functors A,(EnsHom A); ( Obj F is one-to-one & F is faithful implies F is one-to-one )
assume A1:
Obj F is one-to-one
; ( not F is faithful or F is one-to-one )
assume A2:
F is faithful
; F is one-to-one
for x1, x2 being set st x1 in dom F & x2 in dom F & F . x1 = F . x2 holds
x1 = x2
proof
let x1,
x2 be
set ;
( x1 in dom F & x2 in dom F & F . x1 = F . x2 implies x1 = x2 )
assume that A3:
(
x1 in dom F &
x2 in dom F )
and A4:
F . x1 = F . x2
;
x1 = x2
reconsider m1 =
x1,
m2 =
x2 as
Morphism of
A by A3, FUNCT_2:def 1;
set o1 =
dom m1;
set o2 =
cod m1;
set o3 =
dom m2;
set o4 =
cod m2;
reconsider m19 =
m1 as
Morphism of
dom m1,
cod m1 by CAT_1:22;
reconsider m29 =
m2 as
Morphism of
dom m2,
cod m2 by CAT_1:22;
A5:
Hom (dom m1),
(cod m1) <> {}
by CAT_1:19;
then A6:
Hom (F . (dom m1)),
(F . (cod m1)) <> {}
by CAT_1:126;
A7:
(Obj F) . (cod m2) = F . (cod m2)
by CAT_1:def 20;
A8:
(Obj F) . (dom m2) = F . (dom m2)
by CAT_1:def 20;
A9:
Hom (dom m2),
(cod m2) <> {}
by CAT_1:19;
then A10:
Hom (F . (dom m2)),
(F . (cod m2)) <> {}
by CAT_1:126;
A11:
F . m19 =
F . m2
by A4, A5, NATTRA_1:def 1
.=
F . m29
by A9, NATTRA_1:def 1
;
(Obj F) . (dom m1) =
F . (dom m1)
by CAT_1:def 20
.=
dom (F . m29)
by A11, A6, CAT_1:23
.=
(Obj F) . (dom m2)
by A10, A8, CAT_1:23
;
then A12:
(
m2 is
Morphism of
dom m2,
cod m2 &
dom m1 = dom m2 )
by A1, CAT_1:22, FUNCT_2:25;
(Obj F) . (cod m1) =
F . (cod m1)
by CAT_1:def 20
.=
cod (F . m29)
by A11, A6, CAT_1:23
.=
(Obj F) . (cod m2)
by A10, A7, CAT_1:23
;
then
(
m1 is
Morphism of
dom m1,
cod m1 &
m2 is
Morphism of
dom m1,
cod m1 )
by A1, A12, CAT_1:22, FUNCT_2:25;
hence
x1 = x2
by A2, A4, A5, CAT_1:def 24;
verum
end;
hence
F is one-to-one
by FUNCT_1:def 8; verum