Copyright (c) 1992 Association of Mizar Users
environ
vocabulary FUNCT_1, FUNCT_2, FUNCT_5, RELAT_1, BOOLE, FUNCT_3, CAT_1,
NATTRA_1, CAT_2, FINSEQ_2, FUNCOP_1, PARTFUN1, BORSUK_1, ISOCAT_2;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELSET_1, FUNCT_1,
FUNCT_2, FUNCT_3, FUNCT_5, FRAENKEL, CAT_1, CAT_2, NATTRA_1, ISOCAT_1;
constructors DOMAIN_1, ISOCAT_1, MEMBERED, XBOOLE_0;
clusters RELSET_1, SUBSET_1, MEMBERED, ZFMISC_1, XBOOLE_0;
requirements SUBSET, BOOLE;
definitions TARSKI, FUNCT_1, NATTRA_1, ISOCAT_1, XBOOLE_0;
theorems FUNCT_2, CAT_1, TARSKI, ZFMISC_1, FUNCT_1, DOMAIN_1, CAT_2, FUNCT_3,
FUNCOP_1, NATTRA_1, ISOCAT_1, FUNCT_5, RELSET_1, XBOOLE_1;
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;
coherence
proof
A1: rng f c= Funcs(B,C) by RELSET_1:12;
then A2: dom uncurry f = [:dom f,B:] by FUNCT_5:33 .= [:A,B:] by FUNCT_2:def 1
;
rng uncurry f c= C by A1,FUNCT_5:48;
hence thesis by A2,FUNCT_2:def 1,RELSET_1:11;
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) & B <> {} by RELSET_1:12;
hence curry uncurry f = f by FUNCT_5:55;
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 (uncurry f).[a,b] = f.a.b by FUNCT_5:45;
end;
theorem Th3:
for x being set, A being non empty set
for f,g being Function of {x}, A st f.x = g.x holds f = g
proof let x be set, A be non empty set;
let f,g be Function of {x}, A such that
A1: f.x = g.x;
now let y be set;
assume y in {x};
then y = x by TARSKI:def 1;
hence f.y = g.y by A1;
end;
hence f = g by FUNCT_2:18;
end;
theorem Th4:
for A,B being non empty set, x being Element of A,
f being Function of A,B holds f.x in rng f
proof let A,B be non empty set, x be Element of A,
f be Function of A,B;
dom f = A by FUNCT_2:def 1;
hence f.x in rng f by FUNCT_1:def 5;
end;
theorem Th5:
for A,B,C being non empty set, f,g being Function of A,[:B,C:]
st pr1(B,C)*f = pr1(B,C)*g & pr2(B,C)*f = pr2(B,C)*g
holds f = g
proof let A,B,C be non empty set, f,g be Function of A,[:B,C:] such that
A1: pr1(B,C)*f = pr1(B,C)*g & pr2(B,C)*f = pr2(B,C)*g;
now let a be Element of A;
consider b1 being Element of B, c1 being Element of C such that
A2: f.a = [b1,c1] by DOMAIN_1:9;
consider b2 being Element of B, c2 being Element of C such that
A3: g.a = [b2,c2] by DOMAIN_1:9;
A4: pr1(B,C).[b1,c1] = b1 & pr1(B,C).[b2,c2] = b2 &
pr2(B,C).[b1,c1] = c1 & pr2(B,C).[b2,c2] = c2 by FUNCT_3:def 5,def 6;
pr1(B,C).(f.a) = (pr1(B,C)*f).a & pr2(B,C).(f.a) = (pr2(B,C)*f).a &
pr1(B,C).(g.a) = (pr1(B,C)*g).a & pr2(B,C).(g.a) = (pr2(B,C)*g).a
by FUNCT_2:21;
hence f.a = g.a by A1,A2,A3,A4;
end;
hence f = g by FUNCT_2:113;
end;
:: Auxiliary category theory facts
reserve A,B,C for Category,
F,F1 for Functor of A,B;
theorem Th6:
for f being Morphism of A holds (id cod f)*f = f
proof let f be Morphism of A;
reconsider f' = f as Morphism of dom f, cod f by CAT_1:22;
A1: Hom(dom f, cod f) <> {} & Hom(cod f,cod f) <> {} by CAT_1:19,56;
hence (id cod f)*f = (id cod f)*f' by CAT_1:def 13 .= f by A1,CAT_1:57;
end;
theorem Th7:
for f being Morphism of A holds f*(id dom f) = f
proof let f be Morphism of A;
reconsider f' = f as Morphism of dom f, cod f by CAT_1:22;
A1: Hom(dom f, cod f) <> {} & Hom(dom f,dom f) <> {} by CAT_1:19,56;
hence f*(id dom f) = f'*(id dom f) by CAT_1:def 13 .= f by A1,CAT_1:58;
end;
reserve o,m for set;
reserve t for natural_transformation of F,F1;
theorem Th8:
o is Object of Functors(A,B) iff o is Functor of A,B
proof
the Objects of Functors(A,B) = Funct(A,B) by NATTRA_1:def 18;
hence thesis by CAT_2:def 2;
end;
theorem Th9:
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:19,22;
then consider F,F1,t such that
A1: dom m = F & cod m = F1 and
A2: m = [[F,F1],t] by NATTRA_1:40;
take F,F1,t;
the Morphisms of Functors(A,B) = NatTrans(A,B) by NATTRA_1:def 18;
hence F is_naturally_transformable_to F1 by A2,NATTRA_1:35;
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: 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
A2: x = [[F1,F2],t] & 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 F1',F2' be Functor of A,B, t' be natural_transformation of F1',F2'
; assume
A3: x = [[F1',F2'],t'];
then [F1,F2] = [F1',F2'] & t = t' by A2,ZFMISC_1:33;
then F1 = F1' & F2 = F2' by ZFMISC_1:33;
hence b = t'.a by A2,A3,ZFMISC_1:33;
end;
end;
consider f being Function of NatTrans(A,B), the Morphisms of B such that
A4: for x being Element of NatTrans(A,B) holds
P[x,f.x] from FuncExD(A1);
A5: the Morphisms of Functors(A,B) = NatTrans(A,B) by NATTRA_1:def 18;
A6: now let c be Object of Functors(A,B);
reconsider F = c as Functor of A,B by Th8;
take d = F.a;
A7: [[F,F],id F] is Morphism of Functors(A,B) by A5,NATTRA_1:def 16;
thus f.((the Id of Functors(A,B)).c) = f.id c by CAT_1:def 5
.= f.[[F,F],id F] by NATTRA_1:def 18
.= (id F).a by A4,A5,A7
.= id d by NATTRA_1:21
.= (the Id of B).d by CAT_1:def 5;
end;
A8: now let m be Morphism of Functors(A,B);
reconsider m' = m as Element of NatTrans(A,B) by NATTRA_1:def 18;
consider F,F1,t such that
A9: F is_naturally_transformable_to F1 and
A10: dom m = F & cod m = F1 and
A11: m = [[F,F1],t] by Th9;
A12: [[F,F],id F] is Morphism of Functors(A,B) by A5,NATTRA_1:def 16;
A13: [[F1,F1],id F1] is Morphism of Functors(A,B) by A5,NATTRA_1:def 16;
A14: Hom(F.a,F1.a) <> {} by A9,ISOCAT_1:30;
thus f.((the Id of Functors(A,B)).((the Dom of Functors(A,B)).m)) =
f.((the Id of Functors(A,B)).(dom m)) by CAT_1:def 2
.= f.(id dom m) by CAT_1:def 5
.= f.[[F,F],id F] by A10,NATTRA_1:def 18
.= (id F).a by A4,A5,A12
.= id(F.a) by NATTRA_1:21
.= id dom(t.a) by A14,CAT_1:23
.= id dom(f.m') by A4,A11
.= (the Id of B).(dom(f.m')) by CAT_1:def 5
.= (the Id of B).((the Dom of B).(f.m)) by CAT_1:def 2;
thus f.((the Id of Functors(A,B)).((the Cod of Functors(A,B)).m)) =
f.((the Id of Functors(A,B)).(cod m)) by CAT_1:def 3
.= f.(id cod m) by CAT_1:def 5
.= f.[[F1,F1],id F1] by A10,NATTRA_1:def 18
.= (id F1).a by A4,A5,A13
.= id(F1.a) by NATTRA_1:21
.= id cod(t.a) by A14,CAT_1:23
.= id cod(f.m') by A4,A11
.= (the Id of B).(cod(f.m')) by CAT_1:def 5
.= (the Id of B).((the Cod of B).(f.m)) by CAT_1:def 3;
end;
now let m1,m2 be Morphism of Functors(A,B);
consider F,F1,t such that
A15: F is_naturally_transformable_to F1 and
dom m1 = F & cod m1 = F1 and
A16: m1 = [[F,F1],t] by Th9;
consider F1',F2 being Functor of A,B,
t' being natural_transformation of F1',F2 such that
A17: F1' is_naturally_transformable_to F2 and
dom m2 = F1' & cod m2 = F2 and
A18: m2 = [[F1',F2],t'] by Th9;
assume
A19: [m2,m1] in dom(the Comp of Functors(A,B));
A20: F1' = dom m2 by A18,NATTRA_1:39 .= cod m1 by A19,CAT_1:40
.= F1 by A16,NATTRA_1:39;
then reconsider t' as natural_transformation of F1,F2;
A21: Hom(F.a,F1.a) <> {} & Hom(F1.a,F2.a) <> {} by A15,A17,A20,ISOCAT_1:30;
reconsider m1'=m1, m2'=m2 as Element of NatTrans(A,B) by NATTRA_1:def 18;
A22: f.m1' = t.a & f.m2' = t'.a by A4,A16,A18,A20;
then cod(f.m1') = F1.a & dom(f.m2') = F1.a by A21,CAT_1:23;
then A23: [f.m2,f.m1] in dom the Comp of B by CAT_1:40;
A24: m2*m1= [[F,F2],t'`*`t] by A16,A18,A20,NATTRA_1:42;
thus f.((the Comp of Functors(A,B)).[m2,m1]) = f.(m2*m1) by A19,CAT_1:def
4
.= (t'`*`t).a by A4,A5,A24
.= (t'.a)*(t.a) by A15,A17,A20,NATTRA_1:27
.= (t'.a)*(t.a qua Morphism of B) by A21,CAT_1:def 13
.= (the Comp of B).[f.m2,f.m1] by A22,A23,CAT_1:def 4;
end;
then reconsider f as Functor of Functors(A,B),B by A5,A6,A8,CAT_1:def 18;
take f;
let F1,F2 be Functor of A,B, t be natural_transformation of F1,F2;
A25: the Morphisms of Functors(A,B) = NatTrans(A,B) by NATTRA_1:def 18;
assume F1 is_naturally_transformable_to F2;
then [[F1,F2],t] is Morphism of Functors(A,B) by A25,NATTRA_1:35;
hence thesis by A4,A25;
end;
uniqueness
proof let f1,f2 be Functor of Functors(A,B), B such that
A26: 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
A27: 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 Morphisms of Functors(A,B) = NatTrans(A,B) by NATTRA_1:def 18;
then consider F1,F2 being Functor of A,B,
t being natural_transformation of F1,F2 such that
A28: c = [[F1,F2],t] and
A29: F1 is_naturally_transformable_to F2 by NATTRA_1:def 15;
thus f1.c = t.a by A26,A28,A29 .= f2.c by A27,A28,A29;
end;
hence f1 = f2 by FUNCT_2:113;
end;
end;
Lm1:
the Objects of 1Cat(o,m) = {o} & the Morphisms of 1Cat(o,m) = {m}
proof
now let a be set;
thus a in the Objects of 1Cat(o,m) implies a=o by CAT_1:34;
o is Object of 1Cat(o,m) by CAT_1:32;
hence a=o implies a in the Objects of 1Cat(o,m);
end;
hence the Objects of 1Cat(o,m) = {o} by TARSKI:def 1;
now let f be set;
thus f in the Morphisms of 1Cat(o,m) implies f=m by CAT_1:35;
m is Morphism of 1Cat(o,m) by CAT_1:33;
hence f=m implies f in the Morphisms of 1Cat(o,m);
end;
hence thesis by TARSKI:def 1;
end;
canceled;
theorem
Functors(1Cat(o,m),A) ~= A
proof
reconsider a = o as Object of 1Cat(o,m) by CAT_1:32;
take F = a |-> A;
now let x,y be set;
A1: the Morphisms of Functors(1Cat(o,m),A) = NatTrans(1Cat(o,m),A)
by NATTRA_1:def 18;
assume x in the Morphisms 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] & F1 is_naturally_transformable_to F2
by A1,NATTRA_1:def 16;
assume y in the Morphisms 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
A3: y = [[F1',F2'],t'] & F1' is_naturally_transformable_to F2'
by A1,NATTRA_1:def 16;
A4: the Objects of 1Cat(o,m) = {o} & the Morphisms of 1Cat(o,m) = {m} by Lm1;
then reconsider s=t,s'=t' as Function of {a}, the Morphisms of A;
reconsider G1=F1, G1'=F1', G2=F2, G2'=F2' as
Function of {m}, the Morphisms of A by A4;
A5: F1 is_transformable_to F2 & F1' is_transformable_to F2'
by A2,A3,NATTRA_1:def 7;
assume F.x = F.y;
then A6: t.a = F.y by A2,Def1 .= t'.a by A3,Def1;
then A7:
s.a = t'.a by A5,NATTRA_1:def 5 .= s'.a by A5,NATTRA_1:def 5;
A8: id a = m by CAT_1:35;
Hom(F1.a,F2.a) <> {} & Hom(F1'.a,F2'.a) <> {} by A5,NATTRA_1:def 2;
then A9: F1.a = F1'.a & F2.a = F2'.a by A6,CAT_1:24;
then A10: G1.id a = id(F1'.a) by CAT_1:108 .= G1'.id a by CAT_1:108;
G2.id a = id(F2'.a) by A9,CAT_1:108 .= G2'.id a by CAT_1:108;
then F1 = F1' & F2 = F2' by A8,A10,Th3;
hence x = y by A2,A3,A7,Th3;
end;
hence F is one-to-one by FUNCT_2:25;
thus rng F c= the Morphisms of A by RELSET_1:12;
let x be set;
assume x in the Morphisms of A;
then reconsider f = x as Morphism of A;
A11: dom({m} --> id dom f) = {m} by FUNCOP_1:19
.= the Morphisms of 1Cat(o,m) by Lm1;
A12: dom({m} --> id cod f) = {m} by FUNCOP_1:19
.= the Morphisms of 1Cat(o,m) by Lm1;
A13:rng({m} --> id dom f) c= {id dom f} by FUNCOP_1:19;
{id dom f} c= the Morphisms of A by ZFMISC_1:37;
then A14: rng({m} --> id dom f) c= the Morphisms of A by A13,XBOOLE_1:1;
A15: rng({m} --> id cod f) c= {id cod f} by FUNCOP_1:19;
{id cod f} c= the Morphisms of A by ZFMISC_1:37;
then rng({m} --> id cod f) c= the Morphisms of A by A15,XBOOLE_1:1;
then reconsider F1 = {m} --> id dom f, F2 = {m} --> id cod f
as Function of the Morphisms of 1Cat(o,m),the Morphisms of A
by A11,A12,A14,FUNCT_2:def 1,RELSET_1:11;
A16: for g being Morphism of 1Cat(o,m) holds F1.g = id dom f & F2.g = id cod f
proof let g be Morphism of 1Cat(o,m);
g = m by CAT_1:35;
then g in {m} by TARSKI:def 1;
hence F1.g = id dom f & F2.g = id cod f by FUNCOP_1:13;
end;
A17: now let c be Object of 1Cat(o,m);
take d = dom f; thus F1.(id c) = id d by A16;
end;
A18: now let g be Morphism of 1Cat(o,m);
thus F1.(id dom g) = id dom f by A16 .= id dom id dom f by CAT_1:44
.= id dom (F1.g) by A16;
thus F1.(id cod g) = id dom f by A16 .= id cod id dom f by CAT_1:44
.= id cod (F1.g) by A16;
end;
A19: now let h,g be Morphism of 1Cat(o,m) such that dom g = cod h;
A20: Hom(dom f,dom f) <> {} by CAT_1:56;
thus F1.(g*h) = id dom f by A16 .= (id dom f)*(id dom f) by CAT_1:59
.= (id dom f)*(id dom f qua Morphism of A)by A20,CAT_1:def 13
.= (id dom f)*(F1.h)by A16.= (F1.g)*(F1.h)by A16;
end;
A21: now let c be Object of 1Cat(o,m);
take d = cod f; thus F2.(id c) = id d by A16;
end;
A22: now let g be Morphism of 1Cat(o,m);
thus F2.(id dom g) = id cod f by A16 .= id dom id cod f by CAT_1:44
.= id dom (F2.g) by A16;
thus F2.(id cod g) = id cod f by A16 .= id cod id cod f by CAT_1:44
.= id cod (F2.g) by A16;
end;
now let h,g be Morphism of 1Cat(o,m) such that dom g = cod h;
A23: Hom(cod f,cod f) <> {} by CAT_1:56;
thus F2.(g*h) = id cod f by A16 .= (id cod f)*(id cod f) by CAT_1:59
.= (id cod f)*(id cod f qua Morphism of A)by A23,CAT_1:def 13
.= (id cod f)*(F2.h)by A16.= (F2.g)*(F2.h)by A16;
end;
then reconsider F1, F2 as Functor of 1Cat(o,m),A by A17,A18,A19,A21,A22,
CAT_1:96;
A24: 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);
id b = m by CAT_1:35;
then id b in {m} by TARSKI:def 1;
then F1.(id b qua Morphism of 1Cat(o,m)) = id dom f &
F2.(id b qua Morphism of 1Cat(o,m)) = id cod f by FUNCOP_1:13;
then id(F1.b) = id dom f & id(F2.b) = id cod f by CAT_1:108;
hence F1.b = dom f & F2.b = cod f by CAT_1:45;
end;
A25:now let b be Object of 1Cat(o,m);
F1.b = dom f & F2.b = cod f by A24;
hence Hom(F1.b,F2.b) <> {} by CAT_1:19;
end;
then A26:F1 is_transformable_to F2 by NATTRA_1:def 2;
A27:dom({a} --> f) = {a} by FUNCOP_1:19 .= the Objects of 1Cat(o,m) by Lm1;
A28:rng({a} --> f) c= {f} by FUNCOP_1:19;
{f} c= the Morphisms of A by ZFMISC_1:37;
then rng({a} --> f) c= the Morphisms of A by A28,XBOOLE_1:1;
then reconsider t = {a} --> f as
Function of the Objects of 1Cat(o,m), the Morphisms of A
by A27,FUNCT_2:def 1,RELSET_1:11;
now let b be Object of 1Cat(o,m);
b = a by CAT_1:34;
then b in {a} by TARSKI:def 1;
then A29: t.b = f by FUNCOP_1:13;
F1.b = dom f & F2.b = cod f by A24;
then t.b in Hom(F1.b,F2.b) by A29,CAT_1:18;
hence t.b is Morphism of F1.b,F2.b by CAT_1:def 7;
end;
then reconsider t as transformation of F1,F2 by A26,NATTRA_1:def 3;
A30: for b being Object of 1Cat(o,m) holds t.b = f
proof let b be Object of 1Cat(o,m);
b = a by CAT_1:34;
then b in {a} by TARSKI:def 1;
hence f = ({a} --> f).b by FUNCOP_1:13 .= t.b by A26,NATTRA_1:def 5;
end;
A31:now let b1,b2 be Object of 1Cat(o,m) such that
A32: Hom(b1,b2) <> {};
let g be Morphism of b1,b2;
A33: t.b1 = f by A30;
A34: t.b2 = f by A30;
A35: g = m by CAT_1:35;
A36: m in {m} by TARSKI:def 1;
A37: Hom(F1.b1,F2.b1) <> {} & Hom(F2.b1,F2.b2) <> {} by A25,A32,CAT_1:124;
A38: Hom(F1.b2,F2.b2) <> {} & Hom(F1.b1,F1.b2) <> {} by A25,A32,CAT_1:124;
A39: F2.g = F2.m by A32,A35,NATTRA_1:def 1 .= id cod f by A36,FUNCOP_1:13;
A40: F1.g = F1.m by A32,A35,NATTRA_1:def 1 .= id dom f by A36,FUNCOP_1:13;
thus t.b2*F1.g = f*F1.g by A34,A38,CAT_1:def 13
.= f by A40,CAT_1:47
.= F2.g*f by A39,CAT_1:46
.= F2.g*t.b1 by A33,A37,CAT_1:def 13;
end;
A41: F1 is_naturally_transformable_to F2
proof thus F1 is_transformable_to F2 by A25,NATTRA_1:def 2
; thus thesis by A31; end;
then reconsider t as natural_transformation of F1,F2 by A31,NATTRA_1:def 8;
[[F1,F2],t] in NatTrans(1Cat(o,m),A) by A41,NATTRA_1:def 16;
then A42:[[F1,F2],t] in the Morphisms of Functors(1Cat(o,m),A) by NATTRA_1:def
18;
F.[[F1,F2],t] = t.a by A41,Def1 .= f by A30;
hence x in rng F by A42,FUNCT_2:6;
end;
begin :: The isomorphism between C^(A x B) and C^(A^B)
theorem Th12:
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_1:def 20 .= (Obj F).[a,b] by CAT_2:48
.= F.[a,b] by CAT_1:def 20;
end;
theorem Th13:
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:42;
hence thesis by ZFMISC_1:113;
end;
theorem Th14:
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]) <> {};
then A2: Hom(a1,a2) <> {} & Hom(b1,b2) <> {} by Th13;
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 [f,g] in Hom([a1,b1],[a2,b2]) &
Hom([a1,b1],[a2,b2]) = [:Hom(a1,a2),Hom(b1,b2):]
by A1,CAT_1:def 7,CAT_2:42;
then f in Hom(a1,a2) & g in Hom(b1,b2) by ZFMISC_1:106;
hence f is Morphism of a1,a2 & g is Morphism of b1,b2 by CAT_1:def 7;
end;
thus thesis by A2,CAT_2:43;
end;
theorem Th15:
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 by NATTRA_1:def 7;
let u be natural_transformation of F1,F2, a be Object of A;
the Objects of [:A,B:] = [:the Objects of A, the Objects of B:] by CAT_2:
33
;
then reconsider t=u as
Function of [:the Objects of A, the Objects of B:], the Morphisms 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 Th12;
hence Hom((F1?-a).b,(F2?-a).b) <> {} by A2,NATTRA_1:def 2;
end;
A4: now let b be Object of B;
A5: (curry t).a.b = t.[a,b] by CAT_2:3 .= u.[a,b] by A2,NATTRA_1:def 5;
A6: (F1?-a).b = F1.[a,b] & (F2?-a).b = F2.[a,b] by Th12;
Hom((F1?-a).b,(F2?-a).b) <> {} by A3,NATTRA_1:def 2;
hence (curry t).a.b in Hom((F1?-a).b,(F2?-a).b) by A5,A6,CAT_1:def 7;
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 7;
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) <> {};
let f be Morphism of b1,b2;
A9: Hom(a,a) <> {} by CAT_1:56;
then reconsider g = [id a,f] as Morphism of [a,b1],[a,b2] by A8,CAT_2:43;
A10: Hom([a,b1],[a,b2]) <> {} by A8,A9,Th13;
then A11: Hom(F1.[a,b1],F1.[a,b2]) <> {} by CAT_1:126;
A12: Hom(F1.[a,b2],F2.[a,b2]) <> {} by A2,NATTRA_1:def 2;
A13: Hom((F1?-a).b1,(F1?-a).b2) <> {} by A8,CAT_1:126;
A14: (F1?-a).b2 = F1.[a,b2] & (F2?-a).b2 = F2.[a,b2] by Th12;
A15: Hom(F1.[a,b1],F2.[a,b1]) <> {} by A2,NATTRA_1:def 2;
A16: Hom(F2.[a,b1],F2.[a,b2]) <> {} by A10,CAT_1:126;
A17: Hom((F2?-a).b1,(F2?-a).b2) <> {} by A8,CAT_1:126;
A18: (F1?-a).b1 = F1.[a,b1] & (F2?-a).b1 = F2.[a,b1] by Th12;
A19: s.b1 = (curry t).a.b1 by A3,NATTRA_1:def 5 .= t.[a,b1] by CAT_2:3
.= u.[a,b1] by A2,NATTRA_1:def 5;
s.b2 = (curry t).a.b2 by A3,NATTRA_1:def 5 .= t.[a,b2] by CAT_2:3
.= u.[a,b2] by A2,NATTRA_1:def 5;
hence s.b2*(F1?-a).f
= u.[a,b2]*(F1?-a).f by A12,A13,A14,CAT_1:def 13
.= u.[a,b2]*(F1?-a).(f qua Morphism of B) by A8,NATTRA_1:def 1
.= u.[a,b2]*F1.[id a,f] by CAT_2:47
.= u.[a,b2]*(F1.g qua Morphism of C) by A10,NATTRA_1:def 1
.= u.[a,b2]*F1.g by A11,A12,CAT_1:def 13
.= F2.g*u.[a,b1] by A1,A10,NATTRA_1:def 8
.= (F2.g qua Morphism of C)*u.[a,b1] by A15,A16,CAT_1:def 13
.= F2.[id a,f]*u.[a,b1] by A10,NATTRA_1:def 1
.= (F2?-a).(f qua Morphism of B)*u.[a,b1] by CAT_2:47
.= ((F2?-a).f qua Morphism of C)*s.b1 by A8,A19,NATTRA_1:def 1
.= (F2?-a).f*s.b1 by A15,A17,A18,CAT_1:def 13;
end;
hence F1?-a is_naturally_transformable_to F2?-a by A3,NATTRA_1:def 7;
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 Morphisms of B,the Morphisms of C equals
:Def2: (curry F).f;
coherence
proof
the Morphisms of [:A,B:] = [:the Morphisms of A, the Morphisms of B:]
by CAT_2:33;
then reconsider F as
Function of [:the Morphisms of A,the Morphisms of B:], the Morphisms of C;
(curry F).f is Function of the Morphisms of B,the Morphisms of C;
hence thesis;
end;
end;
theorem Th16:
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:106;
hence [f,g] in Hom([a1,b1],[a2,b2]) by CAT_2:42;
end;
theorem Th17:
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)*the Id of B is natural_transformation of F?-a,F?-b
proof let F be Functor of [:A,B:], C;
the Morphisms of [:A,B:] = [:the Morphisms of A, the Morphisms of B:]
by CAT_2:33;
then reconsider G = F as
Function of [:the Morphisms of A,the Morphisms of B:], the Morphisms of C;
let a1,a2 be Object of A such that
A1: Hom(a1,a2) <> {};
let f be Morphism of a1,a2;
reconsider Ff = (curry G).(f qua Morphism of A)
as Function of the Morphisms of B,the Morphisms of C;
reconsider FfI = curry(F,f)*the Id of B
as Function of the Objects of B, the Morphisms of C;
A2:now let b be Object of B;
A3: (F?-a1).b = F.[a1,b] & (F?-a2).b = F.[a2,b] by Th12;
f in Hom(a1,a2) & id b in Hom(b,b) by A1,CAT_1:55,def 7;
then [f,id b] in Hom([a1,b],[a2,b]) by Th16;
then F.[f,id b] in Hom(F.[a1,b],F.[a2,b]) by CAT_1:123;
then Ff.(id b qua Morphism of B) in Hom((F?-a1).b,(F?-a2).b)
by A3,CAT_2:3;
then curry(F,f).id b in Hom((F?-a1).b,(F?-a2).b) by Def2;
then curry(F,f).((the Id of B).b) in Hom((F?-a1).b,(F?-a2).b)
by CAT_1:def 5;
hence (curry(F,f)*the Id of B).b in Hom((F?-a1).b,(F?-a2).b) by FUNCT_2:21
;
end;
A4: F?-a1 is_transformable_to F?-a2
proof let b be Object of B;
thus Hom((F?-a1).b,(F?-a2).b) <> {} by A2;
end;
now let b be Object of B;
(curry(F,f)*the Id of 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 7;
end;
then reconsider t = curry(F,f)*the Id of B as transformation of F?-a1,F?-a2
by A4,NATTRA_1:def 3;
A5:now let b1,b2 be Object of B such that
A6: Hom(b1,b2) <> {};
A7: Hom(a1,a1) <> {} & Hom(a2,a2) <> {} & Hom(b1,b1) <> {} & Hom(b2,b2) <> {}
by CAT_1:56;
A8: Hom((F?-a1).b1,(F?-a2).b1) <> {} by A4,NATTRA_1:def 2;
A9: Hom((F?-a1).b2,(F?-a2).b2) <> {} by A4,NATTRA_1:def 2;
A10: Hom((F?-a1).b1,(F?-a1).b2) <> {} by A6,CAT_1:126;
A11: Hom((F?-a2).b1,(F?-a2).b2) <> {} by A6,CAT_1:126;
let g be Morphism of b1,b2;
A12: t.b2 = FfI.b2 & t.b1 = FfI.b1 by A4,NATTRA_1:def 5;
reconsider ida1 = id a1, ida2 = id a2 as Morphism of A;
reconsider idb1 = id b1, idb2 = id b2 as Morphism of B;
A13: dom id a2 = a2 by CAT_1:44 .= cod f by A1,CAT_1:23;
A14: dom g = b1 by A6,CAT_1:23 .= cod id b1 by CAT_1:44;
A15: cod id a1 = a1 by CAT_1:44 .= dom f by A1,CAT_1:23;
A16: dom id b2 = b2 by CAT_1:44 .= cod g by A6,CAT_1:23;
A17: dom[id a2,g] = [cod f,dom g] by A13,CAT_2:38 .= cod[f,id b1] by A14,CAT_2:
38;
A18: cod[id a1,g] = [dom f,cod g] by A15,CAT_2:38 .= dom[f,id b2] by A16,CAT_2:
38;
A19: [f*ida1,idb2*g]
= [f*ida1,id b2*g] by A6,A7,CAT_1:def 13
.= [f*ida1,g] by A6,CAT_1:57
.= [f*id a1,g] by A1,A7,CAT_1:def 13
.= [f,g] by A1,CAT_1:58
.= [id a2*f,g] by A1,CAT_1:57
.= [ida2*f,g] by A1,A7,CAT_1:def 13
.= [ida2*f,g*id b1] by A6,CAT_1:58
.= [ida2*f,g*idb1] by A6,A7,CAT_1:def 13;
thus t.b2*(F?-a1).g = FfI.b2*(F?-a1).g by A9,A10,A12,CAT_1:def 13
.= (curry(F,f).((the Id of B).b2))*(F?-a1).g by FUNCT_2:21
.= curry(F,f).(id b2)*(F?-a1).g by CAT_1:def 5
.= (Ff.(id b2 qua Morphism of B))*(F?-a1).g by Def2
.= (F.[f,id b2])*(F?-a1).g by CAT_2:3
.= (F.[f,id b2])*(F?-a1).(g qua Morphism of B) by A6,NATTRA_1:def 1
.= (F.[f,id b2])*(F.[id a1,g]) by CAT_2:47
.= F.([f,id b2]*[id a1,g]) by A18,CAT_1:99
.= F.[f*ida1,idb2*g] by A15,A16,CAT_2:39
.= F.([ida2,g]*[f,idb1]) by A13,A14,A19,CAT_2:39
.= F.[id a2,g]*(F.[f,id b1]) by A17,CAT_1:99
.= (F?-a2).(g qua Morphism of B)*(F.[f,id b1]) by CAT_2:47
.= (F?-a2).g*(F.[f,id b1]) by A6,NATTRA_1:def 1
.= (F?-a2).g*(Ff.(id b1 qua Morphism of B)) by CAT_2:3
.= (F?-a2).g*(curry(F,f).(id b1)) by Def2
.= (F?-a2).g*(curry(F,f).((the Id of B).b1)) by CAT_1:def 5
.= (F?-a2).g*(FfI.b1) by FUNCT_2:21
.= (F?-a2).g*t.b1 by A8,A11,A12,CAT_1:def 13;
end;
hence F?-a1 is_naturally_transformable_to F?-a2 by A4,NATTRA_1:def 7;
hence thesis by A5,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
:Def3: curry(F,f)*the Id of B;
coherence
proof Hom(dom f, cod f) <> {} & f is Morphism of dom f, cod f by CAT_1:19,22
;
hence thesis by Th17;
end;
correctness;
end;
theorem Th18:
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;
g is Morphism of dom g, cod g & Hom(dom g,cod g) <> {} by CAT_1:19,22;
hence F?-dom(g) is_naturally_transformable_to F?-cod(g) by Th17;
end;
theorem Th19:
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;
the Morphisms of [:A,B:] = [:the Morphisms of A, the Morphisms of B:]
by CAT_2:33;
then reconsider G = F as
Function of [:the Morphisms of A,the Morphisms of B:], the Morphisms of C;
reconsider Ff = (curry G).f as
Function of the Morphisms of B,the Morphisms of C;
F?-dom f is_naturally_transformable_to F?-cod f by Th18;
then F?-dom f is_transformable_to F?-cod f by NATTRA_1:def 7;
hence (F?-f).b
= (F?-f qua Function of the Objects of B, the Morphisms of C).b
by NATTRA_1:def 5
.= (curry(F,f)*the Id of B).b by Def3
.= curry(F,f).((the Id of B).b) by FUNCT_2:21
.= curry(F,f).id b by CAT_1:def 5
.= Ff.(id b qua Morphism of B) by Def2
.= F.[f,id b] by CAT_2:3;
end;
theorem Th20:
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;
the Morphisms of [:A,B:] = [:the Morphisms of A, the Morphisms of B:]
by CAT_2:33;
then reconsider G = F as
Function of [:the Morphisms of A,the Morphisms of B:], the Morphisms of C;
reconsider Ff = (curry G).(id a qua Morphism of A)
as Function of the Morphisms of B,the Morphisms of C;
dom id a = a & cod id a = a by CAT_1:44;
then reconsider I = F?-id a as transformation of F?-a,F?-a;
now let b be Object of B;
thus (I qua Function of the Objects of B, the Morphisms of C).b
= (curry(F,id a)*the Id of B).b by Def3
.= curry(F,id a).((the Id of B).b) by FUNCT_2:21
.= curry(F,id a).id b by CAT_1:def 5
.= Ff.(id b qua Morphism of B) by Def2
.= F.[id a,id b] by CAT_2:3
.= F.(id [a,b] qua Morphism of [:A,B:]) by CAT_2:41
.= id(F.[a,b]) by CAT_1:108
.= id ((F?-a).b) by Th12;
end;
hence thesis by NATTRA_1:def 4;
end;
theorem Th21:
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;
let t be natural_transformation of F?-dom f, F?-dom g such that
A2: t = F?-f;
A3: F?-dom f is_naturally_transformable_to F?-dom g &
F?-dom g is_naturally_transformable_to F?-cod g by A1,Th18;
then A4: F?-dom f is_transformable_to F?-dom g &
F?-dom g is_transformable_to F?-cod g by NATTRA_1:def 7;
then A5: F?-dom f is_transformable_to F?-cod g by NATTRA_1:19;
F?-dom(g*f) is_naturally_transformable_to F?-cod(g*f) by Th18;
then A6: F?-dom(g*f) is_transformable_to F?-cod(g*f) by NATTRA_1:def 7;
A7: cod(g*f) = cod g & dom(g*f) = dom f by A1,CAT_1:42;
reconsider s = t as transformation of F?-dom f, F?-dom g;
the Morphisms of [:A,B:] = [:the Morphisms of A, the Morphisms of B:]
by CAT_2:33;
then reconsider G = F as
Function of [:the Morphisms of A,the Morphisms of B:], the Morphisms of C;
reconsider Fgf = (curry G).(g*f), Ff = (curry G).f, Fg = (curry G).g
as Function of the Morphisms of B,the Morphisms of C;
now let b be Object of B;
A8: (F?-g).b
= (F?-(g) qua Function of the Objects of B, the Morphisms of C).b
by A4,NATTRA_1:def 5
.= (curry(F,g)*the Id of B).b by Def3
.= curry(F,g).((the Id of B).b) by FUNCT_2:21
.= curry(F,g).id b by CAT_1:def 5
.= Fg.(id b qua Morphism of B) by Def2
.= F.[g,id b] by CAT_2:3;
A9: (F?-f).b
= (F?-(f) qua Function of the Objects of B, the Morphisms of C).b
by A1,A4,NATTRA_1:def 5
.= (curry(F,f)*the Id of B).b by Def3
.= curry(F,f).((the Id of B).b) by FUNCT_2:21
.= curry(F,f).id b by CAT_1:def 5
.= Ff.(id b qua Morphism of B) by Def2
.= F.[f,id b] by CAT_2:3;
dom id b = b by CAT_1:44 .= cod id b by CAT_1:44;
then A10: dom[g, id b] = [cod f, cod id b] by A1,CAT_2:38
.= cod[f, id b] by CAT_2:38;
A11: Hom(b,b) <> {} by CAT_1:56;
A12: Hom((F?-dom g).b,(F?-cod g).b) <> {} &
Hom((F?-dom f).b,(F?-dom g).b) <> {} by A4,NATTRA_1:def 2;
thus F?-(g*f).b
= (F?-(g*f) qua Function of the Objects of B, the Morphisms of C).b
by A6,NATTRA_1:def 5
.= (curry(F,g*f)*the Id of B).b by Def3
.= curry(F,g*f).((the Id of B).b) by FUNCT_2:21
.= curry(F,g*f).id b by CAT_1:def 5
.= Fgf.(id b qua Morphism of B) by Def2
.= F.[g*f,id b] by CAT_2:3
.= F.[g*f,id b*id b] by CAT_1:59
.= F.[g*f,id b*(id b qua Morphism of B)] by A11,CAT_1:def 13
.= F.([g, id b]*[f,id b]) by A10,CAT_2:40
.= (F?-g).b*(s.b qua Morphism of C) by A1,A2,A8,A9,A10,CAT_1:99
.= (F?-g).b*s.b by A12,CAT_1:def 13
.= ((F?-g)`*`s).b by A4,NATTRA_1:def 6;
end;
then F?-(g*f) = (F?-g)`*`s by A5,A7,NATTRA_1:20;
hence thesis by A3,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[set,set] means
for f being Morphism of A
st $1 = f holds $2 = [[F?-dom f,F?-cod f],F?-f];
A1: now let m; assume m in the Morphisms of A;
then reconsider g = m as Morphism of A;
take o = [[F?-dom(g),F?-cod(g)],F?-g];
F?-dom(g) is_naturally_transformable_to F?-cod(g) by Th18;
then o in NatTrans(B,C) by NATTRA_1:35;
hence o in the Morphisms of Functors(B,C) by NATTRA_1:def 18;
thus P[m,o];
end;
consider G being
Function of the Morphisms of A, the Morphisms of Functors(B,C) such that
A2: for m st m in the Morphisms of A holds P[m,G.m] from FuncEx1(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 Th8;
take d;
dom id c = c & cod id c = c by CAT_1:44;
hence G.id c
= [[F?-c,F?-c],F?-id c] by A2
.= [[F?-c,F?-c],id(F?-c)] by Th20
.= id d by NATTRA_1:def 18;
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 Morphisms of A;
reconsider d = F?-dom f, c = F?-cod f as Object of Functors(B,C)
by Th8;
A3: dom id dom f = dom f & cod id dom f = dom f &
dom id cod f = cod f & cod id cod f = cod f by CAT_1:44;
A4: 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,A3
.= [[F?-dom f,F?-dom f],id(F?-dom f)] by Th20
.= id d by NATTRA_1:def 18
.= id dom(G.f) by A4,NATTRA_1:39;
thus G.id cod f
= [[F?-cod f,F?-cod f],F?-id cod f] by A2,A3
.= [[F?-cod f,F?-cod f],id(F?-cod f)] by Th20
.= id c by NATTRA_1:def 18
.= id cod(G.f) by A4,NATTRA_1:39;
end;
let f,g be Morphism of A;
assume
A5: dom g = cod f;
then reconsider t = F?-f as natural_transformation of F?-dom f,F?-dom g;
the Morphisms of Functors(B,C) = NatTrans(B,C) &
F?-dom f is_naturally_transformable_to F?-cod f &
F?-dom g is_naturally_transformable_to F?-cod g by Th18,NATTRA_1:def 18;
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 NATTRA_1:35;
A6: cod(g*f) = cod g & dom(g*f) = dom f by A5,CAT_1:42;
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 A5,Th21
.= gg*ff by A5,A6,NATTRA_1:42
.= 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:113;
end;
end;
Lm2:
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)<>{} & t.a is Morphism of F1.a,F2.a by A1,NATTRA_1:def 2;
hence t.a in Hom(F1.a,F2.a) by CAT_1:def 7;
end;
canceled 2;
theorem Th24:
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;
A1: dom id a = a & cod id a = a by CAT_1:44;
reconsider o = F?-a as Object of Functors(B,C) by Th8;
reconsider i = id a as Morphism of A;
A2:(export F).i = [[F?-a,F?-a],F?-id a] by A1,Def4
.= [[F?-a,F?-a],id(F?-a)] by Th20
.= id o by NATTRA_1:def 18;
thus (export F).a = (Obj export F).a by CAT_1:def 20
.= F?-a by A2,CAT_1:103;
end;
theorem Th25:
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 Th24;
hence (export F).a is Functor of B,C;
end;
theorem Th26:
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:37;
A3: dom id cod f = cod f & dom g = cod id dom g by CAT_1:44;
A4: fg = [(id cod f)*f,g] by A2,Th6
.= [(id cod f)*f,g*(id dom g)] by Th7
.= [id cod f,g]*[f, id dom g] by A3,CAT_2:39;
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 F1?-f = F2?-f & [F1?-dom f,F1?-cod f] = [F2?-dom f,F2?-cod f]
by ZFMISC_1:33;
then A6: F1?-dom f = F2?-dom f & F1?-cod f = F2?-cod f by ZFMISC_1:33;
A7: F1.[f, id dom g] = (F1?-f).dom g by Th19
.= (F2?-f).dom g by A5,A6,ZFMISC_1:33
.= F2.[f,id dom g] by Th19;
A8: F1.[id cod f, g] = (F2?-cod f).g by A6,CAT_2:47
.= F2.[id cod f, g] by CAT_2:47;
A9: cod[f,id dom g] = [cod f, cod id dom g] by CAT_2:38
.= [cod f, dom g] by CAT_1:44
.= [dom id cod f, dom g] by CAT_1:44
.= dom[id cod f,g] by CAT_2:38;
hence F1.fg = F2.[id cod f,g]*F2.[f, id dom g] by A4,A7,A8,CAT_1:99
.= F2.fg by A4,A9,CAT_1:99;
end;
hence F1 = F2 by FUNCT_2:113;
end;
theorem Th27:
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 Objects of A, the Objects of B:], the Morphisms 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 by NATTRA_1:def 7;
let t be natural_transformation of F1,F2;
the Objects of [:A,B:] = [:the Objects of A, the Objects of B:] by CAT_2:
33
;
then reconsider s = t as Function of
[:the Objects of A, the Objects of B:], the Morphisms 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 & S2 = (export F2).a;
let b be Object of B;
A5: S1.b = (F1?-a).b by A4,Th24 .= F1.[a,b] by Th12;
A6: S2.b = (F2?-a).b by A4,Th24 .= F2.[a,b] by Th12;
(curry s).a.b = s.[a,b] by CAT_2:3 .= t.[a,b] by A2,NATTRA_1:def 5;
hence (curry s).a.b in Hom(S1.b,S2.b) by A2,A5,A6,Lm2;
end;
A7: now let a be Object of A;
let S1,S2 be Functor of B,C; assume
S1 = (export F1).a & S2 = (export F2).a;
then for b be Object of B holds Hom(S1.b,S2.b) <> {} by A3;
hence S1 is_transformable_to S2 by NATTRA_1:def 2;
end;
A8: now let a be Object of A;
let S1,S2 be Functor of B,C such that
A9: 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 A7,A9;
let b be Object of B;
(curry s).a.b in Hom(S1.b,S2.b) by A3,A9;
hence (curry s).a.b is Morphism of S1.b,S2.b by CAT_1:def 7;
end;
end;
A10: now let a be Object of A;
let S1,S2 be Functor of B,C, T be transformation of S1,S2; assume
A11: S1 = (export F1).a & S2 = (export F2).a & T = (curry s).a;
then A12: S1 is_transformable_to S2 by A7;
let b1,b2 be Object of B such that
A13: Hom(b1,b2) <> {};
let f be Morphism of b1,b2;
A14: Hom(a,a) <> {} by CAT_1:56;
then reconsider g = [id a,f] as Morphism of [a,b1],[a,b2]
by A13,CAT_2:43;
A15: Hom([a,b1],[a,b2]) <> {} by A13,A14,Th13;
then A16: Hom(F1.[a,b1],F1.[a,b2]) <> {} by CAT_1:126;
A17: Hom(F2.[a,b1],F2.[a,b2]) <> {} by A15,CAT_1:126;
A18: Hom(F1.[a,b1],F2.[a,b1]) <> {} by A2,NATTRA_1:def 2;
A19: Hom(F1.[a,b2],F2.[a,b2]) <> {} by A2,NATTRA_1:def 2;
A20: Hom(S1.b1,S1.b2) <> {} by A13,CAT_1:126;
A21: Hom(S2.b1,S2.b2) <> {} by A13,CAT_1:126;
A22: Hom(S1.b1,S2.b1) <> {} by A12,NATTRA_1:def 2;
A23: Hom(S1.b2,S2.b2) <> {} by A12,NATTRA_1:def 2;
A24: T.b1 = (T qua Function of the Objects of B, the Morphisms of C).b1
by A12,NATTRA_1:def 5
.= s.[a,b1] by A11,CAT_2:3 .= t.[a,b1] by A2,NATTRA_1:def 5;
A25: T.b2 = (T qua Function of the Objects of B, the Morphisms of C).b2
by A12,NATTRA_1:def 5
.= s.[a,b2] by A11,CAT_2:3 .= t.[a,b2] by A2,NATTRA_1:def 5;
A26: S1.f = (F1?-a).f by A11,Th24
.= (F1?-a).(f qua Morphism of B) by A13,NATTRA_1:def 1
.= F1.[id a, f] by CAT_2:47
.= F1.g by A15,NATTRA_1:def 1;
A27: S2.f = (F2?-a).f by A11,Th24
.= (F2?-a).(f qua Morphism of B) by A13,NATTRA_1:def 1
.= F2.[id a, f] by CAT_2:47
.= F2.g by A15,NATTRA_1:def 1;
thus T.b2*S1.f
= t.[a,b2]*(F1.g qua Morphism of C) by A20,A23,A25,A26,CAT_1:def 13
.= t.[a,b2]*F1.g by A16,A19,CAT_1:def 13
.= F2.g*t.[a,b1] by A1,A15,NATTRA_1:def 8
.= (S2.f qua Morphism of C)*T.b1 by A17,A18,A24,A27,CAT_1:def 13
.= S2.f*T.b1 by A21,A22,CAT_1:def 13;
end;
defpred P[set,set] means
for f being Object of A, s being Function of
[:the Objects of A, the Objects of B:], the Morphisms of C
st t = s & $1 = f
holds $2 = [[(export F1).f,(export F2).f],(curry s).f];
A28: now let m; assume m in the Objects of A;
then reconsider a = m as Object of A;
take o = [[(export F1).a,(export F2).a],(curry s).a];
reconsider S1 = (export F1).a, S2 = (export F2).a as Functor of B,C
by Th25;
reconsider T = (curry s).a as transformation of S1,S2 by A8;
A29: S1 is_naturally_transformable_to S2
proof thus S1 is_transformable_to S2 by A7;
take T; thus thesis by A10;
end;
T is natural_transformation of S1,S2
proof thus S1 is_naturally_transformable_to S2 by A29;
thus thesis by A10;
end;
then o in NatTrans(B,C) by A29,NATTRA_1:35;
hence o in the Morphisms of Functors(B,C) by NATTRA_1:def 18;
thus P[m,o];
end;
consider G being
Function of the Objects of A, the Morphisms of Functors(B,C) such that
A30: for m st m in the Objects of A holds P[m,G.m]
from FuncEx1(A28);
A31: now let a be Object of A;
reconsider S1 = (export F1).a, S2 = (export F2).a as Functor of B,C
by Th25;
reconsider T = (curry s).a as transformation of S1,S2 by A8;
A32: S1 is_naturally_transformable_to S2
proof thus S1 is_transformable_to S2 by A7;
take T; thus thesis by A10;
end;
A33: T is natural_transformation of S1,S2
proof thus S1 is_naturally_transformable_to S2 by A32;
thus thesis by A10;
end;
G.a = [[S1,S2],T] by A30;
then dom(G.a) = S1 & cod(G.a) = S2 by A33,NATTRA_1:39;
hence G.a in Hom((export F1).a,(export F2).a) by CAT_1:18;
end;
then A34:
for a be Object of A holds Hom((export F1).a,(export F2).a) <> {};
then A35: export F1 is_transformable_to export F2 by NATTRA_1:def 2;
G is transformation of export F1, export F2
proof thus export F1 is_transformable_to export F2 by A34,NATTRA_1:def 2
;
let a be Object of A; G.a in Hom((export F1).a,(export F2).a) by A31;
hence G.a is Morphism of (export F1).a,(export F2).a by CAT_1:def 7;
end;
then reconsider G as transformation of export F1, export F2;
A36: now let a,b be Object of A such that
A37: Hom(a,b) <> {};
let f be Morphism of a,b;
reconsider g = f as Morphism of A;
A38: F1?-b = (export F1).b by Th24;
then A39: F1?-cod f = (export F1).b by A37,CAT_1:23;
A40: F2?-a = (export F2).a by Th24;
then A41: F2?-dom f = (export F2).a by A37,CAT_1:23;
A42: F1?-a = (export F1).a by Th24;
then A43: F1?-dom f = (export F1).a by A37,CAT_1:23;
A44: F2?-b = (export F2).b by Th24;
then A45: F2?-cod f = (export F2).b by A37,CAT_1:23;
reconsider S1 = (export F1).a, S2 = (export F2).a,
S3 = (export F1).b, S4 = (export F2).b
as Functor of B,C by Th25;
A46: S1 is_naturally_transformable_to S2 by A1,A40,A42,Th15;
then A47: S1 is_transformable_to S2 by NATTRA_1:def 7;
A48: S2 is_naturally_transformable_to S4 by A37,A40,A44,Th17;
then A49: S2 is_transformable_to S4 by NATTRA_1:def 7;
A50: S1 is_naturally_transformable_to S3 by A37,A38,A42,Th17;
then A51: S1 is_transformable_to S3 by NATTRA_1:def 7;
A52: S3 is_naturally_transformable_to S4 by A1,A38,A44,Th15;
then A53: S3 is_transformable_to S4 by NATTRA_1:def 7;
A54: S1 is_transformable_to S4 by A47,A49,NATTRA_1:19;
reconsider T13 = F1?-f as natural_transformation of S1,S3 by A37,A39,A42,
CAT_1:23;
reconsider T12 = (curry s).a as natural_transformation of S1,S2
by A1,A40,A42,Th15;
reconsider T24 = F2?-f as natural_transformation of S2,S4 by A37,A40,A45,
CAT_1:23;
reconsider T34 = (curry s).b as natural_transformation of S3,S4
by A1,A38,A44,Th15;
A55: (export F1).g = [[S1,S3],T13] by A39,A43,Def4;
A56: (export F2).g = [[S2,S4],T24] by A41,A45,Def4;
A57: G.b = G.(b qua set) by A35,NATTRA_1:def 5
.= [[S3,S4],T34] by A30;
A58: G.a = G.(a qua set) by A35,NATTRA_1:def 5
.= [[S1,S2],T12] by A30;
A59: Hom((export F1).a,(export F2).a) <> {} by A31;
A60: Hom((export F2).a,(export F2).b) <> {} by A37,CAT_1:126;
A61: Hom((export F1).b,(export F2).b) <> {} by A31;
A62: Hom((export F1).a,(export F1).b) <> {} by A37,CAT_1:126;
now let c be Object of B;
A63: Hom(S2.c,S4.c) <> {} by A49,NATTRA_1:def 2;
A64: Hom(S1.c,S2.c) <> {} by A47,NATTRA_1:def 2;
A65: Hom(S3.c,S4.c) <> {} by A53,NATTRA_1:def 2;
A66: Hom(S1.c,S3.c) <> {} by A51,NATTRA_1:def 2;
A67: Hom(c,c) <> {} by CAT_1:56;
then A68: Hom([a,c],[b,c]) <> {} by A37,Th13;
A69: Hom(F1.[a,c],F2.[a,c]) <> {} by A2,NATTRA_1:def 2;
A70: Hom(F2.[a,c],F2.[b,c]) <> {} by A68,CAT_1:126;
A71: Hom(F1.[b,c],F2.[b,c]) <> {} by A2,NATTRA_1:def 2;
A72: Hom(F1.[a,c],F1.[b,c]) <> {} by A68,CAT_1:126;
reconsider fi = [f, id c] as Morphism of [a,c], [b,c] by A37,A67,CAT_2:
43;
the Morphisms of [:A,B:] = [:the Morphisms of A, the Morphisms of B:]
by CAT_2:33;
then reconsider FF1 = F1, FF2 = F2 as Function of
[:the Morphisms of A,the Morphisms of B:], the Morphisms of C;
A73: F2.fi = FF2.[f,id c] by A68,NATTRA_1:def 1
.= (curry FF2).f.id c by CAT_2:3
.= curry(F2,f).id c by Def2
.= curry(F2,f).((the Id of B).c) by CAT_1:def 5
.= (curry(F2,f)*the Id of B).c by FUNCT_2:21
.= (F2?-f qua Function of the Objects of B, the Morphisms of C).c
by Def3
.= T24.c by A49,NATTRA_1:def 5;
A74: t.[a,c]
= s.[a,c] by A2,NATTRA_1:def 5
.= ((curry s).a).c by CAT_2:3
.= T12.c by A47,NATTRA_1:def 5;
A75: F1.fi = FF1.[f,id c] by A68,NATTRA_1:def 1
.= (curry FF1).f.id c by CAT_2:3
.= curry(F1,f).id c by Def2
.= curry(F1,f).((the Id of B).c) by CAT_1:def 5
.= (curry(F1,f)*the Id of B).c by FUNCT_2:21
.= (F1?-f qua Function of the Objects of B, the Morphisms of C).c
by Def3
.= T13.c by A51,NATTRA_1:def 5;
A76: t.[b,c]
= s.[b,c] by A2,NATTRA_1:def 5
.= ((curry s).b).c by CAT_2:3
.= T34.c by A53,NATTRA_1:def 5;
thus (T34`*`T13).c
= T34.c*T13.c by A50,A52,NATTRA_1:27
.= (t.[b,c] qua Morphism of C)*F1.fi by A65,A66,A75,A76,CAT_1:def 13
.= t.[b,c]*F1.fi by A71,A72,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 A69,A70,CAT_1:def 13
.= T24.c*T12.c by A63,A64,A73,A74,CAT_1:def 13
.= (T24`*`T12).c by A46,A48,NATTRA_1:27;
end;
then A77: T34`*`T13 = T24`*`T12 by A54,NATTRA_1:20;
thus G.b*(export F1).f
= G.b*((export F1).f qua Morphism of Functors(B,C))
by A61,A62,CAT_1:def 13
.= G.b*(export F1).g by A37,NATTRA_1:def 1
.= [[S1,S4],T34`*`T13] by A55,A57,NATTRA_1:42
.= (export F2).g*G.a by A56,A58,A77,NATTRA_1:42
.= ((export F2).f qua Morphism of Functors(B,C))*G.a
by A37,NATTRA_1:def 1
.= (export F2).f*G.a by A59,A60,CAT_1:def 13;
end;
thus
A78: export F1 is_naturally_transformable_to export F2
proof thus export F1 is_transformable_to export F2 by A34,NATTRA_1:def 2;
thus thesis by A36;
end;
G is natural_transformation of export F1, export F2
proof
thus export F1 is_naturally_transformable_to export F2 by A78;
thus thesis by A36;
end;
then reconsider G as natural_transformation of export F1, export F2;
take G;
let s be Function of
[:the Objects of A, the Objects of B:], the Morphisms of C;
assume
A79: t = s;
let a be Object of A;
thus G.a = G.(a qua set) by A35,NATTRA_1:def 5
.= [[(export F1).a,(export F2).a],(curry s).a] by A30,A79;
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 Objects of A, the Objects of B:], the Morphisms 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,Th27;
uniqueness
proof let T1,T2 be natural_transformation of export F1, export F2 such that
A2: for s being Function of
[:the Objects of A, the Objects of B:], the Morphisms 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 Objects of A, the Objects of B:], the Morphisms of C st t = s
for a being Object of A
holds T2.a = [[(export F1).a,(export F2).a],(curry s).a];
export F1 is_naturally_transformable_to export F2 by A1,Th27;
then A4: export F1 is_transformable_to export F2 by NATTRA_1:def 7;
the Objects of [:A,B:] = [:the Objects of A, the Objects of B:] by CAT_2:
33
;
then reconsider s = t as Function of
[:the Objects of A, the Objects of B:], the Morphisms of C;
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;
hence T1 = T2 by A4,NATTRA_1:20;
end;
end;
theorem Th28:
for F being Functor of [:A,B:],C holds id export F = export id F
proof let F be Functor of [:A,B:],C;
the Objects of [:A,B:] = [:the Objects of A, the Objects of B:] by CAT_2:
33
;
then reconsider s = id F as Function of
[:the Objects of A, the Objects of B:], the Morphisms of C;
now let a be Object of A;
reconsider ff = (export F).a as Functor of B,C by Th8;
A1: now let b be Object of B;
A2: Hom(b,b) <> {} by CAT_1:56;
thus (id ff qua Function of the Objects of B, the Morphisms of C).b
= (id ff).b by NATTRA_1:def 5
.= id(ff.b) by NATTRA_1:21
.= (ff qua Function of the Morphisms of B, the Morphisms of C)
.id b by CAT_1:108
.= ff.id b by A2,NATTRA_1:def 1
.= (F?-a).id b by Th24
.= (F?-a).(id b qua Morphism of B) by A2,NATTRA_1:def 1
.= F.[id a, id b] by CAT_2:47
.= F.(id[a,b] qua Morphism of [:A,B:]) by CAT_2:41
.= id(F.[a,b]) by CAT_1:108
.= (id F).[a,b] by NATTRA_1:21
.= (id F qua Function of the Objects of [:A,B:], the Morphisms of C)
.[a,b] by NATTRA_1:def 5
.= (curry s).a.b by CAT_2:3;
end;
thus (id export F).a
= id((export F).a) by NATTRA_1:21
.= [[ff,ff],id ff] by NATTRA_1:def 18
.= [[(export F).a, (export F).a],(curry s).a] by A1,FUNCT_2:113
.= (export id F).a by Def5;
end;
hence thesis by NATTRA_1:20;
end;
theorem Th29:
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: F1 is_naturally_transformable_to F3 by A1,A2,NATTRA_1:25;
A4: F1 is_transformable_to F2 by A1,NATTRA_1:def 7;
A5: F2 is_transformable_to F3 by A2,NATTRA_1:def 7;
A6: F1 is_transformable_to F3 by A3,NATTRA_1:def 7;
let t1 be natural_transformation of F1,F2,
t2 be natural_transformation of F2,F3;
A7: export F1 is_naturally_transformable_to export F2 by A1,Th27;
then A8: export F1 is_transformable_to export F2 by NATTRA_1:def 7;
A9: export F2 is_naturally_transformable_to export F3 by A2,Th27;
then A10: export F2 is_transformable_to export F3 by NATTRA_1:def 7;
then A11: export F1 is_transformable_to export F3 by A8,NATTRA_1:19;
now let a be Object of A;
the Objects of [:A,B:] = [:the Objects of A, the Objects of B:] by CAT_2:
33
;
then reconsider s1 = t1, s2 = t2, s3 = t2`*`t1 as Function of
[:the Objects of A, the Objects of B:], the Morphisms of C;
reconsider S1 = (export F1).a, S2 = (export F2).a, S3 = (export F3).a
as Functor of B,C by Th8;
A12: S1 = F1?-a & S2 = F2?-a & S3 = F3?-a by Th24;
then A13: S1 is_naturally_transformable_to S2 by A1,Th15;
A14: S2 is_naturally_transformable_to S3 by A2,A12,Th15;
then S1 is_naturally_transformable_to S3 by A13,NATTRA_1:25;
then A15: S1 is_transformable_to S3 by NATTRA_1:def 7;
A16: S1 is_transformable_to S2 by A13,NATTRA_1:def 7;
A17: S2 is_transformable_to S3 by A14,NATTRA_1:def 7;
reconsider T1 = (curry s1).a as natural_transformation of S1,S2
by A1,A12,Th15;
reconsider T2 = (curry s2).a as natural_transformation of S2,S3
by A2,A12,Th15;
reconsider T3 = (curry s3).a as natural_transformation of S1,S3
by A3,A12,Th15;
A18: (export t2).a = [[S2,S3],T2] by A2,Def5;
A19: (export t1).a = [[S1,S2],T1] by A1,Def5;
now let b be Object of B;
A20: Hom(F1.[a,b],F2.[a,b]) <> {} by A4,NATTRA_1:def 2;
A21: Hom(F2.[a,b],F3.[a,b]) <> {} by A5,NATTRA_1:def 2;
A22: Hom(S1.b,S2.b) <> {} by A16,NATTRA_1:def 2;
A23: Hom(S2.b,S3.b) <> {} by A17,NATTRA_1:def 2;
A24: T2.b
= (T2 qua Function of the Objects of B, the Morphisms of C).b
by A17,NATTRA_1:def 5
.= s2.[a,b] by CAT_2:3
.= t2.[a,b] by A5,NATTRA_1:def 5;
A25: T1.b
= (T1 qua Function of the Objects of B, the Morphisms of C).b
by A16,NATTRA_1:def 5
.= s1.[a,b] by CAT_2:3
.= t1.[a,b] by A4,NATTRA_1:def 5;
thus T3.b
= (T3 qua Function of the Objects of B, the Morphisms of C).b
by A15,NATTRA_1:def 5
.= s3.[a,b] by CAT_2:3
.= (t2`*`t1).[a,b] by A6,NATTRA_1:def 5
.= t2.[a,b]*t1.[a,b] by A1,A2,NATTRA_1:27
.= T2.b*(T1.b qua Morphism of C) by A20,A21,A24,A25,CAT_1:def 13
.= T2.b*T1.b by A22,A23,CAT_1:def 13
.= (T2`*`T1).b by A13,A14,NATTRA_1:27;
end;
then A26: T3 = T2`*`T1 by A15,NATTRA_1:20;
A27: Hom((export F1).a,(export F2).a) <> {} by A8,NATTRA_1:def 2;
A28: Hom((export F2).a,(export F3).a) <> {} by A10,NATTRA_1:def 2;
thus (export(t2`*`t1)).a
= [[S1,S3],T3] by A3,Def5
.= (export t2).a*((export t1).a qua Morphism of Functors(B,C))
by A18,A19,A26,NATTRA_1:42
.= (export t2).a*(export t1).a by A27,A28,CAT_1:def 13
.= ((export t2)`*`(export t1)).a by A7,A9,NATTRA_1:27;
end;
hence export(t2`*`t1) = (export t2)`*`(export t1) by A11,NATTRA_1:20;
end;
theorem Th30:
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 by NATTRA_1:def 7;
let t1,t2 be natural_transformation of F1,F2 such that
A3: export t1 = export t2;
now 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 CAT_2:35;
the Objects of [:A,B:] = [:the Objects of A, the Objects of B:] by CAT_2:
33
;
then reconsider s1 = t1, s2 = t2 as
Function of [:the Objects of A, the Objects of B:], the Morphisms of C;
[[(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 ZFMISC_1:33;
thus t1.ab = s1.[a,b] by A2,A4,NATTRA_1:def 5
.= ((curry s2).a).b by A5,CAT_2:3
.= s2.[a,b] by CAT_2:3
.= t2.ab by A2,A4,NATTRA_1:def 5;
end;
hence t1 = t2 by A1,ISOCAT_1:31;
end;
theorem Th31:
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[set,set] 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; assume m in the Morphisms of [:A,B:];
then consider m1 being (Morphism of A), m2 being Morphism of B such that
A2: m = [m1, m2] by CAT_2:37;
consider F1,F2 being Functor of B,C,
t1 being natural_transformation of F1,F2 such that
F1 is_naturally_transformable_to F2 and
A3: dom(G.m1) = F1 & cod(G.m1) = F2 & G.m1 = [[F1,F2],t1] by Th9;
reconsider o = t1.(cod m2)*F1.m2 as set;
take o;
thus o in the Morphisms of C;
thus P[m,o]
proof
let f be (Morphism of A), g be Morphism of B;
assume m = [f,g];
then A4: f = m1 & g = m2 by A2,ZFMISC_1:33;
let f1,f2 be Functor of B,C, t be natural_transformation of f1,f2;
assume A5: G.f = [[f1,f2],t];
then [F1,F2] = [f1,f2] & t1 = t by A3,A4,ZFMISC_1:33;
then F1 =f1 & F2 = f2 by ZFMISC_1:33;
hence o = t.cod g*f1.g by A3,A4,A5,ZFMISC_1:33;
end;
end;
consider F being Function of the Morphisms of [:A,B:], the Morphisms of C
such that
A6: for m st m in the Morphisms of [:A,B:] holds P[m,F.m] from FuncEx1(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
A7: ab = [a,b] by CAT_2:35;
A8: id ab = [id a, id b] by A7,CAT_2:41;
reconsider H = G.a as Functor of B,C by Th8;
take H.b;
A9: Hom(H.b,H.b) <> {} by CAT_1:56;
G.(id a qua Morphism of A) = id(G.a) by CAT_1:108
.= [[H,H],id H] by NATTRA_1:def 18;
hence F.id ab
= (id H).(cod id b)*H.(id b qua Morphism of B) by A6,A8
.= (id H).(cod id b)*id(H.b) by CAT_1:108
.= (id H).b*(id(H.b) qua Morphism of C) by CAT_1:44
.= id(H.b)*(id(H.b) qua Morphism of C) by NATTRA_1:21
.= id(H.b)*id(H.b) by A9,CAT_1:def 13
.= id(H.b) by CAT_1:59;
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
A10: f = [f1,f2] by CAT_2:37;
consider F1,F2 being Functor of B,C,
t being natural_transformation of F1,F2 such that
A11: F1 is_naturally_transformable_to F2 and
A12: dom(G.f1) = F1 & cod(G.f1) = F2 & G.f1 = [[F1,F2],t] by Th9;
A13: id dom f = id[dom f1, dom f2] by A10,CAT_2:38
.= [id dom f1, id dom f2] by CAT_2:41;
reconsider H = G.dom f1 as Functor of B,C by Th8;
A14: id(G.dom f1) = [[H,H],id H] by NATTRA_1:def 18;
A15: F1 = H by A12,CAT_1:109;
A16: Hom(F1.cod f2,F2.cod f2) <> {} by A11,ISOCAT_1:30;
F1.cod f2 = cod(F1.f2) by CAT_1:109;
then A17: dom(t.cod f2) = cod(F1.f2) by A16,CAT_1:23;
A18: Hom(dom(H.f2),dom(H.f2)) <> {} by CAT_1:56;
G.(id dom f1 qua Morphism of A) = id(G.dom f1) by CAT_1:108;
hence F.id dom f
= (id H).(cod id dom f2)*H.(id dom f2 qua Morphism of B)
by A6,A13,A14
.= (id H).(cod id dom f2)*id(H.dom f2) by CAT_1:108
.= (id H).(cod id dom f2)*id dom(H.f2) by CAT_1:109
.= (id H).dom f2*id dom(H.f2) by CAT_1:44
.= id(H.dom f2)*id dom(H.f2) by NATTRA_1:21
.= (id dom(H.f2) qua Morphism of C)*id dom(H.f2) by CAT_1:109
.= id dom(H.f2)*id dom(H.f2) by A18,CAT_1:def 13
.= id dom(F1.f2) by A15,CAT_1:59
.= id dom(t.(cod f2)*F1.f2) by A17,CAT_1:42
.= id dom(F.f) by A6,A10,A12;
A19: id cod f = id[cod f1, cod f2] by A10,CAT_2:38
.= [id cod f1, id cod f2] by CAT_2:41;
reconsider H = G.cod f1 as Functor of B,C by Th8;
A20: id(G.cod f1) = [[H,H],id H] by NATTRA_1:def 18;
A21: F2 = H by A12,CAT_1:109;
A22: Hom(F1.cod f2,F2.cod f2) <> {} by A11,ISOCAT_1:30;
F1.cod f2 = cod(F1.f2) by CAT_1:109;
then A23: dom(t.cod f2) = cod(F1.f2) by A22,CAT_1:23;
A24: Hom(cod(H.f2),cod(H.f2)) <> {} by CAT_1:56;
G.(id cod f1 qua Morphism of A) = id(G.cod f1) by CAT_1:108;
hence F.id cod f
= (id H).(cod id cod f2)*H.(id cod f2 qua Morphism of B)
by A6,A19,A20
.= (id H).(cod id cod f2)*id(H.cod f2) by CAT_1:108
.= (id H).(cod id cod f2)*id cod(H.f2) by CAT_1:109
.= (id H).cod f2*id cod(H.f2) by CAT_1:44
.= id(H.cod f2)*id cod(H.f2) by NATTRA_1:21
.= (id cod(H.f2) qua Morphism of C)*id cod(H.f2) by CAT_1:109
.= id cod(H.f2)*id cod(H.f2) by A24,CAT_1:def 13
.= id cod(H.f2) by CAT_1:59
.= id(F2.cod f2) by A21,CAT_1:109
.= id cod(t.cod f2) by A22,CAT_1:23
.= id cod(t.(cod f2)*F1.f2) by A23,CAT_1:42
.= id cod(F.f) by A6,A10,A12;
end;
let f,g be Morphism of [:A,B:] such that
A25: dom g = cod f;
consider f1 being (Morphism of A), f2 being Morphism of B such that
A26: f = [f1,f2] by CAT_2:37;
consider F1,F2 being Functor of B,C,
t being natural_transformation of F1,F2 such that
A27: F1 is_naturally_transformable_to F2 and
A28: dom(G.f1) = F1 & cod(G.f1) = F2 & G.f1 = [[F1,F2],t] by Th9;
consider g1 being (Morphism of A), g2 being Morphism of B such that
A29: g = [g1,g2] by CAT_2:37;
consider G1,G2 being Functor of B,C,
s being natural_transformation of G1,G2 such that
A30: G1 is_naturally_transformable_to G2 and
A31: dom(G.g1) = G1 & cod(G.g1) = G2 & G.g1 = [[G1,G2],s] by Th9;
[cod f1, cod f2] = cod f & [dom g1, dom g2] = dom g by A26,A29,CAT_2:38
;
then A32: cod f1 = dom g1 & cod f2 = dom g2 by A25,ZFMISC_1:33;
then A33: g*f = [g1*f1,g2*f2] by A26,A29,CAT_2:39;
A34: F2 = G1 by A28,A31,A32,CAT_1:99;
reconsider s as natural_transformation of F2,G2 by A28,A31,A32,CAT_1:99;
A35: G.(g1*f1) = G.g1*G.f1 by A32,CAT_1:99
.= [[F1,G2],s`*`t] by A28,A31,A34,NATTRA_1:42;
A36: F.f = t.(cod f2)*F1.f2 by A6,A26,A28;
A37: cod(g2*f2) = cod g2 by A32,CAT_1:42;
A38: Hom(F2.cod g2,G2.cod g2) <> {} by A30,A34,ISOCAT_1:30;
A39: Hom(F1.cod g2,F2.cod g2) <> {} by A27,ISOCAT_1:30;
A40: Hom(dom f2, dom g2) <> {} by A32,CAT_1:19;
then A41: Hom(F1.dom f2,F1.dom g2) <> {} by CAT_1:126;
A42: Hom(dom g2, cod g2) <> {} by CAT_1:19;
then A43: Hom(F1.dom g2,F1.cod g2) <> {} by CAT_1:126;
then A44: Hom(F1.dom f2,F1.cod g2) <> {} by A41,CAT_1:52;
A45: Hom(F2.dom g2,F2.cod g2) <> {} by A42,CAT_1:126;
A46: Hom(F1.dom g2,F2.dom g2) <> {} by A27,ISOCAT_1:30;
then A47: Hom(F1.dom f2,F2.dom g2) <> {} by A41,CAT_1:52;
A48: Hom(F2.dom g2,G2.cod g2) <> {} by A38,A45,CAT_1:52;
A49: Hom(F1.cod g2,G2.cod g2) <> {} by A38,A39,CAT_1:52;
reconsider f2' = f2 as Morphism of dom f2, dom g2 by A32,CAT_1:22;
reconsider g2' = g2 as Morphism of dom g2, cod g2 by CAT_1:22;
A50: F1.g2 = F1.g2' & F1.f2 = F1.f2' & G1.g2 = F2.g2'
by A34,A40,A42,NATTRA_1:def 1;
thus F.(g*f)
= (s`*`t).(cod(g2*f2))*F1.(g2*f2) by A6,A33,A35
.= s.(cod g2)*t.(cod g2)*F1.(g2*f2) by A27,A30,A34,A37,NATTRA_1:27
.= s.(cod g2)*t.(cod g2)*(F1.g2*F1.f2) by A32,CAT_1:99
.= s.(cod g2)*t.(cod g2)*(F1.g2'*F1.f2' qua Morphism of C)
by A41,A43,A50,CAT_1:def 13
.= s.(cod g2)*t.(cod g2)*(F1.g2'*F1.f2') by A44,A49,CAT_1:def 13
.= s.(cod g2)*(t.(cod g2)*(F1.g2'*F1.f2')) by A38,A39,A44,CAT_1:54
.= s.(cod g2)*(t.(cod g2)*F1.g2'*F1.f2') by A39,A41,A43,CAT_1:54
.= s.(cod g2)*(F2.g2'*t.(dom g2)*F1.f2') by A27,A42,NATTRA_1:def 8
.= s.(cod g2)*(F2.g2'*(t.(dom g2)*F1.f2')) by A41,A45,A46,CAT_1:54
.= s.(cod g2)*F2.g2'*(t.(dom g2)*F1.f2') by A38,A45,A47,CAT_1:54
.= s.(cod g2)*F2.g2'*(t.(dom g2)*F1.f2' qua Morphism of C)
by A47,A48,CAT_1:def 13
.= s.(cod g2)*F2.g2'*(t.(cod f2)*F1.f2) by A32,A41,A46,A50,CAT_1:def
13
.= s.(cod g2)*G1.g2*(t.(cod f2)*F1.f2) by A38,A45,A50,CAT_1:def 13
.= F.g*F.f by A6,A29,A31,A34,A36;
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
A51: f1 is_naturally_transformable_to f2 and
A52: dom(G.f) = f1 & cod(G.f) = f2 and
A53: G.f = [[f1,f2],t] by Th9;
now let g be Morphism of B;
A54: f1 = G.dom f by A52,CAT_1:109;
A55: G.(id dom f qua Morphism of A)
= id(G.dom f) by CAT_1:108
.= [[f1,f1],id f1] by A54,NATTRA_1:def 18;
A56: dom id cod g = cod g by CAT_1:44;
thus (F?-dom f).g
= F.[id dom f, g] by CAT_2:47
.= (id f1).(cod g)*f1.g by A6,A55
.= id(f1.cod g qua Object of C)*f1.g by NATTRA_1:21
.= f1.(id cod g qua Morphism of B)*f1.g by CAT_1:108
.= f1.((id cod g qua Morphism of B)*g) by A56,CAT_1:99
.= f1.g by CAT_1:46;
end;
then A57: f1 = F?-dom f by FUNCT_2:113;
now let g be Morphism of B;
A58: f2 = G.cod f by A52,CAT_1:109;
A59: G.(id cod f qua Morphism of A)
= id(G.cod f) by CAT_1:108
.= [[f2,f2],id f2] by A58,NATTRA_1:def 18;
A60: dom id cod g = cod g by CAT_1:44;
thus (F?-cod f).g
= F.[id cod f, g] by CAT_2:47
.= (id f2).(cod g)*f2.g by A6,A59
.= id(f2.cod g qua Object of C)*f2.g by NATTRA_1:21
.= f2.(id cod g qua Morphism of B)*f2.g by CAT_1:108
.= f2.((id cod g qua Morphism of B)*g) by A60,CAT_1:99
.= f2.g by CAT_1:46;
end;
then A61: f2 = F?-cod f by FUNCT_2:113;
now let b be Object of B;
A62: Hom(f1.b,f2.b) <> {} by A51,ISOCAT_1:30;
A63: Hom(f1.b,f1.b) <> {} by CAT_1:56;
thus (F?-f).b
= F.[f,id b] by Th19
.= t.(cod id b)*f1.(id b qua Morphism of B) by A6,A53
.= t.(cod id b)*id(f1.b) by CAT_1:108
.= t.b*(id(f1.b) qua Morphism of C) by CAT_1:44
.= t.b*id(f1.b) by A62,A63,CAT_1:def 13
.= t.b by A62,CAT_1:58;
end;
hence G.f =[[F?-dom f,F?-cod f],F?-f] by A51,A53,A57,A61,ISOCAT_1:31;
end;
hence thesis by Def4;
end;
theorem Th32:
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[set,set] means
for a being Object of A st $1 = a holds
t.a = [[(export F1).a,(export F2).a],$2];
A2: now let o;
assume o in the Objects of A;
then reconsider a' = 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.a') = f1 & cod(t.a') = f2 & t.a' =[[f1,f2],tau] by Th9;
reconsider m = tau as set;
take m;
thus m in Funcs(the Objects of B, the Morphisms of C) by FUNCT_2:11;
thus P[o,m]
proof
let a be Object of A such that
A4: o = a;
export F1 is_transformable_to export F2 by A1,NATTRA_1:def 7;
then t.a is Morphism of (export F1).a, (export F2).a &
Hom((export F1).a, (export F2).a) <> {} by NATTRA_1:def 2;
then (export F1).a = f1 & (export F2).a = f2 by A3,A4,CAT_1:23;
hence t.a = [[(export F1).a,(export F2).a],m] by A3,A4;
end;
end;
consider t' being Function of
the Objects of A, Funcs(the Objects of B,the Morphisms of C) such that
A5: for o st o in the Objects of A holds P[o,t'.o] from FuncEx1(A2);
A6: the Objects of [:A,B:] =
[:the Objects of A, the Objects of B:] by CAT_2:33;
the Objects of [:A,B:] = [:the Objects of A, the Objects of B:] by CAT_2:
33
;
then reconsider u' = uncurry t' as Function of
the Objects of [:A,B:], the Morphisms of C;
A7: now let ab be Object of [:A,B:];
consider a being Object of A, b being Object of B such that
A8: ab = [a,b] by A6,DOMAIN_1:9;
(export F1).a = F1?-a & (export F2).a = F2?-a by Th24;
then t.a = [[F1?-a,F2?-a],t'.a] by A5;
then [[F1?-a,F2?-a],t'.a] in the Morphisms of Functors(B,C);
then [[F1?-a,F2?-a],t'.a] in NatTrans(B,C) by NATTRA_1:def 18;
then consider G1,G2 being Functor of B,C,
t'' being natural_transformation of G1,G2 such that
A9: [[F1?-a,F2?-a],t'.a] = [[G1,G2],t''] and
A10: G1 is_naturally_transformable_to G2 by NATTRA_1:def 15;
A11: G1 is_transformable_to G2 by A10,NATTRA_1:def 7;
A12: [F1?-a,F2?-a] = [G1,G2] & t'.a = t'' by A9,ZFMISC_1:33;
A13: u'.[a,b] = t'.a.b by Th2
.= (t'' qua Function of the Objects of B, the Morphisms of C).b by A9,
ZFMISC_1:33
.= t''.b by A11,NATTRA_1:def 5;
A14: F1.[a,b] = (F1?-a).b by Th12 .= G1.b by A12,ZFMISC_1:33;
A15: F2.[a,b] = (F2?-a).b by Th12 .= G2.b by A12,ZFMISC_1:33;
Hom(G1.b,G2.b) <> {} by A10,ISOCAT_1:30;
hence u'.ab in Hom(F1.ab,F2.ab) by A8,A13,A14,A15,CAT_1:def 7;
end;
A16: F1 is_transformable_to F2
proof let a be Object of [:A,B:];
thus Hom(F1.a,F2.a) <> {} by A7;
end;
u' is transformation of F1,F2
proof
thus F1 is_transformable_to F2 by A16;
let a be Object of [:A,B:];
u'.a in Hom(F1.a,F2.a) by A7;
hence u'.a is Morphism of F1.a,F2.a by CAT_1:def 7;
end;
then reconsider u = u' as transformation of F1,F2;
A17:now let ab1,ab2 be Object of [:A,B:] such that
A18: Hom(ab1,ab2) <> {};
consider a1 being Object of A, b1 being Object of B such that
A19: ab1 = [a1,b1] by A6,DOMAIN_1:9;
(export F1).a1 = F1?-a1 & (export F2).a1 = F2?-a1 by Th24;
then t.a1 = [[F1?-a1,F2?-a1],t'.a1] by A5;
then [[F1?-a1,F2?-a1],t'.a1] in the Morphisms of Functors(B,C);
then [[F1?-a1,F2?-a1],t'.a1] in NatTrans(B,C) by NATTRA_1:def 18;
then consider G1,H1 being Functor of B,C,
t1 being natural_transformation of G1,H1 such that
A20: [[F1?-a1,F2?-a1],t'.a1] = [[G1,H1],t1] and
A21: G1 is_naturally_transformable_to H1 by NATTRA_1:def 15;
A22: [F1?-a1,F2?-a1] = [G1,H1] & t'.a1 = t1 by A20,ZFMISC_1:33;
then A23: F1?-a1 = G1 & F2?-a1 = H1 by ZFMISC_1:33;
consider a2 being Object of A, b2 being Object of B such that
A24: ab2 = [a2,b2] by A6,DOMAIN_1:9;
(export F1).a2 = F1?-a2 & (export F2).a2 = F2?-a2 by Th24;
then t.a2 = [[F1?-a2,F2?-a2],t'.a2] by A5;
then [[F1?-a2,F2?-a2],t'.a2] in the Morphisms of Functors(B,C);
then [[F1?-a2,F2?-a2],t'.a2] in NatTrans(B,C) by NATTRA_1:def 18;
then consider G2,H2 being Functor of B,C,
t2 being natural_transformation of G2,H2 such that
A25: [[F1?-a2,F2?-a2],t'.a2] = [[G2,H2],t2] and
A26: G2 is_naturally_transformable_to H2 by NATTRA_1:def 15;
A27: [F1?-a2,F2?-a2] = [G2,H2] & t'.a2 = t2 by A25,ZFMISC_1:33;
then A28: F1?-a2 = G2 & F2?-a2 = H2 by ZFMISC_1:33;
let f be Morphism of ab1,ab2;
f is Morphism of [:A,B:] & the Morphisms of [:A,B:] =
[:the Morphisms of A, the Morphisms of B:] by CAT_2:33;
then consider g being (Morphism of A), h being Morphism of B such that
A29: f = [g,h] by DOMAIN_1:9;
A30: Hom(b1,b2) <> {} & Hom(a1,a2) <> {} by A18,A19,A24,Th13;
reconsider g as Morphism of a1,a2 by A18,A19,A24,A29,Th14;
reconsider h as Morphism of b1,b2 by A18,A19,A24,A29,Th14;
A31: dom g = a1 & cod g = a2 by A30,CAT_1:23;
then A32: G1 is_naturally_transformable_to G2 by A23,A28,Th18;
then A33: G1 is_transformable_to G2 by NATTRA_1:def 7;
A34: H1 is_naturally_transformable_to H2 by A23,A28,A31,Th18;
then A35: H1 is_transformable_to H2 by NATTRA_1:def 7;
A36: G1 is_transformable_to H1 by A21,NATTRA_1:def 7;
A37: G2 is_transformable_to H2 by A26,NATTRA_1:def 7;
reconsider v1 = F1?-g as natural_transformation of G1,G2 by A22,A28,A31,
ZFMISC_1:33;
reconsider v2 = F2?-g as natural_transformation of H1,H2 by A22,A28,A31,
ZFMISC_1:33;
A38: Hom(G2.b2,H2.b2) <> {} by A26,ISOCAT_1:30;
A39: Hom(G1.b2,G2.b2) <> {} by A32,ISOCAT_1:30;
A40: Hom(G1.b1,G1.b2) <> {} by A30,CAT_1:126;
A41: Hom(H1.b2,H2.b2) <> {} by A34,ISOCAT_1:30;
A42: Hom(G1.b2,H1.b2) <> {} by A21,ISOCAT_1:30;
A43: Hom(H1.b1,H1.b2) <> {} by A30,CAT_1:126;
A44: Hom(G1.b1,H1.b1) <> {} by A21,ISOCAT_1:30;
A45: Hom(F1.ab1,F2.ab1) <> {} by A16,NATTRA_1:def 2;
A46: Hom(F2.ab1,F2.ab2) <> {} by A18,CAT_1:126;
A47: Hom(F1.ab1,F1.ab2) <> {} by A18,CAT_1:126;
A48: Hom(F1.ab2,F2.ab2) <> {} by A16,NATTRA_1:def 2;
A49: Hom(G1.b1,G2.b2) <> {} by A39,A40,CAT_1:52;
A50: Hom(H1.b1,H2.b2) <> {} by A41,A43,CAT_1:52;
A51: Hom((export F1).a1,(export F1).a2) <> {} by A30,CAT_1:126;
A52: Hom((export F2).a1,(export F2).a2) <> {} by A30,CAT_1:126;
A53: Hom((export F1).a1,(export F2).a1) <> {} by A1,ISOCAT_1:30;
A54: Hom((export F1).a2,(export F2).a2) <> {} by A1,ISOCAT_1:30;
A55: (export F1).a2 = F1?-a2 & (export F2).a1 = F2?-a1 &
(export F1).a1 = F1?-a1 & (export F2).a2 = F2?-a2 by Th24;
reconsider f' = f as Morphism of [:A,B:];
reconsider g' = g as Morphism of A;
reconsider h' = h as Morphism of B;
reconsider e1 = (export F1).g, e2 = (export F2).g
as Morphism of Functors(B,C);
A56: (export F1).g' = [[G1,G2],v1] by A23,A28,A31,Def4;
A57: (export F2).g' = [[H1,H2],v2] by A23,A28,A31,Def4;
A58: t.a1 = [[G1,H1],t1] by A5,A20,A55;
t.a2 = [[G2,H2],t2] by A5,A25,A55;
then [[G1,H2],t2`*`v1]
= t.a2*(export F1).g' by A56,NATTRA_1:42
.= t.a2*e1 by A30,NATTRA_1:def 1
.= t.a2*(export F1).g by A51,A54,CAT_1:def 13
.= (export F2).g*t.a1 by A1,A30,NATTRA_1:def 8
.= e2*t.a1 by A52,A53,CAT_1:def 13
.= (export F2).g'*t.a1 by A30,NATTRA_1:def 1
.= [[G1,H2],v2`*`t1] by A57,A58,NATTRA_1:42;
then A59: t2`*`v1 = v2`*`t1 by ZFMISC_1:33;
A60: u.ab2 = u'.ab2 by A16,NATTRA_1:def 5
.= t'.a2.b2 by A24,Th2 .= t2.b2 by A27,A37,NATTRA_1:def 5;
Hom(a1,a1) <> {} by CAT_1:56;
then A61: g'*(id a1) = g*(id a1) by A30,CAT_1:def 13 .= g by A30,CAT_1:58;
Hom(b2,b2) <> {} by CAT_1:56;
then A62: (id b2)*h' = (id b2)*h by A30,CAT_1:def 13.= h by A30,CAT_1:57;
A63: cod id a1 = a1 & cod h = b2 & dom g = a1 & dom id b2 = b2
by A30,CAT_1:23,44;
then A64: cod[id a1,h] = [a1,b2] by CAT_2:38 .= dom[g,id b2] by A63,CAT_2:38;
then A65: f = [g,id b2]*[id a1, h] by A29,A61,A62,CAT_2:40;
the Morphisms of [:A,B:] = [:the Morphisms of A, the Morphisms of B:]
by CAT_2:33;
then reconsider FF1 = F1, FF2 = F2 as Function of
[:the Morphisms of A, the Morphisms of B:], the Morphisms of C;
A66: curry(F1,g) = (curry FF1).g by Def2;
A67: v1.b2 = (v1 qua Function of the Objects of B, the Morphisms of C).b2
by A33,NATTRA_1:def 5
.= (curry(F1,g)*the Id of B).b2 by Def3
.= curry(F1,g).((the Id of B).b2) by FUNCT_2:21
.= curry(F1,g).id b2 by CAT_1:def 5
.= F1.[g,id b2] by A66,CAT_2:3;
A68: G1.h = (F1?-a1).(h qua Morphism of B) by A23,A30,NATTRA_1:def 1
.= F1.[id a1,h] by CAT_2:47;
A69: F1.f = F1.f' by A18,NATTRA_1:def 1
.= v1.b2*(G1.h qua Morphism of C) by A64,A65,A67,A68,CAT_1:99
.= v1.b2*G1.h by A39,A40,CAT_1:def 13;
A70: u.ab1 = u'.ab1 by A16,NATTRA_1:def 5
.= t'.a1.b1 by A19,Th2 .= t1.b1 by A22,A36,NATTRA_1:def 5;
A71: curry(F2,g) = (curry FF2).g by Def2;
A72: v2.b2 = (v2 qua Function of the Objects of B, the Morphisms of C).b2
by A35,NATTRA_1:def 5
.= (curry(F2,g)*the Id of B).b2 by Def3
.= curry(F2,g).((the Id of B).b2) by FUNCT_2:21
.= curry(F2,g).id b2 by CAT_1:def 5
.= F2.[g,id b2] by A71,CAT_2:3;
A73: H1.h = (F2?-a1).(h qua Morphism of B) by A23,A30,NATTRA_1:def 1
.= F2.[id a1,h] by CAT_2:47;
A74: F2.f = F2.f' by A18,NATTRA_1:def 1
.= v2.b2*(H1.h qua Morphism of C) by A64,A65,A72,A73,CAT_1:99
.= v2.b2*H1.h by A41,A43,CAT_1:def 13;
thus u.ab2*F1.f
= t2.b2*(v1.b2*G1.h qua Morphism of C) by A47,A48,A60,A69,CAT_1:def 13
.= t2.b2*(v1.b2*G1.h) by A38,A49,CAT_1:def 13
.= t2.b2*v1.b2*G1.h by A38,A39,A40,CAT_1:54
.= (v2`*`t1).b2*G1.h by A26,A32,A59,NATTRA_1:27
.= v2.b2*t1.b2*G1.h by A21,A34,NATTRA_1:27
.= v2.b2*(t1.b2*G1.h) by A40,A41,A42,CAT_1:54
.= v2.b2*(H1.h*t1.b1) by A21,A30,NATTRA_1:def 8
.= v2.b2*H1.h*t1.b1 by A41,A43,A44,CAT_1:54
.= F2.f*(u.ab1 qua Morphism of C) by A44,A50,A70,A74,CAT_1:def 13
.= F2.f*u.ab1 by A45,A46,CAT_1:def 13;
end;
thus
A75: F1 is_naturally_transformable_to F2
proof
thus F1 is_transformable_to F2 by A16;
thus thesis by A17;
end;
u is natural_transformation of F1,F2
proof
thus F1 is_naturally_transformable_to F2 by A75;
thus thesis by A17;
end;
then reconsider u as natural_transformation of F1,F2;
take u;
now let s be Function of
[:the Objects of A, the Objects of B:], the Morphisms of C such that
A76: u = s;
let a be Object of A;
t' = curry u' by Th1;
hence t.a = [[(export F1).a,(export F2).a],(curry s).a] by A5,A76;
end;
hence t = export u 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[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 = [[export F1,export F2],export t];
A1: now let o; assume
o in the Morphisms of Functors([:A,B:],C);
then o in NatTrans([:A,B:],C) by NATTRA_1:def 18;
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;
take m = [[export F1, export F2], export t];
export F1 is_naturally_transformable_to export F2 by A3,Th27;
then m in NatTrans(A,Functors(B,C)) by NATTRA_1:def 16;
hence m in the Morphisms of Functors(A,Functors(B,C)) by NATTRA_1:def 18;
thus P[o,m]
proof
let F1',F2' be Functor of [:A,B:],C,
t' be natural_transformation of F1',F2';
assume A4: o = [[F1',F2'],t'];
then [F1,F2] = [F1',F2'] & t = t' by A2,ZFMISC_1:33;
then F1 = F1' & F2 = F2' by ZFMISC_1:33;
hence m = [[export F1', export F2'], export t'] by A2,A4,ZFMISC_1:33;
end;
end;
consider FF being Function of
the Morphisms of Functors([:A,B:],C),
the Morphisms of Functors(A,Functors(B,C))
such that
A5: for o st o in the Morphisms of Functors([:A,B:],C) holds P[o,FF.o]
from FuncEx1(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 Th8;
A6: id c = [[F,F],id F] by NATTRA_1:def 18;
reconsider d = export F as Object of Functors(A,Functors(B,C))
by Th8;
take d;
A7: id export F = export id F by Th28;
thus FF.id c = [[export F, export F], export id F] by A5,A6
.= id d by A7,NATTRA_1:def 18;
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
A8: dom f = F1 & cod f = F2 & f =[[F1,F2],t] by Th9;
A9: id dom f = [[F1,F1],id F1] by A8,NATTRA_1:def 18;
A10: FF.f = [[export F1, export F2], export t] by A5,A8;
then A11: dom(FF.f) = export F1 by NATTRA_1:39;
thus FF.id dom f
= [[export F1, export F1], export id F1] by A5,A9
.= [[export F1, export F1], id export F1] by Th28
.= id dom(FF.f) by A11,NATTRA_1:def 18;
A12: id cod f = [[F2,F2],id F2] by A8,NATTRA_1:def 18;
A13: cod(FF.f) = export F2 by A10,NATTRA_1:39;
thus FF.id cod f = [[export F2, export F2], export id F2] by A5,A12
.= [[export F2, export F2], id export F2] by Th28
.= id cod(FF.f) by A13,NATTRA_1:def 18;
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
A14: F1 is_naturally_transformable_to F2 and
A15: dom f = F1 & cod f = F2 & f =[[F1,F2],t] by Th9;
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 & cod g = G2 & g =[[G1,G2],u] by Th9;
assume A19:dom g = cod f;
then reconsider u as natural_transformation of F2,G2 by A15,A18;
g*f = [[F1,G2],u`*`t] by A15,A18,A19,NATTRA_1:42;
then A20: FF.(g*f) = [[export F1, export G2], export(u`*`t)] by A5;
A21: FF.g = [[export F2, export G2], export u] by A5,A15,A18,A19;
(export u)`*`(export t) = export(u`*`t) by A14,A15,A17,A18,A19,Th29;
hence FF.(g*f) = FF.g*FF.f by A16,A20,A21,NATTRA_1:42;
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:35;
then [[F1,F2],t] in the Morphisms of Functors([:A,B:],C) by NATTRA_1:def 18
;
hence FF.[[F1,F2],t] = [[export F1, export F2],export t] 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
A26: dom f = F1 & cod f = F2 & f =[[F1,F2],t] by Th9;
thus (IT1 qua Function of
the Morphisms of Functors([:A,B:],C),
the Morphisms of Functors(A,Functors(B,C))
).f
= [[export F1, export F2], export t] by A23,A25,A26
.= (IT2 qua Function of
the Morphisms of Functors([:A,B:],C),
the Morphisms of Functors(A,Functors(B,C))
).f by A24,A25,A26;
end;
hence thesis by FUNCT_2:113;
end;
end;
theorem Th33:
export(A,B,C) is_an_isomorphism
proof
A1: dom export(A,B,C) = the Morphisms of Functors([:A,B:],C) by FUNCT_2:def 1;
thus export(A,B,C) is one-to-one
proof let x1,x2 be set;
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
A2: F1 is_naturally_transformable_to F2 and
A3: dom f1 = F1 & cod f1 = F2 & f1 =[[F1,F2],t] by Th9;
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
A4: G1 is_naturally_transformable_to G2 and
A5: dom f2 = G1 & cod f2 = G2 & f2 =[[G1,G2],u] by Th9;
assume
export(A,B,C).x1 = export(A,B,C).x2;
then [[export F1, export F2], export t]
= export(A,B,C).[[G1,G2],u] by A2,A3,A5,Def6
.= [[export G1, export G2], export u] by A4,Def6;
then A6: [export F1, export F2] = [export G1, export G2] & export u =
export t
by ZFMISC_1:33;
then export F1 = export G1 & export F2 = export G2 by ZFMISC_1:33;
then F1 = G1 & F2 = G2 by Th26;
hence x1 = x2 by A2,A3,A5,A6,Th30;
end;
thus rng export(A,B,C) c= the Morphisms of Functors(A,Functors(B,C))
by RELSET_1:12;
let m;
assume m in the Morphisms 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
A7: F1 is_naturally_transformable_to F2 and
A8: dom f = F1 & cod f = F2 & f =[[F1,F2],t] by Th9;
consider G1 being Functor of [:A,B:],C such that
A9: F1 = export G1 by Th31;
consider G2 being Functor of [:A,B:],C such that
A10: F2 = export G2 by Th31;
A11: G1 is_naturally_transformable_to G2 by A7,A9,A10,Th32;
consider u being natural_transformation of G1,G2 such that
A12: t = export u by A7,A9,A10,Th32;
A13: export(A,B,C).[[G1,G2],u] = f by A8,A9,A10,A11,A12,Def6;
[[G1,G2],u] in NatTrans([:A,B:],C) by A11,NATTRA_1:35;
then [[G1,G2],u] in dom export(A,B,C) by A1,NATTRA_1:def 18;
hence thesis by A13,FUNCT_1:def 5;
end;
theorem
Functors([:A,B:],C) ~= Functors(A,Functors(B,C))
proof take export(A,B,C);
thus export(A,B,C) is_an_isomorphism by Th33;
end;
begin :: The isomorphism between (B x C)^A and B^A x C^A
theorem Th35:
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 by NATTRA_1:def 7;
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;
redefine func pr1(A,B) -> Functor of [:A,B:], A;
coherence;
func pr2(A,B) -> Functor of [:A,B:], B;
coherence;
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:];
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
:Def7: pr1(B,C)*F;
correctness;
func Pr2 F -> Functor of A,C equals
:Def8: pr2(B,C)*F;
correctness;
end;
theorem Th36:
for F being Functor of A,B, G being Functor of A,C holds
Pr1<:F,G:> = F & Pr2<:F,G:> = G
proof let F be Functor of A,B, G be Functor of A,C;
thus Pr1<:F,G:> = pr1(B,C)*<:F,G:> by Def7
.= pr1(the Morphisms of B, the Morphisms of C)*<:F,G:> by CAT_2:def 10
.= F by FUNCT_3:82;
thus Pr2<:F,G:> = pr2(B,C)*<:F,G:> by Def8
.= pr2(the Morphisms of B, the Morphisms of C)*<:F,G:> by CAT_2:def 11
.= G by FUNCT_3:82;
end;
theorem Th37:
for F,G being Functor of A, [:B,C:] st Pr1 F = Pr1 G & Pr2 F = Pr2 G
holds F = G
proof let F,G be Functor of A, [:B,C:];
the Morphisms of [:B,C:] = [:the Morphisms of B, the Morphisms of C:]
by CAT_2:33;
then reconsider f = F, g = G as
Function of the Morphisms of A, [:the Morphisms of B, the Morphisms of C:];
assume
A1: Pr1 F = Pr1 G;
A2: pr1(the Morphisms of B, the Morphisms of C)*f
= pr1(B,C)*f by CAT_2:def 10
.= Pr1 G by A1,Def7
.= pr1(B,C)*g by Def7
.= pr1(the Morphisms of B, the Morphisms of C)*g by CAT_2:def 10;
assume
A3: Pr2 F = Pr2 G;
pr2(the Morphisms of B, the Morphisms of C)*f
= pr2(B,C)*f by CAT_2:def 11
.= Pr2 G by A3,Def8
.= pr2(B,C)*g by Def8
.= pr2(the Morphisms of B, the Morphisms of C)*g by CAT_2:def 11;
hence thesis by A2,Th5;
end;
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
:Def9: pr1(B,C)*t;
coherence
proof Pr1 F1 = pr1(B,C)*F1 & Pr1 F2 = pr1(B,C)*F2 by Def7;
hence thesis;
end;
func Pr2 t -> natural_transformation of Pr2 F1, Pr2 F2 equals
:Def10: pr2(B,C)*t;
coherence
proof Pr2 F1 = pr2(B,C)*F1 & Pr2 F2 = pr2(B,C)*F2 by Def8;
hence thesis;
end;
end;
theorem Th38:
for F,G being Functor of A, [:B,C:] st
F is_naturally_transformable_to G
holds Pr1 F is_naturally_transformable_to Pr1 G
& Pr2 F is_naturally_transformable_to Pr2 G
proof let F,G be Functor of A, [:B,C:];
Pr1 F = pr1(B,C)*F & Pr2 F = pr2(B,C)*F &
Pr1 G = pr1(B,C)*G & Pr2 G = pr2(B,C)*G by Def7,Def8;
hence thesis by ISOCAT_1:27;
end;
theorem Th39:
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 & Pr2 s = Pr2 t;
the Morphisms of [:B,C:] = [:the Morphisms of B, the Morphisms of C:]
by CAT_2:33;
then reconsider S = s, T = t as
Function of the Objects of A, [:the Morphisms of B, the Morphisms of C:];
A4: pr1(the Morphisms of B, the Morphisms of C)*S
= pr1(B,C)*S by CAT_2:def 10
.= pr1(B,C)*s by A1,Th35
.= Pr1 s by Def9
.= pr1(B,C)*t by A3,Def9
.= pr1(B,C)*T by A2,Th35
.= pr1(the Morphisms of B, the Morphisms of C)*T by CAT_2:def 10;
pr2(the Morphisms of B, the Morphisms of C)*S
= pr2(B,C)*S by CAT_2:def 11
.= pr2(B,C)*s by A1,Th35
.= Pr2 s by Def10
.= pr2(B,C)*t by A3,Def10
.= pr2(B,C)*T by A2,Th35
.= pr2(the Morphisms of B, the Morphisms of C)*T by CAT_2:def 11;
hence thesis by A4,Th5;
end;
theorem Th40:
for F being Functor of A, [:B,C:]
holds id Pr1 F = Pr1 id F & id Pr2 F = Pr2 id F
proof let F be Functor of A, [:B,C:];
thus id Pr1 F = id(pr1(B,C)*F) by Def7
.= pr1(B,C)*id F by ISOCAT_1:38
.= Pr1 id F by Def9;
thus id Pr2 F = id(pr2(B,C)*F) by Def8
.= pr2(B,C)*id F by ISOCAT_1:38
.= Pr2 id F by Def10;
end;
theorem Th41:
for F,G,H being Functor of A, [:B,C:] st
F is_naturally_transformable_to G &
G is_naturally_transformable_to H
for s being natural_transformation of F,G,
t being natural_transformation of G,H
holds Pr1 t`*`s = (Pr1 t)`*`Pr1 s & Pr2 t`*`s = (Pr2 t)`*`Pr2 s
proof let F,G,H be Functor of A, [:B,C:] such that
A1: F is_naturally_transformable_to G and
A2: G is_naturally_transformable_to H;
let s be natural_transformation of F,G,
t be natural_transformation of G,H;
A3: Pr1 t = pr1(B,C)*t & Pr1 s = pr1(B,C)*s by Def9;
A4: pr1(B,C)*F = Pr1 F & pr1(B,C)*G = Pr1 G & pr1(B,C)*H = Pr1 H by Def7;
thus Pr1 t`*`s = pr1(B,C)*(t`*`s) by Def9
.= (Pr1 t)`*`Pr1 s by A1,A2,A3,A4,ISOCAT_1:32;
A5: Pr2 t = pr2(B,C)*t & Pr2 s = pr2(B,C)*s by Def10;
A6: pr2(B,C)*F = Pr2 F & pr2(B,C)*G = Pr2 G & pr2(B,C)*H = Pr2 H by Def8;
thus Pr2 t`*`s = pr2(B,C)*(t`*`s) by Def10
.= (Pr2 t)`*`Pr2 s by A1,A2,A5,A6,ISOCAT_1:32;
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 = [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 Objects of A, the Morphisms of B;
reconsider s2 = t2 as Function of the Objects of A, the Morphisms of C;
thus <:t1,t2:>.a
= [s1.a,s2.a] by FUNCT_3:79
.= [t1.a,s2.a] by A1,NATTRA_1:def 5
.= [t1.a,t2.a] by A1,NATTRA_1:def 5;
end;
theorem Th42:
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]
proof let F be Functor of A,B, G be Functor of A,C;
let a,b be Object of A such that
A1: Hom(a,b) <> {};
let f be Morphism of a,b;
reconsider g = f as Morphism of A;
thus <:F,G:>.f = <:F,G:>.g by A1,NATTRA_1:def 1
.= [F.g,G.g] by FUNCT_3:79
.= [F.g,G.f] by A1,NATTRA_1:def 1
.= [F.f,G.f] by A1,NATTRA_1:def 1;
end;
theorem Th43:
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:79
.= [id(F.a),G.(id a qua Morphism of A)] by CAT_1:108
.= [id(F.a),id(G.a)] by CAT_1:108
.= id[F.a,G.a] by CAT_2:41;
hence <:F,G:>.a = [F.a,G.a] by CAT_1:107;
end;
Lm4:
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:7;
[F1.a,F2.a] = <:F1,F2:>.a & [G1.a,G2.a] = <:G1,G2:>.a &
[t1.a,t2.a] = <:t1,t2:>.a by A1,Lm3,Th43;
hence <:t1,t2:>.a in Hom(<:F1,F2:>.a,<:G1,G2:>.a) by A2,Th16;
end;
theorem Th44:
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:>
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 a be Object of A;
thus Hom(<:F1,F2:>.a,<:G1,G2:>.a) <> {} 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_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
the Morphisms of [:B,C:] = [:the Morphisms of B, the Morphisms of C:]
by CAT_2:33;
then reconsider t = <:t1,t2:> as
Function of the Objects of A, the Morphisms of [:B,C:];
t is transformation of <:F1,F2:>,<:G1,G2:>
proof thus <:F1,F2:> is_transformable_to <:G1,G2:> by A1,Th44;
let a be Object of A;
t.a in Hom(<:F1,F2:>.a,<:G1,G2:>.a) by A1,Lm4;
hence t.a is Morphism of <:F1,F2:>.a,<:G1,G2:>.a by CAT_1:def 7;
end;
hence thesis;
end;
end;
theorem Th45:
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 Objects of A, the Morphisms of B;
reconsider s2 = t2 as Function of the Objects of A, the Morphisms of C;
<:F1,F2:> is_transformable_to <:G1,G2:> by A1,Th44;
hence <:t1,t2:>.a
= (<:t1,t2:> qua
Function of the Objects of A, the Morphisms of [:B,C:]).a
by NATTRA_1:def 5
.= <:s1,s2:>.a by A1,Def11
.= [t1.a,t2.a] by A1,Lm3;
end;
Lm5:
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;
A3: F1 is_transformable_to G1 & F2 is_transformable_to G2
by A1,A2,NATTRA_1:def 7;
let t1 be natural_transformation of F1,G1,
t2 be natural_transformation of F2,G2;
let a,b be Object of A such that
A4: Hom(a,b) <> {};
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,A4,NATTRA_1:def 8;
A6: <:t1,t2:>.b = [t1.b,t2.b] by A3,Th45;
A7: <:F1,F2:>.f = [F1.f,F2.f] by A4,Th42;
A8: Hom(F1.b,G1.b) <> {} by A3,NATTRA_1:def 2;
A9: Hom(F1.a,F1.b) <> {} by A4,CAT_1:126;
A10: Hom(F2.a,F2.b) <> {} by A4,CAT_1:126;
A11: Hom(F2.b,G2.b) <> {} by A3,NATTRA_1:def 2;
A12: Hom(F1.a,G1.a) <> {} by A3,NATTRA_1:def 2;
A13: Hom(G1.a,G1.b) <> {} by A4,CAT_1:126;
A14: Hom(F2.a,G2.a) <> {} by A3,NATTRA_1:def 2;
A15: Hom(G2.a,G2.b) <> {} by A4,CAT_1:126;
A16: dom(t1.b) = F1.b by A8,CAT_1:23 .= cod(F1.f) by A9,CAT_1:23;
A17: dom(t2.b) = F2.b by A11,CAT_1:23 .= cod(F2.f) by A10,CAT_1:23;
A18: t1.b*F1.f = t1.b*(F1.f qua Morphism of B) by A8,A9,CAT_1:def 13;
A19: t2.b*F2.f = t2.b*(F2.f qua Morphism of C) by A10,A11,CAT_1:def 13;
A20: G1.f*t1.a = G1.f*(t1.a qua Morphism of B) by A12,A13,CAT_1:def 13;
A21: G2.f*t2.a = G2.f*(t2.a qua Morphism of C) by A14,A15,CAT_1:def 13;
A22: cod(t1.a) = G1.a by A12,CAT_1:23 .= dom(G1.f) by A13,CAT_1:23;
A23: cod(t2.a) = G2.a by A14,CAT_1:23 .= dom(G2.f) by A15,CAT_1:23;
A24: <:G1,G2:>.f = [G1.f,G2.f] by A4,Th42;
A25: <:t1,t2:>.a = [t1.a,t2.a] by A3,Th45;
A26: <:F1,F2:> is_transformable_to <:G1,G2:> by A3,Th44;
then A27: Hom(<:F1,F2:>.a,<:G1,G2:>.a) <> {} by NATTRA_1:def 2;
A28: Hom(<:G1,G2:>.a,<:G1,G2:>.b) <> {} by A4,CAT_1:126;
A29: Hom(<:F1,F2:>.a,<:F1,F2:>.b) <> {} by A4,CAT_1:126;
Hom(<:F1,F2:>.b,<:G1,G2:>.b) <> {} by A26,NATTRA_1:def 2;
hence <:t1,t2:>.b*<:F1,F2:>.f
= <:t1,t2:>.b*(<:F1,F2:>.f qua Morphism of [:B,C:]) by A29,CAT_1:def 13
.= [G1.f*t1.a,G2.f*t2.a] by A5,A6,A7,A16,A17,A18,A19,CAT_2:39
.= <:G1,G2:>.f*(<:t1,t2:>.a qua Morphism of [:B,C:])
by A20,A21,A22,A23,A24,A25,CAT_2:39
.= <:G1,G2:>.f*<:t1,t2:>.a by A27,A28,CAT_1:def 13;
end;
theorem Th46:
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 and
A2: F2 is_naturally_transformable_to G2;
F1 is_transformable_to G1 &
F2 is_transformable_to G2 by A1,A2,NATTRA_1:def 7;
hence <:F1,F2:> is_transformable_to <:G1,G2:> by Th44;
consider t1 being natural_transformation of F1,G1,
t2 being natural_transformation of F2,G2;
take <:t1,t2:>;
thus thesis by A1,A2,Lm5;
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 and
A2: 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
<:t1,t2:> is natural_transformation of <:F1,F2:>,<:G1,G2:>
proof
thus <:F1,F2:> is_naturally_transformable_to <:G1,G2:> by A1,A2,Th46;
thus thesis by A1,A2,Lm5;
end;
hence thesis;
end;
end;
theorem Th47:
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 and
A2: F2 is_naturally_transformable_to G2;
A3: F1 is_transformable_to G1 & F2 is_transformable_to G2
by A1,A2,NATTRA_1:def 7;
let t1 be natural_transformation of F1,G1,
t2 be natural_transformation of F2,G2;
reconsider s = t1 as Function of the Objects of A, the Morphisms of B;
A4: <:F1,F2:> is_naturally_transformable_to <:G1,G2:> by A1,A2,Th46;
then A5: <:F1,F2:> is_transformable_to <:G1,G2:> by NATTRA_1:def 7;
thus Pr1<:t1,t2:> = pr1(B,C)*<:t1,t2:> by Def9
.= pr1(B,C)
*(<:t1,t2:> qua transformation of <:F1,F2:>,<:G1,G2:>)
by A4,ISOCAT_1:def 7
.= pr1(B,C)*
(<:t1,t2:> qua Function of the Objects of A, the Morphisms of [:B,C:])
by A5,ISOCAT_1:def 5
.= pr1(B,C)*
(<:t1 qua transformation of F1,G1,t2:>
qua Function of the Objects of A, the Morphisms of [:B,C:])
by A1,A2,Def12
.= pr1(B,C)*<:s,t2:> by A3,Def11
.= pr1(the Morphisms of B, the Morphisms of C)*<:s,t2:> by CAT_2:def 10
.= t1 by FUNCT_3:82;
thus Pr2<:t1,t2:> = pr2(B,C)*<:t1,t2:> by Def10
.= pr2(B,C)
*(<:t1,t2:> qua transformation of <:F1,F2:>,<:G1,G2:>)
by A4,ISOCAT_1:def 7
.= pr2(B,C)*
(<:t1,t2:> qua Function of the Objects of A, the Morphisms of [:B,C:])
by A5,ISOCAT_1:def 5
.= pr2(B,C)*
(<:t1 qua transformation of F1,G1,t2:>
qua Function of the Objects of A, the Morphisms of [:B,C:])
by A1,A2,Def12
.= pr2(B,C)*<:s,t2:> by A3,Def11
.= pr2(the Morphisms of B, the Morphisms of C)*<:s,t2:> by CAT_2:def 11
.= t2 by FUNCT_3:82;
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:]);
A2: the Morphisms of Functors(A,B) = NatTrans(A,B) &
the Morphisms of Functors(A,C) = NatTrans(A,C) by NATTRA_1:def 18;
consider F1,F2 being Functor of A,[:B,C:],
s being natural_transformation of F1,F2 such that
A3: F1 is_naturally_transformable_to F2 and
A4: dom(f) = F1 & cod f = F2 & f = [[F1,F2],s] by Th9;
Pr1 F1 is_naturally_transformable_to Pr1 F2 &
Pr2 F1 is_naturally_transformable_to Pr2 F2 by A3,Th38;
then [[Pr1 F1, Pr1 F2],Pr1 s] is Morphism of Functors(A,B) &
[[Pr2 F1, Pr2 F2],Pr2 s] is Morphism of Functors(A,C) by A2,NATTRA_1:35;
then reconsider g = [[[Pr1 F1, Pr1 F2],Pr1 s],[[Pr2 F1, Pr2 F2],Pr2 s]]
as Morphism of [:Functors(A,B),Functors(A,C):] by CAT_2:36;
take g;
thus P[f,g]
proof
let G1,G2 be Functor of A,[:B,C:],
t be natural_transformation of G1,G2;
assume f = [[G1,G2],t];
then A5: [G1,G2] = [F1,F2] & t = s by A4,ZFMISC_1:33;
then G1 = F1 & G2 = F2 by ZFMISC_1:33;
hence g = [[[Pr1 G1, Pr1 G2],Pr1 t],[[Pr2 G1, Pr2 G2],Pr2 t]] by A5;
end;
end;
consider IT being Function of
the Morphisms of Functors(A,[:B,C:]),
the Morphisms 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 FuncExD(A1);
IT is Functor of Functors(A,[:B,C:]), [:Functors(A,B),Functors(A,C):]
proof
A7: the Morphisms of Functors(A,B) = NatTrans(A,B) by NATTRA_1:def 18;
A8: the Morphisms of Functors(A,C) = NatTrans(A,C) by NATTRA_1:def 18;
thus for c being Object of Functors(A,[:B,C:])
ex d being Object of [:Functors(A,B),Functors(A,C):] st IT.id c = id d
proof let c be Object of Functors(A,[:B,C:]);
reconsider F = c as Functor of A, [:B,C:] by Th8;
reconsider d1 = Pr1 F as Object of Functors(A,B) by Th8;
reconsider d2 = Pr2 F as Object of Functors(A,C) by Th8;
take [d1,d2];
Pr1 id F = id Pr1 F by Th40;
then A9: id d1 = [[Pr1 F, Pr1 F], Pr1 id F] by NATTRA_1:def 18;
Pr2 id F = id Pr2 F by Th40;
then A10: id d2 = [[Pr2 F, Pr2 F], Pr2 id F] by NATTRA_1:def 18;
id c = [[F,F], id F] by NATTRA_1:def 18;
hence IT.id c
= [id d1, id d2] by A6,A9,A10
.= id [d1,d2] by CAT_2:41;
end;
thus for f being Morphism of Functors(A,[:B,C:]) holds
IT.id dom f = id dom(IT.f) & IT.id cod f = id cod(IT.f)
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 & cod f = F2 & f = [[F1,F2],s] by Th9;
Pr1 F1 is_naturally_transformable_to Pr1 F2 by A11,Th38;
then reconsider f1 = [[Pr1 F1, Pr1 F2],Pr1 s]
as Morphism of Functors(A,B) by A7,NATTRA_1:35;
Pr2 F1 is_naturally_transformable_to Pr2 F2 by A11,Th38;
then reconsider f2 = [[Pr2 F1, Pr2 F2],Pr2 s]
as Morphism of Functors(A,C) by A8,NATTRA_1:35;
dom f1 = Pr1 F1 & Pr1 id F1 = id Pr1 F1 by Th40,NATTRA_1:39;
then A13: id dom f1 = [[Pr1 F1, Pr1 F1], Pr1 id F1] by NATTRA_1:def 18;
dom f2 = Pr2 F1 & Pr2 id F1 = id Pr2 F1 by Th40,NATTRA_1:39;
then A14: id dom f2 = [[Pr2 F1, Pr2 F1], Pr2 id F1] by NATTRA_1:def 18;
id dom f = [[F1,F1], id F1] by A12,NATTRA_1:def 18;
hence IT.id dom f
= [id dom f1, id dom f2] by A6,A13,A14
.= id [dom f1, dom f2] by CAT_2:41
.= id dom [f1,f2] by CAT_2:38
.= id dom(IT.f) by A6,A12;
cod f1 = Pr1 F2 & Pr1 id F2 = id Pr1 F2 by Th40,NATTRA_1:39;
then A15: id cod f1 = [[Pr1 F2, Pr1 F2], Pr1 id F2] by NATTRA_1:def 18;
cod f2 = Pr2 F2 & Pr2 id F2 = id Pr2 F2 by Th40,NATTRA_1:39;
then A16: id cod f2 = [[Pr2 F2, Pr2 F2], Pr2 id F2] by NATTRA_1:def 18;
id cod f = [[F2,F2], id F2] by A12,NATTRA_1:def 18;
hence IT.id cod f
= [id cod f1, id cod f2] by A6,A15,A16
.= id [cod f1, cod f2] by CAT_2:41
.= id cod [f1,f2] by CAT_2:38
.= id cod(IT.f) by A6,A12;
end;
let f,g be Morphism of Functors(A,[:B,C:]) such that
A17: dom g = cod f;
consider F1,F2 being Functor of A,[:B,C:],
s being natural_transformation of F1,F2 such that
A18: F1 is_naturally_transformable_to F2 and
A19: dom(f) = F1 & cod f = F2 & f = [[F1,F2],s] by Th9;
consider G1,G2 being Functor of A,[:B,C:],
t being natural_transformation of G1,G2 such that
A20: G1 is_naturally_transformable_to G2 and
A21: dom(g) = G1 & cod g = G2 & g = [[G1,G2],t] by Th9;
reconsider t as natural_transformation of F2,G2 by A17,A19,A21;
A22: IT.f = [[[Pr1 F1, Pr1 F2],Pr1 s],[[Pr2 F1, Pr2 F2],Pr2 s]] by A6,A19;
Pr1 F1 is_naturally_transformable_to Pr1 F2 &
Pr1 F2 is_naturally_transformable_to Pr1 G2 by A17,A18,A19,A20,A21,Th38;
then reconsider g1 = [[Pr1 F2, Pr1 G2],Pr1 t],
f1 = [[Pr1 F1, Pr1 F2],Pr1 s] as Morphism of Functors(A,B)
by A7,NATTRA_1:35;
Pr2 F1 is_naturally_transformable_to Pr2 F2 &
Pr2 F2 is_naturally_transformable_to Pr2 G2 by A17,A18,A19,A20,A21,Th38;
then reconsider g2 = [[Pr2 F2, Pr2 G2],Pr2 t],
f2 = [[Pr2 F1, Pr2 F2],Pr2 s] as Morphism of Functors(A,C)
by A8,NATTRA_1:35;
A23: dom g1 = Pr1 F2 by NATTRA_1:39 .= cod f1 by NATTRA_1:39;
A24: dom g2 = Pr2 F2 by NATTRA_1:39 .= cod f2 by NATTRA_1:39;
A25: g1*f1 = [[Pr1 F1, Pr1 G2],(Pr1 t)`*`Pr1 s] by NATTRA_1:42
.= [[Pr1 F1, Pr1 G2],Pr1 t`*`s] by A17,A18,A19,A20,A21,Th41;
A26: g2*f2 = [[Pr2 F1, Pr2 G2],(Pr2 t)`*`Pr2 s] by NATTRA_1:42
.= [[Pr2 F1, Pr2 G2],Pr2 t`*`s] by A17,A18,A19,A20,A21,Th41;
g*f = [[F1,G2],t`*`s] by A17,A19,A21,NATTRA_1:42;
hence IT.(g*f) = [g1*f1,g2*f2] by A6,A25,A26
.= [g1,g2]*[f1,f2] by A23,A24,CAT_2:39
.= IT.g*IT.f by A6,A17,A19,A21,A22;
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
A27: 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 A27,NATTRA_1:35;
then reconsider f as Morphism of Functors(A,[:B,C:]) by NATTRA_1:def 18;
thus IT.[[F1,F2],t] = IT.f
.= [[[Pr1 F1, Pr1 F2],Pr1 t],[[Pr2 F1, Pr2 F2],Pr2 t]] by A6;
end;
uniqueness
proof let IT1,IT2 be
Functor of Functors(A,[:B,C:]), [:Functors(A,B),Functors(A,C):] such that
A28: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
A29: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
A30: F1 is_naturally_transformable_to F2 and
A31: dom(f) = F1 & cod f = F2 & f = [[F1,F2],s] by Th9;
thus IT1.f
= [[[Pr1 F1, Pr1 F2],Pr1 s],[[Pr2 F1, Pr2 F2],Pr2 s]] by A28,A30,A31
.= IT2.f by A29,A30,A31;
end;
hence IT1 = IT2 by FUNCT_2:113;
end;
end;
theorem Th48:
distribute(A,B,C) is_an_isomorphism
proof
thus distribute(A,B,C) is one-to-one
proof let x1,x2 be set;
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
A2: dom(f1) = F1 & cod f1 = F2 & f1 = [[F1,F2],s] by Th9;
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
A4: dom(f2) = G1 & cod f2 = G2 & f2 = [[G1,G2],t] by Th9;
assume
distribute(A,B,C).x1 = distribute(A,B,C).x2;
then [[[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 [[Pr1 F1,Pr1 F2],Pr1 s] = [[Pr1 G1,Pr1 G2],Pr1 t] &
[[Pr2 F1,Pr2 F2],Pr2 s] = [[Pr2 G1,Pr2 G2],Pr2 t] by ZFMISC_1:33;
then A5: Pr1 s = Pr1 t & Pr2 s = Pr2 t &
[Pr1 F1,Pr1 F2] = [Pr1 G1,Pr1 G2] & [Pr2 F1,Pr2 F2] = [Pr2 G1,Pr2 G2]
by ZFMISC_1:33;
then Pr1 F1 = Pr1 G1 & Pr2 F1 = Pr2 G1 & Pr1 F2 = Pr1 G2 & Pr2 F2 = Pr2
G2
by ZFMISC_1:33;
then s = t & F1 = G1 & F2 = G2 by A1,A3,A5,Th37,Th39;
hence x1 = x2 by A2,A4;
end;
thus rng distribute(A,B,C) c=
the Morphisms of [:Functors(A,B),Functors(A,C):] by RELSET_1:12;
let o;
assume o in the Morphisms 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
A6: o = [o1,o2] by CAT_2:37;
consider F1,F2 being Functor of A,B,
s being natural_transformation of F1,F2 such that
A7: F1 is_naturally_transformable_to F2 and
A8: dom o1 = F1 & cod o1 = F2 & o1 = [[F1,F2],s] by Th9;
consider G1,G2 being Functor of A,C,
t being natural_transformation of G1,G2 such that
A9: G1 is_naturally_transformable_to G2 and
A10: dom o2 = G1 & cod o2 = G2 & o2 = [[G1,G2],t] by Th9;
set f = [[<:F1,G1:>,<:F2,G2:>],<:s,t:>];
A11: <:F1,G1:> is_naturally_transformable_to <:F2,G2:> by A7,A9,Th46;
then f in NatTrans(A,[:B,C:]) by NATTRA_1:35;
then reconsider f as Morphism of Functors(A,[:B,C:]) by NATTRA_1:def 18;
Pr1<:s,t:> = s & Pr2<:s,t:> = t &
Pr1<:F1,G1:> = F1 & Pr1<:F2,G2:> = F2 &
Pr2<:F1,G1:> = G1 & Pr2<:F2,G2:> = G2 by A7,A9,Th36,Th47;
then distribute(A,B,C).f
= o by A6,A8,A10,A11,Def13;
hence o in rng distribute(A,B,C) by Th4;
end;
theorem
Functors(A,[:B,C:]) ~= [:Functors(A,B),Functors(A,C):]
proof
take distribute(A,B,C);
thus distribute(A,B,C) is_an_isomorphism by Th48;
end;