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 A1:
( A,B are_opposite & 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
A2:
F is_naturally_transformable_to G
and
A3:
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 A4:
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);
A5:
F is_transformable_to G
by A2, FUNCTOR2:def 6;
A6:
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))^> )
(
(((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 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 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 A1, 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 A1, Th9;
:: thesis: verum end;
A7:
((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 A6;
hence
not
<^((((dualizing-func C,D) * G) * (dualizing-func A,B)) . a),((((dualizing-func C,D) * F) * (dualizing-func A,B)) . a)^> = {}
by A5, 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 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 A7;
:: 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;
(
(dualizing-func A,B) . a = a &
t . ((dualizing-func A,B) . a) = t ! ((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 A1, A5, A6, Def5, 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)^>
;
:: 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) ;
A8:
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 A9:
<^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 b' =
(dualizing-func A,B) . b;
set a' =
(dualizing-func A,B) . a;
set f' =
(dualizing-func A,B) . f;
A10:
(
(dualizing-func A,B) . a = a &
(dualizing-func A,B) . b = b )
by A1, Def5;
then A11:
<^((dualizing-func A,B) . b),((dualizing-func A,B) . a)^> = <^a,b^>
by A1, Th9;
A12:
(
t ! ((dualizing-func A,B) . a) = t . a &
t ! ((dualizing-func A,B) . b) = t . b &
dt ! a = t . a &
dt ! b = t . b )
by A5, A7, A10, FUNCTOR2:def 4;
A13:
(
<^(F . ((dualizing-func A,B) . b)),(F . ((dualizing-func A,B) . a))^> <> {} &
<^(G . ((dualizing-func A,B) . b)),(G . ((dualizing-func A,B) . a))^> <> {} )
by A9, A11, FUNCTOR0:def 19;
(
(((dualizing-func C,D) * F) * (dualizing-func A,B)) . f = ((dualizing-func C,D) * F) . ((dualizing-func A,B) . f) &
(((dualizing-func C,D) * G) * (dualizing-func A,B)) . f = ((dualizing-func C,D) * G) . ((dualizing-func A,B) . f) )
by A9, FUNCTOR3:7;
then
(
(((dualizing-func C,D) * F) * (dualizing-func A,B)) . f = (dualizing-func C,D) . (F . ((dualizing-func A,B) . f)) &
(((dualizing-func C,D) * G) * (dualizing-func A,B)) . f = (dualizing-func C,D) . (G . ((dualizing-func A,B) . f)) )
by A9, A11, FUNCTOR3:8;
then A14:
(
(((dualizing-func C,D) * F) * (dualizing-func A,B)) . f = F . ((dualizing-func A,B) . f) &
(((dualizing-func C,D) * G) * (dualizing-func A,B)) . f = G . ((dualizing-func A,B) . f) )
by A1, A13, Def5;
A15:
(
<^(F . ((dualizing-func A,B) . b)),(G . ((dualizing-func A,B) . b))^> <> {} &
<^(F . ((dualizing-func A,B) . a)),(G . ((dualizing-func A,B) . a))^> <> {} )
by A5, FUNCTOR2:def 1;
A16:
(
(((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)) . b = G . ((dualizing-func A,B) . b) &
(((dualizing-func C,D) * F) * (dualizing-func A,B)) . b = F . ((dualizing-func A,B) . b) )
by A6;
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 A1, A12, A13, A14, A15, Th9
.=
(t ! ((dualizing-func A,B) . a)) * (F . ((dualizing-func A,B) . f))
by A2, A9, A11, FUNCTOR2:def 7
.=
((((dualizing-func C,D) * F) * (dualizing-func A,B)) . f) * (dt ! a)
by A1, A12, A13, A14, A15, A16, Th9
;
:: thesis: verum end;
thus A17:
((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 A7;
:: 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 A8;
:: thesis: verum
end;
dt is natural_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_naturally_transformable_to ((dualizing-func C,D) * F) * (dualizing-func A,B)
by A17;
:: according to FUNCTOR2:def 7 :: 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 A8;
:: 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) ;
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)^> = {}
(
(((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 = G . ((dualizing-func A,B) . a) )
by A6;
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 A1, Th9;
hence
not
<^((((dualizing-func C,D) * F) * (dualizing-func A,B)) . a),((((dualizing-func C,D) * G) * (dualizing-func A,B)) . a)^> = {}
by A3, 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
A18:
( (((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 A6;
(dualizing-func A,B) . a = a
by A1, Def5;
then A19:
( dt ! a = t . a & t ! ((dualizing-func A,B) . a) = t . a )
by A5, A7, FUNCTOR2:def 4;
A20:
t ! ((dualizing-func A,B) . a) is iso
by A4;
( <^(F . ((dualizing-func A,B) . a)),(G . ((dualizing-func A,B) . a))^> <> {} & <^(G . ((dualizing-func A,B) . a)),(F . ((dualizing-func A,B) . a))^> <> {} )
by A3, A5, FUNCTOR2:def 1;
hence
dt ! a is iso
by A1, A18, A19, A20, Th24; :: thesis: verum