defpred S1[ set , set ] means for F1, F2 being Functor of A,[:B,C:]
for t being natural_transformation of F1,F2 st $1 = [[F1,F2],t] holds
$2 = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]];
A1:
now let f be
Morphism of
(Functors A,[:B,C:]);
:: thesis: ex g being Morphism of [:(Functors A,B),(Functors A,C):] st S1[f,g]A2:
( the
carrier' of
(Functors A,B) = NatTrans A,
B & the
carrier' of
(Functors A,C) = NatTrans A,
C )
by NATTRA_1:def 18;
consider F1,
F2 being
Functor of
A,
[:B,C:],
s being
natural_transformation of
F1,
F2 such that A3:
F1 is_naturally_transformable_to F2
and A4:
(
dom f = F1 &
cod f = F2 &
f = [[F1,F2],s] )
by Th9;
(
Pr1 F1 is_naturally_transformable_to Pr1 F2 &
Pr2 F1 is_naturally_transformable_to Pr2 F2 )
by A3, ISOCAT_1:27;
then
(
[[(Pr1 F1),(Pr1 F2)],(Pr1 s)] is
Morphism of
(Functors A,B) &
[[(Pr2 F1),(Pr2 F2)],(Pr2 s)] is
Morphism of
(Functors A,C) )
by A2, NATTRA_1:35;
then reconsider g =
[[[(Pr1 F1),(Pr1 F2)],(Pr1 s)],[[(Pr2 F1),(Pr2 F2)],(Pr2 s)]] as
Morphism of
[:(Functors A,B),(Functors A,C):] by CAT_2:36;
take g =
g;
:: thesis: S1[f,g]thus
S1[
f,
g]
:: thesis: verumproof
let G1,
G2 be
Functor of
A,
[:B,C:];
:: thesis: for t being natural_transformation of G1,G2 st f = [[G1,G2],t] holds
g = [[[(Pr1 G1),(Pr1 G2)],(Pr1 t)],[[(Pr2 G1),(Pr2 G2)],(Pr2 t)]]let t be
natural_transformation of
G1,
G2;
:: thesis: ( f = [[G1,G2],t] implies g = [[[(Pr1 G1),(Pr1 G2)],(Pr1 t)],[[(Pr2 G1),(Pr2 G2)],(Pr2 t)]] )
assume
f = [[G1,G2],t]
;
:: thesis: g = [[[(Pr1 G1),(Pr1 G2)],(Pr1 t)],[[(Pr2 G1),(Pr2 G2)],(Pr2 t)]]
then A5:
(
[G1,G2] = [F1,F2] &
t = s )
by A4, ZFMISC_1:33;
then
(
G1 = F1 &
G2 = F2 )
by ZFMISC_1:33;
hence
g = [[[(Pr1 G1),(Pr1 G2)],(Pr1 t)],[[(Pr2 G1),(Pr2 G2)],(Pr2 t)]]
by A5;
:: thesis: verum
end; end;
consider IT being Function of the carrier' of (Functors A,[:B,C:]),the carrier' of [:(Functors A,B),(Functors A,C):] such that
A6:
for f being Morphism of (Functors A,[:B,C:]) holds S1[f,IT . f]
from FUNCT_2:sch 3(A1);
IT is Functor of Functors A,[:B,C:],[:(Functors A,B),(Functors A,C):]
proof
A7:
the
carrier' of
(Functors A,B) = NatTrans A,
B
by NATTRA_1:def 18;
A8:
the
carrier' of
(Functors A,C) = NatTrans A,
C
by NATTRA_1:def 18;
thus
for
c being
Object of
(Functors A,[:B,C:]) ex
d being
Object of
[:(Functors A,B),(Functors A,C):] st
IT . (id c) = id d
:: according to ISOCAT_1:def 1 :: thesis: ( ( for b1 being Element of the carrier' of (Functors A,[:B,C:]) holds
( IT . (id (dom b1)) = id (dom (IT . b1)) & IT . (id (cod b1)) = id (cod (IT . b1)) ) ) & ( for b1, b2 being Element of the carrier' of (Functors A,[:B,C:]) holds
( not dom b2 = cod b1 or IT . (b2 * b1) = (IT . b2) * (IT . b1) ) ) )proof
let c be
Object of
(Functors A,[:B,C:]);
:: thesis: ex d being Object of [:(Functors A,B),(Functors A,C):] st IT . (id c) = id d
reconsider F =
c as
Functor of
A,
[:B,C:] by Th8;
reconsider d1 =
Pr1 F as
Object of
(Functors A,B) by Th8;
reconsider d2 =
Pr2 F as
Object of
(Functors A,C) by Th8;
take
[d1,d2]
;
:: thesis: IT . (id c) = id [d1,d2]
Pr1 (id F) = id (Pr1 F)
by ISOCAT_1:38;
then A9:
id d1 = [[(Pr1 F),(Pr1 F)],(Pr1 (id F))]
by NATTRA_1:def 18;
Pr2 (id F) = id (Pr2 F)
by ISOCAT_1:38;
then A10:
id d2 = [[(Pr2 F),(Pr2 F)],(Pr2 (id F))]
by NATTRA_1:def 18;
id c = [[F,F],(id F)]
by NATTRA_1:def 18;
hence IT . (id c) =
[(id d1),(id d2)]
by A6, A9, A10
.=
id [d1,d2]
by CAT_2:41
;
:: thesis: verum
end;
thus
for
f being
Morphism of
(Functors A,[:B,C:]) holds
(
IT . (id (dom f)) = id (dom (IT . f)) &
IT . (id (cod f)) = id (cod (IT . f)) )
:: thesis: for b1, b2 being Element of the carrier' of (Functors A,[:B,C:]) holds
( not dom b2 = cod b1 or IT . (b2 * b1) = (IT . b2) * (IT . b1) )proof
let f be
Morphism of
(Functors A,[:B,C:]);
:: thesis: ( IT . (id (dom f)) = id (dom (IT . f)) & IT . (id (cod f)) = id (cod (IT . f)) )
consider F1,
F2 being
Functor of
A,
[:B,C:],
s being
natural_transformation of
F1,
F2 such that A11:
F1 is_naturally_transformable_to F2
and A12:
(
dom f = F1 &
cod f = F2 &
f = [[F1,F2],s] )
by Th9;
Pr1 F1 is_naturally_transformable_to Pr1 F2
by A11, ISOCAT_1:27;
then reconsider f1 =
[[(Pr1 F1),(Pr1 F2)],(Pr1 s)] as
Morphism of
(Functors A,B) by A7, NATTRA_1:35;
Pr2 F1 is_naturally_transformable_to Pr2 F2
by A11, ISOCAT_1:27;
then reconsider f2 =
[[(Pr2 F1),(Pr2 F2)],(Pr2 s)] as
Morphism of
(Functors A,C) by A8, NATTRA_1:35;
(
dom f1 = Pr1 F1 &
Pr1 (id F1) = id (Pr1 F1) )
by ISOCAT_1:38, NATTRA_1:39;
then A13:
id (dom f1) = [[(Pr1 F1),(Pr1 F1)],(Pr1 (id F1))]
by NATTRA_1:def 18;
(
dom f2 = Pr2 F1 &
Pr2 (id F1) = id (Pr2 F1) )
by ISOCAT_1:38, NATTRA_1:39;
then A14:
id (dom f2) = [[(Pr2 F1),(Pr2 F1)],(Pr2 (id F1))]
by NATTRA_1:def 18;
id (dom f) = [[F1,F1],(id F1)]
by A12, NATTRA_1:def 18;
hence IT . (id (dom f)) =
[(id (dom f1)),(id (dom f2))]
by A6, A13, A14
.=
id [(dom f1),(dom f2)]
by CAT_2:41
.=
id (dom [f1,f2])
by CAT_2:38
.=
id (dom (IT . f))
by A6, A12
;
:: thesis: IT . (id (cod f)) = id (cod (IT . f))
(
cod f1 = Pr1 F2 &
Pr1 (id F2) = id (Pr1 F2) )
by ISOCAT_1:38, NATTRA_1:39;
then A15:
id (cod f1) = [[(Pr1 F2),(Pr1 F2)],(Pr1 (id F2))]
by NATTRA_1:def 18;
(
cod f2 = Pr2 F2 &
Pr2 (id F2) = id (Pr2 F2) )
by ISOCAT_1:38, NATTRA_1:39;
then A16:
id (cod f2) = [[(Pr2 F2),(Pr2 F2)],(Pr2 (id F2))]
by NATTRA_1:def 18;
id (cod f) = [[F2,F2],(id F2)]
by A12, NATTRA_1:def 18;
hence IT . (id (cod f)) =
[(id (cod f1)),(id (cod f2))]
by A6, A15, A16
.=
id [(cod f1),(cod f2)]
by CAT_2:41
.=
id (cod [f1,f2])
by CAT_2:38
.=
id (cod (IT . f))
by A6, A12
;
:: thesis: verum
end;
let f,
g be
Morphism of
(Functors A,[:B,C:]);
:: thesis: ( not dom g = cod f or IT . (g * f) = (IT . g) * (IT . f) )
assume A17:
dom g = cod f
;
:: thesis: IT . (g * f) = (IT . g) * (IT . f)
consider F1,
F2 being
Functor of
A,
[:B,C:],
s being
natural_transformation of
F1,
F2 such that A18:
F1 is_naturally_transformable_to F2
and A19:
(
dom f = F1 &
cod f = F2 &
f = [[F1,F2],s] )
by Th9;
consider G1,
G2 being
Functor of
A,
[:B,C:],
t being
natural_transformation of
G1,
G2 such that A20:
G1 is_naturally_transformable_to G2
and A21:
(
dom g = G1 &
cod g = G2 &
g = [[G1,G2],t] )
by Th9;
reconsider t =
t as
natural_transformation of
F2,
G2 by A17, A19, A21;
A22:
IT . f = [[[(Pr1 F1),(Pr1 F2)],(Pr1 s)],[[(Pr2 F1),(Pr2 F2)],(Pr2 s)]]
by A6, A19;
(
Pr1 F1 is_naturally_transformable_to Pr1 F2 &
Pr1 F2 is_naturally_transformable_to Pr1 G2 )
by A17, A18, A19, A20, A21, ISOCAT_1:27;
then reconsider g1 =
[[(Pr1 F2),(Pr1 G2)],(Pr1 t)],
f1 =
[[(Pr1 F1),(Pr1 F2)],(Pr1 s)] as
Morphism of
(Functors A,B) by A7, NATTRA_1:35;
(
Pr2 F1 is_naturally_transformable_to Pr2 F2 &
Pr2 F2 is_naturally_transformable_to Pr2 G2 )
by A17, A18, A19, A20, A21, ISOCAT_1:27;
then reconsider g2 =
[[(Pr2 F2),(Pr2 G2)],(Pr2 t)],
f2 =
[[(Pr2 F1),(Pr2 F2)],(Pr2 s)] as
Morphism of
(Functors A,C) by A8, NATTRA_1:35;
A23:
dom g1 =
Pr1 F2
by NATTRA_1:39
.=
cod f1
by NATTRA_1:39
;
A24:
dom g2 =
Pr2 F2
by NATTRA_1:39
.=
cod f2
by NATTRA_1:39
;
A25:
g1 * f1 =
[[(Pr1 F1),(Pr1 G2)],((Pr1 t) `*` (Pr1 s))]
by NATTRA_1:42
.=
[[(Pr1 F1),(Pr1 G2)],(Pr1 (t `*` s))]
by A17, A18, A19, A20, A21, ISOCAT_1:32
;
A26:
g2 * f2 =
[[(Pr2 F1),(Pr2 G2)],((Pr2 t) `*` (Pr2 s))]
by NATTRA_1:42
.=
[[(Pr2 F1),(Pr2 G2)],(Pr2 (t `*` s))]
by A17, A18, A19, A20, A21, ISOCAT_1:32
;
g * f = [[F1,G2],(t `*` s)]
by A17, A19, A21, NATTRA_1:42;
hence IT . (g * f) =
[(g1 * f1),(g2 * f2)]
by A6, A25, A26
.=
[g1,g2] * [f1,f2]
by A23, A24, CAT_2:39
.=
(IT . g) * (IT . f)
by A6, A17, A19, A21, A22
;
:: thesis: verum
end;
then reconsider IT = IT as Functor of Functors A,[:B,C:],[:(Functors A,B),(Functors A,C):] ;
take
IT
; :: thesis: for F1, F2 being Functor of A,[:B,C:] st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds IT . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]]
let F1, F2 be Functor of A,[:B,C:]; :: thesis: ( F1 is_naturally_transformable_to F2 implies for t being natural_transformation of F1,F2 holds IT . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]] )
assume A27:
F1 is_naturally_transformable_to F2
; :: thesis: for t being natural_transformation of F1,F2 holds IT . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]]
let t be natural_transformation of F1,F2; :: thesis: IT . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]]
set f = [[F1,F2],t];
[[F1,F2],t] in NatTrans A,[:B,C:]
by A27, NATTRA_1:35;
then reconsider f = [[F1,F2],t] as Morphism of (Functors A,[:B,C:]) by NATTRA_1:def 18;
thus IT . [[F1,F2],t] =
IT . f
.=
[[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]]
by A6
; :: thesis: verum