let A, B be Category; :: thesis: ( A,B are_equivalent implies for F being Equivalence of A,B holds
( F is full & F is faithful & ( for b being Object of B ex a being Object of A st b,F . a are_isomorphic ) ) )
assume A1:
A,B are_equivalent
; :: thesis: for F being Equivalence of A,B holds
( F is full & F is faithful & ( for b being Object of B ex a being Object of A st b,F . a are_isomorphic ) )
let F be Equivalence of A,B; :: thesis: ( F is full & F is faithful & ( for b being Object of B ex a being Object of A st b,F . a are_isomorphic ) )
consider G being Equivalence of B,A such that
A2:
G * F ~= id A
and
A3:
F * G ~= id B
by A1, Th56;
A4:
id A ~= G * F
by A2, NATTRA_1:31;
then A5:
id A is_naturally_transformable_to G * F
by NATTRA_1:def 11;
consider s being natural_transformation of id A,G * F such that
A6:
s is invertible
by A4, NATTRA_1:def 11;
A7:
id B ~= F * G
by A3, NATTRA_1:31;
then A8:
id B is_naturally_transformable_to F * G
by NATTRA_1:def 11;
A9:
ex t being natural_transformation of id B,F * G st t is invertible
by A7, NATTRA_1:def 11;
A10:
G is faithful
by A3, Th57;
thus
F is full
:: thesis: ( F is faithful & ( for b being Object of B ex a being Object of A st b,F . a are_isomorphic ) )proof
let a,
a' be
Object of
A;
:: according to CAT_1:def 23 :: thesis: ( Hom (F . a),(F . a') = {} or for b1 being Morphism of F . a,F . a' holds
( not Hom a,a' = {} & ex b2 being Morphism of a,a' st b1 = F . b2 ) )
assume A11:
Hom (F . a),
(F . a') <> {}
;
:: thesis: for b1 being Morphism of F . a,F . a' holds
( not Hom a,a' = {} & ex b2 being Morphism of a,a' st b1 = F . b2 )
let g be
Morphism of
F . a,
F . a';
:: thesis: ( not Hom a,a' = {} & ex b1 being Morphism of a,a' st g = F . b1 )
A12:
(
(id A) . a = a &
(id A) . a' = a' )
by CAT_1:118;
A13:
(
(G * F) . a = G . (F . a) &
(G * F) . a' = G . (F . a') )
by CAT_1:113;
then reconsider h =
G . g as
Morphism of
(G * F) . a,
(G * F) . a' ;
A14:
Hom ((id A) . a),
((G * F) . a) <> {}
by A5, Th30;
A15:
Hom ((G * F) . a),
((G * F) . a') <> {}
by A11, A13, CAT_1:126;
G * F is_naturally_transformable_to id A
by A2, NATTRA_1:def 11;
then A16:
Hom ((G * F) . a'),
((id A) . a') <> {}
by Th30;
A17:
Hom ((id A) . a),
((G * F) . a') <> {}
by A14, A15, CAT_1:52;
hence A18:
Hom a,
a' <> {}
by A12, A16, CAT_1:52;
:: thesis: ex b1 being Morphism of a,a' st g = F . b1
reconsider f1 =
s . a as
Morphism of
a,
(G * F) . a by CAT_1:118;
reconsider f2 =
s . a' as
Morphism of
a',
(G * F) . a' by CAT_1:118;
take f =
(f2 " ) * (h * f1);
:: thesis: g = F . f
A19:
Hom ((id A) . a'),
((G * F) . a') <> {}
by A5, Th30;
s . a is
invertible
by A6, NATTRA_1:def 10;
then A20:
s . a is
epi
by A14, CAT_1:73;
A21:
s . a' is
invertible
by A6, NATTRA_1:def 10;
A22:
(id A) . f = ((s . a') " ) * (h * (s . a))
by A12, A18, NATTRA_1:16;
h * (s . a) =
(id ((G * F) . a')) * (h * (s . a))
by A17, CAT_1:57
.=
((s . a') * ((s . a') " )) * (h * (s . a))
by A19, A21, CAT_1:def 14
.=
(s . a') * ((id A) . f)
by A16, A17, A19, A22, CAT_1:54
.=
((G * F) . f) * (s . a)
by A5, A18, NATTRA_1:def 8
;
then A23:
h = (G * F) . f
by A14, A15, A20, CAT_1:65;
G . g =
G . g
by A11, NATTRA_1:def 1
.=
(G * F) . f
by A18, A23, NATTRA_1:def 1
.=
G . (F . f)
by FUNCT_2:21
.=
G . (F . f)
by A18, NATTRA_1:def 1
;
hence g =
F . f
by A10, A11, CAT_1:def 24
.=
F . f
by A18, NATTRA_1:def 1
;
:: thesis: verum
end;
thus
F is faithful
by A2, Th57; :: thesis: for b being Object of B ex a being Object of A st b,F . a are_isomorphic
let b be Object of B; :: thesis: ex a being Object of A st b,F . a are_isomorphic
take
G . b
; :: thesis: b,F . (G . b) are_isomorphic
A24:
( F . (G . b) = (F * G) . b & (id B) . b = b )
by CAT_1:113, CAT_1:118;
id B is_transformable_to F * G
by A8, NATTRA_1:def 7;
hence
b,F . (G . b) are_isomorphic
by A9, A24, Th9; :: thesis: verum