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:4;
reconsider m29 =
m2 as
Morphism of
dom m2,
cod m2 by CAT_1:4;
A5:
Hom (
(dom m1),
(cod m1))
<> {}
by CAT_1:2;
then A6:
Hom (
(F . (dom m1)),
(F . (cod m1)))
<> {}
by CAT_1:84;
A7:
(Obj F) . (cod m2) = F . (cod m2)
by CAT_1:def 17;
A8:
(Obj F) . (dom m2) = F . (dom m2)
by CAT_1:def 17;
A9:
Hom (
(dom m2),
(cod m2))
<> {}
by CAT_1:2;
then A10:
Hom (
(F . (dom m2)),
(F . (cod m2)))
<> {}
by CAT_1:84;
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 17
.=
dom (F . m29)
by A11, A6, CAT_1:5
.=
(Obj F) . (dom m2)
by A10, A8, CAT_1:5
;
then A12:
(
m2 is
Morphism of
dom m2,
cod m2 &
dom m1 = dom m2 )
by A1, CAT_1:4, FUNCT_2:19;
(Obj F) . (cod m1) =
F . (cod m1)
by CAT_1:def 17
.=
cod (F . m29)
by A11, A6, CAT_1:5
.=
(Obj F) . (cod m2)
by A10, A7, CAT_1:5
;
then
(
m1 is
Morphism of
dom m1,
cod m1 &
m2 is
Morphism of
dom m1,
cod m1 )
by A1, A12, CAT_1:4, FUNCT_2:19;
hence
x1 = x2
by A2, A4, A5, CAT_1:def 21;
verum
end;
hence
F is one-to-one
by FUNCT_1:def 4; verum