let A, B be category; for F being covariant Functor of A,B st A,B are_isomorphic_under F holds
F is bijective
let F be covariant Functor of A,B; ( A,B are_isomorphic_under F implies F is bijective )
assume that
A is subcategory of A
and
B is subcategory of B
; YELLOW20:def 4 ( for G being covariant Functor of A,B holds
( not G is bijective or ex a9, a being Object of A st
( a9 = a & not G . a9 = F . a ) or ex b9, c9, b, c being Object of A st
( <^b9,c9^> <> {} & b9 = b & c9 = c & ex f9 being Morphism of b9,c9 ex f being Morphism of b,c st
( f9 = f & not G . f9 = (Morph-Map (F,b,c)) . f ) ) ) or F is bijective )
given G being covariant Functor of A,B such that A1:
G is bijective
and
A2:
for a9, a being Object of A st a9 = a holds
G . a9 = F . a
and
A3:
for b9, c9, b, c being Object of A st <^b9,c9^> <> {} & b9 = b & c9 = c holds
for f9 being Morphism of b9,c9
for f being Morphism of b,c st f9 = f holds
G . f9 = (Morph-Map (F,b,c)) . f
; F is bijective
( G is injective & G is surjective )
by A1;
then A4:
( G is one-to-one & G is faithful & G is full & G is onto )
;
A5:
now for a, b being Object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds F . f = G . flet a,
b be
Object of
A;
( <^a,b^> <> {} implies for f being Morphism of a,b holds F . f = G . f )assume A6:
<^a,b^> <> {}
;
for f being Morphism of a,b holds F . f = G . flet f be
Morphism of
a,
b;
F . f = G . f
<^(F . a),(F . b)^> <> {}
by A6, FUNCTOR0:def 18;
hence F . f =
(Morph-Map (F,a,b)) . f
by A6, FUNCTOR0:def 15
.=
G . f
by A3, A6
;
verum end;
for a being Object of A holds F . a = G . a
by A2;
then
FunctorStr(# the ObjectMap of F, the MorphMap of F #) = FunctorStr(# the ObjectMap of G, the MorphMap of G #)
by A5, YELLOW18:1;
hence
( the ObjectMap of F is one-to-one & the MorphMap of F is "1-1" & ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st
( f = the MorphMap of F & f is "onto" ) & the ObjectMap of F is onto )
by A4; FUNCTOR0:def 6,FUNCTOR0:def 7,FUNCTOR0:def 30,FUNCTOR0:def 32,FUNCTOR0:def 33,FUNCTOR0:def 34,FUNCTOR0:def 35 verum