let A, B, C, D be category; :: thesis: ( A,B are_opposite & C,D are_opposite implies for F, G being covariant Functor of B,C st F,G are_naturally_equivalent holds
((dualizing-func C,D) * G) * (dualizing-func A,B),((dualizing-func C,D) * F) * (dualizing-func A,B) are_naturally_equivalent )
assume that
A1: A,B are_opposite and
A2: C,D are_opposite ; :: thesis: for F, G being covariant Functor of B,C st F,G are_naturally_equivalent holds
((dualizing-func C,D) * G) * (dualizing-func A,B),((dualizing-func C,D) * F) * (dualizing-func A,B) are_naturally_equivalent
let F, G be covariant Functor of B,C; :: thesis: ( F,G are_naturally_equivalent implies ((dualizing-func C,D) * G) * (dualizing-func A,B),((dualizing-func C,D) * F) * (dualizing-func A,B) are_naturally_equivalent )
assume that
A3: F is_naturally_transformable_to G and
A4: G is_transformable_to F ; :: according to FUNCTOR3:def 4 :: thesis: ( for b1 being natural_transformation of F,G holds
not for b2 being Element of the carrier of B holds b1 ! b2 is iso or ((dualizing-func C,D) * G) * (dualizing-func A,B),((dualizing-func C,D) * F) * (dualizing-func A,B) are_naturally_equivalent )
given t being natural_transformation of F,G such that A5: for a being object of B holds t ! a is iso ; :: thesis: ((dualizing-func C,D) * G) * (dualizing-func A,B),((dualizing-func C,D) * F) * (dualizing-func A,B) are_naturally_equivalent
set dAB = dualizing-func A,B;
set dCD = dualizing-func C,D;
set dF = ((dualizing-func C,D) * F) * (dualizing-func A,B);
set dG = ((dualizing-func C,D) * G) * (dualizing-func A,B);
A6: F is_transformable_to G by A3, FUNCTOR2:def 6;
A7: now
let a be object of A; :: thesis: ( (((dualizing-func C,D) * G) * (dualizing-func A,B)) . a = (dualizing-func C,D) . (G . ((dualizing-func A,B) . a)) & (((dualizing-func C,D) * F) * (dualizing-func A,B)) . a = (dualizing-func C,D) . (F . ((dualizing-func A,B) . a)) & (((dualizing-func C,D) * G) * (dualizing-func A,B)) . a = G . ((dualizing-func A,B) . a) & (((dualizing-func C,D) * F) * (dualizing-func A,B)) . a = F . ((dualizing-func A,B) . a) & <^((((dualizing-func C,D) * G) * (dualizing-func A,B)) . a),((((dualizing-func C,D) * F) * (dualizing-func A,B)) . a)^> = <^(F . ((dualizing-func A,B) . a)),(G . ((dualizing-func A,B) . a))^> )
A8: (((dualizing-func C,D) * G) * (dualizing-func A,B)) . a = ((dualizing-func C,D) * G) . ((dualizing-func A,B) . a) by FUNCTOR0:34;
(((dualizing-func C,D) * F) * (dualizing-func A,B)) . a = ((dualizing-func C,D) * F) . ((dualizing-func A,B) . a) by FUNCTOR0:34;
hence ( (((dualizing-func C,D) * G) * (dualizing-func A,B)) . a = (dualizing-func C,D) . (G . ((dualizing-func A,B) . a)) & (((dualizing-func C,D) * F) * (dualizing-func A,B)) . a = (dualizing-func C,D) . (F . ((dualizing-func A,B) . a)) ) by A8, FUNCTOR0:34; :: thesis: ( (((dualizing-func C,D) * G) * (dualizing-func A,B)) . a = G . ((dualizing-func A,B) . a) & (((dualizing-func C,D) * F) * (dualizing-func A,B)) . a = F . ((dualizing-func A,B) . a) & <^((((dualizing-func C,D) * G) * (dualizing-func A,B)) . a),((((dualizing-func C,D) * F) * (dualizing-func A,B)) . a)^> = <^(F . ((dualizing-func A,B) . a)),(G . ((dualizing-func A,B) . a))^> )
hence ( (((dualizing-func C,D) * G) * (dualizing-func A,B)) . a = G . ((dualizing-func A,B) . a) & (((dualizing-func C,D) * F) * (dualizing-func A,B)) . a = F . ((dualizing-func A,B) . a) ) by A2, Def5; :: thesis: <^((((dualizing-func C,D) * G) * (dualizing-func A,B)) . a),((((dualizing-func C,D) * F) * (dualizing-func A,B)) . a)^> = <^(F . ((dualizing-func A,B) . a)),(G . ((dualizing-func A,B) . a))^>
hence <^((((dualizing-func C,D) * G) * (dualizing-func A,B)) . a),((((dualizing-func C,D) * F) * (dualizing-func A,B)) . a)^> = <^(F . ((dualizing-func A,B) . a)),(G . ((dualizing-func A,B) . a))^> by A2, Th9; :: thesis: verum
end;
A9: ((dualizing-func C,D) * G) * (dualizing-func A,B) is_transformable_to ((dualizing-func C,D) * F) * (dualizing-func A,B)
proof
let a be object of A; :: according to FUNCTOR2:def 1 :: thesis: not <^((((dualizing-func C,D) * G) * (dualizing-func A,B)) . a),((((dualizing-func C,D) * F) * (dualizing-func A,B)) . a)^> = {}
<^((((dualizing-func C,D) * G) * (dualizing-func A,B)) . a),((((dualizing-func C,D) * F) * (dualizing-func A,B)) . a)^> = <^(F . ((dualizing-func A,B) . a)),(G . ((dualizing-func A,B) . a))^> by A7;
hence not <^((((dualizing-func C,D) * G) * (dualizing-func A,B)) . a),((((dualizing-func C,D) * F) * (dualizing-func A,B)) . a)^> = {} by A6, FUNCTOR2:def 1; :: thesis: verum
end;
dom t = the carrier of B by PARTFUN1:def 4
.= the carrier of A by A1, Def3 ;
then reconsider dt = t as ManySortedSet of the carrier of A by PARTFUN1:def 4, RELAT_1:def 18;
dt is transformation of ((dualizing-func C,D) * G) * (dualizing-func A,B),((dualizing-func C,D) * F) * (dualizing-func A,B)
proof
thus ((dualizing-func C,D) * G) * (dualizing-func A,B) is_transformable_to ((dualizing-func C,D) * F) * (dualizing-func A,B) by A9; :: according to FUNCTOR2:def 2 :: thesis: for b1 being Element of the carrier of A holds dt . b1 is Element of <^((((dualizing-func C,D) * G) * (dualizing-func A,B)) . b1),((((dualizing-func C,D) * F) * (dualizing-func A,B)) . b1)^>
let a be object of A; :: thesis: dt . a is Element of <^((((dualizing-func C,D) * G) * (dualizing-func A,B)) . a),((((dualizing-func C,D) * F) * (dualizing-func A,B)) . a)^>
set b = (dualizing-func A,B) . a;
A10: (dualizing-func A,B) . a = a by A1, Def5;
t . ((dualizing-func A,B) . a) = t ! ((dualizing-func A,B) . a) by A6, FUNCTOR2:def 4;
hence dt . a is Element of <^((((dualizing-func C,D) * G) * (dualizing-func A,B)) . a),((((dualizing-func C,D) * F) * (dualizing-func A,B)) . a)^> by A7, A10; :: thesis: verum
end;
then reconsider dt = dt as transformation of ((dualizing-func C,D) * G) * (dualizing-func A,B),((dualizing-func C,D) * F) * (dualizing-func A,B) ;
A11: now
let a, b be object of A; :: thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds (dt ! b) * ((((dualizing-func C,D) * G) * (dualizing-func A,B)) . f) = ((((dualizing-func C,D) * F) * (dualizing-func A,B)) . f) * (dt ! a) )
assume A12: <^a,b^> <> {} ; :: thesis: for f being Morphism of a,b holds (dt ! b) * ((((dualizing-func C,D) * G) * (dualizing-func A,B)) . f) = ((((dualizing-func C,D) * F) * (dualizing-func A,B)) . f) * (dt ! a)
let f be Morphism of a,b; :: thesis: (dt ! b) * ((((dualizing-func C,D) * G) * (dualizing-func A,B)) . f) = ((((dualizing-func C,D) * F) * (dualizing-func A,B)) . f) * (dt ! a)
set b9 = (dualizing-func A,B) . b;
set a9 = (dualizing-func A,B) . a;
set f9 = (dualizing-func A,B) . f;
A13: (dualizing-func A,B) . a = a by A1, Def5;
A14: (dualizing-func A,B) . b = b by A1, Def5;
then A15: <^((dualizing-func A,B) . b),((dualizing-func A,B) . a)^> = <^a,b^> by A1, A13, Th9;
A16: t ! ((dualizing-func A,B) . a) = t . a by A6, A13, FUNCTOR2:def 4;
A17: t ! ((dualizing-func A,B) . b) = t . b by A6, A14, FUNCTOR2:def 4;
A18: dt ! a = t . a by A9, FUNCTOR2:def 4;
A19: dt ! b = t . b by A9, FUNCTOR2:def 4;
A20: <^(F . ((dualizing-func A,B) . b)),(F . ((dualizing-func A,B) . a))^> <> {} by A12, A15, FUNCTOR0:def 19;
A21: <^(G . ((dualizing-func A,B) . b)),(G . ((dualizing-func A,B) . a))^> <> {} by A12, A15, FUNCTOR0:def 19;
A22: (((dualizing-func C,D) * F) * (dualizing-func A,B)) . f = ((dualizing-func C,D) * F) . ((dualizing-func A,B) . f) by A12, FUNCTOR3:7;
A23: (((dualizing-func C,D) * G) * (dualizing-func A,B)) . f = ((dualizing-func C,D) * G) . ((dualizing-func A,B) . f) by A12, FUNCTOR3:7;
A24: (((dualizing-func C,D) * F) * (dualizing-func A,B)) . f = (dualizing-func C,D) . (F . ((dualizing-func A,B) . f)) by A12, A15, A22, FUNCTOR3:8;
A25: (((dualizing-func C,D) * G) * (dualizing-func A,B)) . f = (dualizing-func C,D) . (G . ((dualizing-func A,B) . f)) by A12, A15, A23, FUNCTOR3:8;
A26: (((dualizing-func C,D) * F) * (dualizing-func A,B)) . f = F . ((dualizing-func A,B) . f) by A2, A20, A24, Def5;
A27: (((dualizing-func C,D) * G) * (dualizing-func A,B)) . f = G . ((dualizing-func A,B) . f) by A2, A21, A25, Def5;
A28: <^(F . ((dualizing-func A,B) . b)),(G . ((dualizing-func A,B) . b))^> <> {} by A6, FUNCTOR2:def 1;
A29: <^(F . ((dualizing-func A,B) . a)),(G . ((dualizing-func A,B) . a))^> <> {} by A6, FUNCTOR2:def 1;
A30: (((dualizing-func C,D) * G) * (dualizing-func A,B)) . a = G . ((dualizing-func A,B) . a) by A7;
A31: (((dualizing-func C,D) * F) * (dualizing-func A,B)) . a = F . ((dualizing-func A,B) . a) by A7;
A32: (((dualizing-func C,D) * G) * (dualizing-func A,B)) . b = G . ((dualizing-func A,B) . b) by A7;
A33: (((dualizing-func C,D) * F) * (dualizing-func A,B)) . b = F . ((dualizing-func A,B) . b) by A7;
hence (dt ! b) * ((((dualizing-func C,D) * G) * (dualizing-func A,B)) . f) = (G . ((dualizing-func A,B) . f)) * (t ! ((dualizing-func A,B) . b)) by A2, A17, A19, A21, A27, A28, A30, A32, Th9
.= (t ! ((dualizing-func A,B) . a)) * (F . ((dualizing-func A,B) . f)) by A3, A12, A15, FUNCTOR2:def 7
.= ((((dualizing-func C,D) * F) * (dualizing-func A,B)) . f) * (dt ! a) by A2, A16, A18, A20, A26, A29, A30, A31, A33, Th9 ;
:: thesis: verum
end;
thus ((dualizing-func C,D) * G) * (dualizing-func A,B) is_naturally_transformable_to ((dualizing-func C,D) * F) * (dualizing-func A,B) :: according to FUNCTOR3:def 4 :: thesis: ( ((dualizing-func C,D) * F) * (dualizing-func A,B) is_transformable_to ((dualizing-func C,D) * G) * (dualizing-func A,B) & ex b1 being natural_transformation of ((dualizing-func C,D) * G) * (dualizing-func A,B),((dualizing-func C,D) * F) * (dualizing-func A,B) st
for b2 being Element of the carrier of A holds b1 ! b2 is iso )
proof
thus ((dualizing-func C,D) * G) * (dualizing-func A,B) is_transformable_to ((dualizing-func C,D) * F) * (dualizing-func A,B) by A9; :: according to FUNCTOR2:def 6 :: thesis: ex b1 being transformation of ((dualizing-func C,D) * G) * (dualizing-func A,B),((dualizing-func C,D) * F) * (dualizing-func A,B) st
for b2, b3 being Element of the carrier of A holds
( <^b2,b3^> = {} or for b4 being Element of <^b2,b3^> holds (b1 ! b3) * ((((dualizing-func C,D) * G) * (dualizing-func A,B)) . b4) = ((((dualizing-func C,D) * F) * (dualizing-func A,B)) . b4) * (b1 ! b2) )
take dt ; :: thesis: for b1, b2 being Element of the carrier of A holds
( <^b1,b2^> = {} or for b3 being Element of <^b1,b2^> holds (dt ! b2) * ((((dualizing-func C,D) * G) * (dualizing-func A,B)) . b3) = ((((dualizing-func C,D) * F) * (dualizing-func A,B)) . b3) * (dt ! b1) )
thus for b1, b2 being Element of the carrier of A holds
( <^b1,b2^> = {} or for b3 being Element of <^b1,b2^> holds (dt ! b2) * ((((dualizing-func C,D) * G) * (dualizing-func A,B)) . b3) = ((((dualizing-func C,D) * F) * (dualizing-func A,B)) . b3) * (dt ! b1) ) by A11; :: thesis: verum
end;
then reconsider dt = dt as natural_transformation of ((dualizing-func C,D) * G) * (dualizing-func A,B),((dualizing-func C,D) * F) * (dualizing-func A,B) by A11, FUNCTOR2:def 7;
thus ((dualizing-func C,D) * F) * (dualizing-func A,B) is_transformable_to ((dualizing-func C,D) * G) * (dualizing-func A,B) :: thesis: ex b1 being natural_transformation of ((dualizing-func C,D) * G) * (dualizing-func A,B),((dualizing-func C,D) * F) * (dualizing-func A,B) st
for b2 being Element of the carrier of A holds b1 ! b2 is iso
proof
let a be object of A; :: according to FUNCTOR2:def 1 :: thesis: not <^((((dualizing-func C,D) * F) * (dualizing-func A,B)) . a),((((dualizing-func C,D) * G) * (dualizing-func A,B)) . a)^> = {}
A34: (((dualizing-func C,D) * F) * (dualizing-func A,B)) . a = F . ((dualizing-func A,B) . a) by A7;
(((dualizing-func C,D) * G) * (dualizing-func A,B)) . a = G . ((dualizing-func A,B) . a) by A7;
then <^((((dualizing-func C,D) * F) * (dualizing-func A,B)) . a),((((dualizing-func C,D) * G) * (dualizing-func A,B)) . a)^> = <^(G . ((dualizing-func A,B) . a)),(F . ((dualizing-func A,B) . a))^> by A2, A34, Th9;
hence not <^((((dualizing-func C,D) * F) * (dualizing-func A,B)) . a),((((dualizing-func C,D) * G) * (dualizing-func A,B)) . a)^> = {} by A4, FUNCTOR2:def 1; :: thesis: verum
end;
take dt ; :: thesis: for b1 being Element of the carrier of A holds dt ! b1 is iso
let a be object of A; :: thesis: dt ! a is iso
A35: (((dualizing-func C,D) * G) * (dualizing-func A,B)) . a = G . ((dualizing-func A,B) . a) by A7;
A36: (((dualizing-func C,D) * F) * (dualizing-func A,B)) . a = F . ((dualizing-func A,B) . a) by A7;
A37: (dualizing-func A,B) . a = a by A1, Def5;
A38: dt ! a = t . a by A9, FUNCTOR2:def 4;
A39: t ! ((dualizing-func A,B) . a) = t . a by A6, A37, FUNCTOR2:def 4;
A40: t ! ((dualizing-func A,B) . a) is iso by A5;
A41: <^(F . ((dualizing-func A,B) . a)),(G . ((dualizing-func A,B) . a))^> <> {} by A6, FUNCTOR2:def 1;
<^(G . ((dualizing-func A,B) . a)),(F . ((dualizing-func A,B) . a))^> <> {} by A4, FUNCTOR2:def 1;
hence dt ! a is iso by A2, A35, A36, A38, A39, A40, A41, Th24; :: thesis: verum