let A, B be category; :: thesis: 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; :: thesis: ( A,B are_anti-isomorphic_under F implies F is bijective )

assume that

A is subcategory of A and

B is subcategory of B ; :: according to YELLOW20:def 5 :: thesis: ( for G being contravariant 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 contravariant 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 ; :: thesis: 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 ) ;

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 V7() & 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; :: according to FUNCTOR0:def 6,FUNCTOR0:def 7,FUNCTOR0:def 30,FUNCTOR0:def 32,FUNCTOR0:def 33,FUNCTOR0:def 34,FUNCTOR0:def 35 :: thesis: verum

F is bijective

let F be contravariant Functor of A,B; :: thesis: ( A,B are_anti-isomorphic_under F implies F is bijective )

assume that

A is subcategory of A and

B is subcategory of B ; :: according to YELLOW20:def 5 :: thesis: ( for G being contravariant 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 contravariant 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 ; :: thesis: 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 :: thesis: for a, b being Object of A st <^a,b^> <> {} holds

for f being Morphism of a,b holds F . f = G . f

for a being Object of A holds F . a = G . a
by A2;for f being Morphism of a,b holds F . f = G . f

let a, b be Object of A; :: thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds F . f = G . f )

assume A6: <^a,b^> <> {} ; :: thesis: for f being Morphism of a,b holds F . f = G . f

let f be Morphism of a,b; :: thesis: F . f = G . f

<^(F . b),(F . a)^> <> {} by A6, FUNCTOR0:def 19;

hence F . f = (Morph-Map (F,a,b)) . f by A6, FUNCTOR0:def 16

.= G . f by A3, A6 ;

:: thesis: verum

end;assume A6: <^a,b^> <> {} ; :: thesis: for f being Morphism of a,b holds F . f = G . f

let f be Morphism of a,b; :: thesis: F . f = G . f

<^(F . b),(F . a)^> <> {} by A6, FUNCTOR0:def 19;

hence F . f = (Morph-Map (F,a,b)) . f by A6, FUNCTOR0:def 16

.= G . f by A3, A6 ;

:: thesis: verum

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 V7() & 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; :: according to FUNCTOR0:def 6,FUNCTOR0:def 7,FUNCTOR0:def 30,FUNCTOR0:def 32,FUNCTOR0:def 33,FUNCTOR0:def 34,FUNCTOR0:def 35 :: thesis: verum