let C, D be Category; for T being Functor of C,D holds
( T is faithful iff for c, c9 being Object of C holds hom (T,c,c9) is one-to-one )
let T be Functor of C,D; ( T is faithful iff for c, c9 being Object of C holds hom (T,c,c9) is one-to-one )
thus
( T is faithful implies for c, c9 being Object of C holds hom (T,c,c9) is one-to-one )
( ( for c, c9 being Object of C holds hom (T,c,c9) is one-to-one ) implies T is faithful )proof
assume A1:
T is
faithful
;
for c, c9 being Object of C holds hom (T,c,c9) is one-to-one
let c,
c9 be
Object of
C;
hom (T,c,c9) is one-to-one
now ( Hom ((T . c),(T . c9)) <> {} implies hom (T,c,c9) is one-to-one )A2:
now for f1, f2 being object st f1 in Hom (c,c9) & f2 in Hom (c,c9) & (hom (T,c,c9)) . f1 = (hom (T,c,c9)) . f2 holds
f1 = f2let f1,
f2 be
object ;
( f1 in Hom (c,c9) & f2 in Hom (c,c9) & (hom (T,c,c9)) . f1 = (hom (T,c,c9)) . f2 implies f1 = f2 )assume that A3:
f1 in Hom (
c,
c9)
and A4:
f2 in Hom (
c,
c9)
;
( (hom (T,c,c9)) . f1 = (hom (T,c,c9)) . f2 implies f1 = f2 )A5:
f2 is
Morphism of
c,
c9
by A4, Def3;
then A6:
T . f2 = (hom (T,c,c9)) . f2
by A3, Th83;
A7:
f1 is
Morphism of
c,
c9
by A3, Def3;
then
T . f1 = (hom (T,c,c9)) . f1
by A3, Th83;
hence
(
(hom (T,c,c9)) . f1 = (hom (T,c,c9)) . f2 implies
f1 = f2 )
by A1, A3, A7, A5, A6;
verum end; assume
Hom (
(T . c),
(T . c9))
<> {}
;
hom (T,c,c9) is one-to-one hence
hom (
T,
c,
c9) is
one-to-one
by A2, FUNCT_2:19;
verum end;
hence
hom (
T,
c,
c9) is
one-to-one
;
verum
end;
assume A8:
for c, c9 being Object of C holds hom (T,c,c9) is one-to-one
; T is faithful
let c, c9 be Object of C; CAT_1:def 27 ( Hom (c,c9) <> {} implies for f1, f2 being Morphism of c,c9 st T . f1 = T . f2 holds
f1 = f2 )
assume A9:
Hom (c,c9) <> {}
; for f1, f2 being Morphism of c,c9 st T . f1 = T . f2 holds
f1 = f2
let f1, f2 be Morphism of c,c9; ( T . f1 = T . f2 implies f1 = f2 )
A10:
T . f2 = (hom (T,c,c9)) . f2
by A9, Th83;
A11:
( f2 in Hom (c,c9) & T . f1 = (hom (T,c,c9)) . f1 )
by A9, Def3, Th83;
A12:
hom (T,c,c9) is one-to-one
by A8;
( Hom ((T . c),(T . c9)) <> {} & f1 in Hom (c,c9) )
by A9, Def3, Th79;
hence
( T . f1 = T . f2 implies f1 = f2 )
by A12, A11, A10, FUNCT_2:19; verum