let A be Category; :: thesis: 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); :: thesis: ( Obj F is one-to-one & F is faithful implies F is one-to-one )
assume A1:
Obj F is one-to-one
; :: thesis: ( not F is faithful or F is one-to-one )
assume A2:
F is faithful
; :: thesis: 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 ;
:: thesis: ( x1 in dom F & x2 in dom F & F . x1 = F . x2 implies x1 = x2 )
assume A3:
(
x1 in dom F &
x2 in dom F &
F . x1 = F . x2 )
;
:: thesis: x1 = x2
then reconsider m1 =
x1,
m2 =
x2 as
Morphism of
A by FUNCT_2:def 1;
A4:
m1 is
Morphism of
dom m1,
cod m1
by CAT_1:22;
set o1 =
dom m1;
set o2 =
cod m1;
A5:
m2 is
Morphism of
dom m2,
cod m2
by CAT_1:22;
set o3 =
dom m2;
set o4 =
cod m2;
reconsider m1' =
m1 as
Morphism of
dom m1,
cod m1 by CAT_1:22;
reconsider m2' =
m2 as
Morphism of
dom m2,
cod m2 by CAT_1:22;
A6:
Hom (dom m1),
(cod m1) <> {}
by CAT_1:19;
A7:
Hom (dom m2),
(cod m2) <> {}
by CAT_1:19;
then A8:
Hom (F . (dom m2)),
(F . (cod m2)) <> {}
by CAT_1:126;
A9:
F . m1' =
F . m2
by A3, A6, NATTRA_1:def 1
.=
F . m2'
by A7, NATTRA_1:def 1
;
A10:
Hom (F . (dom m1)),
(F . (cod m1)) <> {}
by A6, CAT_1:126;
A11:
(Obj F) . (dom m2) = F . (dom m2)
by CAT_1:def 20;
(Obj F) . (dom m1) =
F . (dom m1)
by CAT_1:def 20
.=
dom (F . m2')
by A9, A10, CAT_1:23
.=
(Obj F) . (dom m2)
by A8, A11, CAT_1:23
;
then A12:
dom m1 = dom m2
by A1, FUNCT_2:25;
A13:
(Obj F) . (cod m2) = F . (cod m2)
by CAT_1:def 20;
(Obj F) . (cod m1) =
F . (cod m1)
by CAT_1:def 20
.=
cod (F . m2')
by A9, A10, CAT_1:23
.=
(Obj F) . (cod m2)
by A8, A13, CAT_1:23
;
then
m2 is
Morphism of
dom m1,
cod m1
by A1, A5, A12, FUNCT_2:25;
hence
x1 = x2
by A2, A3, A4, A6, CAT_1:def 24;
:: thesis: verum
end;
hence
F is one-to-one
by FUNCT_1:def 8; :: thesis: verum