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
( A is SubCatStr of A & B is SubCatStr of B & the carrier of A = the carrier of A & the carrier of B = the carrier of B & the Arrows of A = the Arrows of A & the Arrows of B = the Arrows of B ) by ALTCAT_2:21;
hence ( A is subcategory of A & B is subcategory of B ) by 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 A st a' = a holds
G . a' = F . a ) & ( for b', c', b, c being object of A st <^b',c'^> <> {} & b' = b & c' = c holds
for f' being Morphism of b',c'
for f being Morphism of b,c st f' = f holds
G . f' = (Morph-Map F,b,c) . f ) )
take F ; :: thesis: ( F is bijective & ( for a', a being object of A st a' = a holds
F . a' = F . a ) & ( for b', c', b, c being object of A st <^b',c'^> <> {} & b' = b & c' = c holds
for f' being Morphism of b',c'
for f being Morphism of b,c st f' = f holds
F . f' = (Morph-Map F,b,c) . f ) )
thus ( F is bijective & ( for a', a being object of A st a' = a holds
F . a' = F . a ) ) by A1; :: thesis: for b', c', b, c being object of A st <^b',c'^> <> {} & b' = b & c' = c holds
for f' being Morphism of b',c'
for f being Morphism of b,c st f' = f holds
F . f' = (Morph-Map F,b,c) . f
let b', c' be object of A; :: thesis: for b, c being object of A st <^b',c'^> <> {} & b' = b & c' = c holds
for f' being Morphism of b',c'
for f being Morphism of b,c st f' = f holds
F . f' = (Morph-Map F,b,c) . f
let b, c be object of A; :: thesis: ( <^b',c'^> <> {} & b' = b & c' = c implies for f' being Morphism of b',c'
for f being Morphism of b,c 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 b',c'
for f being Morphism of b,c 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 b',c'
for f being Morphism of b,c st f' = f holds
F . f' = (Morph-Map F,b,c) . f by A2, FUNCTOR0:def 16; :: thesis: verum