let A, B be category; for F being contravariant Functor of A,B st A,B are_anti-isomorphic_under F holds
F is bijective
let F be contravariant Functor of A,B; ( A,B are_anti-isomorphic_under F implies F is bijective )
assume that
A is subcategory of
and
B is subcategory of
; YELLOW20:def 5 ( for G being contravariant Functor of A,B holds
( not G is bijective or ex a', a being object of st
( a' = a & not G . a' = F . a ) or ex b', c', b, c being object of st
( <^b',c'^> <> {} & b' = b & c' = c & ex f' being Morphism of , ex f being Morphism of , st
( f' = f & not G . f' = (Morph-Map F,b,c) . f ) ) ) or F is bijective )
given G being contravariant Functor of A,B such that A1:
G is bijective
and
A2:
for a', a being object of st a' = a holds
G . a' = F . a
and
A3:
for b', c', b, c being object of st <^b',c'^> <> {} & b' = b & c' = c holds
for f' being Morphism of ,
for f being Morphism of , st f' = f holds
G . f' = (Morph-Map F,b,c) . f
; F is bijective
( G is injective & G is surjective )
by A1, FUNCTOR0:def 36;
then A4:
( G is one-to-one & G is faithful & G is full & G is onto )
by FUNCTOR0:def 34, FUNCTOR0:def 35;
A5:
now let a,
b be
object of ;
( <^a,b^> <> {} implies for f being Morphism of , holds F . f = G . f )assume A6:
<^a,b^> <> {}
;
for f being Morphism of , holds F . f = G . flet f be
Morphism of ,;
F . f = G . f
<^(F . b),(F . a)^> <> {}
by A6, FUNCTOR0:def 20;
hence F . f =
(Morph-Map F,a,b) . f
by A6, FUNCTOR0:def 17
.=
G . f
by A3, A6
;
verum end;
for a being object of 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:2;
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 7, FUNCTOR0:def 8, FUNCTOR0:def 31, FUNCTOR0:def 33; FUNCTOR0:def 7,FUNCTOR0:def 8,FUNCTOR0:def 31,FUNCTOR0:def 33,FUNCTOR0:def 34,FUNCTOR0:def 35,FUNCTOR0:def 36 verum