:: deftheorem defines are_isomorphic_under YELLOW20:def 4 :
for A, B being category
for F being FunctorStr over A,B
for A9, B9 being category holds
( A9,B9 are_isomorphic_under F iff ( A9 is subcategory of A & B9 is subcategory of B & ex G being covariant Functor of A9,B9 st
( G is bijective & ( for a9 being Object of A9
for a being Object of A st a9 = a holds
G . a9 = F . a ) & ( for b9, c9 being Object of A9
for 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 ) ) ) );