let A, B be Category; ( 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
; 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; ( 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, Th47;
A4:
id A ~= G * F
by A2, NATTRA_1:28;
then A5:
id A is_naturally_transformable_to G * F
;
consider s being natural_transformation of id A,G * F such that
A6:
s is invertible
by A4;
A7:
G is faithful
by A3, Th48;
thus
F is full
( F is faithful & ( for b being Object of B ex a being Object of A st b,F . a are_isomorphic ) )proof
let a,
a9 be
Object of
A;
CAT_1:def 26 ( Hom ((F . a),(F . a9)) = {} or for b1 being Morphism of F . a,F . a9 holds
( not Hom (a,a9) = {} & ex b2 being Morphism of a,a9 st b1 = F . b2 ) )
assume A8:
Hom (
(F . a),
(F . a9))
<> {}
;
for b1 being Morphism of F . a,F . a9 holds
( not Hom (a,a9) = {} & ex b2 being Morphism of a,a9 st b1 = F . b2 )
reconsider f2 =
s . a9 as
Morphism of
a9,
(G * F) . a9 by CAT_1:79;
reconsider f1 =
s . a as
Morphism of
a,
(G * F) . a by CAT_1:79;
A9:
s . a9 is
invertible
by A6;
A10:
Hom (
((id A) . a9),
((G * F) . a9))
<> {}
by A5, Th23;
let g be
Morphism of
F . a,
F . a9;
( not Hom (a,a9) = {} & ex b1 being Morphism of a,a9 st g = F . b1 )
A11:
(G * F) . a = G . (F . a)
by CAT_1:76;
then reconsider h =
G /. g as
Morphism of
(G * F) . a,
(G * F) . a9 by CAT_1:76;
A12:
Hom (
((id A) . a),
((G * F) . a))
<> {}
by A5, Th23;
(G * F) . a9 = G . (F . a9)
by CAT_1:76;
then A13:
Hom (
((G * F) . a),
((G * F) . a9))
<> {}
by A8, A11, CAT_1:84;
then A14:
Hom (
((id A) . a),
((G * F) . a9))
<> {}
by A12, CAT_1:24;
s . a is
invertible
by A6;
then A15:
s . a is
epi
by CAT_1:43;
G * F is_naturally_transformable_to id A
by A2;
then A16:
Hom (
((G * F) . a9),
((id A) . a9))
<> {}
by Th23;
A17:
(
(id A) . a = a &
(id A) . a9 = a9 )
by CAT_1:79;
hence A18:
Hom (
a,
a9)
<> {}
by A16, A14, CAT_1:24;
ex b1 being Morphism of a,a9 st g = F . b1
take f =
(f2 ") * (h * f1);
g = F . f
A19:
(id A) /. f = ((s . a9) ") * (h * (s . a))
by A17, A18, NATTRA_1:16;
h * (s . a) =
(id ((G * F) . a9)) * (h * (s . a))
by A14, CAT_1:28
.=
((s . a9) * ((s . a9) ")) * (h * (s . a))
by A9, CAT_1:def 17
.=
(s . a9) * ((id A) /. f)
by A16, A14, A10, A19, CAT_1:25
.=
((G * F) /. f) * (s . a)
by A5, A18, NATTRA_1:def 8
;
then A20:
h = (G * F) /. f
by A13, A15;
G . g =
G /. g
by A8, CAT_3:def 10
.=
(G * F) . f
by A18, A20, CAT_3:def 10
.=
G . (F . f)
by FUNCT_2:15
.=
G . (F /. f)
by A18, CAT_3:def 10
;
hence g =
F /. f
by A7, A8
.=
F . f
by A18, CAT_3:def 10
;
verum
end;
thus
F is faithful
by A2, Th48; for b being Object of B ex a being Object of A st b,F . a are_isomorphic
let b be Object of B; ex a being Object of A st b,F . a are_isomorphic
take
G . b
; b,F . (G . b) are_isomorphic
A21:
( F . (G . b) = (F * G) . b & (id B) . b = b )
by CAT_1:76, CAT_1:79;
A22:
id B ~= F * G
by A3, NATTRA_1:28;
then
id B is_naturally_transformable_to F * G
;
then A23:
id B is_transformable_to F * G
;
ex t being natural_transformation of id B,F * G st t is invertible
by A22;
hence
b,F . (G . b) are_isomorphic
by A21, A23, Th4; verum