:: Some Isomorphisms Between Functor Categories
:: by Andrzej Trybulec
::
:: Received June 5, 1992
:: Copyright (c) 1992-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, FUNCT_1, FUNCT_2, FUNCT_5, ZFMISC_1, RELAT_1, TARSKI,
SUBSET_1, MCART_1, CAT_1, GRAPH_1, NATTRA_1, STRUCT_0, CAT_2, FINSEQ_2,
PZFMISC1, FUNCOP_1, PARTFUN1, BORSUK_1, ISOCAT_2, MONOID_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1,
PARTFUN1, FUNCOP_1, BINOP_1, FUNCT_3, FUNCT_2, FUNCT_5, STRUCT_0,
GRAPH_1, CAT_1, CAT_2, CAT_3, NATTRA_1, ISOCAT_1;
constructors DOMAIN_1, ISOCAT_1, FUNCOP_1, RELSET_1, CAT_3, RELAT_2, FUNCT_5,
FUNCT_4;
registrations XBOOLE_0, RELSET_1, FUNCT_2, STRUCT_0, CAT_1;
requirements SUBSET, BOOLE;
definitions TARSKI, FUNCT_1, NATTRA_1, ISOCAT_1, XBOOLE_0;
equalities TARSKI, CAT_1, BINOP_1, CAT_2;
expansions NATTRA_1;
theorems FUNCT_2, CAT_1, TARSKI, ZFMISC_1, FUNCT_1, DOMAIN_1, CAT_2, FUNCT_3,
FUNCOP_1, NATTRA_1, ISOCAT_1, FUNCT_5, CAT_3, XTUPLE_0;
schemes FUNCT_2;
begin :: Preliminaries
definition
let A,B,C be non empty set;
let f be Function of A, Funcs(B,C);
redefine func uncurry f -> Function of [:A,B:],C; :: redefines uncurry (FUNCT_5, definition)
coherence
proof
A1: rng f c= Funcs(B,C);
dom uncurry f = [:dom f,B:] by A1,FUNCT_5:26
.= [:A,B:] by FUNCT_2:def 1;
hence thesis;
end;
end;
theorem Th1:
for A,B,C being non empty set, f being Function of A,Funcs(B,C)
holds curry uncurry f = f
proof
let A,B,C be non empty set, f be Function of A,Funcs(B,C);
rng f c= Funcs(B,C);
hence thesis by FUNCT_5:48;
end;
theorem Th2:
for A,B,C being non empty set, f being Function of A, Funcs(B,C)
for a being Element of A, b being Element of B
holds (uncurry f).(a,b) = f.a.b
proof
let A,B,C be non empty set, f be Function of A, Funcs(B,C);
let a be Element of A, b be Element of B;
dom f = A & dom(f.a) = B by FUNCT_2:def 1;
hence thesis by FUNCT_5:38;
end;
::$CT 2
:: Auxiliary category theory facts
reserve A,B,C for Category,
F,F1 for Functor of A,B;
theorem Th3:
for f being Morphism of A holds (id cod f)(*)f = f
proof
let f be Morphism of A;
reconsider f9 = f as Morphism of dom f, cod f by CAT_1:4;
A1: Hom(dom f, cod f) <> {} by CAT_1:2;
Hom(cod f,cod f) <> {};
hence (id cod f)(*)f = (id cod f)*f9 by A1,CAT_1:def 13
.= f by A1,CAT_1:28;
end;
theorem Th4:
for f being Morphism of A holds f(*)(id dom f) = f
proof
let f be Morphism of A;
reconsider f9 = f as Morphism of dom f, cod f by CAT_1:4;
A1: Hom(dom f, cod f) <> {} by CAT_1:2;
Hom(dom f,dom f) <> {};
hence f(*)(id dom f) = f9*(id dom f) by A1,CAT_1:def 13
.= f by A1,CAT_1:29;
end;
reserve o,m for set;
reserve t for natural_transformation of F,F1;
theorem Th5:
o is Object of Functors(A,B) iff o is Functor of A,B
proof
the carrier of Functors(A,B) = Funct(A,B) by NATTRA_1:def 17;
hence thesis by CAT_2:def 2;
end;
theorem Th6:
for f being Morphism of Functors(A,B) ex F1,F2 being Functor of A
,B, t being natural_transformation of F1,F2 st F1 is_naturally_transformable_to
F2 & dom f = F1 & cod f = F2 & f = [[F1,F2],t]
proof
let m be Morphism of Functors(A,B);
Hom(dom m,cod m) <> {} & m is Morphism of dom m, cod m by CAT_1:2,4;
then consider F,F1,t such that
A1: dom m = F & cod m = F1 and
A2: m = [[F,F1],t] by NATTRA_1:34;
take F,F1,t;
the carrier' of Functors(A,B) = NatTrans(A,B) by NATTRA_1:def 17;
hence F is_naturally_transformable_to F1 by A2,NATTRA_1:32;
thus thesis by A1,A2;
end;
begin :: The isomorphism between A^1 and A
definition
let A,B;
let a be Object of A;
func a |-> B -> Functor of Functors(A,B), B means
:Def1:
for F1,F2 being Functor of A,B, t being natural_transformation of F1,F2 st F1
is_naturally_transformable_to F2 holds it.[[F1,F2],t] = t.a;
existence
proof
defpred P[set,set] means for F1,F2 being Functor of A,B, t be
natural_transformation of F1,F2 st $1 = [[F1,F2],t] holds $2 = t.a;
A1: the carrier' of Functors(A,B) = NatTrans(A,B) by NATTRA_1:def 17;
A2: now
let x be Element of NatTrans(A,B);
consider F1,F2 being Functor of A,B, t being natural_transformation of
F1,F2 such that
A3: x = [[F1,F2],t] and
F1 is_naturally_transformable_to F2 by NATTRA_1:def 16;
reconsider b = t.a as Morphism of B;
take b;
thus P[x,b]
proof
let F19,F29 be Functor of A,B, t9 be natural_transformation of F19,F29;
assume
A4: x = [[F19,F29],t9];
then [F1,F2] = [F19,F29] by A3,XTUPLE_0:1;
then F1 = F19 & F2 = F29 by XTUPLE_0:1;
hence thesis by A3,A4,XTUPLE_0:1;
end;
end;
consider f being Function of NatTrans(A,B), the carrier' of B such that
A5: for x being Element of NatTrans(A,B) holds P[x,f.x] from FUNCT_2:
sch 3(A2);
A6: the carrier' of Functors(A,B) = NatTrans(A,B) by NATTRA_1:def 17;
then reconsider ff=f as
Function of the carrier' of Functors(A,B), the carrier' of B;
A7: now
let c be Object of Functors(A,B);
reconsider F = c as Functor of A,B by Th5;
take d = F.a;
A8: [[F,F],id F] is Morphism of Functors(A,B) by A6,NATTRA_1:def 16;
thus f.id c
= f.[[F,F],id F] by NATTRA_1:def 17
.= (id F).a by A5,A6,A8
.= id d by NATTRA_1:20;
end;
A9: now
let m1,m2 be Morphism of Functors(A,B);
assume
A10: [m2,m1] in dom(the Comp of Functors(A,B));
reconsider m19=m1, m29=m2 as Element of NatTrans(A,B) by NATTRA_1:def 17;
consider F,F1,t such that
A11: F is_naturally_transformable_to F1 and
dom m1 = F and
cod m1 = F1 and
A12: m1 = [[F,F1],t] by Th6;
A13: Hom(F.a,F1.a) <> {} by A11,ISOCAT_1:25;
A14: f.m19 = t.a by A5,A12;
consider F19,F2 being Functor of A,B, t9 being natural_transformation of
F19,F2 such that
A15: F19 is_naturally_transformable_to F2 and
dom m2 = F19 and
cod m2 = F2 and
A16: m2 = [[F19,F2],t9] by Th6;
A17: F19 = dom m2 by A16,NATTRA_1:33
.= cod m1 by A10,CAT_1:15
.= F1 by A12,NATTRA_1:33;
then reconsider t9 as natural_transformation of F1,F2;
A18: Hom(F1.a,F2.a) <> {} by A15,A17,ISOCAT_1:25;
A19: f.m29 = t9.a by A5,A16,A17;
A20: m2(*)m1= [[F,F2],t9`*`t] by A12,A16,A17,NATTRA_1:36;
thus ff.(m2(*)m1) = (t9`*`t).a by A5,A6,A20
.= (t9.a)*(t.a) by A11,A15,A17,NATTRA_1:25
.= (t9.a)(*)(t.a) by A13,A18,CAT_1:def 13
.= (ff.m2)(*)(ff.m1) by A14,A19;
end;
now
let m be Morphism of Functors(A,B);
reconsider m9 = m as Element of NatTrans(A,B) by NATTRA_1:def 17;
consider F,F1,t such that
A21: F is_naturally_transformable_to F1 and
A22: dom m = F and
A23: cod m = F1 and
A24: m = [[F,F1],t] by Th6;
A25: Hom(F.a,F1.a) <> {} by A21,ISOCAT_1:25;
A26: [[F,F],id F] is Morphism of Functors(A,B) by A6,NATTRA_1:def 16;
thus f.(id dom m)
= f.[[F,F],id F] by A22,NATTRA_1:def 17
.= (id F).a by A5,A6,A26
.= id(F.a) by NATTRA_1:20
.= id dom(t.a) by A25,CAT_1:5
.= id dom(f.m9) by A5,A24
.= id dom(ff.m);
A27: [[F1,F1],id F1] is Morphism of Functors(A,B) by A6,NATTRA_1:def 16;
thus
f.(id cod m)
= f.[[F1,F1],id F1] by A23,NATTRA_1:def 17
.= (id F1).a by A5,A6,A27
.= id(F1.a) by NATTRA_1:20
.= id cod(t.a) by A25,CAT_1:5
.= id cod(f.m9) by A5,A24
.= id cod(ff.m);
end;
then reconsider f as Functor of Functors(A,B),B by A7,A9,CAT_1:def 21;
take f;
let F1,F2 be Functor of A,B, t be natural_transformation of F1,F2;
assume F1 is_naturally_transformable_to F2;
then [[F1,F2],t] is Morphism of Functors(A,B) by A1,NATTRA_1:32;
hence thesis by A5,A1;
end;
uniqueness
proof
let f1,f2 be Functor of Functors(A,B), B such that
A28: for F1,F2 being Functor of A,B, t be natural_transformation of F1
,F2 st F1 is_naturally_transformable_to F2 holds f1.[[F1,F2],t] = t.a and
A29: for F1,F2 being Functor of A,B, t be natural_transformation of F1
,F2 st F1 is_naturally_transformable_to F2 holds f2.[[F1,F2],t] = t.a;
now
let c be Morphism of Functors(A,B);
the carrier' of Functors(A,B) = NatTrans(A,B) by NATTRA_1:def 17;
then consider
F1,F2 being Functor of A,B, t being natural_transformation of
F1,F2 such that
A30: c = [[F1,F2],t] & F1 is_naturally_transformable_to F2 by NATTRA_1:def 15;
thus f1.c = t.a by A28,A30
.= f2.c by A29,A30;
end;
hence f1 = f2 by FUNCT_2:63;
end;
end;
theorem
Functors(1Cat(o,m),A) ~= A
proof
reconsider a = o as Object of 1Cat(o,m) by TARSKI:def 1;
take F = a |-> A;
now
let x,y be object;
A1: the carrier' of Functors(1Cat(o,m),A) = NatTrans(1Cat(o,m),A) by
NATTRA_1:def 17;
assume x in the carrier' of Functors(1Cat(o,m),A);
then consider F1,F2 being Functor of 1Cat(o,m),A, t being
natural_transformation of F1,F2 such that
A2: x = [[F1,F2],t] and
A3: F1 is_naturally_transformable_to F2 by A1,NATTRA_1:def 16;
assume y in the carrier' of Functors(1Cat(o,m),A);
then consider F19,F29 being Functor of 1Cat(o,m),A, t9 being
natural_transformation of F19,F29 such that
A4: y = [[F19,F29],t9] and
A5: F19 is_naturally_transformable_to F29 by A1,NATTRA_1:def 16;
assume F.x = F.y;
then
A6: t.a = F.y by A2,A3,Def1
.= t9.a by A4,A5,Def1;
reconsider G1=F1, G19=F19, G2=F2, G29=F29 as Function of {m}, the carrier'
of A;
reconsider s=t,s9=t9 as Function of {a}, the carrier' of A;
A7: id a = m by TARSKI:def 1;
A8: F1 is_transformable_to F2 by A3;
then
A9: Hom(F1.a,F2.a) <> {};
A10: F19 is_transformable_to F29 by A5;
then
A11: Hom(F19.a,F29.a) <> {};
then F1.a = F19.a by A6,A9,CAT_1:6;
then G1.id a = id(F19.a) by CAT_1:71
.= G19.id a by CAT_1:71;
then
A12: F1 = F19 by A7,FUNCT_2:125;
F2.a = F29.a by A6,A9,A11,CAT_1:6;
then G2.id a = id(F29.a) by CAT_1:71
.= G29.id a by CAT_1:71;
then
A13: F2 = F29 by A7,FUNCT_2:125;
s.a = t9.a by A8,A6,NATTRA_1:def 5
.= s9.a by A10,NATTRA_1:def 5;
hence x = y by A2,A4,A12,A13,FUNCT_2:125;
end;
hence F is one-to-one by FUNCT_2:19;
thus rng F c= the carrier' of A;
let x be object;
assume x in the carrier' of A;
then reconsider f = x as Morphism of A;
reconsider F1 = {m} --> id dom f, F2 = {m} --> id cod f as Function of the
carrier' of 1Cat(o,m),the carrier' of A;
A14: now
let g be Morphism of 1Cat(o,m);
thus F1.(id dom g) = id dom f by FUNCOP_1:7
.= id dom id dom f
.= id dom (F1.g) by FUNCOP_1:7;
thus F1.(id cod g) = id dom f by FUNCOP_1:7
.= id cod id dom f
.= id cod (F1.g) by FUNCOP_1:7;
end;
A15: now
let h,g be Morphism of 1Cat(o,m) such that
dom g = cod h;
A16: Hom(dom f,dom f) <> {};
thus F1.(g(*)h) = id dom f by FUNCOP_1:7
.= (id dom f)*(id dom f)
.= (id dom f)(*)(id dom f qua Morphism of A)by A16,CAT_1:def 13
.= (id dom f)(*)(F1.h)by FUNCOP_1:7
.= (F1.g)(*)(F1.h)by FUNCOP_1:7;
end;
A17: now
let h,g be Morphism of 1Cat(o,m) such that
dom g = cod h;
A18: Hom(cod f,cod f) <> {};
thus F2.(g(*)h) = id cod f by FUNCOP_1:7
.= (id cod f)*(id cod f)
.= (id cod f)(*)(id cod f qua Morphism of A)by A18,CAT_1:def 13
.= (id cod f)(*)(F2.h)by FUNCOP_1:7
.= (F2.g)(*)(F2.h)by FUNCOP_1:7;
end;
A19: now
let g be Morphism of 1Cat(o,m);
thus F2.(id dom g) = id cod f by FUNCOP_1:7
.= id dom id cod f
.= id dom (F2.g) by FUNCOP_1:7;
thus F2.(id cod g) = id cod f by FUNCOP_1:7
.= id cod id cod f
.= id cod (F2.g) by FUNCOP_1:7;
end;
( for c being Object of 1Cat(o,m) ex d being Object of A st F1.(id c) =
id d)& for c being Object of 1Cat(o,m) ex d being Object of A st F2.(id c) = id
d by FUNCOP_1:7;
then reconsider F1, F2 as Functor of 1Cat(o,m),A by A14,A15,A19,A17,CAT_1:61;
reconsider t = {a} --> f as Function of the carrier of 1Cat(o,m), the
carrier' of A;
A20: for b being Object of 1Cat(o,m) holds F1.b = dom f & F2.b = cod f
proof
let b be Object of 1Cat(o,m);
F2.(id b qua Morphism of 1Cat(o,m)) = id cod f by FUNCOP_1:7;
then
A21: id(F2.b) = id cod f by CAT_1:71;
F1.(id b qua Morphism of 1Cat(o,m)) = id dom f by FUNCOP_1:7;
then id(F1.b) = id dom f by CAT_1:71;
hence thesis by A21,CAT_1:59;
end;
A22: now
let b be Object of 1Cat(o,m);
A23: F2.b = cod f by A20;
t.b = f & F1.b = dom f by A20,FUNCOP_1:7;
then t.b in Hom(F1.b,F2.b) by A23;
hence t.b is Morphism of F1.b,F2.b by CAT_1:def 5;
end;
A24: now
let b be Object of 1Cat(o,m);
F1.b = dom f & F2.b = cod f by A20;
hence Hom(F1.b,F2.b) <> {} by CAT_1:2;
end;
then
A25: F1 is_transformable_to F2;
then reconsider t as transformation of F1,F2 by A22,NATTRA_1:def 3;
A26: for b being Object of 1Cat(o,m) holds t.b = f
proof
let b be Object of 1Cat(o,m);
thus f = ({a} --> f).b by FUNCOP_1:7
.= t.b by A25,NATTRA_1:def 5;
end;
A27: now
let b1,b2 be Object of 1Cat(o,m) such that
A28: Hom(b1,b2) <> {};
A29: Hom(F2.b1,F2.b2) <> {} by A28,CAT_1:82;
let g be Morphism of b1,b2;
A30: t.b1 = f & Hom(F1.b1,F2.b1) <> {} by A24,A26;
A31: Hom(F1.b1,F1.b2) <> {} by A28,CAT_1:82;
A32: m in {m} by TARSKI:def 1;
A33: g = m by TARSKI:def 1;
then
A34: F2/.g = F2.m by A28,CAT_3:def 10
.= id cod f by A32,FUNCOP_1:7;
A35: F1/.g = F1.m by A28,A33,CAT_3:def 10
.= id dom f by A32,FUNCOP_1:7;
t.b2 = f & Hom(F1.b2,F2.b2) <> {} by A24,A26;
hence t.b2*F1/.g = f(*)(F1/.g) by A31,CAT_1:def 13
.= f by A35,CAT_1:22
.= (F2/.g)(*)f by A34,CAT_1:21
.= F2/.g*t.b1 by A30,A29,CAT_1:def 13;
end;
F1 is_transformable_to F2 by A24;
then
A36: F1 is_naturally_transformable_to F2 by A27;
then reconsider t as natural_transformation of F1,F2 by A27,NATTRA_1:def 8;
[[F1,F2],t] in NatTrans(1Cat(o,m),A) by A36,NATTRA_1:def 16;
then
A37: [[F1,F2],t] in the carrier' of Functors(1Cat(o,m),A) by NATTRA_1:def 17;
F.[[F1,F2],t] = t.a by A36,Def1
.= f by A26;
hence thesis by A37,FUNCT_2:4;
end;
begin :: The isomorphism between C^(A x B) and C^(A^B)
theorem Th8:
for F being Functor of [:A,B:],C, a being Object of A, b being
Object of B holds (F?-a).b = F.[a,b]
proof
let F be Functor of [:A,B:],C, a be Object of A, b be Object of B;
thus (F?-a).b = (Obj F).(a,b) by CAT_2:37
.= F.[a,b];
end;
theorem Th9:
for a1,a2 being Object of A, b1,b2 being Object of B holds Hom(
a1,a2) <> {} & Hom(b1,b2) <> {} iff Hom([a1,b1],[a2,b2]) <> {}
proof
let a1,a2 be Object of A, b1,b2 be Object of B;
Hom([a1,b1],[a2,b2]) = [:Hom(a1,a2),Hom(b1,b2):] by CAT_2:32;
hence thesis by ZFMISC_1:90;
end;
theorem Th10:
for a1,a2 being Object of A, b1,b2 being Object of B st Hom([a1,
b1],[a2,b2]) <> {} for f being (Morphism of A), g being Morphism of B holds [f,
g] is Morphism of [a1,b1],[a2,b2] iff f is Morphism of a1,a2 & g is Morphism of
b1,b2
proof
let a1,a2 be Object of A, b1,b2 be Object of B;
assume
A1: Hom([a1,b1],[a2,b2]) <> {};
let f be Morphism of A;
let g be Morphism of B;
thus [f,g] is Morphism of [a1,b1],[a2,b2] implies f is Morphism of a1,a2 & g
is Morphism of b1,b2
proof
assume [f,g] is Morphism of [a1,b1],[a2,b2];
then
A2: [f,g] in Hom([a1,b1],[a2,b2]) by A1,CAT_1:def 5;
Hom([a1,b1],[a2,b2]) = [:Hom(a1,a2),Hom(b1,b2):] by CAT_2:32;
then f in Hom(a1,a2) & g in Hom(b1,b2) by A2,ZFMISC_1:87;
hence thesis by CAT_1:def 5;
end;
Hom(a1,a2) <> {} & Hom(b1,b2) <> {} by A1,Th9;
hence thesis by CAT_2:33;
end;
theorem Th11:
for F1,F2 being Functor of [:A,B:],C st F1
is_naturally_transformable_to F2 for t being natural_transformation of F1,F2, a
being Object of A holds F1?-a is_naturally_transformable_to F2?-a & (curry t).a
is natural_transformation of F1?-a,F2?-a
proof
let F1,F2 be Functor of [:A,B:],C;
assume
A1: F1 is_naturally_transformable_to F2;
then
A2: F1 is_transformable_to F2;
let u be natural_transformation of F1,F2, a be Object of A;
reconsider
t=u as Function of [:the carrier of A, the carrier of B:], the
carrier' of C;
A3: F1?-a is_transformable_to F2?-a
proof
let b be Object of B;
(F1?-a).b = F1.[a,b] & (F2?-a).b = F2.[a,b] by Th8;
hence thesis by A2;
end;
A4: now
let b be Object of B;
A5: (F1?-a).b = F1.[a,b] & (F2?-a).b = F2.[a,b] by Th8;
A6: Hom((F1?-a).b,(F2?-a).b) <> {} by A3;
(curry t).a.b = t.(a,b) by FUNCT_5:69
.= u.[a,b] by A2,NATTRA_1:def 5;
hence (curry t).a.b in Hom((F1?-a).b,(F2?-a).b) by A5,A6,CAT_1:def 5;
end;
now
let b be Object of B;
(curry t).a.b in Hom((F1?-a).b,(F2?-a).b) by A4;
hence (curry t).a.b is Morphism of (F1?-a).b,(F2?-a).b by CAT_1:def 5;
end;
then reconsider s = (curry t).a as transformation of F1?-a,F2?-a by A3,
NATTRA_1:def 3;
A7: now
let b1,b2 be Object of B such that
A8: Hom(b1,b2) <> {};
A9: Hom((F1?-a).b1,(F1?-a).b2) <> {} by A8,CAT_1:84;
let f be Morphism of b1,b2;
A10: Hom(a,a) <> {};
then reconsider g = [id a,f] as Morphism of [a,b1],[a,b2] by A8,CAT_2:33;
A11: Hom([a,b1],[a,b2]) <> {} by A8,A10,Th9;
then
A12: Hom(F1.[a,b1],F1.[a,b2]) <> {} by CAT_1:84;
A13: s.b1 = (curry t).a.b1 by A3,NATTRA_1:def 5
.= t.(a,b1) by FUNCT_5:69
.= u.[a,b1] by A2,NATTRA_1:def 5;
A14: Hom(F1.[a,b2],F2.[a,b2]) <> {} by A2;
A15: Hom((F2?-a).b1,(F2?-a).b2) <> {} by A8,CAT_1:84;
A16: (F1?-a).b1 = F1.[a,b1] & (F2?-a).b1 = F2.[a,b1] by Th8;
A17: (F1?-a).b2 = F1.[a,b2] & (F2?-a).b2 = F2.[a,b2] by Th8;
A18: Hom(F1.[a,b1],F2.[a,b1]) <> {} by A2;
A19: Hom(F2.[a,b1],F2.[a,b2]) <> {} by A11,CAT_1:84;
s.b2 = (curry t).a.b2 by A3,NATTRA_1:def 5
.= t.(a,b2) by FUNCT_5:69
.= u.[a,b2] by A2,NATTRA_1:def 5;
hence s.b2*(F1?-a)/.f
= (u.[a,b2])(*)((F1?-a)/.f) by A14,A9,A17,CAT_1:def 13
.= (u.[a,b2])(*)((F1?-a).(f qua Morphism of B)) by A8,CAT_3:def 10
.= (u.[a,b2])(*)(F1.(id a,f)) by CAT_2:36
.= (u.[a,b2])(*)(F1/.g qua Morphism of C) by A11,CAT_3:def 10
.= u.[a,b2]*F1/.g by A12,A14,CAT_1:def 13
.= F2/.g*u.[a,b1] by A1,A11,NATTRA_1:def 8
.= (F2/.g qua Morphism of C)(*)(u.[a,b1]) by A18,A19,CAT_1:def 13
.= F2.(id a,f)(*)(u.[a,b1]) by A11,CAT_3:def 10
.= ((F2?-a).(f qua Morphism of B))(*)(u.[a,b1]) by CAT_2:36
.= ((F2?-a)/.f qua Morphism of C)(*)(s.b1) by A8,A13,CAT_3:def 10
.= (F2?-a)/.f*s.b1 by A18,A15,A16,CAT_1:def 13;
end;
hence F1?-a is_naturally_transformable_to F2?-a by A3;
hence thesis by A7,NATTRA_1:def 8;
end;
definition
let A,B,C;
let F be Functor of [:A,B:],C;
let f be Morphism of A;
func curry(F,f) -> Function of the carrier' of B,the carrier' of C equals
(
curry F).f;
coherence
proof
reconsider
F as Function of [:the carrier' of A,the carrier' of B:], the
carrier' of C;
(curry F).f is Function of the carrier' of B,the carrier' of C;
hence thesis;
end;
end;
theorem Th12:
for a1,a2 being Object of A, b1,b2 being Object of B, f being (
Morphism of A), g being Morphism of B st f in Hom(a1,a2) & g in Hom(b1,b2)
holds [f,g] in Hom([a1,b1],[a2,b2])
proof
let a1,a2 be Object of A, b1,b2 be Object of B, f be (Morphism of A), g be
Morphism of B;
assume f in Hom(a1,a2) & g in Hom(b1,b2);
then [f,g] in [:Hom(a1,a2),Hom(b1,b2):] by ZFMISC_1:87;
hence thesis by CAT_2:32;
end;
theorem Th13:
for F being Functor of [:A,B:], C for a,b being Object of A st
Hom(a,b) <> {} for f being Morphism of a,b holds F?-a
is_naturally_transformable_to F?-b & curry(F,f)*IdMap B is
natural_transformation of F?-a,F?-b
proof
let F be Functor of [:A,B:], C;
let a1,a2 be Object of A such that
A1: Hom(a1,a2) <> {};
reconsider
G = F as Function of [:the carrier' of A,the carrier' of B:], the
carrier' of C;
let f be Morphism of a1,a2;
reconsider Ff = (curry G).(f qua Morphism of A) as Function of the carrier'
of B,the carrier' of C;
A2: now
let b be Object of B;
f in Hom(a1,a2) & id b in Hom(b,b) by A1,CAT_1:def 5;
then [f,id b] in Hom([a1,b],[a2,b]) by Th12;
then
A3: F.(f,id b) in Hom(F.[a1,b],F.[a2,b]) by CAT_1:81;
A4: id b = (IdMap B).b by ISOCAT_1:def 12;
(F?-a1).b = F.[a1,b] & (F?-a2).b = F.[a2,b] by Th8;
then Ff.(id b qua Morphism of B) in Hom((F?-a1).b,(F?-a2).b)
by A3,FUNCT_5:69;
hence (curry(F,f)*IdMap B).b in Hom((F?-a1).b,(F?-a2).b)
by A4,FUNCT_2:15;
end;
A5: F?-a1 is_transformable_to F?-a2
by A2;
reconsider FfI = curry(F,f)*IdMap B as Function of the carrier of B, the
carrier' of C;
now
let b be Object of B;
(curry(F,f)*IdMap B).b in Hom((F?-a1).b,(F?-a2).b) by A2;
hence FfI.b is Morphism of (F?-a1).b,(F?-a2).b by CAT_1:def 5;
end;
then reconsider
t = curry(F,f)*IdMap B as transformation of F?-a1,F?-a2 by A5,NATTRA_1:def 3;
A6: now
reconsider ida1 = id a1, ida2 = id a2 as Morphism of A;
A7: Hom(a1,a1) <> {};
A8: Hom(a2,a2) <> {};
let b1,b2 be Object of B such that
A9: Hom(b1,b2) <> {};
A10: Hom((F?-a2).b1,(F?-a2).b2) <> {} by A9,CAT_1:84;
let g be Morphism of b1,b2;
reconsider idb1 = id b1, idb2 = id b2 as Morphism of B;
A11: Hom(b1,b1) <> {};
A12: dom id b2 = b2
.= cod g by A9,CAT_1:5;
Hom(b2,b2) <> {};
then
A13: [f(*)ida1,idb2(*)g] = [f(*)ida1,(id b2)*g] by A9,CAT_1:def 13
.= [f(*)ida1,g] by A9,CAT_1:28
.= [f*id a1,g] by A1,A7,CAT_1:def 13
.= [f,g] by A1,CAT_1:29
.= [id a2*f,g] by A1,CAT_1:28
.= [ida2(*)f,g] by A1,A8,CAT_1:def 13
.= [ida2(*)f,g*id b1] by A9,CAT_1:29
.= [ida2(*)f,g(*)idb1] by A9,A11,CAT_1:def 13;
A14: Hom((F?-a1).b2,(F?-a2).b2) <> {} & t.b2 = FfI.b2 by A5,NATTRA_1:def 5;
A15: cod id a1 = a1
.= dom f by A1,CAT_1:5;
then
A16: cod[id a1,g] = [dom f,cod g] by CAT_2:28
.= dom[f,id b2] by A12,CAT_2:28;
A17: Hom((F?-a1).b1,(F?-a2).b1) <> {} & t.b1 = FfI.b1 by A5,NATTRA_1:def 5;
A18: dom g = b1 by A9,CAT_1:5
.= cod id b1;
A19: dom id a2 = a2
.= cod f by A1,CAT_1:5;
then
A20: dom[id a2,g] = [cod f,dom g] by CAT_2:28
.= cod[f,id b1] by A18,CAT_2:28;
A21: id b2 = (IdMap B).b2 by ISOCAT_1:def 12;
A22: id b1 = (IdMap B).b1 by ISOCAT_1:def 12;
Hom((F?-a1).b1,(F?-a1).b2) <> {} by A9,CAT_1:84;
hence t.b2*(F?-a1)/.g = (FfI.b2)(*)((F?-a1)/.g) by A14,CAT_1:def 13
.= (Ff.(id b2 qua Morphism of B))(*)((F?-a1)/.g) by A21,FUNCT_2:15
.= (F.(f,id b2))(*)((F?-a1)/.g) by FUNCT_5:69
.= (F.[f,id b2])(*)((F?-a1).(g qua Morphism of B)) by A9,CAT_3:def 10
.= (F.(f,id b2))(*)(F.(id a1,g)) by CAT_2:36
.= F.([f,id b2](*)[id a1,g]) by A16,CAT_1:64
.= F.[f(*)ida1,idb2(*)g] by A15,A12,CAT_2:29
.= F.([ida2,g](*)[f,idb1]) by A19,A18,A13,CAT_2:29
.= F.(id a2,g)(*)(F.[f,id b1]) by A20,CAT_1:64
.= ((F?-a2).(g qua Morphism of B))(*)(F.[f,id b1]) by CAT_2:36
.= ((F?-a2)/.g)(*)(F.(f,id b1)) by A9,CAT_3:def 10
.= ((F?-a2)/.g)(*)(Ff.(id b1 qua Morphism of B)) by FUNCT_5:69
.= ((F?-a2)/.g)(*)(FfI.b1) by A22,FUNCT_2:15
.= (F?-a2)/.g*t.b1 by A10,A17,CAT_1:def 13;
end;
hence F?-a1 is_naturally_transformable_to F?-a2 by A5;
hence thesis by A6,NATTRA_1:def 8;
end;
definition
let A,B,C;
let F be Functor of [:A,B:],C;
let f be Morphism of A;
func F?-f -> natural_transformation of F?-dom f, F?-cod f equals
curry(F,f)*
IdMap B;
coherence
proof
Hom(dom f, cod f) <> {} & f is Morphism of dom f, cod f by CAT_1:2,4;
hence thesis by Th13;
end;
correctness;
end;
theorem Th14:
for F being Functor of [:A,B:],C, g being Morphism of A holds F
?-dom(g) is_naturally_transformable_to F?-cod(g)
proof
let F be Functor of [:A,B:],C, g be Morphism of A;
Hom(dom g,cod g) <> {} by CAT_1:2;
hence thesis by Th13;
end;
theorem Th15:
for F being Functor of [:A,B:],C, f being (Morphism of A), b
being Object of B holds (F?-f).b = F.(f, id b)
proof
let F be Functor of [:A,B:],C, f be (Morphism of A), b be Object of B;
reconsider
G = F as Function of [:the carrier' of A,the carrier' of B:], the
carrier' of C;
reconsider Ff = (curry G).f as Function of the carrier' of B,the carrier' of
C;
A1: id b = (IdMap B).b by ISOCAT_1:def 12;
F?-dom f is_naturally_transformable_to F?-cod f by Th14;
then F?-dom f is_transformable_to F?-cod f;
hence (F?-f).b = (curry(F,f)*IdMap B).b by NATTRA_1:def 5
.= Ff.(id b qua Morphism of B) by A1,FUNCT_2:15
.= F.(f,id b) by FUNCT_5:69;
end;
theorem Th16:
for F being Functor of [:A,B:],C, a being Object of A holds id(F
?-a) = F?-id a
proof
let F be Functor of [:A,B:],C, a be Object of A;
reconsider
G = F as Function of [:the carrier' of A,the carrier' of B:], the
carrier' of C;
reconsider Ff = (curry G).(id a qua Morphism of A) as Function of the
carrier' of B,the carrier' of C;
reconsider I = F?-id a as transformation of F?-a,F?-a;
now
let b be Object of B;
A1: id b = (IdMap B).b by ISOCAT_1:def 12;
thus (I qua Function of the carrier of B, the carrier' of C).b = Ff.(id b
qua Morphism of B) by A1,FUNCT_2:15
.= F.(id a,id b) by FUNCT_5:69
.= F.(id [a,b] qua Morphism of [:A,B:]) by CAT_2:31
.= id(F.[a,b]) by CAT_1:71
.= id ((F?-a).b) by Th8;
end;
hence thesis by NATTRA_1:def 4;
end;
theorem Th17:
for F being Functor of [:A,B:],C, g,f being Morphism of A st dom
g = cod f for t being natural_transformation of F?-dom f, F?-dom g st t = F?-f
holds F?-(g(*)f) = (F?-g)`*`t
proof
let F be Functor of [:A,B:],C, g,f be Morphism of A such that
A1: dom g = cod f;
A2: F?-dom f is_naturally_transformable_to F?-dom g by A1,Th14;
then
A3: F?-dom f is_transformable_to F?-dom g;
reconsider
G = F as Function of [:the carrier' of A,the carrier' of B:], the
carrier' of C;
reconsider Fgf = (curry G).(g(*)f), Ff = (curry G).f, Fg = (curry G).g as
Function of the carrier' of B,the carrier' of C;
let t be natural_transformation of F?-dom f, F?-dom g such that
A4: t = F?-f;
reconsider s = t as transformation of F?-dom f, F?-dom g;
A5: F?-dom g is_naturally_transformable_to F?-cod g by Th14;
then
A6: F?-dom g is_transformable_to F?-cod g;
F?-dom(g(*)f) is_naturally_transformable_to F?-cod(g(*)f) by Th14;
then
A7: F?-dom(g(*)f) is_transformable_to F?-cod(g(*)f);
A8: now
let b be Object of B;
A9: Hom(b,b) <> {};
A10: id b = (IdMap B).b by ISOCAT_1:def 12;
A11: (F?-g).b = (curry(F,g)*IdMap B).b by A6,NATTRA_1:def 5
.= Fg.(id b qua Morphism of B) by A10,FUNCT_2:15
.= F.(g,id b) by FUNCT_5:69;
dom id b = b
.= cod id b;
then
A12: dom[g, id b] = [cod f, cod id b] by A1,CAT_2:28
.= cod[f, id b] by CAT_2:28;
A13: Hom((F?-dom g).b,(F?-cod g).b) <> {} & Hom((F?-dom f).b,(F?-dom g).b)
<> {} by A3,A6;
A14: (F?-f).b = (curry(F,f)*IdMap B).b by A1,A3,NATTRA_1:def 5
.= Ff.(id b qua Morphism of B) by A10,FUNCT_2:15
.= F.(f,id b) by FUNCT_5:69;
thus F?-(g(*)f).b = (curry(F,g(*)f)*IdMap B).b by A7,NATTRA_1:def 5
.= Fgf.(id b qua Morphism of B) by A10,FUNCT_2:15
.= F.(g(*)f,id b) by FUNCT_5:69
.= F.[g(*)f,id b*id b]
.= F.[g(*)f,id b(*)(id b qua Morphism of B)] by A9,CAT_1:def 13
.= F.([g, id b](*)[f,id b]) by A12,CAT_2:30
.= ((F?-g).b)(*)(s.b qua Morphism of C) by A1,A4,A11,A14,A12,CAT_1:64
.= (F?-g).b*s.b by A13,CAT_1:def 13
.= ((F?-g)`*`s).b by A3,A6,NATTRA_1:def 6;
end;
cod(g(*)f) = cod g & dom(g(*)f) = dom f by A1,CAT_1:17;
then F?-(g(*)f) = (F?-g)`*`s by A3,A6,A8,NATTRA_1:18,19;
hence thesis by A2,A5,NATTRA_1:def 9;
end;
definition
let A,B,C;
let F be Functor of [:A,B:],C;
func export F -> Functor of A, Functors(B,C) means
:Def4:
for f being Morphism of A holds it.f =[[F?-dom f,F?-cod f],F?-f];
existence
proof
defpred P[object,object] means
for f being Morphism of A st $1 = f holds $2 = [[
F?-dom f,F?-cod f],F?-f];
A1: now
let m be object;
assume m in the carrier' of A;
then reconsider g = m as Morphism of A;
reconsider o = [[F?-dom(g),F?-cod(g)],F?-g] as object;
take o;
F?-dom(g) is_naturally_transformable_to F?-cod(g) by Th14;
then o in NatTrans(B,C) by NATTRA_1:32;
hence o in the carrier' of Functors(B,C) by NATTRA_1:def 17;
thus P[m,o];
end;
consider G being Function of the carrier' of A, the carrier' of Functors(B
,C) such that
A2: for m being object st m in the carrier' of A holds P[m,G.m]
from FUNCT_2:sch 1(A1);
G is Functor of A, Functors(B,C)
proof
thus for c being Object of A ex d being Object of Functors(B,C) st G.id
c = id d
proof
let c be Object of A;
reconsider d = F?-c as Object of Functors(B,C) by Th5;
take d;
thus G.id c = [[F?-c,F?-c],F?-id c] by A2
.= [[F?-c,F?-c],id(F?-c)] by Th16
.= id d by NATTRA_1:def 17;
end;
thus for f being Morphism of A holds G.id dom f = id dom(G.f) & G.id cod
f = id cod(G.f)
proof
let f be Element of the carrier' of A;
reconsider d = F?-dom f, c = F?-cod f as Object of Functors(B,C) by Th5
;
A3: G.f = [[F?-dom f,F?-cod f],F?-f] by A2;
thus G.id dom f = [[F?-dom f,F?-dom f],F?-id dom f] by A2
.= [[F?-dom f,F?-dom f],id(F?-dom f)] by Th16
.= id d by NATTRA_1:def 17
.= id dom(G.f) by A3,NATTRA_1:33;
thus G.id cod f = [[F?-cod f,F?-cod f],F?-id cod f] by A2
.= [[F?-cod f,F?-cod f],id(F?-cod f)] by Th16
.= id c by NATTRA_1:def 17
.= id cod(G.f) by A3,NATTRA_1:33;
end;
let f,g be Morphism of A;
assume
A4: dom g = cod f;
then reconsider t = F?-f as natural_transformation of F?-dom f,F?-dom g;
A5: cod(g(*)f) = cod g & dom(g(*)f) = dom f by A4,CAT_1:17;
A6: F?-dom g is_naturally_transformable_to F?-cod g by Th14;
the carrier' of Functors(B,C) = NatTrans(B,C) & F?-dom f
is_naturally_transformable_to F?-cod f by Th14,NATTRA_1:def 17;
then reconsider
gg = [[F?-dom g,F?-cod g],F?-g], ff = [[F?-dom f,F?-cod f],F
?-f] as Morphism of Functors(B,C) by A6,NATTRA_1:32;
A7: G.f = ff by A2;
thus G.(g(*)f) = [[F?-dom(g(*)f),F?-cod(g(*)f)],F?-(g(*)f)] by A2
.= [[F?-dom(g(*)f),F?-cod(g(*)f)],(F?-g)`*`t] by A4,Th17
.= gg(*)ff by A4,A5,NATTRA_1:36
.= (G.g)(*)(G.f) by A2,A7;
end;
then reconsider G as Functor of A, Functors(B,C);
take G;
thus thesis by A2;
end;
uniqueness
proof
let G1,G2 be Functor of A, Functors(B,C) such that
A8: for f being Morphism of A holds G1.f =[[F?-dom f,F?-cod f],F?-f] and
A9: for f being Morphism of A holds G2.f =[[F?-dom f,F?-cod f],F?-f];
now
let f be Morphism of A;
thus G1.f =[[F?-dom f,F?-cod f],F?-f] by A8
.= G2.f by A9;
end;
hence thesis by FUNCT_2:63;
end;
end;
Lm1: for F1,F2 being Functor of A,B st F1 is_transformable_to F2 for t being
transformation of F1,F2, a being Object of A holds t.a in Hom(F1.a,F2.a)
proof
let F1,F2 be Functor of A,B such that
A1: F1 is_transformable_to F2;
let t be transformation of F1,F2, a be Object of A;
Hom(F1.a,F2.a)<>{} by A1;
hence thesis by CAT_1:def 5;
end;
theorem Th18:
for F being Functor of [:A,B:],C, a being Object of A holds (
export F).a = F?-a
proof
let F be Functor of [:A,B:],C, a be Object of A;
reconsider o = F?-a as Object of Functors(B,C) by Th5;
reconsider i = id a as Morphism of A;
(export F).i = [[F?-a,F?-a],F?-id a] by Def4
.= [[F?-a,F?-a],id(F?-a)] by Th16
.= id o by NATTRA_1:def 17;
hence thesis by CAT_1:67;
end;
theorem Th19:
for F being Functor of [:A,B:],C, a being Object of A holds (
export F).a is Functor of B,C
proof
let F be Functor of [:A,B:],C, a be Object of A;
(export F).a = (F?-a) by Th18;
hence thesis;
end;
theorem Th20:
for F1,F2 being Functor of [:A,B:],C holds export F1 = export F2
implies F1 = F2
proof
let F1,F2 be Functor of [:A,B:],C such that
A1: export F1 = export F2;
now
let fg be Morphism of [:A,B:];
consider f being (Morphism of A), g being Morphism of B such that
A2: fg = [f,g] by CAT_2:27;
A3: dom id cod f = cod f & dom g = cod id dom g;
A4: fg = [(id cod f)(*)f,g] by A2,Th3
.= [(id cod f)(*)f,g(*)(id dom g)] by Th4
.= [id cod f,g](*)[f, id dom g] by A3,CAT_2:29;
A5: [[F1?-dom f,F1?-cod f],F1?-f] = (export F2).f by A1,Def4
.= [[F2?-dom f,F2?-cod f],F2?-f] by Def4;
then
A6: [F1?-dom f,F1?-cod f] = [F2?-dom f,F2?-cod f] by XTUPLE_0:1;
then
A7: F1?-dom f = F2?-dom f by XTUPLE_0:1;
A8: F1?-cod f = F2?-cod f by A6,XTUPLE_0:1;
then
A9: F1.(id cod f, g) = (F2?-cod f).g by CAT_2:36
.= F2.(id cod f, g) by CAT_2:36;
A10: cod[f,id dom g] = [cod f, cod id dom g] by CAT_2:28
.= [cod f, dom g]
.= [dom id cod f, dom g]
.= dom[id cod f,g] by CAT_2:28;
F1.(f, id dom g) = (F1?-f).dom g by Th15
.= (F2?-f).dom g by A5,A7,A8,XTUPLE_0:1
.= F2.(f,id dom g) by Th15;
hence F1.fg = (F2.[id cod f,g])(*)(F2.[f, id dom g]) by A4,A9,A10,CAT_1:64
.= F2.fg by A4,A10,CAT_1:64;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th21:
for F1,F2 being Functor of [:A,B:], C st F1
is_naturally_transformable_to F2 for t being natural_transformation of F1,F2
holds export F1 is_naturally_transformable_to export F2 & ex G being
natural_transformation of export F1, export F2 st for s being Function of [:the
carrier of A, the carrier of B:], the carrier' of C st t = s for a being Object
of A holds G.a = [[(export F1).a,(export F2).a],(curry s).a]
proof
let F1,F2 be Functor of [:A,B:], C;
assume
A1: F1 is_naturally_transformable_to F2;
then
A2: F1 is_transformable_to F2;
let t be natural_transformation of F1,F2;
reconsider
s = t as Function of [:the carrier of A, the carrier of B:], the
carrier' of C;
A3: now
let a be Object of A;
let S1,S2 be Functor of B,C such that
A4: S1 = (export F1).a and
A5: S2 = (export F2).a;
let b be Object of B;
A6: S2.b = (F2?-a).b by A5,Th18
.= F2.[a,b] by Th8;
A7: (curry s).a.b = s.(a,b) by FUNCT_5:69
.= t.[a,b] by A2,NATTRA_1:def 5;
S1.b = (F1?-a).b by A4,Th18
.= F1.[a,b] by Th8;
hence (curry s).a.b in Hom(S1.b,S2.b) by A2,A6,A7,Lm1;
end;
A8: for a be Object of A, S1,S2 be Functor of B,C st
S1 = (export F1).a & S2 = (export F2).a holds S1 is_transformable_to S2
by A3;
A9: now
let a be Object of A;
let S1,S2 be Functor of B,C, T be transformation of S1,S2;
assume that
A10: S1 = (export F1).a and
A11: S2 = (export F2).a and
A12: T = (curry s).a;
let b1,b2 be Object of B such that
A13: Hom(b1,b2) <> {};
A14: Hom(S1.b1,S1.b2) <> {} by A13,CAT_1:84;
A15: T.b2 = (T qua Function of the carrier of B, the carrier' of C).b2 by A8
,A10,A11,NATTRA_1:def 5
.= s.(a,b2) by A12,FUNCT_5:69
.= t.[a,b2] by A2,NATTRA_1:def 5;
A16: Hom(F1.[a,b2],F2.[a,b2]) <> {} by A2;
let f be Morphism of b1,b2;
A17: Hom(a,a) <> {};
then reconsider g = [id a,f] as Morphism of [a,b1],[a,b2] by A13,CAT_2:33;
A18: Hom([a,b1],[a,b2]) <> {} by A13,A17,Th9;
then
A19: Hom(F1.[a,b1],F1.[a,b2]) <> {} by CAT_1:84;
A20: S1 is_transformable_to S2 by A8,A10,A11;
then
A21: Hom(S1.b1,S2.b1) <> {};
A22: T.b1 = (T qua Function of the carrier of B, the carrier' of C).b1 by A8
,A10,A11,NATTRA_1:def 5
.= s.(a,b1) by A12,FUNCT_5:69
.= t.[a,b1] by A2,NATTRA_1:def 5;
A23: Hom(F1.[a,b1],F2.[a,b1]) <> {} by A2;
A24: Hom(S1.b2,S2.b2) <> {} by A20;
A25: Hom(S2.b1,S2.b2) <> {} by A13,CAT_1:84;
A26: S2/.f = (F2?-a)/.f by A11,Th18
.= (F2?-a)/.(f qua Morphism of B) by A13,CAT_3:def 10
.= F2.(id a, f) by CAT_2:36
.= F2/.g by A18,CAT_3:def 10;
A27: Hom(F2.[a,b1],F2.[a,b2]) <> {} by A18,CAT_1:84;
A28: S1/.f = (F1?-a)/.f by A10,Th18
.= (F1?-a)/.(f qua Morphism of B) by A13,CAT_3:def 10
.= F1.(id a, f) by CAT_2:36
.= F1/.g by A18,CAT_3:def 10;
thus T.b2*S1/.f = (T.b2)(*)(S1/.f) by A14,A24,CAT_1:def 13
.= t.[a,b2]*F1/.g by A19,A16,A15,A28,CAT_1:def 13
.= F2/.g*t.[a,b1] by A1,A18,NATTRA_1:def 8
.= (S2/.f qua Morphism of C)(*)(T.b1) by A27,A23,A22,A26,CAT_1:def 13
.= S2/.f*T.b1 by A25,A21,CAT_1:def 13;
end;
defpred P[object,object] means
for f being Object of A, s being Function of [:the
carrier of A, the carrier of B:], the carrier' of C st t = s & $1 = f holds $2
= [[(export F1).f,(export F2).f],(curry s).f];
A29: now
let a be Object of A;
let S1,S2 be Functor of B,C such that
A30: S1 = (export F1).a & S2 = (export F2).a;
thus (curry s).a is transformation of S1,S2
proof
thus S1 is_transformable_to S2 by A8,A30;
let b be Object of B;
(curry s).a.b in Hom(S1.b,S2.b) by A3,A30;
hence thesis by CAT_1:def 5;
end;
end;
A31: now
let m be object;
assume m in the carrier of A;
then reconsider a = m as Object of A;
reconsider S1 = (export F1).a, S2 = (export F2).a as Functor of B,C by Th19
;
reconsider o = [[(export F1).a,(export F2).a],(curry s).a] as object;
take o;
reconsider T = (curry s).a as transformation of S1,S2 by A29;
A32: S1 is_naturally_transformable_to S2
proof
thus S1 is_transformable_to S2 by A8;
take T;
thus thesis by A9;
end;
for a,b being Object of B st Hom(a,b) <> {} for f being Morphism of a,
b holds (T.b)*(S1/.f) = (S2/.f)*(T.a) by A9;
then T is natural_transformation of S1,S2 by A32,NATTRA_1:def 8;
then o in NatTrans(B,C) by A32,NATTRA_1:32;
hence o in the carrier' of Functors(B,C) by NATTRA_1:def 17;
thus P[m,o];
end;
consider G being Function of the carrier of A, the carrier' of Functors(B,C)
such that
A33: for m being object st m in the carrier of A holds P[m,G.m]
from FUNCT_2:sch 1(
A31);
A34: now
let a be Object of A;
reconsider S1 = (export F1).a, S2 = (export F2).a as Functor of B,C by Th19
;
reconsider T = (curry s).a as transformation of S1,S2 by A29;
A35: G.a = [[S1,S2],T] by A33;
A36: S1 is_naturally_transformable_to S2
proof
thus S1 is_transformable_to S2 by A8;
take T;
thus thesis by A9;
end;
for a,b being Object of B st Hom(a,b) <> {} for f being Morphism of a,
b holds (T.b)*(S1/.f) = (S2/.f)*(T.a) by A9;
then T is natural_transformation of S1,S2 by A36,NATTRA_1:def 8;
then dom(G.a) = S1 & cod(G.a) = S2 by A35,NATTRA_1:33;
hence G.a in Hom((export F1).a,(export F2).a);
end;
then
A37: for a be Object of A holds Hom((export F1).a,(export F2).a) <> {};
G is transformation of export F1, export F2
proof
thus export F1 is_transformable_to export F2 by A37;
let a be Object of A;
G.a in Hom((export F1).a,(export F2).a) by A34;
hence thesis by CAT_1:def 5;
end;
then reconsider G as transformation of export F1, export F2;
A38: export F1 is_transformable_to export F2 by A37;
A39: now
let a,b be Object of A such that
A40: Hom(a,b) <> {};
A41: Hom((export F2).a,(export F2).b) <> {} by A40,CAT_1:84;
reconsider S1 = (export F1).a, S2 = (export F2).a, S3 = (export F1).b, S4
= (export F2).b as Functor of B,C by Th19;
let f be Morphism of a,b;
A42: F2?-a = (export F2).a by Th18;
A43: F1?-a = (export F1).a by Th18;
then reconsider
T12 = (curry s).a as natural_transformation of S1,S2 by A1,A42,Th11;
A44: F2?-b = (export F2).b by Th18;
then
A45: F2?-cod f = (export F2).b by A40,CAT_1:5;
then reconsider T24 = F2?-f as natural_transformation of S2,S4 by A40,A42,
CAT_1:5;
A46: G.a = G.(a qua set) by A38,NATTRA_1:def 5
.= [[S1,S2],T12] by A33;
A47: F1?-b = (export F1).b by Th18;
then reconsider
T34 = (curry s).b as natural_transformation of S3,S4 by A1,A44,Th11;
A48: S3 is_naturally_transformable_to S4 by A1,A47,A44,Th11;
then
A49: S3 is_transformable_to S4;
A50: F1?-cod f = (export F1).b by A40,A47,CAT_1:5;
then reconsider T13 = F1?-f as natural_transformation of S1,S3 by A40,A43,
CAT_1:5;
A51: G.b = G.(b qua set) by A38,NATTRA_1:def 5
.= [[S3,S4],T34] by A33;
A52: S1 is_naturally_transformable_to S2 by A1,A42,A43,Th11;
then
A53: S1 is_transformable_to S2;
reconsider g = f as Morphism of A;
A54: Hom((export F1).a,(export F2).a) <> {} by A34;
F2?-dom f = (export F2).a by A40,A42,CAT_1:5;
then
A55: (export F2).g = [[S2,S4],T24] by A45,Def4;
A56: Hom((export F1).a,(export F1).b) <> {} by A40,CAT_1:84;
A57: S2 is_naturally_transformable_to S4 by A40,A42,A44,Th13;
then
A58: S2 is_transformable_to S4;
A59: S1 is_naturally_transformable_to S3 by A40,A47,A43,Th13;
then
A60: S1 is_transformable_to S3;
now
reconsider
FF1 = F1, FF2 = F2 as Function of [:the carrier' of A,the
carrier' of B:], the carrier' of C;
let c be Object of B;
A61: Hom(F1.[a,c],F2.[a,c]) <> {} by A2;
A62: Hom(F1.[b,c],F2.[b,c]) <> {} by A2;
A63: Hom(S3.c,S4.c) <> {} & Hom(S1.c,S3.c) <> {} by A60,A49;
A64: Hom(S2.c,S4.c) <> {} & Hom(S1.c,S2.c) <> {} by A53,A58;
A65: t.[b,c] = s.(b,c) by A2,NATTRA_1:def 5
.= ((curry s).b).c by FUNCT_5:69
.= T34.c by A49,NATTRA_1:def 5;
A66: t.[a,c] = s.(a,c) by A2,NATTRA_1:def 5
.= ((curry s).a).c by FUNCT_5:69
.= T12.c by A53,NATTRA_1:def 5;
A67: Hom(c,c) <> {};
then reconsider fi = [f, id c] as Morphism of [a,c], [b,c] by A40,
CAT_2:33;
A68: Hom([a,c],[b,c]) <> {} by A40,A67,Th9;
then
A69: Hom(F2.[a,c],F2.[b,c]) <> {} by CAT_1:84;
A70: id c = (IdMap B).c by ISOCAT_1:def 12;
A71: F1/.fi = FF1.(f,id c) by A68,CAT_3:def 10
.= curry(F1,f).id c by FUNCT_5:69
.= (F1?-f qua Function of the carrier of B, the carrier' of C).c by A70
,
FUNCT_2:15
.= T13.c by A60,NATTRA_1:def 5;
A72: F2/.fi = FF2.(f,id c) by A68,CAT_3:def 10
.= curry(F2,f).id c by FUNCT_5:69
.= (F2?-f qua Function of the carrier of B, the carrier' of C).c by A70
,
FUNCT_2:15
.= T24.c by A58,NATTRA_1:def 5;
A73: Hom(F1.[a,c],F1.[b,c]) <> {} by A68,CAT_1:84;
thus (T34`*`T13).c = T34.c*T13.c by A59,A48,NATTRA_1:25
.= (t.[b,c] qua Morphism of C)(*)(F1/.fi) by A63,A71,A65,CAT_1:def 13
.= t.[b,c]*F1/.fi by A62,A73,CAT_1:def 13
.= F2/.fi*t.[a,c] by A1,A68,NATTRA_1:def 8
.= (F2/.fi)(*)(t.[a,c] qua Morphism of C) by A61,A69,CAT_1:def 13
.= T24.c*T12.c by A64,A72,A66,CAT_1:def 13
.= (T24`*`T12).c by A52,A57,NATTRA_1:25;
end;
then
A74: T34`*`T13 = T24`*`T12 by A53,A58,NATTRA_1:18,19;
F1?-dom f = (export F1).a by A40,A43,CAT_1:5;
then
A75: (export F1).g = [[S1,S3],T13] by A50,Def4;
Hom((export F1).b,(export F2).b) <> {} by A34;
hence
G.b*(export F1)/.f = (G.b)(*)((export F1)/.f qua Morphism of Functors(B,C))
by A56,CAT_1:def 13
.= (G.b)(*)((export F1).g) by A40,CAT_3:def 10
.= [[S1,S4],T34`*`T13] by A75,A51,NATTRA_1:36
.= ((export F2)/.g)(*)(G.a) by A55,A46,A74,NATTRA_1:36
.= ((export F2)/.f qua Morphism of Functors(B,C))(*)(G.a) by A40,
CAT_3:def 10
.= (export F2)/.f*G.a by A54,A41,CAT_1:def 13;
end;
A76: export F1 is_transformable_to export F2 by A37;
hence export F1 is_naturally_transformable_to export F2 by A39;
export F1 is_naturally_transformable_to export F2 by A39,A76;
then reconsider G as natural_transformation of export F1, export F2 by A39,
NATTRA_1:def 8;
take G;
let s be Function of [:the carrier of A, the carrier of B:], the carrier' of
C;
assume
A77: t = s;
let a be Object of A;
thus G.a = G.(a qua set) by A38,NATTRA_1:def 5
.= [[(export F1).a,(export F2).a],(curry s).a] by A33,A77;
end;
definition
let A,B,C;
let F1,F2 be Functor of [:A,B:],C such that
A1: F1 is_naturally_transformable_to F2;
let t be natural_transformation of F1,F2;
func export t -> natural_transformation of export F1, export F2 means
:Def5:
for s being Function of [:the carrier of A, the carrier of B:], the carrier' of
C st t = s for a being Object of A holds it.a = [[(export F1).a,(export F2).a],
(curry s).a];
existence by A1,Th21;
uniqueness
proof
reconsider
s = t as Function of [:the carrier of A, the carrier of B:],
the carrier' of C;
let T1,T2 be natural_transformation of export F1, export F2 such that
A2: for s being Function of [:the carrier of A, the carrier of B:],
the carrier' of C st t = s for a being Object of A holds T1.a = [[(export F1).a
,(export F2).a],(curry s).a] and
A3: for s being Function of [:the carrier of A, the carrier of B:],
the carrier' of C st t = s for a being Object of A holds T2.a = [[(export F1).a
,(export F2).a],(curry s).a];
A4: now
let a be Object of A;
T1.a = [[(export F1).a,(export F2).a],(curry s).a] by A2;
hence T1.a = T2.a by A3;
end;
export F1 is_naturally_transformable_to export F2 by A1,Th21;
then export F1 is_transformable_to export F2;
hence T1 = T2 by A4,NATTRA_1:19;
end;
end;
theorem Th22:
for F being Functor of [:A,B:],C holds id export F = export id F
proof
let F be Functor of [:A,B:],C;
reconsider
s = id F as Function of [:the carrier of A, the carrier of B:],
the carrier' of C;
now
let a be Object of A;
reconsider ff = (export F).a as Functor of B,C by Th5;
A1: now
let b be Object of B;
thus (id ff qua Function of the carrier of B, the carrier' of C).b = (id
ff).b by NATTRA_1:def 5
.= id(ff.b) by NATTRA_1:20
.= (ff qua Function of the carrier' of B, the carrier' of C) .id b
by CAT_1:71
.= (F?-a).id b by Th18
.= F.(id a, id b) by CAT_2:36
.= F.(id[a,b] qua Morphism of [:A,B:]) by CAT_2:31
.= id(F.[a,b]) by CAT_1:71
.= (id F).[a,b] by NATTRA_1:20
.= (id F qua Function of the carrier of [:A,B:], the carrier' of C)
.(a,b) by NATTRA_1:def 5
.= (curry s).a.b by FUNCT_5:69;
end;
thus (id export F).a = id((export F).a) by NATTRA_1:20
.= [[ff,ff],id ff] by NATTRA_1:def 17
.= [[(export F).a, (export F).a],(curry s).a] by A1,FUNCT_2:63
.= (export id F).a by Def5;
end;
hence thesis by NATTRA_1:19;
end;
theorem Th23:
for F1,F2,F3 being Functor of [:A,B:],C st F1
is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 for t1
being natural_transformation of F1,F2, t2 being natural_transformation of F2,F3
holds export(t2`*`t1) = (export t2)`*`(export t1)
proof
let F1,F2,F3 be Functor of [:A,B:],C such that
A1: F1 is_naturally_transformable_to F2 and
A2: F2 is_naturally_transformable_to F3;
A3: F2 is_transformable_to F3 by A2;
let t1 be natural_transformation of F1,F2, t2 be natural_transformation of
F2,F3;
A4: F1 is_transformable_to F2 by A1;
A5: export F1 is_naturally_transformable_to export F2 by A1,Th21;
then
A6: export F1 is_transformable_to export F2;
A7: export F2 is_naturally_transformable_to export F3 by A2,Th21;
then
A8: export F2 is_transformable_to export F3;
A9: F1 is_naturally_transformable_to F3 by A1,A2,NATTRA_1:23;
then
A10: F1 is_transformable_to F3;
now
let a be Object of A;
reconsider S1 = (export F1).a, S2 = (export F2).a, S3 = (export F3).a as
Functor of B,C by Th5;
reconsider
s1 = t1, s2 = t2, s3 = t2`*`t1 as Function of [:the carrier of
A, the carrier of B:], the carrier' of C;
A11: S2 = F2?-a by Th18;
A12: S3 = F3?-a by Th18;
then reconsider
T2 = (curry s2).a as natural_transformation of S2,S3 by A2,A11,Th11;
A13: S2 is_naturally_transformable_to S3 by A2,A11,A12,Th11;
then
A14: S2 is_transformable_to S3;
A15: S1 = F1?-a by Th18;
then reconsider
T1 = (curry s1).a as natural_transformation of S1,S2 by A1,A11,Th11;
A16: (export t2).a = [[S2,S3],T2] & (export t1).a = [[S1,S2],T1] by A1,A2,Def5;
A17: S1 is_naturally_transformable_to S2 by A1,A15,A11,Th11;
then S1 is_naturally_transformable_to S3 by A13,NATTRA_1:23;
then
A18: S1 is_transformable_to S3;
reconsider T3 = (curry s3).a as natural_transformation of S1,S3 by A9,A15
,A12,Th11;
A19: Hom((export F1).a,(export F2).a) <> {} & Hom((export F2).a,(export F3
).a) <> {} by A6,A8;
A20: S1 is_transformable_to S2 by A17;
now
let b be Object of B;
A21: Hom(F1.[a,b],F2.[a,b]) <> {} & Hom(F2.[a,b],F3.[a,b]) <> {} by A4,A3;
A22: Hom(S1.b,S2.b) <> {} & Hom(S2.b,S3.b) <> {} by A20,A14;
A23: T1.b = (T1 qua Function of the carrier of B, the carrier' of C).b
by A20,NATTRA_1:def 5
.= s1.(a,b) by FUNCT_5:69
.= t1.[a,b] by A4,NATTRA_1:def 5;
A24: T2.b = (T2 qua Function of the carrier of B, the carrier' of C).b
by A14,NATTRA_1:def 5
.= s2.(a,b) by FUNCT_5:69
.= t2.[a,b] by A3,NATTRA_1:def 5;
thus T3.b = (T3 qua Function of the carrier of B, the carrier' of C).b
by A18,NATTRA_1:def 5
.= s3.(a,b) by FUNCT_5:69
.= (t2`*`t1).[a,b] by A10,NATTRA_1:def 5
.= t2.[a,b]*t1.[a,b] by A1,A2,NATTRA_1:25
.= (T2.b)(*)(T1.b qua Morphism of C) by A21,A24,A23,CAT_1:def 13
.= T2.b*T1.b by A22,CAT_1:def 13
.= (T2`*`T1).b by A17,A13,NATTRA_1:25;
end;
then
A25: T3 = T2`*`T1 by A18,NATTRA_1:19;
thus (export(t2`*`t1)).a = [[S1,S3],T3] by A9,Def5
.= ((export t2).a)(*)((export t1).a qua Morphism of Functors(B,C))
by A16,A25,NATTRA_1:36
.= (export t2).a*(export t1).a by A19,CAT_1:def 13
.= ((export t2)`*`(export t1)).a by A5,A7,NATTRA_1:25;
end;
hence thesis by A6,A8,NATTRA_1:18,19;
end;
theorem Th24:
for F1,F2 being Functor of [:A,B:],C st F1
is_naturally_transformable_to F2 for t1,t2 being natural_transformation of F1,
F2 holds export t1 = export t2 implies t1 = t2
proof
let F1,F2 be Functor of [:A,B:],C;
assume
A1: F1 is_naturally_transformable_to F2;
then
A2: F1 is_transformable_to F2;
let t1,t2 be natural_transformation of F1,F2 such that
A3: export t1 = export t2;
now
reconsider
s1 = t1, s2 = t2 as Function of [:the carrier of A, the carrier
of B:], the carrier' of C;
let ab be Object of [:A,B:];
consider a being Object of A, b being Object of B such that
A4: ab = [a,b] by DOMAIN_1:1;
[[(export F1).a,(export F2).a],(curry s1).a] = (export t1).a by A1,Def5
.= [[(export F1).a,(export F2).a],(curry s2).a] by A1,A3,Def5;
then
A5: (curry s1).a = (curry s2.a) by XTUPLE_0:1;
thus t1.ab = s1.(a,b) by A2,A4,NATTRA_1:def 5
.= ((curry s2).a).b by A5,FUNCT_5:69
.= s2.(a,b) by FUNCT_5:69
.= t2.ab by A2,A4,NATTRA_1:def 5;
end;
hence thesis by A1,ISOCAT_1:26;
end;
theorem Th25:
for G being Functor of A, Functors(B,C) ex F being Functor of [:
A,B:],C st G = export F
proof
let G be Functor of A, Functors(B,C);
defpred P[object,object] means
for f being (Morphism of A), g being Morphism of B
st $1 = [f,g] for f1,f2 being Functor of B,C, t being natural_transformation of
f1,f2 st G.f = [[f1,f2],t] holds $2 = (t.(cod g))(*)(f1.g);
A1: now
let m be object;
assume m in the carrier' of [:A,B:];
then consider m1 being (Morphism of A), m2 being Morphism of B such that
A2: m = [m1, m2] by CAT_2:27;
consider F1,F2 being Functor of B,C, t1 being natural_transformation of F1
,F2 such that
F1 is_naturally_transformable_to F2 and
dom(G.m1) = F1 and
cod(G.m1) = F2 and
A3: G.m1 = [[F1,F2],t1] by Th6;
reconsider o = (t1.(cod m2))(*)(F1.m2) as object;
take o;
thus o in the carrier' of C;
thus P[m,o]
proof
let f be (Morphism of A), g be Morphism of B;
assume
A4: m = [f,g];
then
A5: g = m2 by A2,XTUPLE_0:1;
let f1,f2 be Functor of B,C, t be natural_transformation of f1,f2;
assume
A6: G.f = [[f1,f2],t];
A7: f = m1 by A2,A4,XTUPLE_0:1;
then [F1,F2] = [f1,f2] by A3,A6,XTUPLE_0:1;
then F1 =f1 & F2 = f2 by XTUPLE_0:1;
hence thesis by A3,A7,A5,A6,XTUPLE_0:1;
end;
end;
consider F being Function of the carrier' of [:A,B:], the carrier' of C such
that
A8: for m being object st m in the carrier' of [:A,B:] holds P[m,F.m]
from FUNCT_2:
sch 1 (A1);
F is Functor of [:A,B:],C
proof
thus for ab being Object of [:A,B:] ex c being Object of C st F.id ab = id
c
proof
let ab be Object of [:A,B:];
consider a being Object of A, b being Object of B such that
A9: ab = [a,b] by CAT_2:25;
reconsider H = G.a as Functor of B,C by Th5;
take H.b;
A10: Hom(H.b,H.b) <> {};
A11: G.(id a qua Morphism of A) = id(G.a) by CAT_1:71
.= [[H,H],id H] by NATTRA_1:def 17;
id ab = [id a, id b] by A9,CAT_2:31;
hence F.id ab = ((id H).(cod id b))(*)(H.(id b qua Morphism of B))
by A8,A11
.= ((id H).(cod id b))(*)id(H.b) by CAT_1:71
.= ((id H).b)(*)(id(H.b) qua Morphism of C)
.= id(H.b)(*)(id(H.b) qua Morphism of C) by NATTRA_1:20
.= id(H.b)*id(H.b) by A10,CAT_1:def 13
.= id(H.b);
end;
thus for f being Morphism of [:A,B:] holds F.id dom f = id dom(F.f) & F.id
cod f = id cod(F.f)
proof
let f be Morphism of [:A,B:];
consider f1 being (Morphism of A), f2 being Morphism of B such that
A12: f = [f1,f2] by CAT_2:27;
reconsider H = G.dom f1 as Functor of B,C by Th5;
A13: Hom(dom(H.f2),dom(H.f2)) <> {};
A14: id(G.dom f1) = [[H,H],id H] & G.(id dom f1 qua Morphism of A) = id(
G.dom f1) by CAT_1:71,NATTRA_1:def 17;
consider F1,F2 being Functor of B,C, t being natural_transformation of
F1,F2 such that
A15: F1 is_naturally_transformable_to F2 and
A16: dom(G.f1) = F1 and
A17: cod(G.f1) = F2 and
A18: G.f1 = [[F1,F2],t] by Th6;
A19: F1.cod f2 = cod(F1.f2) by CAT_1:72;
Hom(F1.cod f2,F2.cod f2) <> {} by A15,ISOCAT_1:25;
then
A20: dom(t.cod f2) = cod(F1.f2) by A19,CAT_1:5;
A21: F1 = H by A16,CAT_1:72;
id dom f = id[dom f1, dom f2] by A12,CAT_2:28
.= [id dom f1, id dom f2] by CAT_2:31;
hence
F.id dom f
= ((id H).(cod id dom f2))(*)(H.(id dom f2 qua Morphism of B))
by A8,A14
.= ((id H).(cod id dom f2))(*)id(H.dom f2) by CAT_1:71
.= ((id H).(cod id dom f2))(*)id dom(H.f2) by CAT_1:72
.= ((id H).dom f2)(*)id dom(H.f2)
.= id(H.dom f2)(*)id dom(H.f2) by NATTRA_1:20
.= (id dom(H.f2) qua Morphism of C)(*)id dom(H.f2) by CAT_1:72
.= id dom(H.f2)*id dom(H.f2) by A13,CAT_1:def 13
.= id dom(F1.f2) by A21
.= id dom((t.(cod f2))(*)(F1.f2)) by A20,CAT_1:17
.= id dom(F.f) by A8,A12,A18;
reconsider H = G.cod f1 as Functor of B,C by Th5;
A22: F2 = H by A17,CAT_1:72;
A23: Hom(cod(H.f2),cod(H.f2)) <> {};
A24: id cod f = id[cod f1, cod f2] by A12,CAT_2:28
.= [id cod f1, id cod f2] by CAT_2:31;
A25: Hom(F1.cod f2,F2.cod f2) <> {} by A15,ISOCAT_1:25;
F1.cod f2 = cod(F1.f2) by CAT_1:72;
then
A26: dom(t.cod f2) = cod(F1.f2) by A25,CAT_1:5;
id(G.cod f1) = [[H,H],id H] & G.(id cod f1 qua Morphism of A) = id(
G.cod f1) by CAT_1:71,NATTRA_1:def 17;
hence
F.id cod f
= ((id H).(cod id cod f2))(*)(H.(id cod f2 qua Morphism of B))
by A8,A24
.= ((id H).(cod id cod f2))(*)id(H.cod f2) by CAT_1:71
.= ((id H).(cod id cod f2))(*)id cod(H.f2) by CAT_1:72
.= ((id H).cod f2)(*)id cod(H.f2)
.= id(H.cod f2)(*)id cod(H.f2) by NATTRA_1:20
.= (id cod(H.f2) qua Morphism of C)(*)id cod(H.f2) by CAT_1:72
.= id cod(H.f2)*id cod(H.f2) by A23,CAT_1:def 13
.= id cod(H.f2)
.= id(F2.cod f2) by A22,CAT_1:72
.= id cod(t.cod f2) by A25,CAT_1:5
.= id cod((t.(cod f2))(*)(F1.f2)) by A26,CAT_1:17
.= id cod(F.f) by A8,A12,A18;
end;
let f,g be Morphism of [:A,B:] such that
A27: dom g = cod f;
consider g1 being (Morphism of A), g2 being Morphism of B such that
A28: g = [g1,g2] by CAT_2:27;
reconsider g29 = g2 as Morphism of dom g2, cod g2 by CAT_1:4;
consider f1 being (Morphism of A), f2 being Morphism of B such that
A29: f = [f1,f2] by CAT_2:27;
A30: [cod f1, cod f2] = cod f by A29,CAT_2:28;
consider G1,G2 being Functor of B,C, s being natural_transformation of G1,
G2 such that
A31: G1 is_naturally_transformable_to G2 and
A32: dom(G.g1) = G1 and
cod(G.g1) = G2 and
A33: G.g1 = [[G1,G2],s] by Th6;
consider F1,F2 being Functor of B,C, t being natural_transformation of F1,
F2 such that
A34: F1 is_naturally_transformable_to F2 and
dom(G.f1) = F1 and
A35: cod(G.f1) = F2 and
A36: G.f1 = [[F1,F2],t] by Th6;
A37: F.f = (t.(cod f2))(*)(F1.f2) by A8,A29,A36;
A38: [dom g1, dom g2] = dom g by A28,CAT_2:28;
then
A39: cod f1 = dom g1 by A27,A30,XTUPLE_0:1;
then reconsider s as natural_transformation of F2,G2 by A35,A32,CAT_1:64;
A40: cod f2 = dom g2 by A27,A30,A38,XTUPLE_0:1;
then
A41: g(*)f = [g1(*)f1,g2(*)f2] by A29,A28,A39,CAT_2:29;
reconsider f29 = f2 as Morphism of dom f2, dom g2 by A40,CAT_1:4;
A42: cod(g2(*)f2) = cod g2 by A40,CAT_1:17;
A43: Hom(dom f2, dom g2) <> {} by A40,CAT_1:2;
then
A44: Hom(F1.dom f2,F1.dom g2) <> {} by CAT_1:84;
A45: Hom(F1.dom g2,F2.dom g2) <> {} by A34,ISOCAT_1:25;
then
A46: Hom(F1.dom f2,F2.dom g2) <> {} by A44,CAT_1:24;
A47: Hom(dom g2, cod g2) <> {} by CAT_1:2;
then
A48: F1/.g2 = F1/.g29 by CAT_3:def 10;
A49: F2 = G1 by A35,A32,A39,CAT_1:64;
then
A50: Hom(F2.cod g2,G2.cod g2) <> {} by A31,ISOCAT_1:25;
A51: G1/.g2 = F2/.g29 by A49,A47,CAT_3:def 10;
A52: Hom(F2.dom g2,F2.cod g2) <> {} by A47,CAT_1:84;
then
A53: Hom(F2.dom g2,G2.cod g2) <> {} by A50,CAT_1:24;
A54: Hom(F1.dom g2,F1.cod g2) <> {} by A47,CAT_1:84;
then
A55: Hom(F1.dom f2,F1.cod g2) <> {} by A44,CAT_1:24;
A56: Hom(F1.cod g2,F2.cod g2) <> {} by A34,ISOCAT_1:25;
then
A57: Hom(F1.cod g2,G2.cod g2) <> {} by A50,CAT_1:24;
A58: F1/.f2 = F1/.f29 by A43,CAT_3:def 10;
G.(g1(*)f1) = (G.g1)(*)(G.f1) by A39,CAT_1:64
.= [[F1,G2],s`*`t] by A36,A33,A49,NATTRA_1:36;
hence F.(g(*)f) = ((s`*`t).(cod(g2(*)f2)))(*)(F1.(g2(*)f2)) by A8,A41
.= (s.(cod g2)*t.(cod g2))(*)(F1.(g2(*)f2))
by A34,A31,A49,A42,NATTRA_1:25
.= (s.(cod g2)*t.(cod g2))(*)((F1/.g2)(*)(F1/.f2)) by A40,CAT_1:64
.= (s.(cod g2)*t.(cod g2))(*)(F1/.g29*F1/.f29 qua Morphism of C)
by A44,A54,A48,A58,CAT_1:def 13
.= s.(cod g2)*t.(cod g2)*(F1/.g29*F1/.f29) by A55,A57,CAT_1:def 13
.= s.(cod g2)*(t.(cod g2)*(F1/.g29*F1/.f29)) by A50,A56,A55,CAT_1:25
.= s.(cod g2)*(t.(cod g2)*F1/.g29*F1/.f29) by A56,A44,A54,CAT_1:25
.= s.(cod g2)*(F2/.g29*t.(dom g2)*F1/.f29) by A34,A47,NATTRA_1:def 8
.= s.(cod g2)*(F2/.g29*(t.(dom g2)*F1/.f29)) by A44,A52,A45,CAT_1:25
.= s.(cod g2)*F2/.g29*(t.(dom g2)*F1/.f29) by A50,A52,A46,CAT_1:25
.= (s.(cod g2)*F2/.g29)(*)(t.(dom g2)*F1/.f29 qua Morphism of C)
by A46,A53,CAT_1:def 13
.= (s.(cod g2)*F2/.g29)(*)((t.(cod f2))(*)(F1.f2))
by A40,A44,A45,A58,CAT_1:def 13
.= (s.(cod g2))(*)(G1/.g2)(*)((t.(cod f2))(*)(F1.f2))
by A50,A52,A51,CAT_1:def 13
.= (F.g)(*)(F.f) by A8,A28,A33,A49,A37;
end;
then reconsider F as Functor of [:A,B:],C;
take F;
now
let f be Morphism of A;
consider f1,f2 being Functor of B,C, t being natural_transformation of f1,
f2 such that
A59: f1 is_naturally_transformable_to f2 and
A60: dom(G.f) = f1 and
A61: cod(G.f) = f2 and
A62: G.f = [[f1,f2],t] by Th6;
now
let g be Morphism of B;
A63: dom id cod g = cod g;
A64: f1 = G.dom f by A60,CAT_1:72;
A65: G.(id dom f qua Morphism of A) = id(G.dom f) by CAT_1:71
.= [[f1,f1],id f1] by A64,NATTRA_1:def 17;
thus (F?-dom f).g = F.(id dom f, g) by CAT_2:36
.= F.[id dom f, g]
.= ((id f1).(cod g))(*)(f1.g) by A8,A65
.= id(f1.cod g qua Object of C)(*)(f1.g) by NATTRA_1:20
.= (f1.(id cod g qua Morphism of B))(*)(f1.g) by CAT_1:71
.= f1.((id cod g qua Morphism of B)(*)g) by A63,CAT_1:64
.= f1.g by CAT_1:21;
end;
then
A66: f1 = F?-dom f by FUNCT_2:63;
now
let g be Morphism of B;
A67: dom id cod g = cod g;
A68: f2 = G.cod f by A61,CAT_1:72;
A69: G.(id cod f qua Morphism of A) = id(G.cod f) by CAT_1:71
.= [[f2,f2],id f2] by A68,NATTRA_1:def 17;
thus (F?-cod f).g = F.(id cod f, g) by CAT_2:36
.= F.[id cod f, g]
.= ((id f2).(cod g))(*)(f2.g) by A8,A69
.= id(f2.cod g qua Object of C)(*)(f2.g) by NATTRA_1:20
.= (f2.(id cod g qua Morphism of B))(*)(f2.g) by CAT_1:71
.= f2.((id cod g qua Morphism of B)(*)g) by A67,CAT_1:64
.= f2.g by CAT_1:21;
end;
then
A70: f2 = F?-cod f by FUNCT_2:63;
now
let b be Object of B;
A71: Hom(f1.b,f1.b) <> {};
A72: Hom(f1.b,f2.b) <> {} by A59,ISOCAT_1:25;
thus (F?-f).b = F.(f,id b) by Th15
.= F.[f,id b]
.= (t.(cod id b))(*)(f1.(id b qua Morphism of B)) by A8,A62
.= (t.(cod id b))(*)id(f1.b) by CAT_1:71
.= (t.b)(*)(id(f1.b) qua Morphism of C)
.= t.b*id(f1.b) by A72,A71,CAT_1:def 13
.= t.b by A72,CAT_1:29;
end;
hence G.f =[[F?-dom f,F?-cod f],F?-f] by A59,A62,A66,A70,ISOCAT_1:26;
end;
hence thesis by Def4;
end;
theorem Th26:
for F1,F2 being Functor of [:A,B:],C st export F1
is_naturally_transformable_to export F2 for t being natural_transformation of
export F1, export F2 holds F1 is_naturally_transformable_to F2 & ex u being
natural_transformation of F1,F2 st t = export u
proof
let F1,F2 be Functor of [:A,B:],C such that
A1: export F1 is_naturally_transformable_to export F2;
let t be natural_transformation of export F1, export F2;
defpred P[object,object] means
for a being Object of A st $1 = a holds t.a = [[(
export F1).a,(export F2).a],$2];
A2: now
let o be object;
assume o in the carrier of A;
then reconsider a9 = o as Object of A;
consider f1,f2 being Functor of B,C, tau being natural_transformation of
f1,f2 such that
f1 is_naturally_transformable_to f2 and
A3: dom(t.a9) = f1 and
A4: cod(t.a9) = f2 & t.a9 =[[f1,f2],tau] by Th6;
reconsider m = tau as object;
take m;
thus m in Funcs(the carrier of B, the carrier' of C) by FUNCT_2:8;
thus P[o,m]
proof
let a be Object of A such that
A5: o = a;
export F1 is_transformable_to export F2 by A1;
then
A6: Hom((export F1).a, (export F2).a) <> {};
then (export F1).a = f1 by A3,A5,CAT_1:5;
hence thesis by A4,A5,A6,CAT_1:5;
end;
end;
consider t9 being Function of the carrier of A, Funcs(the carrier of B,the
carrier' of C) such that
A7: for o being object st o in the carrier of A holds P[o,t9.o]
from FUNCT_2:sch 1(A2);
reconsider u9 = uncurry t9 as Function of the carrier of [:A,B:], the
carrier' of C;
A8: now
let ab be Object of [:A,B:];
consider a being Object of A, b being Object of B such that
A9: ab = [a,b] by DOMAIN_1:1;
(export F1).a = F1?-a & (export F2).a = F2?-a by Th18;
then t.a = [[F1?-a,F2?-a],t9.a] by A7;
then [[F1?-a,F2?-a],t9.a] in the carrier' of Functors(B,C);
then [[F1?-a,F2?-a],t9.a] in NatTrans(B,C) by NATTRA_1:def 17;
then consider
G1,G2 being Functor of B,C, t99 being natural_transformation of
G1,G2 such that
A10: [[F1?-a,F2?-a],t9.a] = [[G1,G2],t99] and
A11: G1 is_naturally_transformable_to G2 by NATTRA_1:def 15;
A12: G1 is_transformable_to G2 by A11;
A13: [F1?-a,F2?-a] = [G1,G2] by A10,XTUPLE_0:1;
A14: F1.[a,b] = (F1?-a).b by Th8
.= G1.b by A13,XTUPLE_0:1;
A15: Hom(G1.b,G2.b) <> {} by A11,ISOCAT_1:25;
A16: F2.[a,b] = (F2?-a).b by Th8
.= G2.b by A13,XTUPLE_0:1;
u9.(a,b) = t9.a.b by Th2
.= (t99 qua Function of the carrier of B, the carrier' of C).b by A10,
XTUPLE_0:1
.= t99.b by A12,NATTRA_1:def 5;
hence u9.ab in Hom(F1.ab,F2.ab) by A9,A14,A16,A15,CAT_1:def 5;
end;
A17: F1 is_transformable_to F2
by A8;
u9 is transformation of F1,F2
proof
thus F1 is_transformable_to F2 by A17;
let a be Object of [:A,B:];
u9.a in Hom(F1.a,F2.a) by A8;
hence thesis by CAT_1:def 5;
end;
then reconsider u = u9 as transformation of F1,F2;
A18: now
reconsider FF1 = F1, FF2 = F2 as Function of [:the carrier' of A, the
carrier' of B:], the carrier' of C;
let ab1,ab2 be Object of [:A,B:] such that
A19: Hom(ab1,ab2) <> {};
A20: Hom(F2.ab1,F2.ab2) <> {} by A19,CAT_1:84;
consider a2 being Object of A, b2 being Object of B such that
A21: ab2 = [a2,b2] by DOMAIN_1:1;
(export F1).a2 = F1?-a2 & (export F2).a2 = F2?-a2 by Th18;
then t.a2 = [[F1?-a2,F2?-a2],t9.a2] by A7;
then [[F1?-a2,F2?-a2],t9.a2] in the carrier' of Functors(B,C);
then [[F1?-a2,F2?-a2],t9.a2] in NatTrans(B,C) by NATTRA_1:def 17;
then consider
G2,H2 being Functor of B,C, t2 being natural_transformation of G2
,H2 such that
A22: [[F1?-a2,F2?-a2],t9.a2] = [[G2,H2],t2] and
A23: G2 is_naturally_transformable_to H2 by NATTRA_1:def 15;
A24: t9.a2 = t2 & G2 is_transformable_to H2 by A22,A23,XTUPLE_0:1;
consider a1 being Object of A, b1 being Object of B such that
A25: ab1 = [a1,b1] by DOMAIN_1:1;
(export F1).a1 = F1?-a1 & (export F2).a1 = F2?-a1 by Th18;
then t.a1 = [[F1?-a1,F2?-a1],t9.a1] by A7;
then [[F1?-a1,F2?-a1],t9.a1] in the carrier' of Functors(B,C);
then [[F1?-a1,F2?-a1],t9.a1] in NatTrans(B,C) by NATTRA_1:def 17;
then consider
G1,H1 being Functor of B,C, t1 being natural_transformation of G1
,H1 such that
A26: [[F1?-a1,F2?-a1],t9.a1] = [[G1,H1],t1] and
A27: G1 is_naturally_transformable_to H1 by NATTRA_1:def 15;
A28: t9.a1 = t1 & G1 is_transformable_to H1 by A26,A27,XTUPLE_0:1;
A29: u.ab1 = u9.(a1,b1) by A17,A25,NATTRA_1:def 5
.= t9.a1.b1 by Th2
.= t1.b1 by A28,NATTRA_1:def 5;
A30: Hom(G1.b2,H1.b2) <> {} by A27,ISOCAT_1:25;
A31: Hom(F1.ab1,F1.ab2) <> {} by A19,CAT_1:84;
A32: Hom(F1.ab2,F2.ab2) <> {} by A17;
(export F2).a1 = F2?-a1 & (export F1).a1 = F1?-a1 by Th18;
then
A33: t.a1 = [[G1,H1],t1] by A7,A26;
A34: Hom(G1.b1,H1.b1) <> {} by A27,ISOCAT_1:25;
(export F1).a2 = F1?-a2 & (export F2).a2 = F2?-a2 by Th18;
then
A35: t.a2 = [[G2,H2],t2] by A7,A22;
A36: Hom((export F1).a2,(export F2).a2) <> {} by A1,ISOCAT_1:25;
A37: Hom((export F1).a1,(export F2).a1) <> {} by A1,ISOCAT_1:25;
let f be Morphism of ab1,ab2;
consider g being (Morphism of A), h being Morphism of B such that
A38: f = [g,h] by DOMAIN_1:1;
reconsider g as Morphism of a1,a2 by A19,A25,A21,A38,Th10;
A39: Hom(a1,a2) <> {} by A19,A25,A21,Th9;
then
A40: dom g = a1 & cod g = a2 by CAT_1:5;
reconsider h as Morphism of b1,b2 by A19,A25,A21,A38,Th10;
reconsider g9 = g as Morphism of A;
reconsider h9 = h as Morphism of B;
reconsider f9 = f as Morphism of [:A,B:];
A41: dom id b2 = b2;
Hom(a1,a1) <> {};
then
A42: g9(*)(id a1) = g*(id a1) by A39,CAT_1:def 13
.= g by A39,CAT_1:29;
A43: dom g = a1 by A39,CAT_1:5;
A44: Hom((export F2).a1,(export F2).a2) <> {} by A39,CAT_1:84;
reconsider e1 = (export F1)/.g, e2 = (export F2)/.g
as Morphism of Functors(B,C);
A45: Hom(F1.ab1,F2.ab1) <> {} by A17;
A46: Hom(b1,b2) <> {} by A19,A25,A21,Th9;
then
A47: Hom(G1.b1,G1.b2) <> {} by CAT_1:84;
A48: [F1?-a1,F2?-a1] = [G1,H1] by A26,XTUPLE_0:1;
then
A49: F2?-a1 = H1 by XTUPLE_0:1;
then
A50: H1/.h = (F2?-a1)/.(h qua Morphism of B) by A46,CAT_3:def 10
.= F2.(id a1,h) by CAT_2:36;
A51: [F1?-a2,F2?-a2] = [G2,H2] by A22,XTUPLE_0:1;
then
A52: F2?-a2 = H2 by XTUPLE_0:1;
then
A53: Hom(H1.b2,H2.b2) <> {} by A49,A40,Th14,ISOCAT_1:25;
A54: F1?-a2 = G2 by A51,XTUPLE_0:1;
then reconsider v1 = F1?-g as natural_transformation of G1,G2 by A48,A40,
XTUPLE_0:1;
A55: Hom((export F1).a1,(export F1).a2) <> {} by A39,CAT_1:84;
cod id a1 = a1 & cod h = b2 by A46,CAT_1:5;
then
A56: cod[id a1,h] = [a1,b2] by CAT_2:28
.= dom[g,id b2] by A43,A41,CAT_2:28;
reconsider v2 = F2?-g as natural_transformation of H1,H2 by A48,A52,A40,
XTUPLE_0:1;
A57: (export F2).g9 = [[H1,H2],v2] by A49,A52,A40,Def4;
A58: id b2 = (IdMap B).b2 by ISOCAT_1:def 12;
A59: H1 is_naturally_transformable_to H2 by A49,A52,A40,Th14;
then H1 is_transformable_to H2;
then
A60: v2.b2 = (curry(F2,g)*IdMap B).b2 by NATTRA_1:def 5
.= curry(F2,g).((IdMap B).b2) by FUNCT_2:15
.= F2.(g,id b2) by A58,FUNCT_5:69;
A61: F1?-a1 = G1 by A48,XTUPLE_0:1;
then
A62: G1/.h = (F1?-a1)/.(h qua Morphism of B) by A46,CAT_3:def 10
.= F1.(id a1,h) by CAT_2:36;
(export F1).g9 = [[G1,G2],v1] by A61,A54,A40,Def4;
then [[G1,H2],t2`*`v1] = (t.a2)(*)((export F1).g9) by A35,NATTRA_1:36
.= (t.a2)(*)e1 by A39,CAT_3:def 10
.= t.a2*(export F1)/.g by A55,A36,CAT_1:def 13
.= (export F2)/.g*t.a1 by A1,A39,NATTRA_1:def 8
.= e2(*)(t.a1) by A44,A37,CAT_1:def 13
.= ((export F2).g9)(*)(t.a1) by A39,CAT_3:def 10
.= [[G1,H2],v2`*`t1] by A57,A33,NATTRA_1:36;
then
A63: t2`*`v1 = v2`*`t1 by XTUPLE_0:1;
A64: id b2 = (IdMap B).b2 by ISOCAT_1:def 12;
A65: G1 is_naturally_transformable_to G2 by A61,A54,A40,Th14;
then G1 is_transformable_to G2;
then
A66: v1.b2 = (curry(F1,g)*IdMap B).b2 by NATTRA_1:def 5
.= curry(F1,g).((IdMap B).b2) by FUNCT_2:15
.= F1.(g,id b2) by A64,FUNCT_5:69;
A67: u.ab2 = u9.(a2,b2) by A17,A21,NATTRA_1:def 5
.= t9.a2.b2 by Th2
.= t2.b2 by A24,NATTRA_1:def 5;
A68: Hom(G2.b2,H2.b2) <> {} by A23,ISOCAT_1:25;
Hom(b2,b2) <> {};
then (id b2)(*)h9 = (id b2)*h by A46,CAT_1:def 13
.= h by A46,CAT_1:28;
then
A69: f = [g,id b2](*)[id a1, h] by A38,A42,A56,CAT_2:30;
A70: Hom(H1.b1,H1.b2) <> {} by A46,CAT_1:84;
then
A71: Hom(H1.b1,H2.b2) <> {} by A53,CAT_1:24;
A72: F2/.f = F2/.f9 by A19,CAT_3:def 10
.= (v2.b2)(*)(H1/.h qua Morphism of C) by A56,A69,A60,A50,CAT_1:64
.= v2.b2*H1/.h by A53,A70,CAT_1:def 13;
A73: Hom(G1.b2,G2.b2) <> {} by A61,A54,A40,Th14,ISOCAT_1:25;
then
A74: Hom(G1.b1,G2.b2) <> {} by A47,CAT_1:24;
F1/.f = F1/.f9 by A19,CAT_3:def 10
.= (v1.b2)(*)(G1/.h qua Morphism of C) by A56,A69,A66,A62,CAT_1:64
.= v1.b2*G1/.h by A73,A47,CAT_1:def 13;
hence u.ab2*F1/.f = (t2.b2)(*)(v1.b2*G1/.h qua Morphism of C)
by A31,A32,A67,CAT_1:def 13
.= t2.b2*(v1.b2*G1/.h) by A68,A74,CAT_1:def 13
.= t2.b2*v1.b2*G1/.h by A68,A73,A47,CAT_1:25
.= (v2`*`t1).b2*G1/.h by A23,A65,A63,NATTRA_1:25
.= v2.b2*t1.b2*G1/.h by A27,A59,NATTRA_1:25
.= v2.b2*(t1.b2*G1/.h) by A47,A53,A30,CAT_1:25
.= v2.b2*(H1/.h*t1.b1) by A27,A46,NATTRA_1:def 8
.= v2.b2*H1/.h*t1.b1 by A53,A70,A34,CAT_1:25
.= (F2/.f)(*)(u.ab1 qua Morphism of C) by A34,A71,A29,A72,CAT_1:def 13
.= F2/.f*u.ab1 by A45,A20,CAT_1:def 13;
end;
hence
A75: F1 is_naturally_transformable_to F2 by A17;
then reconsider u as natural_transformation of F1,F2 by A18,NATTRA_1:def 8;
take u;
now
let s be Function of [:the carrier of A, the carrier of B:], the carrier'
of C such that
A76: u = s;
let a be Object of A;
t9 = curry u9 by Th1;
hence t.a = [[(export F1).a,(export F2).a],(curry s).a] by A7,A76;
end;
hence thesis by A75,Def5;
end;
definition
let A,B,C;
func export(A,B,C)-> Functor of Functors([:A,B:],C),Functors(A,Functors(B,C)
) means
:Def6:
for F1,F2 being Functor of [:A,B:], C st F1
is_naturally_transformable_to F2 for t being natural_transformation of F1,F2
holds it.[[F1,F2],t] = [[export F1, export F2],export t];
existence
proof
defpred P[object,object] means
for F1,F2 being Functor of [:A,B:], C, t being
natural_transformation of F1,F2 st $1 = [[F1,F2],t] holds $2 = [[export F1,
export F2],export t];
A1: now
let o be object;
assume o in the carrier' of Functors([:A,B:],C);
then o in NatTrans([:A,B:],C) by NATTRA_1:def 17;
then consider F1,F2 being Functor of [:A,B:],C, t being
natural_transformation of F1,F2 such that
A2: o = [[F1,F2],t] and
A3: F1 is_naturally_transformable_to F2 by NATTRA_1:def 16;
reconsider m = [[export F1, export F2], export t] as object;
take m;
export F1 is_naturally_transformable_to export F2 by A3,Th21;
then m in NatTrans(A,Functors(B,C)) by NATTRA_1:def 16;
hence m in the carrier' of Functors(A,Functors(B,C)) by NATTRA_1:def 17;
thus P[o,m]
proof
let F19,F29 be Functor of [:A,B:],C, t9 be natural_transformation of
F19,F29;
assume
A4: o = [[F19,F29],t9];
then [F1,F2] = [F19,F29] by A2,XTUPLE_0:1;
then F1 = F19 & F2 = F29 by XTUPLE_0:1;
hence thesis by A2,A4,XTUPLE_0:1;
end;
end;
consider FF being Function of the carrier' of Functors([:A,B:],C), the
carrier' of Functors(A,Functors(B,C)) such that
A5: for o being object st o in the carrier' of Functors([:A,B:],C)
holds P[o,FF.o]
from FUNCT_2:sch 1(A1);
FF is Functor of Functors([:A,B:],C),Functors(A,Functors(B,C))
proof
thus for c being Object of Functors([:A,B:],C) ex d being Object of
Functors(A,Functors(B,C)) st FF.id c = id d
proof
let c be Object of Functors([:A,B:],C);
reconsider F = c as Functor of [:A,B:],C by Th5;
reconsider d = export F as Object of Functors(A,Functors(B,C)) by Th5;
take d;
A6: id export F = export id F by Th22;
id c = [[F,F],id F] by NATTRA_1:def 17;
hence FF.id c = [[export F, export F], export id F] by A5
.= id d by A6,NATTRA_1:def 17;
end;
thus for f being Morphism of Functors([:A,B:],C) holds FF.id dom f = id
dom(FF.f) & FF.id cod f = id cod(FF.f)
proof
let f be Morphism of Functors([:A,B:],C);
consider F1,F2 being Functor of [:A,B:],C, t being
natural_transformation of F1,F2 such that
F1 is_naturally_transformable_to F2 and
A7: dom f = F1 and
A8: cod f = F2 and
A9: f =[[F1,F2],t] by Th6;
A10: FF.f = [[export F1, export F2], export t] by A5,A9;
then
A11: dom(FF.f) = export F1 by NATTRA_1:33;
id dom f = [[F1,F1],id F1] by A7,NATTRA_1:def 17;
hence FF.id dom f = [[export F1, export F1], export id F1] by A5
.= [[export F1, export F1], id export F1] by Th22
.= id dom(FF.f) by A11,NATTRA_1:def 17;
A12: cod(FF.f) = export F2 by A10,NATTRA_1:33;
id cod f = [[F2,F2],id F2] by A8,NATTRA_1:def 17;
hence FF.id cod f = [[export F2, export F2], export id F2] by A5
.= [[export F2, export F2], id export F2] by Th22
.= id cod(FF.f) by A12,NATTRA_1:def 17;
end;
let f,g be Morphism of Functors([:A,B:],C);
consider F1,F2 being Functor of [:A,B:],C, t being
natural_transformation of F1,F2 such that
A13: F1 is_naturally_transformable_to F2 and
dom f = F1 and
A14: cod f = F2 and
A15: f =[[F1,F2],t] by Th6;
A16: FF.f = [[export F1, export F2], export t] by A5,A15;
consider G1,G2 being Functor of [:A,B:],C, u being
natural_transformation of G1,G2 such that
A17: G1 is_naturally_transformable_to G2 and
A18: dom g = G1 and
cod g = G2 and
A19: g =[[G1,G2],u] by Th6;
assume
A20: dom g = cod f;
then reconsider u as natural_transformation of F2,G2 by A14,A18;
g(*)f = [[F1,G2],u`*`t] by A14,A15,A18,A19,A20,NATTRA_1:36;
then
A21: FF.(g(*)f) = [[export F1, export G2], export(u`*`t)] by A5;
FF.g = [[export F2, export G2], export u] & (export u)`*`(export t)
= export(u`*`t) by A5,A13,A14,A17,A18,A19,A20,Th23;
hence thesis by A16,A21,NATTRA_1:36;
end;
then reconsider
FF as Functor of Functors([:A,B:],C),Functors(A,Functors(B, C));
take FF;
let F1,F2 be Functor of [:A,B:], C such that
A22: F1 is_naturally_transformable_to F2;
let t be natural_transformation of F1,F2;
[[F1,F2],t] in NatTrans([:A,B:],C) by A22,NATTRA_1:32;
then [[F1,F2],t] in the carrier' of Functors([:A,B:],C) by NATTRA_1:def 17;
hence thesis by A5;
end;
uniqueness
proof
let IT1,IT2 be Functor of Functors([:A,B:],C),Functors(A,Functors(B,C))
such that
A23: for F1,F2 being Functor of [:A,B:], C st F1
is_naturally_transformable_to F2 for t being natural_transformation of F1,F2
holds IT1.[[F1,F2],t] = [[export F1, export F2],export t] and
A24: for F1,F2 being Functor of [:A,B:], C st F1
is_naturally_transformable_to F2 for t being natural_transformation of F1,F2
holds IT2.[[F1,F2],t] = [[export F1, export F2],export t];
now
let f be Morphism of Functors([:A,B:],C);
consider F1,F2 being Functor of [:A,B:],C, t being
natural_transformation of F1,F2 such that
A25: F1 is_naturally_transformable_to F2 and
dom f = F1 and
cod f = F2 and
A26: f =[[F1,F2],t] by Th6;
thus (IT1 qua Function of the carrier' of Functors([:A,B:],C), the
carrier' of Functors(A,Functors(B,C)) ).f = [[export F1, export F2], export t]
by A23,A25,A26
.= (IT2 qua Function of the carrier' of Functors([:A,B:],C), the
carrier' of Functors(A,Functors(B,C)) ).f by A24,A25,A26;
end;
hence thesis by FUNCT_2:63;
end;
end;
registration
let A,B,C;
cluster export(A,B,C) -> isomorphic;
coherence
proof
thus export(A,B,C) is one-to-one
proof
let x1,x2 be object;
assume x1 in dom export(A,B,C);
then reconsider f1 = x1 as Morphism of Functors([:A,B:],C);
consider F1,F2 being Functor of [:A,B:],C, t being natural_transformation
of F1,F2 such that
A1: F1 is_naturally_transformable_to F2 and
dom f1 = F1 and
cod f1 = F2 and
A2: f1 =[[F1,F2],t] by Th6;
assume x2 in dom export(A,B,C);
then reconsider f2 = x2 as Morphism of Functors([:A,B:],C);
consider G1,G2 being Functor of [:A,B:],C, u being natural_transformation
of G1,G2 such that
A3: G1 is_naturally_transformable_to G2 and
dom f2 = G1 and
cod f2 = G2 and
A4: f2 =[[G1,G2],u] by Th6;
assume export(A,B,C).x1 = export(A,B,C).x2;
then
A5: [[export F1, export F2], export t] = export(A,B,C).[[G1,G2],u] by A1,A2,A4
,Def6
.= [[export G1, export G2], export u] by A3,Def6;
then
A6: [export F1, export F2] = [export G1, export G2] by XTUPLE_0:1;
then export F1 = export G1 by XTUPLE_0:1;
then
A7: F1 = G1 by Th20;
export F2 = export G2 by A6,XTUPLE_0:1;
then
A8: F2 = G2 by Th20;
export u = export t by A5,XTUPLE_0:1;
hence thesis by A1,A2,A4,A7,A8,Th24;
end;
thus rng export(A,B,C) c= the carrier' of Functors(A,Functors(B,C));
let m be object;
assume m in the carrier' of Functors(A,Functors(B,C));
then reconsider f = m as Morphism of Functors(A,Functors(B,C));
consider F1,F2 being Functor of A,Functors(B,C), t being
natural_transformation of F1,F2 such that
A9: F1 is_naturally_transformable_to F2 and
dom f = F1 and
cod f = F2 and
A10: f =[[F1,F2],t] by Th6;
consider G1 being Functor of [:A,B:],C such that
A11: F1 = export G1 by Th25;
consider G2 being Functor of [:A,B:],C such that
A12: F2 = export G2 by Th25;
consider u being natural_transformation of G1,G2 such that
A13: t = export u by A9,A11,A12,Th26;
A14: G1 is_naturally_transformable_to G2 by A9,A11,A12,Th26;
then dom export(A,B,C) = the carrier' of Functors([:A,B:],C) & [[G1,G2],u]
in NatTrans([:A,B:],C) by FUNCT_2:def 1,NATTRA_1:32;
then
A15: [[G1,G2],u] in dom export(A,B,C) by NATTRA_1:def 17;
export(A,B,C).[[G1,G2],u] = f by A10,A11,A12,A14,A13,Def6;
hence thesis by A15,FUNCT_1:def 3;
end;
end;
theorem
Functors([:A,B:],C) ~= Functors(A,Functors(B,C))
proof
take export(A,B,C);
thus thesis;
end;
begin :: The isomorphism between (B x C)^A and B^A x C^A
theorem Th28:
for F1,F2 being Functor of A,B, G being Functor of B,C st F1
is_naturally_transformable_to F2 for t being natural_transformation of F1,F2
holds G*t = G*(t qua Function)
proof
let F1,F2 be Functor of A,B, G be Functor of B,C;
assume
A1: F1 is_naturally_transformable_to F2;
then
A2: F1 is_transformable_to F2;
let t be natural_transformation of F1,F2;
thus G*t = G*(t qua transformation of F1,F2) by A1,ISOCAT_1:def 7
.= G*(t qua Function) by A2,ISOCAT_1:def 5;
end;
definition
let A,B,C;
let F be Functor of A,B, G be Functor of A,C;
redefine func <:F,G:> -> Functor of A, [:B,C:]; :: redefines <: (FUNCT_3, definition)
coherence
proof
thus <:F,G:> is Functor of A, [:B,C:];
end;
end;
definition
let A,B,C;
let F be Functor of A, [:B,C:];
func Pr1 F -> Functor of A,B equals
pr1(B,C)*F;
correctness;
func Pr2 F -> Functor of A,C equals
pr2(B,C)*F;
correctness;
end;
theorem Th29:
for F being Functor of A,B, G being Functor of A,C holds Pr1<:F,
G:> = F & Pr2<:F,G:> = G
by FUNCT_3:62;
theorem Th30:
for F,G being Functor of A, [:B,C:] st Pr1 F = Pr1 G & Pr2 F =
Pr2 G holds F = G
by FUNCT_3:80;
definition
let A,B,C;
let F1,F2 be Functor of A, [:B,C:];
let t be natural_transformation of F1,F2;
func Pr1 t -> natural_transformation of Pr1 F1, Pr1 F2 equals
pr1(B,C)*t;
coherence;
func Pr2 t -> natural_transformation of Pr2 F1, Pr2 F2 equals
pr2(B,C)*t;
coherence;
end;
theorem Th31:
for F1,F2,G1,G2 being Functor of A, [:B,C:] st F1
is_naturally_transformable_to F2 & G1 is_naturally_transformable_to G2 for s
being natural_transformation of F1,F2, t being natural_transformation of G1,G2
st Pr1 s = Pr1 t & Pr2 s = Pr2 t holds s = t
proof
let F1,F2,G1,G2 be Functor of A, [:B,C:] such that
A1: F1 is_naturally_transformable_to F2 and
A2: G1 is_naturally_transformable_to G2;
let s be natural_transformation of F1,F2, t be natural_transformation of G1,
G2 such that
A3: Pr1 s = Pr1 t and
A4: Pr2 s = Pr2 t;
reconsider S = s, T = t as Function of the carrier of A, [:the carrier' of B
, the carrier' of C:];
A5: pr2(the carrier' of B, the carrier' of C)*S = pr2(B,C)*S
.= Pr2 s by A1,Th28
.= pr2(B,C)*T by A2,A4,Th28
.= pr2(the carrier' of B, the carrier' of C)*T;
pr1(the carrier' of B, the carrier' of C)*S = pr1(B,C)*S
.= Pr1 s by A1,Th28
.= pr1(B,C)*T by A2,A3,Th28
.= pr1(the carrier' of B, the carrier' of C)*T;
hence thesis by A5,FUNCT_3:80;
end;
Lm2: for F1,G1 being Functor of A,B, F2,G2 being Functor of A,C st F1
is_transformable_to G1 & F2 is_transformable_to G2 for t1 being transformation
of F1,G1, t2 being transformation of F2,G2 for a being Object of A holds <:t1,
t2:>.a = [t1.a,t2.a]
proof
let F1,G1 be Functor of A,B, F2,G2 be Functor of A,C such that
A1: F1 is_transformable_to G1 and
A2: F2 is_transformable_to G2;
let t1 be transformation of F1,G1, t2 be transformation of F2,G2;
let a be Object of A;
reconsider s1 = t1 as Function of the carrier of A, the carrier' of B;
reconsider s2 = t2 as Function of the carrier of A, the carrier' of C;
thus <:t1,t2:>.a = [s1.a,s2.a] by FUNCT_3:59
.= [t1.a,s2.a] by A1,NATTRA_1:def 5
.= [t1.a,t2.a] by A2,NATTRA_1:def 5;
end;
theorem Th32: :: poprawic na /. !!!
for F being Functor of A,B, G being Functor of A,C for a,b being
Object of A st Hom(a,b) <> {} for f being Morphism of a,b
holds <:F,G:>.f = [F.f,G.f] by FUNCT_3:59;
theorem Th33:
for F being Functor of A,B, G being Functor of A,C for a being
Object of A holds <:F,G:>.a = [F.a,G.a]
proof
let F be Functor of A,B, G be Functor of A,C;
let a be Object of A;
<:F,G:>.(id a qua Morphism of A) = [F.(id a qua Morphism of A),G.(id a
qua Morphism of A)] by FUNCT_3:59
.= [id(F.a),G.(id a qua Morphism of A)] by CAT_1:71
.= [id(F.a),id(G.a)] by CAT_1:71
.= id[F.a,G.a] by CAT_2:31;
hence thesis by CAT_1:70;
end;
Lm3: for F1,G1 being Functor of A,B, F2,G2 being Functor of A,C st F1
is_transformable_to G1 & F2 is_transformable_to G2 for t1 being transformation
of F1,G1, t2 being transformation of F2,G2 for a being Object of A holds <:t1,
t2:>.a in Hom(<:F1,F2:>.a,<:G1,G2:>.a)
proof
let F1,G1 be Functor of A,B, F2,G2 be Functor of A,C such that
A1: F1 is_transformable_to G1 & F2 is_transformable_to G2;
let t1 be transformation of F1,G1, t2 be transformation of F2,G2;
let a be Object of A;
A2: t1.a in Hom(F1.a,G1.a) & t2.a in Hom(F2.a,G2.a) by A1,ISOCAT_1:4;
A3: [F1.a,F2.a] = <:F1,F2:>.a & [G1.a,G2.a] = <:G1,G2:>.a by Th33;
[t1.a,t2.a] = <:t1,t2:>.a by A1,Lm2;
hence thesis by A2,A3,Th12;
end;
theorem Th34:
for F1,G1 being Functor of A,B, F2,G2 being Functor of A,C st F1
is_transformable_to G1 & F2 is_transformable_to G2 holds <:F1,F2:>
is_transformable_to <:G1,G2:>
by Lm3;
definition
let A,B,C;
let F1,G1 be Functor of A,B, F2,G2 be Functor of A,C such that
A1: F1 is_transformable_to G1 & F2 is_transformable_to G2;
let t1 be transformation of F1,G1, t2 be transformation of F2,G2;
func <:t1,t2:> -> transformation of <:F1,F2:>,<:G1,G2:> equals
:Def11:
<:t1,
t2:>;
coherence
proof
reconsider t = <:t1,t2:> as Function of the carrier of A, the carrier' of
[:B,C:];
t is transformation of <:F1,F2:>,<:G1,G2:>
proof
thus <:F1,F2:> is_transformable_to <:G1,G2:> by A1,Th34;
let a be Object of A;
t.a in Hom(<:F1,F2:>.a,<:G1,G2:>.a) by A1,Lm3;
hence thesis by CAT_1:def 5;
end;
hence thesis;
end;
end;
theorem Th35:
for F1,G1 being Functor of A,B, F2,G2 being Functor of A,C st F1
is_transformable_to G1 & F2 is_transformable_to G2 for t1 being transformation
of F1,G1, t2 being transformation of F2,G2 for a being Object of A holds <:t1,
t2:>.a = [t1.a,t2.a]
proof
let F1,G1 be Functor of A,B, F2,G2 be Functor of A,C such that
A1: F1 is_transformable_to G1 & F2 is_transformable_to G2;
let t1 be transformation of F1,G1, t2 be transformation of F2,G2;
let a be Object of A;
reconsider s1 = t1 as Function of the carrier of A, the carrier' of B;
reconsider s2 = t2 as Function of the carrier of A, the carrier' of C;
thus <:t1,t2:>.a = (<:t1,t2:> qua Function of the carrier of A, the carrier'
of [:B,C:]).a by A1,Th34,NATTRA_1:def 5
.= <:s1,s2:>.a by A1,Def11
.= [t1.a,t2.a] by A1,Lm2;
end;
Lm4: for F1,G1 being Functor of A,B, F2,G2 being Functor of A,C st F1
is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 for t1
being natural_transformation of F1,G1, t2 being natural_transformation of F2,G2
for a,b being Object of A st Hom(a,b) <> {} for f being Morphism of a,b holds
<:t1,t2:>.b*<:F1,F2:>/.f = <:G1,G2:>/.f*<:t1,t2:>.a
proof
let F1,G1 be Functor of A,B, F2,G2 be Functor of A,C such that
A1: F1 is_naturally_transformable_to G1 and
A2: F2 is_naturally_transformable_to G2;
let t1 be natural_transformation of F1,G1, t2 be natural_transformation of
F2,G2;
let a,b be Object of A such that
A3: Hom(a,b) <> {};
A4: Hom(F1.a,F1.b) <> {} by A3,CAT_1:84;
let f be Morphism of a,b;
A5: t1.b*F1/.f = G1/.f*t1.a & t2.b*F2/.f = G2/.f*t2.a
by A1,A2,A3,NATTRA_1:def 8;
A6: G1/.f = G1.f & G2/.f = G2.f by A3,CAT_3:def 10;
A7: <:G1,G2:>/.f = <:G1,G2:>.f by A3,CAT_3:def 10
.= [G1/.f,G2/.f] by A6,A3,Th32;
A8: F1/.f = F1.f & F2/.f = F2.f by A3,CAT_3:def 10;
A9: <:F1,F2:>/.f = <:F1,F2:>.f by A3,CAT_3:def 10
.= [F1/.f,F2/.f] by A3,Th32,A8;
A10: F2 is_transformable_to G2 by A2;
then
A11: Hom(F2.b,G2.b) <> {};
A12: F1 is_transformable_to G1 by A1;
then
A13: <:t1,t2:>.b = [t1.b,t2.b] by A10,Th35;
A14: <:t1,t2:>.a = [t1.a,t2.a] by A12,A10,Th35;
A15: Hom(G2.a,G2.b) <> {} by A3,CAT_1:84;
A16: <:F1,F2:> is_transformable_to <:G1,G2:> by A12,A10,Th34;
then
A17: Hom(<:F1,F2:>.a,<:G1,G2:>.a) <> {};
A18: Hom(<:G1,G2:>.a,<:G1,G2:>.b) <> {} by A3,CAT_1:84;
A19: Hom(G1.a,G1.b) <> {} by A3,CAT_1:84;
A20: Hom(F2.a,F2.b) <> {} by A3,CAT_1:84;
then
A21: t2.b*F2/.f = (t2.b)(*)(F2/.f qua Morphism of C) by A11,CAT_1:def 13;
A22: Hom(F2.a,G2.a) <> {} by A10;
then
A23: G2/.f*t2.a = (G2/.f)(*)(t2.a qua Morphism of C) by A15,CAT_1:def 13;
A24: cod(t2.a) = G2.a by A22,CAT_1:5
.= dom(G2/.f) by A15,CAT_1:5;
A25: Hom(F1.b,G1.b) <> {} by A12;
then
A26: dom(t1.b) = F1.b by CAT_1:5
.= cod(F1/.f) by A4,CAT_1:5;
A27: Hom(F1.a,G1.a) <> {} by A12;
then
A28: G1/.f*t1.a = (G1/.f)(*)(t1.a qua Morphism of B) by A19,CAT_1:def 13;
A29: cod(t1.a) = G1.a by A27,CAT_1:5
.= dom(G1/.f) by A19,CAT_1:5;
A30: dom(t2.b) = F2.b by A11,CAT_1:5
.= cod(F2/.f) by A20,CAT_1:5;
A31: t1.b*F1/.f = (t1.b)(*)(F1/.f qua Morphism of B) by A25,A4,CAT_1:def 13;
A32: Hom(<:F1,F2:>.b,<:G1,G2:>.b) <> {} by A16;
Hom(<:F1,F2:>.a,<:F1,F2:>.b) <> {} by A3,CAT_1:84;
hence
<:t1,t2:>.b*<:F1,F2:>/.f = (<:t1,t2:>.b)(*)(<:F1,F2:>/.f
qua Morphism of [:B,C:]) by A32,CAT_1:def 13
.= [G1/.f*t1.a,G2/.f*t2.a] by A5,A13,A9,A26,A30,A31,A21,CAT_2:29
.= (<:G1,G2:>/.f)(*)(<:t1,t2:>.a qua Morphism of [:B,C:])
by A28,A23,A29,A24,A7,A14,CAT_2:29
.= <:G1,G2:>/.f*<:t1,t2:>.a by A17,A18,CAT_1:def 13;
end;
theorem Th36:
for F1,G1 being Functor of A,B, F2,G2 being Functor of A,C st F1
is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 holds <:
F1,F2:> is_naturally_transformable_to <:G1,G2:>
proof
let F1,G1 be Functor of A,B, F2,G2 be Functor of A,C such that
A1: F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2;
F1 is_transformable_to G1 & F2 is_transformable_to G2 by A1;
hence <:F1,F2:> is_transformable_to <:G1,G2:> by Th34;
set t1 = the natural_transformation of F1,G1,t2 = the natural_transformation of
F2,G2;
take <:t1,t2:>;
thus thesis by A1,Lm4;
end;
definition
let A,B,C;
let F1,G1 be Functor of A,B, F2,G2 be Functor of A,C such that
A1: F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2;
let t1 be natural_transformation of F1,G1, t2 be natural_transformation of
F2,G2;
func <:t1,t2:> -> natural_transformation of <:F1,F2:>,<:G1,G2:> equals
:
Def12: <:t1,t2:>;
coherence
proof
<:F1,F2:> is_naturally_transformable_to <:G1,G2:> & for a,b being
Object of A st Hom(a,b) <> {} for f being Morphism of a,b
holds <:t1,t2:>.b*<:F1,F2:>/.f = <:G1,G2:>/.f*<:t1,t2:>.a by A1,Lm4,Th36;
hence thesis by NATTRA_1:def 8;
end;
end;
theorem Th37:
for F1,G1 being Functor of A,B, F2,G2 being Functor of A,C st F1
is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2 for t1
being natural_transformation of F1,G1, t2 being natural_transformation of F2,G2
holds Pr1<:t1,t2:> = t1 & Pr2<:t1,t2:> = t2
proof
let F1,G1 be Functor of A,B, F2,G2 be Functor of A,C such that
A1: F1 is_naturally_transformable_to G1 & F2 is_naturally_transformable_to G2;
A2: F1 is_transformable_to G1 & F2 is_transformable_to G2 by A1;
let t1 be natural_transformation of F1,G1, t2 be natural_transformation of
F2,G2;
reconsider s = t1 as Function of the carrier of A, the carrier' of B;
<:F1,F2:> is_naturally_transformable_to <:G1,G2:> by A1,Th36;
then
A3: <:F1,F2:> is_transformable_to <:G1,G2:>;
thus Pr1<:t1,t2:> = pr1(B,C) *(<:t1,t2:> qua transformation of <:F1,F2:>,<:
G1,G2:>) by A1,Th36,ISOCAT_1:def 7
.= pr1(B,C)* (<:t1,t2:> qua Function of the carrier of A, the carrier'
of [:B,C:]) by A3,ISOCAT_1:def 5
.= pr1(B,C)* (<:t1 qua transformation of F1,G1,t2:> qua Function of the
carrier of A, the carrier' of [:B,C:]) by A1,Def12
.= pr1(B,C)*<:s,t2:> by A2,Def11
.= pr1(the carrier' of B, the carrier' of C)*<:s,t2:>
.= t1 by FUNCT_3:62;
thus Pr2<:t1,t2:> = pr2(B,C) *(<:t1,t2:> qua transformation of <:F1,F2:>,<:
G1,G2:>) by A1,Th36,ISOCAT_1:def 7
.= pr2(B,C)* (<:t1,t2:> qua Function of the carrier of A, the carrier'
of [:B,C:]) by A3,ISOCAT_1:def 5
.= pr2(B,C)* (<:t1 qua transformation of F1,G1,t2:> qua Function of the
carrier of A, the carrier' of [:B,C:]) by A1,Def12
.= pr2(B,C)*<:s,t2:> by A2,Def11
.= pr2(the carrier' of B, the carrier' of C)*<:s,t2:>
.= t2 by FUNCT_3:62;
end;
definition
let A,B,C;
func distribute(A,B,C) -> Functor of Functors(A,[:B,C:]), [:Functors(A,B),
Functors(A,C):] means
:Def13:
for F1,F2 being Functor of A,[:B,C:] st F1
is_naturally_transformable_to F2 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]];
existence
proof
defpred P[set,set] means
for F1,F2 being Functor of A,[:B,C:],
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:]);
consider F1,F2 being Functor of A,[:B,C:], s being
natural_transformation of F1,F2 such that
A2: F1 is_naturally_transformable_to F2 and
dom(f) = F1 and
cod f = F2 and
A3: f = [[F1,F2],s] by Th6;
the carrier' of Functors(A,C) = NatTrans(A,C) & Pr2 F1
is_naturally_transformable_to Pr2 F2 by A2,ISOCAT_1:22,NATTRA_1:def 17;
then reconsider PPr2 = [[Pr2 F1, Pr2 F2],Pr2 s]
as Morphism of Functors(A,C) by NATTRA_1:32;
the carrier' of Functors(A,B) = NatTrans(A,B) & Pr1 F1
is_naturally_transformable_to Pr1 F2 by A2,ISOCAT_1:22,NATTRA_1:def 17;
then reconsider PPr1 = [[Pr1 F1, Pr1 F2],Pr1 s]
as Morphism of Functors(A,B) by NATTRA_1:32;
take g = [PPr1,PPr2];
thus P[f,g]
proof
let G1,G2 be Functor of A,[:B,C:], t be natural_transformation of G1,
G2;
assume
A4: f = [[G1,G2],t];
then [G1,G2] = [F1,F2] by A3,XTUPLE_0:1;
then
A5: G1 = F1 & G2 = F2 by XTUPLE_0:1;
t = s by A3,A4,XTUPLE_0:1;
hence thesis by A5;
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 P[f,IT.f] from
FUNCT_2:sch 3(A1);
IT is Functor of Functors(A,[:B,C:]), [:Functors(A,B),Functors(A,C):]
proof
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
proof
let c be Object of Functors(A,[:B,C:]);
reconsider F = c as Functor of A, [:B,C:] by Th5;
reconsider d2 = Pr2 F as Object of Functors(A,C) by Th5;
reconsider d1 = Pr1 F as Object of Functors(A,B) by Th5;
take [d1,d2];
Pr1 id F = id Pr1 F by ISOCAT_1:33;
then
A7: id d1 = [[Pr1 F, Pr1 F], Pr1 id F] by NATTRA_1:def 17;
Pr2 id F = id Pr2 F by ISOCAT_1:33;
then
A8: id d2 = [[Pr2 F, Pr2 F], Pr2 id F] by NATTRA_1:def 17;
id c = [[F,F], id F] by NATTRA_1:def 17;
hence IT.id c = [id d1, id d2] by A6,A7,A8
.= id [d1,d2] by CAT_2:31;
end;
A9: the carrier' of Functors(A,C) = NatTrans(A,C) by NATTRA_1:def 17;
A10: the carrier' of Functors(A,B) = NatTrans(A,B) by NATTRA_1:def 17;
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)
proof
let f be Morphism of Functors(A,[:B,C:]);
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 and
A13: cod f = F2 and
A14: f = [[F1,F2],s] by Th6;
Pr1 F1 is_naturally_transformable_to Pr1 F2 by A11,ISOCAT_1:22;
then reconsider
f1 = [[Pr1 F1, Pr1 F2],Pr1 s] as Morphism of Functors(A,B)
by A10,NATTRA_1:32;
dom f1 = Pr1 F1 & Pr1 id F1 = id Pr1 F1 by ISOCAT_1:33,NATTRA_1:33;
then
A15: id dom f1 = [[Pr1 F1, Pr1 F1], Pr1 id F1] by NATTRA_1:def 17;
Pr2 F1 is_naturally_transformable_to Pr2 F2 by A11,ISOCAT_1:22;
then reconsider
f2 = [[Pr2 F1, Pr2 F2],Pr2 s] as Morphism of Functors(A,C)
by A9,NATTRA_1:32;
dom f2 = Pr2 F1 & Pr2 id F1 = id Pr2 F1 by ISOCAT_1:33,NATTRA_1:33;
then
A16: id dom f2 = [[Pr2 F1, Pr2 F1], Pr2 id F1] by NATTRA_1:def 17;
id dom f = [[F1,F1], id F1] by A12,NATTRA_1:def 17;
hence IT.id dom f = [id dom f1, id dom f2] by A6,A15,A16
.= id [dom f1, dom f2] by CAT_2:31
.= id dom [f1,f2] by CAT_2:28
.= id dom(IT.f) by A6,A14;
cod f1 = Pr1 F2 & Pr1 id F2 = id Pr1 F2 by ISOCAT_1:33,NATTRA_1:33;
then
A17: id cod f1 = [[Pr1 F2, Pr1 F2], Pr1 id F2] by NATTRA_1:def 17;
cod f2 = Pr2 F2 & Pr2 id F2 = id Pr2 F2 by ISOCAT_1:33,NATTRA_1:33;
then
A18: id cod f2 = [[Pr2 F2, Pr2 F2], Pr2 id F2] by NATTRA_1:def 17;
id cod f = [[F2,F2], id F2] by A13,NATTRA_1:def 17;
hence IT.id cod f = [id cod f1, id cod f2] by A6,A17,A18
.= id [cod f1, cod f2] by CAT_2:31
.= id cod [f1,f2] by CAT_2:28
.= id cod(IT.f) by A6,A14;
end;
let f,g be Morphism of Functors(A,[:B,C:]) such that
A19: dom g = cod f;
consider F1,F2 being Functor of A,[:B,C:], s being
natural_transformation of F1,F2 such that
A20: F1 is_naturally_transformable_to F2 and
dom(f) = F1 and
A21: cod f = F2 and
A22: f = [[F1,F2],s] by Th6;
consider G1,G2 being Functor of A,[:B,C:], t being
natural_transformation of G1,G2 such that
A23: G1 is_naturally_transformable_to G2 and
A24: dom(g) = G1 and
cod g = G2 and
A25: g = [[G1,G2],t] by Th6;
reconsider t as natural_transformation of F2,G2 by A19,A21,A24;
A26: g(*)f = [[F1,G2],t`*`s] by A19,A21,A22,A24,A25,NATTRA_1:36;
A27: Pr2 F1 is_naturally_transformable_to Pr2 F2 by A20,ISOCAT_1:22;
Pr2 F2 is_naturally_transformable_to Pr2 G2 by A19,A21,A23,A24,
ISOCAT_1:22;
then reconsider
g2 = [[Pr2 F2, Pr2 G2],Pr2 t], f2 = [[Pr2 F1, Pr2 F2],Pr2 s]
as Morphism of Functors(A,C) by A9,A27,NATTRA_1:32;
A28: g2(*)f2 = [[Pr2 F1, Pr2 G2],(Pr2 t)`*`Pr2 s] by NATTRA_1:36
.= [[Pr2 F1, Pr2 G2],Pr2 t`*`s] by A19,A20,A21,A23,A24,ISOCAT_1:27;
A29: dom g2 = Pr2 F2 by NATTRA_1:33
.= cod f2 by NATTRA_1:33;
A30: Pr1 F1 is_naturally_transformable_to Pr1 F2 by A20,ISOCAT_1:22;
Pr1 F2 is_naturally_transformable_to Pr1 G2 by A19,A21,A23,A24,
ISOCAT_1:22;
then reconsider
g1 = [[Pr1 F2, Pr1 G2],Pr1 t], f1 = [[Pr1 F1, Pr1 F2],Pr1 s]
as Morphism of Functors(A,B) by A10,A30,NATTRA_1:32;
A31: dom g1 = Pr1 F2 by NATTRA_1:33
.= cod f1 by NATTRA_1:33;
A32: IT.f = [[[Pr1 F1, Pr1 F2],Pr1 s],[[Pr2 F1, Pr2 F2],Pr2 s]] by A6,A22;
g1(*)f1 = [[Pr1 F1, Pr1 G2],(Pr1 t)`*`Pr1 s] by NATTRA_1:36
.= [[Pr1 F1, Pr1 G2],Pr1 t`*`s] by A19,A20,A21,A23,A24,ISOCAT_1:27;
hence IT.(g(*)f) = [g1(*)f1,g2(*)f2] by A6,A28,A26
.= [g1,g2](*)[f1,f2] by A31,A29,CAT_2:29
.= (IT.g)(*)(IT.f) by A6,A19,A21,A24,A25,A32;
end;
then reconsider
IT as Functor of Functors(A,[:B,C:]), [:Functors(A,B),Functors(
A,C):];
take IT;
let F1,F2 be Functor of A,[:B,C:] such that
A33: F1 is_naturally_transformable_to F2;
let t be natural_transformation of F1,F2;
set f = [[F1,F2],t];
f in NatTrans(A,[:B,C:]) by A33,NATTRA_1:32;
then reconsider f as Morphism of Functors(A,[:B,C:]) by NATTRA_1:def 17;
thus IT.[[F1,F2],t] = IT.f
.= [[[Pr1 F1, Pr1 F2],Pr1 t],[[Pr2 F1, Pr2 F2],Pr2 t]] by A6;
end;
uniqueness
proof
let IT1,IT2 be Functor of Functors(A,[:B,C:]), [:Functors(A,B),Functors(A,
C):] such that
A34: for F1,F2 being Functor of A,[:B,C:] st F1
is_naturally_transformable_to F2 for t being natural_transformation of F1,F2
holds IT1.[[F1,F2],t] = [[[Pr1 F1, Pr1 F2],Pr1 t],[[Pr2 F1, Pr2 F2],Pr2 t]]
and
A35: for F1,F2 being Functor of A,[:B,C:] st F1
is_naturally_transformable_to F2 for t being natural_transformation of F1,F2
holds IT2.[[F1,F2],t] = [[[Pr1 F1, Pr1 F2],Pr1 t],[[Pr2 F1, Pr2 F2],Pr2 t]];
now
let f be Morphism of Functors(A,[:B,C:]);
consider F1,F2 being Functor of A,[:B,C:], s being
natural_transformation of F1,F2 such that
A36: F1 is_naturally_transformable_to F2 and
dom(f) = F1 and
cod f = F2 and
A37: f = [[F1,F2],s] by Th6;
thus IT1.f = [[[Pr1 F1, Pr1 F2],Pr1 s],[[Pr2 F1, Pr2 F2],Pr2 s]] by A34
,A36,A37
.= IT2.f by A35,A36,A37;
end;
hence IT1 = IT2 by FUNCT_2:63;
end;
end;
registration
let A,B,C;
cluster distribute(A,B,C) -> isomorphic;
coherence
proof
thus distribute(A,B,C) is one-to-one
proof
let x1,x2 be object;
assume x1 in dom distribute(A,B,C);
then reconsider f1 = x1 as Morphism of Functors(A,[:B,C:]);
consider F1,F2 being Functor of A,[:B,C:], s being natural_transformation
of F1,F2 such that
A1: F1 is_naturally_transformable_to F2 and
dom(f1) = F1 and
cod f1 = F2 and
A2: f1 = [[F1,F2],s] by Th6;
assume x2 in dom distribute(A,B,C);
then reconsider f2 = x2 as Morphism of Functors(A,[:B,C:]);
consider G1,G2 being Functor of A,[:B,C:], t being natural_transformation
of G1,G2 such that
A3: G1 is_naturally_transformable_to G2 and
dom(f2) = G1 and
cod f2 = G2 and
A4: f2 = [[G1,G2],t] by Th6;
assume distribute(A,B,C).x1 = distribute(A,B,C).x2;
then
A5: [[[Pr1 F1,Pr1 F2],Pr1 s],[[Pr2 F1, Pr2 F2],Pr2 s]] = distribute(A,B,C)
.[[G1,G2],t] by A1,A2,A4,Def13
.= [[[Pr1 G1,Pr1 G2],Pr1 t],[[Pr2 G1, Pr2 G2],Pr2 t]] by A3,Def13;
then
A6: [[Pr1 F1,Pr1 F2],Pr1 s] = [[Pr1 G1,Pr1 G2],Pr1 t] by XTUPLE_0:1;
A7: [[Pr2 F1,Pr2 F2],Pr2 s] = [[Pr2 G1,Pr2 G2],Pr2 t] by A5,XTUPLE_0:1;
then
A8: Pr2 s = Pr2 t by XTUPLE_0:1;
A9: [Pr2 F1,Pr2 F2] = [Pr2 G1,Pr2 G2] by A7,XTUPLE_0:1;
then
A10: Pr2 F1 = Pr2 G1 by XTUPLE_0:1;
A11: [Pr1 F1,Pr1 F2] = [Pr1 G1,Pr1 G2] by A6,XTUPLE_0:1;
then Pr1 F1 = Pr1 G1 by XTUPLE_0:1;
then
A12: F1 = G1 by A10,Th30;
Pr1 s = Pr1 t by A6,XTUPLE_0:1;
then
A13: s = t by A1,A3,A8,Th31;
A14: Pr2 F2 = Pr2 G2 by A9,XTUPLE_0:1;
Pr1 F2 = Pr1 G2 by A11,XTUPLE_0:1;
hence thesis by A2,A4,A14,A13,A12,Th30;
end;
thus rng distribute(A,B,C) c= the carrier' of [:Functors(A,B),Functors(A,C)
:];
let o be object;
assume o in the carrier' of [:Functors(A,B),Functors(A,C):];
then consider
o1 being (Morphism of Functors(A,B)), o2 being Morphism of Functors
(A,C) such that
A15: o = [o1,o2] by CAT_2:27;
consider G1,G2 being Functor of A,C, t being natural_transformation of G1,G2
such that
A16: G1 is_naturally_transformable_to G2 and
dom o2 = G1 and
cod o2 = G2 and
A17: o2 = [[G1,G2],t] by Th6;
consider F1,F2 being Functor of A,B, s being natural_transformation of F1,F2
such that
A18: F1 is_naturally_transformable_to F2 and
dom o1 = F1 and
cod o1 = F2 and
A19: o1 = [[F1,F2],s] by Th6;
set f = [[<:F1,G1:>,<:F2,G2:>],<:s,t:>];
A20: <:F1,G1:> is_naturally_transformable_to <:F2,G2:> by A18,A16,Th36;
then f in NatTrans(A,[:B,C:]) by NATTRA_1:32;
then reconsider f as Morphism of Functors(A,[:B,C:]) by NATTRA_1:def 17;
A21: Pr1<:F1,G1:> = F1 & Pr1<:F2,G2:> = F2 by Th29;
A22: Pr2<:F1,G1:> = G1 & Pr2<:F2,G2:> = G2 by Th29;
Pr1<:s,t:> = s & Pr2<:s,t:> = t by A18,A16,Th37;
then distribute(A,B,C).f = o by A15,A19,A17,A20,A21,A22,Def13;
hence thesis by FUNCT_2:112;
end;
end;
theorem
Functors(A,[:B,C:]) ~= [:Functors(A,B),Functors(A,C):]
proof
take distribute(A,B,C);
thus thesis;
end;