let A1, A2 be category; :: thesis: for F being covariant Functor of A1,A2 st F is bijective holds

for B1 being non empty subcategory of A1

for B2 being non empty subcategory of A2 st B1,B2 are_isomorphic_under F holds

B2,B1 are_isomorphic_under F "

let F be covariant Functor of A1,A2; :: thesis: ( F is bijective implies for B1 being non empty subcategory of A1

for B2 being non empty subcategory of A2 st B1,B2 are_isomorphic_under F holds

B2,B1 are_isomorphic_under F " )

assume A1: F is bijective ; :: thesis: for B1 being non empty subcategory of A1

for B2 being non empty subcategory of A2 st B1,B2 are_isomorphic_under F holds

B2,B1 are_isomorphic_under F "

F is surjective by A1;

then F is onto ;

then A2: F is coreflexive by FUNCTOR0:46;

ex H being Functor of A2,A1 st

( H = F " & H is bijective & H is covariant ) by A1, FUNCTOR0:48;

then reconsider F9 = F " as covariant Functor of A2,A1 ;

let B1 be non empty subcategory of A1; :: thesis: for B2 being non empty subcategory of A2 st B1,B2 are_isomorphic_under F holds

B2,B1 are_isomorphic_under F "

let B2 be non empty subcategory of A2; :: thesis: ( B1,B2 are_isomorphic_under F implies B2,B1 are_isomorphic_under F " )

assume that

B1 is subcategory of A1 and

B2 is subcategory of A2 ; :: according to YELLOW20:def 4 :: thesis: ( for G being covariant Functor of B1,B2 holds

( not G is bijective or ex a9 being Object of B1 ex a being Object of A1 st

( a9 = a & not G . a9 = F . a ) or ex b9, c9 being Object of B1 ex b, c being Object of A1 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 B2,B1 are_isomorphic_under F " )

given G being covariant Functor of B1,B2 such that A3: G is bijective and

A4: for a being Object of B1

for a1 being Object of A1 st a = a1 holds

G . a = F . a1 and

A5: for b, c being Object of B1

for b1, c1 being Object of A1 st <^b,c^> <> {} & b = b1 & c = c1 holds

for f being Morphism of b,c

for f1 being Morphism of b1,c1 st f = f1 holds

G . f = (Morph-Map (F,b1,c1)) . f1 ; :: thesis: B2,B1 are_isomorphic_under F "

G is surjective by A3;

then G is onto ;

then A6: G is coreflexive by FUNCTOR0:46;

thus ( B2 is subcategory of A2 & B1 is subcategory of A1 ) ; :: according to YELLOW20:def 4 :: thesis: ex G being covariant Functor of B2,B1 st

( G is bijective & ( for a9 being Object of B2

for a being Object of A2 st a9 = a holds

G . a9 = (F ") . a ) & ( for b9, c9 being Object of B2

for b, c being Object of A2 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 ) )

consider H being Functor of B2,B1 such that

A7: H = G " and

A8: ( H is bijective & H is covariant ) by A3, FUNCTOR0:48;

reconsider H = H as covariant Functor of B2,B1 by A8;

take H ; :: thesis: ( H is bijective & ( for a9 being Object of B2

for a being Object of A2 st a9 = a holds

H . a9 = (F ") . a ) & ( for b9, c9 being Object of B2

for b, c being Object of A2 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

H . f9 = (Morph-Map ((F "),b,c)) . f ) )

thus H is bijective by A8; :: thesis: ( ( for a9 being Object of B2

for a being Object of A2 st a9 = a holds

H . a9 = (F ") . a ) & ( for b9, c9 being Object of B2

for b, c being Object of A2 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

H . f9 = (Morph-Map ((F "),b,c)) . f ) )

A9: the carrier of B1 c= the carrier of A1 by ALTCAT_2:def 11;

for f9 being Morphism of b,c

for f being Morphism of b,c st f9 = f holds

H . f9 = (Morph-Map ((F "),b,c)) . f

let b1, c1 be Object of A2; :: thesis: ( <^b,c^> <> {} & b = b1 & c = c1 implies for f9 being Morphism of b,c

for f being Morphism of b1,c1 st f9 = f holds

H . f9 = (Morph-Map ((F "),b1,c1)) . f )

assume that

A12: <^b,c^> <> {} and

A13: ( b = b1 & c = c1 ) ; :: thesis: for f9 being Morphism of b,c

for f being Morphism of b1,c1 st f9 = f holds

H . f9 = (Morph-Map ((F "),b1,c1)) . f

let f be Morphism of b,c; :: thesis: for f being Morphism of b1,c1 st f = f holds

H . f = (Morph-Map ((F "),b1,c1)) . f

let f1 be Morphism of b1,c1; :: thesis: ( f = f1 implies H . f = (Morph-Map ((F "),b1,c1)) . f1 )

assume A14: f = f1 ; :: thesis: H . f = (Morph-Map ((F "),b1,c1)) . f1

A15: ( <^b,c^> c= <^b1,c1^> & f in <^b,c^> ) by A12, A13, ALTCAT_2:31;

A16: ( G . (H . b) = b & G . (H . c) = c ) by A3, A7, A6, Th1;

A17: <^(H . b),(H . c)^> <> {} by A12, FUNCTOR0:def 18;

then A18: H . f in <^(H . b),(H . c)^> ;

A19: ( F . ((F ") . b1) = b1 & F . ((F ") . c1) = c1 ) by A1, A2, Th1;

A20: ( H . b = (F ") . b1 & H . c = (F ") . c1 ) by A10, A13;

then A21: <^(H . b),(H . c)^> c= <^((F ") . b1),((F ") . c1)^> by ALTCAT_2:31;

then reconsider Hf = H . f as Morphism of ((F ") . b1),((F ") . c1) by A18;

G . (H . f) = (Morph-Map (F,((F ") . b1),((F ") . c1))) . Hf by A5, A20, A17

.= F . Hf by A21, A18, A15, A19, FUNCTOR0:def 15 ;

then F . Hf = f by A3, A7, A17, A16, Th2;

hence H . f = F9 . f1 by A1, A14, A21, A18, A19, Th2

.= (Morph-Map ((F "),b1,c1)) . f1 by A21, A18, A15, FUNCTOR0:def 15 ;

:: thesis: verum

for B1 being non empty subcategory of A1

for B2 being non empty subcategory of A2 st B1,B2 are_isomorphic_under F holds

B2,B1 are_isomorphic_under F "

let F be covariant Functor of A1,A2; :: thesis: ( F is bijective implies for B1 being non empty subcategory of A1

for B2 being non empty subcategory of A2 st B1,B2 are_isomorphic_under F holds

B2,B1 are_isomorphic_under F " )

assume A1: F is bijective ; :: thesis: for B1 being non empty subcategory of A1

for B2 being non empty subcategory of A2 st B1,B2 are_isomorphic_under F holds

B2,B1 are_isomorphic_under F "

F is surjective by A1;

then F is onto ;

then A2: F is coreflexive by FUNCTOR0:46;

ex H being Functor of A2,A1 st

( H = F " & H is bijective & H is covariant ) by A1, FUNCTOR0:48;

then reconsider F9 = F " as covariant Functor of A2,A1 ;

let B1 be non empty subcategory of A1; :: thesis: for B2 being non empty subcategory of A2 st B1,B2 are_isomorphic_under F holds

B2,B1 are_isomorphic_under F "

let B2 be non empty subcategory of A2; :: thesis: ( B1,B2 are_isomorphic_under F implies B2,B1 are_isomorphic_under F " )

assume that

B1 is subcategory of A1 and

B2 is subcategory of A2 ; :: according to YELLOW20:def 4 :: thesis: ( for G being covariant Functor of B1,B2 holds

( not G is bijective or ex a9 being Object of B1 ex a being Object of A1 st

( a9 = a & not G . a9 = F . a ) or ex b9, c9 being Object of B1 ex b, c being Object of A1 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 B2,B1 are_isomorphic_under F " )

given G being covariant Functor of B1,B2 such that A3: G is bijective and

A4: for a being Object of B1

for a1 being Object of A1 st a = a1 holds

G . a = F . a1 and

A5: for b, c being Object of B1

for b1, c1 being Object of A1 st <^b,c^> <> {} & b = b1 & c = c1 holds

for f being Morphism of b,c

for f1 being Morphism of b1,c1 st f = f1 holds

G . f = (Morph-Map (F,b1,c1)) . f1 ; :: thesis: B2,B1 are_isomorphic_under F "

G is surjective by A3;

then G is onto ;

then A6: G is coreflexive by FUNCTOR0:46;

thus ( B2 is subcategory of A2 & B1 is subcategory of A1 ) ; :: according to YELLOW20:def 4 :: thesis: ex G being covariant Functor of B2,B1 st

( G is bijective & ( for a9 being Object of B2

for a being Object of A2 st a9 = a holds

G . a9 = (F ") . a ) & ( for b9, c9 being Object of B2

for b, c being Object of A2 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 ) )

consider H being Functor of B2,B1 such that

A7: H = G " and

A8: ( H is bijective & H is covariant ) by A3, FUNCTOR0:48;

reconsider H = H as covariant Functor of B2,B1 by A8;

take H ; :: thesis: ( H is bijective & ( for a9 being Object of B2

for a being Object of A2 st a9 = a holds

H . a9 = (F ") . a ) & ( for b9, c9 being Object of B2

for b, c being Object of A2 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

H . f9 = (Morph-Map ((F "),b,c)) . f ) )

thus H is bijective by A8; :: thesis: ( ( for a9 being Object of B2

for a being Object of A2 st a9 = a holds

H . a9 = (F ") . a ) & ( for b9, c9 being Object of B2

for b, c being Object of A2 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

H . f9 = (Morph-Map ((F "),b,c)) . f ) )

A9: the carrier of B1 c= the carrier of A1 by ALTCAT_2:def 11;

hereby :: thesis: for b9, c9 being Object of B2

for b, c being Object of A2 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

H . f9 = (Morph-Map ((F "),b,c)) . f

let b, c be Object of B2; :: thesis: for b, c being Object of A2 st <^b,c^> <> {} & b = b & c = c holds for b, c being Object of A2 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

H . f9 = (Morph-Map ((F "),b,c)) . f

let a be Object of B2; :: thesis: for a1 being Object of A2 st a = a1 holds

H . a = (F ") . a1

let a1 be Object of A2; :: thesis: ( a = a1 implies H . a = (F ") . a1 )

reconsider Ha = H . a as Object of A1 by A9;

G . (H . a) = F . Ha by A4;

then A11: F . Ha = a by A3, A7, A6, Th1;

assume a = a1 ; :: thesis: H . a = (F ") . a1

hence H . a = (F ") . a1 by A1, A2, A11, Th1; :: thesis: verum

end;H . a = (F ") . a1

let a1 be Object of A2; :: thesis: ( a = a1 implies H . a = (F ") . a1 )

reconsider Ha = H . a as Object of A1 by A9;

G . (H . a) = F . Ha by A4;

then A11: F . Ha = a by A3, A7, A6, Th1;

assume a = a1 ; :: thesis: H . a = (F ") . a1

hence H . a = (F ") . a1 by A1, A2, A11, Th1; :: thesis: verum

for f9 being Morphism of b,c

for f being Morphism of b,c st f9 = f holds

H . f9 = (Morph-Map ((F "),b,c)) . f

let b1, c1 be Object of A2; :: thesis: ( <^b,c^> <> {} & b = b1 & c = c1 implies for f9 being Morphism of b,c

for f being Morphism of b1,c1 st f9 = f holds

H . f9 = (Morph-Map ((F "),b1,c1)) . f )

assume that

A12: <^b,c^> <> {} and

A13: ( b = b1 & c = c1 ) ; :: thesis: for f9 being Morphism of b,c

for f being Morphism of b1,c1 st f9 = f holds

H . f9 = (Morph-Map ((F "),b1,c1)) . f

let f be Morphism of b,c; :: thesis: for f being Morphism of b1,c1 st f = f holds

H . f = (Morph-Map ((F "),b1,c1)) . f

let f1 be Morphism of b1,c1; :: thesis: ( f = f1 implies H . f = (Morph-Map ((F "),b1,c1)) . f1 )

assume A14: f = f1 ; :: thesis: H . f = (Morph-Map ((F "),b1,c1)) . f1

A15: ( <^b,c^> c= <^b1,c1^> & f in <^b,c^> ) by A12, A13, ALTCAT_2:31;

A16: ( G . (H . b) = b & G . (H . c) = c ) by A3, A7, A6, Th1;

A17: <^(H . b),(H . c)^> <> {} by A12, FUNCTOR0:def 18;

then A18: H . f in <^(H . b),(H . c)^> ;

A19: ( F . ((F ") . b1) = b1 & F . ((F ") . c1) = c1 ) by A1, A2, Th1;

A20: ( H . b = (F ") . b1 & H . c = (F ") . c1 ) by A10, A13;

then A21: <^(H . b),(H . c)^> c= <^((F ") . b1),((F ") . c1)^> by ALTCAT_2:31;

then reconsider Hf = H . f as Morphism of ((F ") . b1),((F ") . c1) by A18;

G . (H . f) = (Morph-Map (F,((F ") . b1),((F ") . c1))) . Hf by A5, A20, A17

.= F . Hf by A21, A18, A15, A19, FUNCTOR0:def 15 ;

then F . Hf = f by A3, A7, A17, A16, Th2;

hence H . f = F9 . f1 by A1, A14, A21, A18, A19, Th2

.= (Morph-Map ((F "),b1,c1)) . f1 by A21, A18, A15, FUNCTOR0:def 15 ;

:: thesis: verum