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:
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 A8:
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 )
reconsider f2 =
s . a' as
Morphism of
a',
(G * F) . a' by CAT_1:118;
reconsider f1 =
s . a as
Morphism of
a,
(G * F) . a by CAT_1:118;
A9:
s . a' is
invertible
by A6, NATTRA_1:def 10;
A10:
Hom ((id A) . a'),
((G * F) . a') <> {}
by A5, Th30;
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 )
A11:
(G * F) . a = G . (F . a)
by CAT_1:113;
then reconsider h =
G . g as
Morphism of
(G * F) . a,
(G * F) . a' by CAT_1:113;
A12:
Hom ((id A) . a),
((G * F) . a) <> {}
by A5, Th30;
(G * F) . a' = G . (F . a')
by CAT_1:113;
then A13:
Hom ((G * F) . a),
((G * F) . a') <> {}
by A8, A11, CAT_1:126;
then A14:
Hom ((id A) . a),
((G * F) . a') <> {}
by A12, CAT_1:52;
s . a is
invertible
by A6, NATTRA_1:def 10;
then A15:
s . a is
epi
by A12, CAT_1:73;
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:
(
(id A) . a = a &
(id A) . a' = a' )
by CAT_1:118;
hence A18:
Hom a,
a' <> {}
by A16, A14, CAT_1:52;
:: thesis: ex b1 being Morphism of a,a' st g = F . b1
take f =
(f2 " ) * (h * f1);
:: thesis: g = F . f
A19:
(id A) . f = ((s . a') " ) * (h * (s . a))
by A17, A18, NATTRA_1:16;
h * (s . a) =
(id ((G * F) . a')) * (h * (s . a))
by A14, CAT_1:57
.=
((s . a') * ((s . a') " )) * (h * (s . a))
by A10, A9, CAT_1:def 14
.=
(s . a') * ((id A) . f)
by A16, A14, A10, A19, CAT_1:54
.=
((G * F) . f) * (s . a)
by A5, A18, NATTRA_1:def 8
;
then A20:
h = (G * F) . f
by A12, A13, A15, CAT_1:65;
G . g =
G . g
by A8, NATTRA_1:def 1
.=
(G * F) . f
by A18, A20, 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 A7, A8, 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
A21:
( F . (G . b) = (F * G) . b & (id B) . b = b )
by CAT_1:113, CAT_1:118;
A22:
id B ~= F * G
by A3, NATTRA_1:31;
then
id B is_naturally_transformable_to F * G
by NATTRA_1:def 11;
then A23:
id B is_transformable_to F * G
by NATTRA_1:def 7;
ex t being natural_transformation of id B,F * G st t is invertible
by A22, NATTRA_1:def 11;
hence
b,F . (G . b) are_isomorphic
by A21, A23, Th9; :: thesis: verum