let A, B be category; :: thesis: for F being covariant Functor of A,B st F is bijective holds
A,B are_isomorphic_under F
let F be covariant Functor of A,B; :: thesis: ( F is bijective implies A,B are_isomorphic_under F )
assume A1: F is bijective ; :: thesis: A,B are_isomorphic_under F
( the Arrows of A = the Arrows of A & the Arrows of B = the Arrows of B ) ;
hence ( A is subcategory of & B is subcategory of ) by ALTCAT_2:21, ALTCAT_4:35; :: according to YELLOW20:def 4 :: thesis: ex G being covariant Functor of A,B st
( G is bijective & ( for a', a being object of st a' = a holds
G . a' = F . a ) & ( 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 ) )
take F ; :: thesis: ( F is bijective & ( for a', a being object of st a' = a holds
F . a' = F . a ) & ( 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
F . f' = (Morph-Map F,b,c) . f ) )
thus ( F is bijective & ( for a', a being object of st a' = a holds
F . a' = F . a ) ) by A1; :: thesis: 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
F . f' = (Morph-Map F,b,c) . f
let b', c' be object of ; :: thesis: for 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
F . f' = (Morph-Map F,b,c) . f
let b, c be object of ; :: thesis: ( <^b',c'^> <> {} & b' = b & c' = c implies for f' being Morphism of ,
for f being Morphism of , st f' = f holds
F . f' = (Morph-Map F,b,c) . f )
assume A2: ( <^b',c'^> <> {} & b' = b & c' = c ) ; :: thesis: for f' being Morphism of ,
for f being Morphism of , st f' = f holds
F . f' = (Morph-Map F,b,c) . f
then <^(F . b),(F . c)^> <> {} by FUNCTOR0:def 19;
hence for f' being Morphism of ,
for f being Morphism of , st f' = f holds
F . f' = (Morph-Map F,b,c) . f by A2, FUNCTOR0:def 16; :: thesis: verum