Copyright (c) 1991 Association of Mizar Users
environ
vocabulary CAT_1, FUNCT_1, RELAT_1, FUNCT_3, NATTRA_1, BOOLE, WELLORD1,
PARTFUN1, SEQ_1, ISOCAT_1;
notation TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_3,
CAT_1, CAT_2, NATTRA_1;
constructors NATTRA_1, MEMBERED, PARTFUN1, XBOOLE_0;
clusters RELSET_1, MEMBERED, ZFMISC_1, XBOOLE_0;
requirements SUBSET, BOOLE;
definitions TARSKI, CAT_1, FUNCT_1, NATTRA_1, XBOOLE_0;
theorems FUNCT_2, CAT_1, ZFMISC_1, FUNCT_1, CAT_2, FUNCT_3, NATTRA_1, RELAT_1,
RELSET_1, XBOOLE_1;
begin
:: Auxiliary theorems
reserve A,B,C,D for Category,
F for Functor of A,B,
G for Functor of B,C;
theorem Th1:
for F,G being Function st F is one-to-one & G is one-to-one
holds [:F,G:] is one-to-one
proof let F,G be Function such that
A1: F is one-to-one and
A2: G is one-to-one;
let z1,z2 be set such that
A3: z1 in dom [:F,G:] & z2 in dom [:F,G:] & [:F,G:].z1 = [:F,G:].z2;
A4: dom[:F,G:] = [:dom F, dom G:] by FUNCT_3:def 9;
then consider x1,y1 being set such that
A5: x1 in dom F & y1 in dom G & z1 = [x1,y1] by A3,ZFMISC_1:103;
consider x2,y2 being set such that
A6: x2 in dom F & y2 in dom G & z2 = [x2,y2] by A3,A4,ZFMISC_1:103;
[:F,G:].z1 = [F.x1,G.y1] & [:F,G:].z2 = [F.x2,G.y2]
by A5,A6,FUNCT_3:def 9;
then F.x1 = F.x2 & G.y1 = G.y2 by A3,ZFMISC_1:33;
then x1 = x2 & y1 = y2 by A1,A2,A5,A6,FUNCT_1:def 8;
hence z1 = z2 by A5,A6;
end;
theorem Th2:
rng pr1(A,B) = the Morphisms of A & rng pr2(B,A) = the Morphisms of A
proof
thus rng pr1(A,B) = rng pr1(the Morphisms of A, the Morphisms of B)
by CAT_2:def 10 .= the Morphisms of A by FUNCT_3:60;
thus rng pr2(B,A) = rng pr2(the Morphisms of B, the Morphisms of A)
by CAT_2:def 11 .= the Morphisms of A by FUNCT_3:62;
end;
theorem Th3:
for f being Morphism of A st f is invertible holds F.f is invertible
proof let f be Morphism of A;
given g being Morphism of A such that
A1: dom g = cod f & cod g = dom f & f*g = id cod f & g*f = id dom f;
take F.g;
thus dom(F.g) = cod(F.f) & cod(F.g) = dom(F.f) by A1,CAT_1:99;
thus F.f*F.g = F.(f*g) by A1,CAT_1:99
.= id cod(F.f) by A1,CAT_1:98;
thus F.g*F.f = F.(g*f) by A1,CAT_1:99
.= id dom(F.f) by A1,CAT_1:98;
end;
theorem Th4:
for F being Functor of A,B, G being Functor of B,A holds
F*id A = F & id A*G = G
proof let F be Functor of A,B, G be Functor of B,A;
id A = id the Morphisms of A by CAT_1:def 21;
hence thesis by FUNCT_2:23;
end;
canceled 2;
theorem Th7:
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;
theorem Th8:
for F1,F2 being Functor of A,B, G1,G2 being Functor of B,C st
F1 is_transformable_to F2 &
G1 is_transformable_to G2
holds G1*F1 is_transformable_to G2*F2
proof let F1,F2 be Functor of A,B, G1,G2 be Functor of B,C such that
A1: F1 is_transformable_to F2 and
A2: G1 is_transformable_to G2;
let a be Object of A;
A3: G1.(F1.a) = (G1*F1).a & G2.(F2.a) = (G2*F2).a by CAT_1:113;
Hom(F1.a,F2.a) <> {} by A1,NATTRA_1:def 2;
then A4: Hom(G1.(F1.a),G1.(F2.a)) <> {} by CAT_1:126;
Hom(G1.(F2.a),G2.(F2.a)) <> {} by A2,NATTRA_1:def 2;
hence Hom((G1*F1).a,(G2*F2).a) <> {} by A3,A4,CAT_1:52;
end;
theorem Th9:
for F1,F2 being Functor of A,B st F1 is_transformable_to F2
for t being transformation of F1,F2 st t is invertible
for a being Object of A holds F1.a, F2.a are_isomorphic
proof let F1,F2 be Functor of A,B such that
A1: F1 is_transformable_to F2;
let t be transformation of F1,F2 such that
A2: t is invertible;
let a be Object of A;
thus Hom(F1.a,F2.a)<>{} by A1,NATTRA_1:def 2;
t.a is invertible by A2,NATTRA_1:def 10;
hence thesis;
end;
definition let C,D;
redefine mode Functor of C,D means
(for c being Object of C ex d being Object of D st it.id c = id d) &
(for f being Morphism of C holds
it.id dom f = id dom(it.f) & it.id cod f = id cod(it.f)) &
for f,g being Morphism of C st dom g = cod f
holds it.(g*f) = it.g*it.f;
compatibility by CAT_1:96,97,98,99;
end;
definition let A;
redefine func id A -> Functor of A,A;
coherence;
let B,C;
let F be Functor of A,B, G be Functor of B,C;
func G*F -> Functor of A,C;
coherence
proof
thus G*F is Functor of A,C;
end;
end;
reserve o,m for set;
theorem Th10:
F is_an_isomorphism implies
for g being Morphism of B ex f being Morphism of A st F.f = g
proof assume F is_an_isomorphism;
then A1: rng F = the Morphisms of B by CAT_1:def 22;
let g be Morphism of B;
consider f being set such that
A2: f in dom F & F.f = g by A1,FUNCT_1:def 5;
reconsider f as Morphism of A by A2,FUNCT_2:def 1;
take f;
thus F.f = g by A2;
end;
theorem Th11:
F is_an_isomorphism implies
for b being Object of B ex a being Object of A st F.a = b
proof assume F is_an_isomorphism;
then A1: rng Obj F = the Objects of B by CAT_1:def 22;
let b be Object of B;
consider a being set such that
A2: a in dom Obj F & (Obj F).a = b by A1,FUNCT_1:def 5;
reconsider a as Object of A by A2,FUNCT_2:def 1;
take a;
thus F.a = b by A2,CAT_1:def 20;
end;
theorem Th12:
F is one-to-one implies Obj F is one-to-one
proof assume
A1: F is one-to-one;
let x1,x2 be set;
assume x1 in dom Obj F & x2 in dom Obj F;
then reconsider a1 = x1, a2 = x2 as Object of A by FUNCT_2:def 1;
A2: dom F = the Morphisms of A by FUNCT_2:def 1;
assume
(Obj F).x1 = (Obj F).x2;
then F.a1 = (Obj F).a2 by CAT_1:def 20 .= F.a2 by CAT_1:def 20;
then F.(id a1 qua Morphism of A) = id(F.a2) by CAT_1:108
.= F.(id a2 qua Morphism of A)by CAT_1:108;
then id a1 = id a2 by A1,A2,FUNCT_1:def 8;
hence x1 = x2 by CAT_1:45;
end;
definition let A,B,F;
assume
A1: F is_an_isomorphism;
func F" -> Functor of B,A equals
:Def2: F";
coherence
proof
A2: F is one-to-one by A1,CAT_1:def 22;
then A3: Obj F is one-to-one by Th12;
A4: rng F = the Morphisms of B by A1,CAT_1:def 22;
A5: dom F = the Morphisms of A by FUNCT_2:def 1;
reconsider G = F" as Function of the Morphisms of B, the Morphisms of A
by A2,A4,FUNCT_2:31;
G is Functor of B,A
proof
thus for c being Object of B ex d being Object of A st G.(id c) = id d
proof let b be Object of B;
consider a being Object of A such that
A6: F.a = b by A1,Th11;
take a;
thus G.(id b) = G.(F.(id a qua Morphism of A)) by A6,CAT_1:108 .=id a
by A2,A5,FUNCT_1:56;
end;
thus for f being Morphism of B
holds G.(id dom f) = id dom(G.f) & G.(id cod f) = id cod(G.f)
proof let f be Morphism of B;
consider g being Morphism of A such that
A7: f = F.g by A1,Th10;
thus G.(id dom f) = G.(id(F.dom g)) by A7,CAT_1:109
.= G.(F.(id dom g qua Morphism of A)) by CAT_1:108
.= id dom g by A2,A5,FUNCT_1:56
.= id dom(G.f) by A2,A5,A7,FUNCT_1:56;
thus G.(id cod f) = G.(id(F.cod g)) by A7,CAT_1:109
.= G.(F.(id cod g qua Morphism of A)) by CAT_1:108
.= id cod g by A2,A5,FUNCT_1:56
.= id cod(G.f) by A2,A5,A7,FUNCT_1:56;
end;
let f,g be Morphism of B;
consider f' being Morphism of A such that
A8: f = F.f' by A1,Th10;
consider g' being Morphism of A such that
A9: g = F.g' by A1,Th10;
A10: dom Obj F = the Objects of A by FUNCT_2:def 1;
assume
A11: dom g = cod f;
(Obj F).dom g' = F.dom g' by CAT_1:def 20 .= cod f by A9,A11,CAT_1:109
.= F.cod f' by A8,CAT_1:109 .= (Obj F).cod f' by CAT_1:def 20;
then dom g' = cod f' by A3,A10,FUNCT_1:def 8;
hence G.(g*f) = G.(F.(g'*f')) by A8,A9,CAT_1:99
.= g'*f' by A2,A5,FUNCT_1:56
.= g'*(G.f) by A2,A5,A8,FUNCT_1:56
.= (G.g)*(G.f) by A2,A5,A9,FUNCT_1:56;
end;
hence thesis;
end;
end;
definition let A,B,F;
redefine attr F is isomorphic means
:Def3: F is one-to-one & rng F = the Morphisms of B;
compatibility
proof
thus F is_an_isomorphism implies
F is one-to-one & rng F = the Morphisms of B by CAT_1:def 22;
assume
A1: F is one-to-one & rng F = the Morphisms of B;
hence F is one-to-one & rng F = the Morphisms of B;
thus rng Obj F c= the Objects of B by RELSET_1:12;
let x be set;
assume x in the Objects of B;
then reconsider d = x as Object of B;
consider f being set such that
A2: f in dom F & id d = F.f by A1,FUNCT_1:def 5;
reconsider f as Morphism of A by A2,FUNCT_2:def 1;
A3: dom Obj F = the Objects of A by FUNCT_2:def 1;
reconsider c = id dom f as Morphism of A;
F.c = id dom(id d) by A2,CAT_1:98 .= id d by CAT_1:44;
then (Obj F).(dom f) = d by CAT_1:103;
hence x in rng Obj F by A3,FUNCT_1:def 5;
end;
synonym F is_an_isomorphism;
end;
theorem Th13:
F is_an_isomorphism implies F" is_an_isomorphism
proof assume
A1: F is_an_isomorphism;
then A2: F is one-to-one by CAT_1:def 22;
A3: F" = (F qua Function of the Morphisms of A, the Morphisms of B)" by A1,Def2
;
hence F" is one-to-one by A2,FUNCT_1:62;
thus rng(F") = dom F by A2,A3,FUNCT_1:55
.= the Morphisms of A by FUNCT_2:def 1;
end;
theorem
F is_an_isomorphism implies (Obj F)" = Obj F"
proof assume
A1: F is_an_isomorphism;
then A2: F is one-to-one by Def3;
A3: rng Obj F = the Objects of B by A1,CAT_1:def 22;
A4: Obj F is one-to-one by A2,Th12;
then reconsider G = (Obj F)" as Function of the Objects of B, the Objects of
A
by A3,FUNCT_2:31;
now let b be Object of B;
F.(id(G.b) qua Morphism of A)
= id((Obj F).(G.b)) by CAT_1:104
.= id b by A3,A4,FUNCT_1:57;
then id(G.b)
= (F qua Function of the Morphisms of A, the Morphisms of B)".id b
by A2,FUNCT_2:32
.= F".(id b qua Morphism of B) by A1,Def2;
hence G.b = (Obj F").b by CAT_1:103;
end;
hence (Obj F)" = Obj F" by FUNCT_2:113;
end;
theorem
F is_an_isomorphism implies F"" = F
proof assume
A1: F is_an_isomorphism;
then A2: F is one-to-one by CAT_1:def 22;
A3: F" is_an_isomorphism by A1,Th13;
reconsider f = F as Function of the Morphisms of A, the Morphisms of B;
reconsider g = F" as Function of the Morphisms of B, the Morphisms of A;
thus F"" = g" by A3,Def2 .= f"" by A1,Def2 .= F by A2,FUNCT_1:65;
end;
theorem Th16:
F is_an_isomorphism implies F*F" = id B & F"*F = id A
proof assume
A1: F is_an_isomorphism;
then A2: F is one-to-one by Def3;
reconsider f = F as Function of the Morphisms of A, the Morphisms of B;
A3: dom f = the Morphisms of A by FUNCT_2:def 1;
A4: rng f = the Morphisms of B by A1,Def3;
thus F*F" = f*f" by A1,Def2 .= id the Morphisms of B by A2,A4,FUNCT_1:61
.= id B by CAT_1:def 21;
thus F"*F = f"*f by A1,Def2 .= id the Morphisms of A by A2,A3,FUNCT_1:61
.= id A by CAT_1:def 21;
end;
theorem Th17:
F is_an_isomorphism & G is_an_isomorphism implies
G*F is_an_isomorphism
proof assume that
A1: F is one-to-one and
A2: rng F = the Morphisms of B and
A3: G is one-to-one and
A4: rng G = the Morphisms of C;
thus G*F is one-to-one by A1,A3,FUNCT_1:46;
dom G = the Morphisms of B by FUNCT_2:def 1;
hence rng(G*F) = the Morphisms of C by A2,A4,RELAT_1:47;
end;
:: Isomorphism of categories
definition let A,B;
pred A,B are_isomorphic means
ex F being Functor of A,B st F is_an_isomorphism;
reflexivity
proof let A;
id A is_an_isomorphism by CAT_1:122; hence thesis;
end;
symmetry
proof let A,B;
given F being Functor of A,B such that
A1: F is_an_isomorphism;
take F";
thus thesis by A1,Th13;
end;
synonym A ~= B;
end;
canceled 2;
theorem
A ~= B & B ~= C implies A ~= C
proof
given F1 being Functor of A,B such that
A1: F1 is_an_isomorphism;
given F2 being Functor of B,C such that
A2: F2 is_an_isomorphism;
take F2*F1;
thus thesis by A1,A2,Th17;
end;
theorem
[:1Cat(o,m),A:] ~= A
proof
take F = pr2(1Cat(o,m),A);
A1: the Morphisms of [:1Cat(o,m),A:] =
[:the Morphisms of 1Cat(o,m), the Morphisms of A:] by CAT_2:33;
set X = [:the Morphisms of 1Cat(o,m), the Morphisms of A:];
now let x1,x2 be set;
assume x1 in X; then consider x11,x12 being set such that
A2: x11 in the Morphisms of 1Cat(o,m) & x12 in the Morphisms of A and
A3: x1 = [x11,x12] by ZFMISC_1:def 2;
assume x2 in X; then consider x21,x22 being set such that
A4: x21 in the Morphisms of 1Cat(o,m) & x22 in the Morphisms of A and
A5: x2 = [x21,x22] by ZFMISC_1:def 2;
reconsider f11 = x11, f21 = x21 as Morphism of 1Cat(o,m) by A2,A4;
reconsider f12 = x12, f22 = x22 as Morphism of A by A2,A4;
assume
A6: F.x1 = F.x2;
A7: f12 = F.[f11,f12] by CAT_2:60 .= F.[f21,f22] by A3,A5,A6
.= f22 by CAT_2:60;
f11 = m by CAT_1:35 .= f21 by CAT_1:35;
hence x1 = x2 by A3,A5,A7;
end;
hence F is one-to-one by A1,FUNCT_2:25;
thus rng F = the Morphisms of A by Th2;
end;
theorem
[:A,B:] ~= [:B,A:]
proof
take F = <:pr2(A,B),pr1(A,B):>;
A1: rng pr2(A,B) = the Morphisms of B & rng pr1(A,B) = the Morphisms of A
by Th2;
A2: the Morphisms of [:B,A:] = [: the Morphisms of B, the Morphisms of A:] &
the Morphisms of [:A,B:] = [: the Morphisms of A, the Morphisms of B:]
by CAT_2:33;
A3: dom pr1(A,B) = the Morphisms of [:A,B:] &
dom pr2(A,B) = the Morphisms of [:A,B:] by FUNCT_2:def 1;
now let x1,x2 be set;
assume x1 in [:the Morphisms of A,the Morphisms of B:];
then consider x11,x12 being set such that
A4: x11 in the Morphisms of A & x12 in the Morphisms of B and
A5: x1 = [x11,x12] by ZFMISC_1:def 2;
assume x2 in [:the Morphisms of A,the Morphisms of B:];
then consider x21,x22 being set such that
A6: x21 in the Morphisms of A & x22 in the Morphisms of B and
A7: x2 = [x21,x22] by ZFMISC_1:def 2;
reconsider f11 = x11, f21 = x21 as Morphism of A by A4,A6;
reconsider f12 = x12, f22 = x22 as Morphism of B by A4,A6;
assume
A8: F.x1 = F.x2;
[f12,f11] = [f12,pr1(A,B).[f11,f12]] by CAT_2:58
.= [pr2(A,B).[f11,f12],pr1(A,B).[f11,f12]] by CAT_2:60
.= F.[f21,f22] by A3,A5,A7,A8,FUNCT_3:69
.= [pr2(A,B).[f21,f22],pr1(A,B).[f21,f22]]by A3,FUNCT_3:69
.= [f22,pr1(A,B).[f21,f22]]by CAT_2:60
.= [f22,f21] by CAT_2:58;
then x12 = x22 & x11 = x21 by ZFMISC_1:33;
hence x1 = x2 by A5,A7;
end;
hence F is one-to-one by A2,FUNCT_2:25;
thus rng F c= the Morphisms of [:B,A:] by A1,A2,FUNCT_3:71;
let x be set;
assume x in the Morphisms of [:B,A:];
then consider x1,x2 being set such that
A9: x1 in the Morphisms of B & x2 in the Morphisms of A and
A10: x = [x1,x2] by A2,ZFMISC_1:def 2;
reconsider x1 as Morphism of B by A9;
reconsider x2 as Morphism of A by A9;
F.[x2,x1] = [pr2(A,B).[x2,x1],pr1(A,B).[x2,x1]] by A3,FUNCT_3:69
.= [x1,pr1(A,B).[x2,x1]] by CAT_2:60 .= [x1,x2] by CAT_2:58;
hence x in rng F by A10,FUNCT_2:6;
end;
theorem
[:[:A,B:],C:] ~= [:A,[:B,C:]:]
proof
set X = pr1(A,B)*pr1([:A,B:],C);
set Y = <:pr2(A,B)*pr1([:A,B:],C),pr2([:A,B:],C):>;
A1:the Morphisms of [:A,[:B,C:]:] =
[:the Morphisms of A,the Morphisms of [:B,C:]:] by CAT_2:33;
A2:the Morphisms of [:B,C:] = [:the Morphisms of B, the Morphisms of C:]
by CAT_2:33;
A3:the Morphisms of [:A,B:] = [:the Morphisms of A, the Morphisms of B:]
by CAT_2:33;
A4:the Morphisms of [:[:A,B:],C:] =
[:the Morphisms of [:A,B:],the Morphisms of C:] by CAT_2:33;
take F = <:X, Y:>;
A5: dom X = the Morphisms of [:[:A,B:],C:] by FUNCT_2:def 1;
A6: dom Y = the Morphisms of [:[:A,B:],C:] by FUNCT_2:def 1;
A7: dom pr2([:A,B:],C) = the Morphisms of [:[:A,B:],C:] by FUNCT_2:def 1;
A8: dom(pr2(A,B)*pr1([:A,B:],C)) = the Morphisms of [:[:A,B:],C:]
by FUNCT_2:def 1;
now let x,y be set;
assume
x in [:[:the Morphisms of A,the Morphisms of B:],the Morphisms of C:];
then consider x1,x2 being set such that
A9: x1 in [:the Morphisms of A,the Morphisms of B:]
& x2 in the Morphisms of C and
A10: x = [x1,x2] by ZFMISC_1:def 2;
consider x11,x12 being set such that
A11: x11 in the Morphisms of A & x12 in the Morphisms of B and
A12: x1 = [x11,x12] by A9,ZFMISC_1:def 2;
assume
y in [:[:the Morphisms of A,the Morphisms of B:],the Morphisms of C:];
then consider y1,y2 being set such that
A13: y1 in [:the Morphisms of A,the Morphisms of B:]
& y2 in the Morphisms of C and
A14: y = [y1,y2] by ZFMISC_1:def 2;
consider y11,y12 being set such that
A15: y11 in the Morphisms of A & y12 in the Morphisms of B and
A16: y1 = [y11,y12] by A13,ZFMISC_1:def 2;
reconsider f11 = x11, g11 = y11 as Morphism of A by A11,A15;
reconsider f12 = x12, g12 = y12 as Morphism of B by A11,A15;
reconsider f2 = x2, g2 = y2 as Morphism of C by A9,A13;
assume
A17: F.x = F.y;
A18: [f11,[f12,f2]] = [pr1(A,B).[f11,f12],[f12,f2]] by CAT_2:58
.= [pr1(A,B).(pr1([:A,B:],C).[[f11,f12],f2]),[f12,f2]] by CAT_2:58
.= [X.[[f11,f12],f2],[f12,f2]] by FUNCT_2:21
.= [X.[[f11,f12],f2],[pr2(A,B).[f11,f12],f2]] by CAT_2:60
.= [X.[[f11,f12],f2],[pr2(A,B).(pr1([:A,B:],C).[[f11,f12],f2]),f2]]
by CAT_2:58
.= [X.[[f11,f12],f2],[(pr2(A,B)*pr1([:A,B:],C)).[[f11,f12],f2],f2]]
by FUNCT_2:21
.= [X.[[f11,f12],f2],[(pr2(A,B)*pr1([:A,B:],C)).[[f11,f12],f2],
pr2([:A,B:],C).[[f11,f12],f2]]] by CAT_2:60
.= [X.[[f11,f12],f2],Y.[[f11,f12],f2]] by A7,A8,FUNCT_3:69
.= F.[[g11,g12],g2] by A5,A6,A10,A12,A14,A16,A17,FUNCT_3:69
.= [X.[[g11,g12],g2],Y.[[g11,g12],g2]] by A5,A6,FUNCT_3:69
.= [X.[[g11,g12],g2],[(pr2(A,B)*pr1([:A,B:],C)).[[g11,g12],g2],
pr2([:A,B:],C).[[g11,g12],g2]]] by A7,A8,FUNCT_3:69
.= [X.[[g11,g12],g2],[(pr2(A,B)*pr1([:A,B:],C)).[[g11,g12],g2],g2]]
by CAT_2:60
.= [X.[[g11,g12],g2],[pr2(A,B).(pr1([:A,B:],C).[[g11,g12],g2]),g2]]
by FUNCT_2:21
.= [X.[[g11,g12],g2],[pr2(A,B).[g11,g12],g2]]by CAT_2:58
.= [X.[[g11,g12],g2],[g12,g2]]by CAT_2:60
.= [pr1(A,B).(pr1([:A,B:],C).[[g11,g12],g2]),[g12,g2]]by FUNCT_2:21
.= [pr1(A,B).[g11,g12],[g12,g2]]by CAT_2:58
.= [g11,[g12,g2]] by CAT_2:58;
then x11 = y11 & [x12,x2] = [y12,y2] by ZFMISC_1:33;
then x12 = y12 & x2 = y2 by ZFMISC_1:33;
hence x = y by A10,A12,A14,A16,A18,ZFMISC_1:33;
end;
hence F is one-to-one by A3,A4,FUNCT_2:25;
A19: rng F c= [:rng X, rng Y:] by FUNCT_3:71;
A20: rng X c= the Morphisms of A by RELSET_1:12;
A21: rng Y c= [:rng(pr2(A,B)*pr1([:A,B:],C)),rng pr2([:A,B:],C):]
by FUNCT_3:71;
A22: rng(pr2(A,B)*pr1([:A,B:],C)) c= the Morphisms of B by RELSET_1:12;
rng pr2([:A,B:],C) c= the Morphisms of C by RELSET_1:12;
then [:rng(pr2(A,B)*pr1([:A,B:],C)),rng pr2([:A,B:],C):]
c= the Morphisms of [:B,C:] by A2,A22,ZFMISC_1:119;
then rng Y c= the Morphisms of [:B,C:] by A21,XBOOLE_1:1;
then [:rng X, rng Y:] c= [:the Morphisms of A, the Morphisms of [:B,C:]:]
by A20,ZFMISC_1:119;
hence rng F c= the Morphisms of [:A,[:B,C:]:] by A1,A19,XBOOLE_1:1;
let x be set;
assume x in the Morphisms of [:A,[:B,C:]:];
then consider x1,x2 being set such that
A23: x1 in the Morphisms of A & x2 in the Morphisms of [:B,C:] and
A24: x = [x1,x2] by A1,ZFMISC_1:def 2;
consider x21,x22 being set such that
A25: x21 in the Morphisms of B & x22 in the Morphisms of C and
A26: x2 = [x21,x22] by A2,A23,ZFMISC_1:def 2;
reconsider x1 as Morphism of A by A23;
reconsider x21 as Morphism of B by A25;
reconsider x22 as Morphism of C by A25;
F.[[x1,x21],x22] = [X.[[x1,x21],x22],Y.[[x1,x21],x22]] by A5,A6,FUNCT_3:69
.= [pr1(A,B).(pr1([:A,B:],C).[[x1,x21],x22]),Y.[[x1,x21],x22]]
by FUNCT_2:21
.= [pr1(A,B).[x1,x21],Y.[[x1,x21],x22]] by CAT_2:58
.= [x1,Y.[[x1,x21],x22]] by CAT_2:58
.= [x1,[(pr2(A,B)*pr1([:A,B:],C)).[[x1,x21],x22],
pr2([:A,B:],C).[[x1,x21],x22]]] by A7,A8,FUNCT_3:69
.= [x1,[pr2(A,B).(pr1([:A,B:],C).[[x1,x21],x22]),
pr2([:A,B:],C).[[x1,x21],x22]]] by FUNCT_2:21
.= [x1,[pr2(A,B).[x1,x21],pr2([:A,B:],C).[[x1,x21],x22]]] by CAT_2:58
.= [x1,[x21,pr2([:A,B:],C).[[x1,x21],x22]]] by CAT_2:60
.= [x1,[x21,x22]] by CAT_2:60;
hence x in rng F by A24,A26,FUNCT_2:6;
end;
theorem
A ~= B & C ~= D implies [:A,C:] ~= [:B,D:]
proof
given F being Functor of A,B such that
A1: F is_an_isomorphism;
given G being Functor of C,D such that
A2: G is_an_isomorphism;
take [:F,G:];
F is one-to-one & G is one-to-one by A1,A2,Def3;
hence [:F,G:] is one-to-one by Th1;
thus rng [:F,G:] = [:rng F, rng G:] by FUNCT_3:88
.= [: the Morphisms of B, rng G:] by A1,Def3
.= [: the Morphisms of B, the Morphisms of D:] by A2,Def3
.= the Morphisms of [:B,D:] by CAT_2:33;
end;
definition let A,B,C; let F1,F2 be Functor of A,B such that
A1: F1 is_transformable_to F2;
let t be transformation of F1,F2;
let G be Functor of B,C;
func G*t -> transformation of G*F1,G*F2 equals
:Def5: G*t;
coherence
proof
reconsider Gt = G*t as Function of the Objects of A, the Morphisms of C;
Gt is transformation of G*F1, G*F2
proof
thus G*F1 is_transformable_to G*F2 by A1,Th8;
let a be Object of A;
A2: G.(F1.a) = (G*F1).a & G.(F2.a) = (G*F2).a by CAT_1:113;
A3: Gt.a = G.((t qua Function of the Objects of A, the Morphisms of B).a)
by FUNCT_2:21
.= G.(t.a qua Morphism of B) by A1,NATTRA_1:def 5;
t.a in Hom(F1.a,F2.a) by A1,Th7;
then G.(t.a qua Morphism of B) in
Hom((G*F1).a,(G*F2).a) by A2,CAT_1:123;
hence Gt.a is Morphism of (G*F1).a,(G*F2).a by A3,CAT_1:def 7;
end;
hence thesis;
end;
correctness;
end;
definition let A,B,C; let G1,G2 be Functor of B,C such that
A1: G1 is_transformable_to G2;
let F be Functor of A,B;
let t be transformation of G1,G2;
func t*F -> transformation of G1*F,G2*F equals
:Def6: t*Obj F;
coherence
proof
reconsider tF = t*Obj F as
Function of the Objects of A, the Morphisms of C;
tF is transformation of G1*F, G2*F
proof
thus G1*F is_transformable_to G2*F by A1,Th8;
let a be Object of A;
A2: tF.a = t.((Obj F).a qua set) by FUNCT_2:21
.= t.((Obj F).a) by A1,NATTRA_1:def 5
.= t.(F.a) by CAT_1:def 20;
G1.(F.a) = (G1*F).a & G2.(F.a) = (G2*F).a by CAT_1:113;
hence tF.a is Morphism of (G1*F).a,(G2*F).a by A2;
end;
hence thesis;
end;
correctness;
end;
theorem Th25:
for G1,G2 be Functor of B,C st G1 is_transformable_to G2
for F be Functor of A,B, t be transformation of G1,G2, a be Object of A
holds (t*F).a = t.(F.a)
proof let G1,G2 be Functor of B,C such that
A1: G1 is_transformable_to G2;
let F be Functor of A,B, t be transformation of G1,G2, a be Object of A;
G1*F is_transformable_to G2*F by A1,Th8;
hence (t*F).a
= (t*F).(a qua set) by NATTRA_1:def 5
.= ((t qua Function of the Objects of B, the Morphisms of C)*Obj F).a
by A1,Def6
.= t.((Obj F).a qua set) by FUNCT_2:21
.= t.((Obj F).a) by A1,NATTRA_1:def 5
.= t.(F.a) by CAT_1:def 20;
end;
theorem Th26:
for F1,F2 be Functor of A,B st F1 is_transformable_to F2
for t be transformation of F1,F2, G be Functor of B,C, a being Object of A
holds (G*t).a = G.(t.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, G be Functor of B,C, a be Object of A;
A2: G*F1 is_transformable_to G*F2 by A1,Th8;
A3: Hom(F1.a,F2.a) <> {} by A1,NATTRA_1:def 2;
thus (G*t).a
= (G*t).(a qua set) by A2,NATTRA_1:def 5
.= ((G qua Function of the Morphisms of B, the Morphisms of C)*
(t qua Function of the Objects of A, the Morphisms of B)).a
by A1,Def5
.= G.(t.(a qua set)) by FUNCT_2:21
.= G.(t.a qua Morphism of B) by A1,NATTRA_1:def 5
.= G.(t.a) by A3,NATTRA_1:def 1;
end;
theorem Th27:
for F1,F2 being Functor of A,B, G1,G2 being Functor of B,C st
F1 is_naturally_transformable_to F2 &
G1 is_naturally_transformable_to G2
holds G1*F1 is_naturally_transformable_to G2*F2
proof let F1,F2 be Functor of A,B, G1,G2 be Functor of B,C such that
A1: F1 is_naturally_transformable_to F2 and
A2: G1 is_naturally_transformable_to G2;
A3: F1 is_transformable_to F2 & G1 is_transformable_to G2
by A1,A2,NATTRA_1:def 7;
hence
A4: G1*F1 is_transformable_to G2*F2 by Th8;
consider t1 being natural_transformation of F1,F2,
t2 being natural_transformation of G1,G2;
take t = (t2*F2)`*`(G1*t1);
A5: G1*F1 is_transformable_to G1*F2 by A3,Th8;
A6: G1*F2 is_transformable_to G2*F2 by A3,Th8;
let a,b be Object of A; assume
A7: Hom(a,b) <> {};
then A8: Hom(F2.a,F2.b) <> {} by CAT_1:126;
A9: Hom(G1.(F2.b),G2.(F2.b)) <> {} by A3,NATTRA_1:def 2;
A10: Hom(F1.b,F2.b) <> {} by A3,NATTRA_1:def 2;
then A11: Hom(G1.(F1.b),G1.(F2.b)) <> {} by CAT_1:126;
A12: Hom(F1.a,F1.b) <> {} by A7,CAT_1:126;
then A13: Hom(G1.(F1.a),G1.(F1.b)) <> {} by CAT_1:126;
A14: Hom(G1.(F2.a),G1.(F2.b)) <> {} by A8,CAT_1:126;
A15: Hom(F1.a,F2.a) <> {} by A3,NATTRA_1:def 2;
then A16: Hom(G1.(F1.a),G1.(F2.a)) <> {} by CAT_1:126;
A17: Hom(G2.(F2.a),G2.(F2.b)) <> {} by A8,CAT_1:126;
A18: Hom(G1.(F2.a),G2.(F2.a)) <> {} by A3,NATTRA_1:def 2;
A19: Hom((G1*F1).b,(G2*F2).b) <> {} by A4,NATTRA_1:def 2;
A20: Hom((G1*F1).a,(G2*F2).a) <> {} by A4,NATTRA_1:def 2;
A21: Hom((G1*F1).a,(G1*F1).b) <> {} by A7,CAT_1:126;
A22: Hom((G2*F2).a,(G2*F2).b) <> {} by A7,CAT_1:126;
A23: Hom(G1.(F1.a),G2.(F2.a)) <> {} by A16,A18,CAT_1:52;
A24: Hom(G1.(F1.b),G2.(F2.b)) <> {} by A9,A11,CAT_1:52;
A25: Hom((G1*F2).b,(G2*F2).b) <> {} by A6,NATTRA_1:def 2;
A26: Hom((G1*F1).b,(G1*F2).b) <> {} by A5,NATTRA_1:def 2;
A27: Hom((G1*F2).a,(G2*F2).a) <> {} by A6,NATTRA_1:def 2;
A28: Hom((G1*F1).a,(G1*F2).a) <> {} by A5,NATTRA_1:def 2;
let f be Morphism of a,b;
thus t.b*(G1*F1).f
= t.b*((G1*F1).f qua Morphism of C) by A19,A21,CAT_1:def 13
.= t.b*(G1.(F1.f) qua Morphism of C) by A7,NATTRA_1:11
.= (t2*F2).b*(G1*t1).b*G1.(F1.f) by A5,A6,NATTRA_1:def 6
.= ((t2*F2).b qua Morphism of C)*(G1*t1).b*G1.(F1.f) by A25,A26,CAT_1:def
13
.= (t2*F2).b*G1.(t1.b)*G1.(F1.f) by A3,Th26
.= (t2.(F2.b) qua Morphism of C)*G1.(t1.b)*G1.(F1.f) by A3,Th25
.= (t2.(F2.b)*G1.(t1.b) qua Morphism of C)*G1.(F1.f) by A9,A11,CAT_1:def
13
.= t2.(F2.b)*G1.(t1.b)*G1.(F1.f) by A13,A24,CAT_1:def 13
.= t2.(F2.b)*(G1.(t1.b)*G1.(F1.f)) by A9,A11,A13,CAT_1:54
.= t2.(F2.b)*(G1.(t1.b*F1.f)) by A10,A12,NATTRA_1:13
.= t2.(F2.b)*(G1.(F2.f*t1.a)) by A1,A7,NATTRA_1:def 8
.= t2.(F2.b)*(G1.(F2.f)*G1.(t1.a)) by A8,A15,NATTRA_1:13
.= t2.(F2.b)*G1.(F2.f)*G1.(t1.a) by A9,A14,A16,CAT_1:54
.= G2.(F2.f)*t2.(F2.a)*G1.(t1.a) by A2,A8,NATTRA_1:def 8
.= G2.(F2.f)*(t2.(F2.a)*G1.(t1.a)) by A16,A17,A18,CAT_1:54
.= G2.(F2.f)*(t2.(F2.a)*G1.(t1.a) qua Morphism of C) by A17,A23,CAT_1:def
13
.= G2.(F2.f)*((t2.(F2.a) qua Morphism of C)*G1.(t1.a))
by A16,A18,CAT_1:def 13
.= G2.(F2.f)*((t2*F2).a*G1.(t1.a)) by A3,Th25
.= G2.(F2.f)*(((t2*F2).a qua Morphism of C)*(G1*t1).a) by A3,Th26
.= G2.(F2.f)*((t2*F2).a*(G1*t1).a) by A27,A28,CAT_1:def 13
.= G2.(F2.f)*t.a by A5,A6,NATTRA_1:def 6
.= ((G2*F2).f qua Morphism of C)*t.a by A7,NATTRA_1:11
.= (G2*F2).f*t.a by A20,A22,CAT_1:def 13;
end;
definition let A,B,C; let F1,F2 be Functor of A,B such that
A1: F1 is_naturally_transformable_to F2;
let t be natural_transformation of F1,F2;
let G be Functor of B,C;
func G*t -> natural_transformation of G*F1,G*F2 equals
:Def7: G*t;
coherence
proof
A2: F1 is_transformable_to F2 by A1,NATTRA_1:def 7;
G*t is natural_transformation of G*F1, G*F2
proof
thus G*F1 is_naturally_transformable_to G*F2 by A1,Th27;
then A3: G*F1 is_transformable_to G*F2 by NATTRA_1:def 7;
let a,b be Object of A such that
A4: Hom(a,b) <> {};
let f be Morphism of a,b;
A5: Hom(F1.b,F2.b) <> {} by A2,NATTRA_1:def 2;
A6: Hom(F1.a,F1.b) <> {} by A4,CAT_1:126;
A7: Hom(F1.a,F2.a) <> {} by A2,NATTRA_1:def 2;
A8: Hom(F2.a,F2.b) <> {} by A4,CAT_1:126;
A9: Hom((G*F1).b,(G*F2).b) <> {} by A3,NATTRA_1:def 2;
A10: Hom((G*F1).a,(G*F1).b) <> {} by A4,CAT_1:126;
A11: Hom(G.(F1.b),G.(F2.b)) <> {} by A5,CAT_1:126;
A12: Hom(G.(F1.a),G.(F1.b)) <> {} by A6,CAT_1:126;
A13: Hom(G.(F2.a),G.(F2.b)) <> {} by A8,CAT_1:126;
A14: Hom(G.(F1.a),G.(F2.a)) <> {} by A7,CAT_1:126;
A15: Hom((G*F1).a,(G*F2).a) <> {} by A3,NATTRA_1:def 2;
A16: Hom((G*F2).a,(G*F2).b) <> {} by A4,CAT_1:126;
thus (G*t).b*(G*F1).f
= (G*t).b*((G*F1).f qua Morphism of C) by A9,A10,CAT_1:def 13
.= (G*t).b*G.(F1.f) by A4,NATTRA_1:11
.= (G.(t.b) qua Morphism of C)*G.(F1.f) by A2,Th26
.= G.(t.b)*G.(F1.f) by A11,A12,CAT_1:def 13
.= G.(t.b*F1.f) by A5,A6,NATTRA_1:13
.= G.(F2.f*t.a) by A1,A4,NATTRA_1:def 8
.= G.(F2.f)*G.(t.a)by A7,A8,NATTRA_1:13
.= G.(F2.f)*(G.(t.a) qua Morphism of C)by A13,A14,CAT_1:def 13
.= G.(F2.f)*(G*t).a by A2,Th26
.= ((G*F2).f qua Morphism of C)*(G*t).a by A4,NATTRA_1:11
.= (G*F2).f*(G*t).a by A15,A16,CAT_1:def 13;
end;
hence thesis;
end;
correctness;
end;
theorem Th28:
for F1,F2 be Functor of A,B st F1 is_naturally_transformable_to F2
for t be natural_transformation of F1,F2, G be Functor of B,C,
a being Object of A
holds (G*t).a = G.(t.a)
proof let F1,F2 be Functor of A,B; 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, G be Functor of B,C,
a be Object of A;
thus (G*t).a = (G*(t qua transformation of F1,F2)).a by A1,Def7
.= G.(t.a) by A2,Th26;
end;
definition let A,B,C; let G1,G2 be Functor of B,C such that
A1: G1 is_naturally_transformable_to G2;
let F be Functor of A,B;
let t be natural_transformation of G1,G2;
func t*F -> natural_transformation of G1*F,G2*F equals
:Def8: t*F;
coherence
proof
A2: G1 is_transformable_to G2 by A1,NATTRA_1:def 7;
t*F is natural_transformation of G1*F, G2*F
proof
thus G1*F is_naturally_transformable_to G2*F by A1,Th27;
then A3: G1*F is_transformable_to G2*F by NATTRA_1:def 7;
let a,b be Object of A; assume
A4: Hom(a,b) <> {};
then A5: Hom(F.a,F.b) <> {} by CAT_1:126;
A6: Hom((G1*F).a,(G1*F).b) <> {} by A4,CAT_1:126;
A7: Hom((G1*F).b,(G2*F).b) <> {} by A3,NATTRA_1:def 2;
A8: Hom(G1.(F.b),G2.(F.b)) <> {} by A2,NATTRA_1:def 2;
A9: Hom(G1.(F.a),G1.(F.b)) <> {} by A5,CAT_1:126;
A10: Hom(G2.(F.a),G2.(F.b)) <> {} by A5,CAT_1:126;
A11: Hom(G1.(F.a),G2.(F.a)) <> {} by A2,NATTRA_1:def 2;
A12: Hom((G2*F).a,(G2*F).b) <> {} by A4,CAT_1:126;
A13: Hom((G1*F).a,(G2*F).a) <> {} by A3,NATTRA_1:def 2;
let f be Morphism of a,b;
thus (t*F).b*(G1*F).f
= (t*F).b*((G1*F).f qua Morphism of C) by A6,A7,CAT_1:def 13
.= (t*F).b*G1.(F.f) by A4,NATTRA_1:11
.= (t.(F.b) qua Morphism of C)*G1.(F.f) by A2,Th25
.= t.(F.b)*G1.(F.f) by A8,A9,CAT_1:def 13
.= G2.(F.f)*t.(F.a) by A1,A5,NATTRA_1:def 8
.= G2.(F.f)*(t.(F.a) qua Morphism of C) by A10,A11,CAT_1:def 13
.= G2.(F.f)*(t*F).a by A2,Th25
.= ((G2*F).f qua Morphism of C)*(t*F).a by A4,NATTRA_1:11
.= (G2*F).f*(t*F).a by A12,A13,CAT_1:def 13;
end;
hence thesis;
end;
correctness;
end;
theorem Th29:
for G1,G2 be Functor of B,C st G1 is_naturally_transformable_to G2
for F be Functor of A,B, t be natural_transformation of G1,G2,
a be Object of A
holds (t*F).a = t.(F.a)
proof let G1,G2 be Functor of B,C;
assume
A1: G1 is_naturally_transformable_to G2;
then A2: G1 is_transformable_to G2 by NATTRA_1:def 7;
let F be Functor of A,B, t be natural_transformation of G1,G2,
a be Object of A;
thus (t*F).a = ((t qua transformation of G1,G2)*F).a by A1,Def8
.= t.(F.a) by A2,Th25;
end;
reserve F,F1,F2,F3 for Functor of A,B,
G,G1,G2,G3 for Functor of B,C,
H,H1,H2 for Functor of C,D,
s for natural_transformation of F1,F2,
s' for natural_transformation of F2,F3,
t for natural_transformation of G1,G2,
t' for natural_transformation of G2,G3,
u for natural_transformation of H1,H2;
theorem Th30:
F1 is_naturally_transformable_to F2 implies
for a being Object of A holds Hom(F1.a,F2.a) <> {}
proof assume F1 is_naturally_transformable_to F2;
then A1: F1 is_transformable_to F2 by NATTRA_1:def 7;
let a be Object of A;
thus Hom(F1.a,F2.a) <> {} by A1,NATTRA_1:def 2;
end;
theorem Th31:
F1 is_naturally_transformable_to F2 implies
for t1,t2 being natural_transformation of F1,F2 st
for a being Object of A holds t1.a = t2.a
holds t1 = t2
proof assume F1 is_naturally_transformable_to F2;
then F1 is_transformable_to F2 by NATTRA_1:def 7;
hence thesis by NATTRA_1:20;
end;
theorem Th32:
F1 is_naturally_transformable_to F2 &
F2 is_naturally_transformable_to F3
implies G*(s'`*`s) = (G*s')`*`(G*s)
proof assume
A1: F1 is_naturally_transformable_to F2 &
F2 is_naturally_transformable_to F3;
then A2: F1 is_naturally_transformable_to F3 by NATTRA_1:25;
A3: G*F1 is_naturally_transformable_to G*F2 &
G*F2 is_naturally_transformable_to G*F3 by A1,Th27;
then A4: G*F1 is_naturally_transformable_to G*F3 by NATTRA_1:25;
now let a be Object of A;
A5: G.(s'.a) = (G*s').a & G.(s.a) = (G*s).a by A1,Th28;
A6: G.(F1.a) = (G*F1).a & G.(F2.a) = (G*F2).a & G.(F3.a) = (G*F3).a
by CAT_1:113;
A7: Hom(F1.a,F2.a) <> {} & Hom(F2.a,F3.a) <> {} by A1,Th30;
thus (G*(s'`*`s)).a = G.((s'`*`s).a) by A2,Th28
.= G.((s'.a)*(s.a)) by A1,NATTRA_1:27
.= G.(s'.a)*G.(s.a) by A7,NATTRA_1:13
.= ((G*s')`*`(G*s)).a by A3,A5,A6,NATTRA_1:27;
end;
hence thesis by A4,Th31;
end;
theorem Th33:
G1 is_naturally_transformable_to G2 &
G2 is_naturally_transformable_to G3
implies (t'`*`t)*F = (t'*F)`*`(t*F)
proof assume
A1: G1 is_naturally_transformable_to G2 &
G2 is_naturally_transformable_to G3;
then A2: G1 is_naturally_transformable_to G3 by NATTRA_1:25;
A3: G1*F is_naturally_transformable_to G2*F &
G2*F is_naturally_transformable_to G3*F by A1,Th27;
then A4: G1*F is_naturally_transformable_to G3*F by NATTRA_1:25;
now let a be Object of A;
A5: t'.(F.a) = (t'*F).a & t.(F.a) = (t*F).a by A1,Th29;
A6: G1.(F.a) = (G1*F).a & G2.(F.a) = (G2*F).a & G3.(F.a) = (G3*F).a
by CAT_1:113;
thus ((t'`*`t)*F).a = (t'`*`t).(F.a) by A2,Th29
.= (t'.(F.a))*(t.(F.a)) by A1,NATTRA_1:27
.= ((t'*F)`*`(t*F)).a by A3,A5,A6,NATTRA_1:27;
end;
hence thesis by A4,Th31;
end;
theorem Th34:
H1 is_naturally_transformable_to H2 implies u*G*F = u*(G*F)
proof assume
A1: H1 is_naturally_transformable_to H2;
then A2: H1*G is_naturally_transformable_to H2*G by Th27;
then A3: H1*G*F is_naturally_transformable_to H2*G*F by Th27;
A4: H1*(G*F) = H1*G*F & H2*(G*F) = H2*G*F by RELAT_1:55;
then reconsider v = u*(G*F) as natural_transformation of H1*G*F, H2*G*F;
now let a be Object of A;
thus (u*G*F).a = (u*G).(F.a) by A2,Th29
.= u.(G.(F.a)) by A1,Th29
.= u.((G*F).a) by CAT_1:113
.= v.a by A1,A4,Th29;
end;
hence thesis by A3,Th31;
end;
theorem Th35:
G1 is_naturally_transformable_to G2 implies H*t*F = H*(t*F)
proof assume
A1: G1 is_naturally_transformable_to G2;
then A2: H*G1 is_naturally_transformable_to H*G2 by Th27;
then A3: G1*F is_naturally_transformable_to G2*F &
H*G1*F is_naturally_transformable_to H*G2*F by A1,Th27;
A4: H*(G1*F) = H*G1*F & H*(G2*F) = H*G2*F by RELAT_1:55;
then reconsider v = H*(t*F) as natural_transformation of H*G1*F, H*G2*F;
now let a be Object of A;
A5: G1.(F.a) = (G1*F).a & G2.(F.a) = (G2*F).a by CAT_1:113;
thus (H*t*F).a = (H*t).(F.a) by A2,Th29
.= H.(t.(F.a)) by A1,Th28
.= H.((t*F).a) by A1,A5,Th29
.= v.a by A3,A4,Th28;
end;
hence thesis by A3,Th31;
end;
theorem Th36:
F1 is_naturally_transformable_to F2 implies H*G*s = H*(G*s)
proof assume
A1: F1 is_naturally_transformable_to F2;
then A2: G*F1 is_naturally_transformable_to G*F2 &
H*G*F1 is_naturally_transformable_to H*G*F2 by Th27;
A3: H*(G*F1) = H*G*F1 & H*(G*F2) = H*G*F2 by RELAT_1:55;
then reconsider v = H*(G*s) as natural_transformation of H*G*F1, H*G*F2;
now let a be Object of A;
A4: Hom(F1.a,F2.a) <> {} by A1,Th30;
A5: G.(F1.a) = (G*F1).a & G.(F2.a) = (G*F2).a by CAT_1:113;
thus (H*G*s).a = (H*G).(s.a) by A1,Th28
.= H.(G.(s.a)) by A4,NATTRA_1:11
.= H.((G*s).a) by A1,A5,Th28
.= v.a by A2,A3,Th28;
end;
hence thesis by A2,Th31;
end;
theorem Th37:
(id G)*F = id(G*F)
proof
now let a be Object of A;
thus ((id G)*F).a = id G.(F.a) by Th29
.= id(G.(F.a)) by NATTRA_1:21
.= id((G*F).a) by CAT_1:113
.= id(G*F).a by NATTRA_1:21;
end;
hence thesis by Th31;
end;
theorem Th38:
G*id F = id(G*F)
proof
now let a be Object of A;
thus (G*id F).a = G.(id F.a) by Th28
.= G.id(F.a) by NATTRA_1:21
.= id(G.(F.a)) by NATTRA_1:15
.= id((G*F).a) by CAT_1:113
.= (id(G*F)).a by NATTRA_1:21;
end;
hence thesis by Th31;
end;
theorem Th39:
G1 is_naturally_transformable_to G2 implies t*id B = t
proof assume
A1: G1 is_naturally_transformable_to G2;
A2: G1*id B = G1 & G2*id B = G2 by Th4;
then reconsider s = t*id B as natural_transformation of G1,G2;
now let b be Object of B;
thus s.b = t.((id B).b) by A1,A2,Th29 .= t.b by CAT_1:118;
end;
hence thesis by A1,Th31;
end;
theorem Th40:
F1 is_naturally_transformable_to F2 implies (id B)*s = s
proof assume
A1: F1 is_naturally_transformable_to F2;
A2: (id B)*F1 = F1 & (id B)*F2 = F2 by Th4;
then reconsider t = (id B)*s as natural_transformation of F1,F2;
now let a be Object of A;
A3: Hom(F1.a,F2.a) <> {} by A1,Th30;
thus t.a = (id B).(s.a) by A1,A2,Th28
.= (id B).(s.a qua Morphism of B) by A3,NATTRA_1:def 1
.= s.a by CAT_1:115;
end;
hence thesis by A1,Th31;
end;
definition let A,B,C,F1,F2,G1,G2;
let s,t;
func t(#)s -> natural_transformation of G1*F1,G2*F2 equals
:Def9: (t*F2)`*`(G1*s);
correctness;
end;
theorem Th41:
F1 is_naturally_transformable_to F2 &
G1 is_naturally_transformable_to G2 implies
t(#)s = (G2*s)`*`(t*F1)
proof assume that
A1: F1 is_naturally_transformable_to F2 and
A2: G1 is_naturally_transformable_to G2;
A3: G2*F1 is_naturally_transformable_to G2*F2 by A1,Th27;
A4: G1*F1 is_naturally_transformable_to G2*F1 by A2,Th27;
A5: G1*F1 is_naturally_transformable_to G1*F2 by A1,Th27;
A6: G1*F2 is_naturally_transformable_to G2*F2 by A2,Th27;
then A7: G1*F1 is_naturally_transformable_to G2*F2 by A5,NATTRA_1:25;
now let a be Object of A;
A8: Hom(F1.a,F2.a) <> {} by A1,Th30;
A9: (t*F2).a = t.(F2.a) & (G1*s).a = G1.(s.a)
& (G1*F1).a = G1.(F1.a) & (G1*F2).a = G1.(F2.a) & (G2*F2).a = G2.(F2.a)
by A1,A2,Th28,Th29,CAT_1:113;
A10: (t*F1).a = t.(F1.a) & (G2*s).a = G2.(s.a)
& (G1*F1).a = G1.(F1.a) & (G2*F1).a = G2.(F1.a) & (G2*F2).a = G2.(F2.a)
by A1,A2,Th28,Th29,CAT_1:113;
thus ((t*F2)`*`(G1*s)).a
= t.(F2.a)*G1.(s.a) by A5,A6,A9,NATTRA_1:27
.= (G2*s).a*(t*F1).a by A2,A8,A10,NATTRA_1:def 8
.= ((G2*s)`*`(t*F1)).a by A3,A4,NATTRA_1:27;
end;
then (t*F2)`*`(G1*s) = (G2*s)`*`(t*F1) by A7,Th31;
hence thesis by Def9;
end;
theorem
F1 is_naturally_transformable_to F2 implies (id id B)(#)s = s
proof assume
A1:F1 is_naturally_transformable_to F2;
then A2:(id B)*F1 is_naturally_transformable_to (id B)*F2 by Th27;
thus (id id B)(#)s
= ((id id B)*F2)`*`((id B)*s) by Def9
.= (id((id B)*F2))`*`((id B)*s) by Th37
.= (id B)*s by A2,NATTRA_1:26
.= s by A1,Th40;
end;
theorem
G1 is_naturally_transformable_to G2 implies t(#)(id id B) = t
proof assume
A1: G1 is_naturally_transformable_to G2;
then A2: G1*id B is_naturally_transformable_to G2*id B by Th27;
thus t(#)(id id B)
= (t*id B)`*`(G1*id id B) by Def9
.= (t*id B)`*`id(G1*id B) by Th38
.= t*id B by A2,NATTRA_1:26
.= t by A1,Th39;
end;
theorem
F1 is_naturally_transformable_to F2 &
G1 is_naturally_transformable_to G2 &
H1 is_naturally_transformable_to H2 implies
u(#)(t(#)s) = (u(#)t)(#)s
proof assume that
A1: F1 is_naturally_transformable_to F2 and
A2: G1 is_naturally_transformable_to G2 and
A3: H1 is_naturally_transformable_to H2;
A4: H1*G1*F1 = H1*(G1*F1) & H1*G1*F2 = H1*(G1*F2) &
H1*G2*F2 = H1*(G2*F2) & H2*G2*F2 = H2*(G2*F2) by RELAT_1:55;
A5: u*(G2*F2) = u*G2*F2 & H1*(t*F2) = H1*t*F2 & H1*(G1*s) = H1*G1*s
by A1,A2,A3,Th34,Th35,Th36;
A6: H1*G1*F1 is_naturally_transformable_to H1*G1*F2 by A1,Th27;
A7: H1*G1 is_naturally_transformable_to H1*G2 by A2,Th27;
then A8: G1*F2 is_naturally_transformable_to G2*F2 &
H1*G1*F2 is_naturally_transformable_to H1*G2*F2 by A2,Th27;
A9: H1*G2 is_naturally_transformable_to H2*G2 by A3,Th27;
then A10: H1*G2*F2 is_naturally_transformable_to H2*G2*F2 by Th27;
A11: G1*F1 is_naturally_transformable_to G1*F2 by A1,Th27;
thus u(#)(t(#)s)
= u(#)((t*F2)`*`(G1*s)) by Def9
.= (u*(G2*F2))`*`(H1*((t*F2)`*`(G1*s))) by Def9
.= (u*(G2*F2))`*`((H1*(t*F2))`*`(H1*(G1*s))) by A8,A11,Th32
.= (u*G2*F2)`*`(H1*t*F2)`*`((H1*G1)*s) by A4,A5,A6,A8,A10,NATTRA_1:28
.= (((u*G2)`*`(H1*t))*F2)`*`((H1*G1)*s) by A7,A9,Th33
.= ((u*G2)`*`(H1*t))(#)s by Def9
.= u(#)t(#)s by Def9;
end;
theorem
G1 is_naturally_transformable_to G2 implies t*F = t(#)id F
proof assume
G1 is_naturally_transformable_to G2;
then G1*F is_naturally_transformable_to G2*F by Th27;
hence t*F = (t*F)`*`id(G1*F) by NATTRA_1:26
.= (t*F)`*`(G1*id F) by Th38
.= t(#)id F by Def9;
end;
theorem
F1 is_naturally_transformable_to F2 implies G*s = (id G)(#)s
proof assume
F1 is_naturally_transformable_to F2;
then G*F1 is_naturally_transformable_to G*F2 by Th27;
hence G*s = id(G*F2)`*`(G*s) by NATTRA_1:26
.= ((id G)*F2)`*`(G*s) by Th37
.= (id G)(#)s by Def9;
end;
theorem
F1 is_naturally_transformable_to F2 &
F2 is_naturally_transformable_to F3 &
G1 is_naturally_transformable_to G2 &
G2 is_naturally_transformable_to G3 implies
(t'`*`t)(#)(s'`*`s) = (t'(#)s')`*`(t(#)s)
proof assume that
A1: F1 is_naturally_transformable_to F2 and
A2: F2 is_naturally_transformable_to F3 and
A3: G1 is_naturally_transformable_to G2 and
A4: G2 is_naturally_transformable_to G3;
A5: G3*F2 is_naturally_transformable_to G3*F3 &
G3*F1 is_naturally_transformable_to G3*F2 by A1,A2,Th27;
A6: G1 is_naturally_transformable_to G3 by A3,A4,NATTRA_1:25;
A7: F1 is_naturally_transformable_to F3 by A1,A2,NATTRA_1:25;
A8: G1*F1 is_naturally_transformable_to G3*F1 &
G1*F1 is_naturally_transformable_to G2*F1 &
G2*F1 is_naturally_transformable_to G3*F1 by A3,A4,A6,Th27;
A9: G2*F2 is_naturally_transformable_to G3*F2 by A4,Th27;
A10: G2*F1 is_naturally_transformable_to G2*F2 by A1,Th27;
then A11: G1*F1 is_naturally_transformable_to G2*F2 by A8,NATTRA_1:25;
A12: t'(#)s' = (G3*s')`*`(t'*F2) & t(#)s = (G2*s)`*`(t*F1) by A1,A2,A3,A4,Th41;
thus (t'`*`t)(#)(s'`*`s)
= (G3*(s'`*`s))`*`((t'`*`t)*F1) by A6,A7,Th41
.= (G3*s')`*`(G3*s)`*`((t'`*`t)*F1) by A1,A2,Th32
.= (G3*s')`*`(G3*s)`*`((t'*F1)`*`(t*F1)) by A3,A4,Th33
.= (G3*s')`*`((G3*s)`*`((t'*F1)`*`(t*F1))) by A5,A8,NATTRA_1:28
.= (G3*s')`*`((G3*s)`*`(t'*F1)`*`(t*F1)) by A5,A8,NATTRA_1:28
.= (G3*s')`*`((t'(#)s)`*`(t*F1)) by A1,A4,Th41
.= (G3*s')`*`((t'*F2)`*`(G2*s)`*`(t*F1)) by Def9
.= (G3*s')`*`((t'*F2)`*`((G2*s)`*`(t*F1))) by A8,A9,A10,NATTRA_1:28
.= (t'(#)s')`*`(t(#)s) by A5,A9,A11,A12,NATTRA_1:28;
end;
theorem Th48:
for F being Functor of A,B, G being Functor of C,D
for I,J being Functor of B,C st I ~= J holds G*I ~= G*J & I*F ~= J*F
proof let F be Functor of A,B, G be Functor of C,D;
let I,J be Functor of B,C;
assume
A1:I is_naturally_transformable_to J;
given t being natural_transformation of I,J such that
A2: t is invertible;
thus G*I ~= G*J
proof
thus G*I is_naturally_transformable_to G*J by A1,Th27;
take G*t;
let b be Object of B;
I is_transformable_to J by A1,NATTRA_1:def 7;
then A3: Hom(I.b,J.b) <> {} by NATTRA_1:def 2;
A4: (G*t).b = G.(t.b) by A1,Th28
.= G.(t.b qua Morphism of C) by A3,NATTRA_1:def 1;
t.b is invertible by A2,NATTRA_1:def 10;
hence (G*t).b is invertible by A4,Th3;
end;
thus I*F is_naturally_transformable_to J*F by A1,Th27;
take t*F;
let a be Object of A;
(t*F).a = t.(F.a) by A1,Th29;
hence (t*F).a is invertible by A2,NATTRA_1:def 10;
end;
theorem Th49:
for F being Functor of A,B, G being Functor of B,A
for I being Functor of A,A st I ~= id A holds F*I ~= F & I*G ~= G
proof let F be Functor of A,B, G be Functor of B,A;
let I be Functor of A,A;
F*id A = F & id A*G = G by Th4;
hence thesis by Th48;
end;
definition
let A,B be Category;
pred A is_equivalent_with B means
:Def10: ex F being Functor of A,B, G being Functor of B,A st
G*F ~= id A & F*G ~= id B;
reflexivity
proof let A;
take id A, id A;
thus thesis by Th4;
end;
symmetry;
synonym A,B are_equivalent;
end;
theorem
A ~= B implies A is_equivalent_with B
proof given F being Functor of A,B such that
A1: F is_an_isomorphism;
take F,F";
thus F"*F ~= id A & F*F" ~= id B by A1,Th16;
end;
canceled 2;
theorem Th53:
A,B are_equivalent & B,C are_equivalent implies A,C are_equivalent
proof
given F1 being Functor of A,B, G1 being Functor of B,A such that
A1: G1*F1 ~= id A & F1*G1 ~= id B;
given F2 being Functor of B,C, G2 being Functor of C,B such that
A2: G2*F2 ~= id B & F2*G2 ~= id C;
take F2*F1,G1*G2;
(G1*G2)*F2 = G1*(G2*F2) & G1*id B = G1 by Th4,RELAT_1:55;
then A3: (G1*G2)*F2 ~= G1 by A2,Th49;
(G1*G2)*(F2*F1) = ((G1*G2)*F2)*F1 by RELAT_1:55;
then (G1*G2)*(F2*F1) ~= G1*F1 by A3,Th48;
hence (G1*G2)*(F2*F1) ~= id A by A1,NATTRA_1:32;
(F2*F1)*G1 = F2*(F1*G1) & F2*id B = F2 by Th4,RELAT_1:55;
then A4: (F2*F1)*G1 ~= F2 by A1,Th49;
(F2*F1)*(G1*G2) = ((F2*F1)*G1)*G2 by RELAT_1:55;
then (F2*F1)*(G1*G2) ~= F2*G2 by A4,Th48;
hence (F2*F1)*(G1*G2) ~= id C by A2,NATTRA_1:32;
end;
definition let A,B;
assume
A1: A,B are_equivalent;
mode Equivalence of A,B -> Functor of A,B means
:Def11: ex G being Functor of B,A st G*it ~= id A & it*G ~= id B;
existence by A1,Def10;
end;
theorem
id A is Equivalence of A,A
proof
thus A is_equivalent_with A;
take id A;
thus thesis by Th4;
end;
theorem
A,B are_equivalent & B,C are_equivalent implies
for F being Equivalence of A,B, G being Equivalence of B,C holds
G*F is Equivalence of A,C
proof assume
A1: A,B are_equivalent & B,C are_equivalent;
let F be Equivalence of A,B, G be Equivalence of B,C;
consider F' being Functor of B,A such that
A2: F'*F ~= id A & F*F' ~= id B by A1,Def11;
consider G' being Functor of C,B such that
A3: G'*G ~= id B & G*G' ~= id C by A1,Def11;
thus A,C are_equivalent by A1,Th53;
take F'*G';
(F'*G')*G = F'*(G'*G) & F'*id B = F' by Th4,RELAT_1:55;
then A4: (F'*G')*G ~= F' by A3,Th49;
(F'*G')*(G*F) = ((F'*G')*G)*F by RELAT_1:55;
then (F'*G')*(G*F) ~= F'*F by A4,Th48;
hence (F'*G')*(G*F) ~= id A by A2,NATTRA_1:32;
(G*F)*F' = G*(F*F') & G*id B = G by Th4,RELAT_1:55;
then A5: (G*F)*F' ~= G by A2,Th49;
(G*F)*(F'*G') = ((G*F)*F')*G' by RELAT_1:55;
then (G*F)*(F'*G') ~= G*G' by A5,Th48;
hence (G*F)*(F'*G') ~= id C by A3,NATTRA_1:32;
end;
theorem Th56:
A,B are_equivalent implies
for F being Equivalence of A,B ex G being Equivalence of B,A
st G*F ~= id A & F*G ~= id B
proof assume
A1: A,B are_equivalent;
let F be Equivalence of A,B;
consider G be Functor of B,A such that
A2: G*F ~= id A & F*G ~= id B by A1,Def11;
G is Equivalence of B,A
proof thus B,A are_equivalent by A1;
take F; thus thesis by A2;
end;
hence thesis by A2;
end;
theorem Th57:
for F being Functor of A,B, G being Functor of B,A st G*F ~= id A
holds F is faithful
proof
let F be Functor of A,B, G be Functor of B,A; assume
G*F ~= id A;
then A1: id A ~= G*F by NATTRA_1:31;
then A2: id A is_naturally_transformable_to G*F by NATTRA_1:def 11;
consider s being natural_transformation of id A, G*F such that
A3: s is invertible by A1,NATTRA_1:def 11;
thus F is faithful
proof let a,a' be Object of A; assume
A4: Hom(a,a') <> {};
then A5: Hom((id A).a,(id A).a') <> {} by CAT_1:126;
A6: Hom((id A).a',(G*F).a') <> {} by A2,Th30;
let f1,f2 be Morphism of a,a';
assume
A7: F.(f1 qua Morphism of A) = F.(f2 qua Morphism of A);
A8: (G*F).f1 = (G*F).(f1 qua Morphism of A) by A4,NATTRA_1:def 1
.= G.(F.(f2 qua Morphism of A)) by A7,FUNCT_2:21
.= (G*F).(f2 qua Morphism of A) by FUNCT_2:21
.= (G*F).f2 by A4,NATTRA_1:def 1;
s.a' is invertible by A3,NATTRA_1:def 10;
then A9: s.a' is monic by A6,CAT_1:73;
A10: s.a'*(id A).f1 = (G*F).f1*s.a by A2,A4,NATTRA_1:def 8
.= s.a'*(id A).f2 by A2,A4,A8,NATTRA_1:def 8;
thus f1 = (id A).f1 by A4,NATTRA_1:16
.= (id A).f2 by A5,A6,A9,A10,CAT_1:60
.= f2 by A4,NATTRA_1:16;
end;
end;
theorem
A,B are_equivalent implies
for F being Equivalence of A,B
holds F is full & F is faithful &
for b being Object of B ex a being Object of A st b, F.a are_isomorphic
proof assume
A1: A,B are_equivalent;
let F be Equivalence of A,B;
consider G being Equivalence of B,A such that
A2: G*F ~= id A and
A3: F*G ~= id B by A1,Th56;
A4: id A ~= G*F by A2,NATTRA_1:31;
then A5: id A is_naturally_transformable_to G*F by NATTRA_1:def 11;
consider s being natural_transformation of id A, G*F such that
A6: s is invertible by A4,NATTRA_1:def 11;
A7: id B ~= F*G by A3,NATTRA_1:31;
then A8: id B is_naturally_transformable_to F*G by NATTRA_1:def 11;
A9: ex t being natural_transformation of id B, F*G st
t is invertible by A7,NATTRA_1:def 11;
A10: G is faithful by A3,Th57;
thus F is full
proof let a,a' be Object of A such that
A11: Hom(F.a,F.a') <> {};
let g be Morphism of F.a,F.a';
A12: (id A).a = a & (id A).a' = a' by CAT_1:118;
A13: (G*F).a = G.(F.a) & (G*F).a' = G.(F.a') by CAT_1:113;
then reconsider h = G.g as Morphism of (G*F).a, (G*F).a';
A14: Hom((id A).a,(G*F).a) <> {} by A5,Th30;
A15: Hom((G*F).a,(G*F).a') <> {} by A11,A13,CAT_1:126;
(G*F) is_naturally_transformable_to id A by A2,NATTRA_1:def 11;
then A16: Hom((G*F).a',(id A).a') <> {} by Th30;
A17: Hom((id A).a,(G*F).a') <> {} by A14,A15,CAT_1:52;
hence
A18: Hom(a,a') <> {} by A12,A16,CAT_1:52;
reconsider f1 = s.a as Morphism of a, (G*F).a by CAT_1:118;
reconsider f2 = s.a' as Morphism of a', (G*F).a' by CAT_1:118;
take f = f2"*(h*f1);
A19: Hom((id A).a',(G*F).a') <> {} by A5,Th30;
s.a is invertible by A6,NATTRA_1:def 10;
then A20: s.a is epi by A14,CAT_1:73;
A21: s.a' is invertible by A6,NATTRA_1:def 10;
A22: (id A).f = ((s.a')"*(h*(s.a))) by A12,A18,NATTRA_1:16;
h*s.a = id((G*F).a')*(h*(s.a)) by A17,CAT_1:57
.= s.a'*(s.a')"*(h*(s.a)) by A19,A21,CAT_1:def 14
.= s.a'*(id A).f by A16,A17,A19,A22,CAT_1:54
.= (G*F).f*s.a by A5,A18,NATTRA_1:def 8;
then A23: h = (G*F).f by A14,A15,A20,CAT_1:65;
G.(g qua Morphism of B) = G.g by A11,NATTRA_1:def 1
.= (G*F).(f qua Morphism of A) by A18,A23,NATTRA_1:def 1
.= G.(F.(f qua Morphism of A)) by FUNCT_2:21
.= G.(F.f qua Morphism of B) by A18,NATTRA_1:def 1;
hence g = F.f by A10,A11,CAT_1:def 24
.= F.(f qua Morphism of A) by A18,NATTRA_1:def 1;
end;
thus F is faithful by A2,Th57;
let b be Object of B;
take G.b;
A24: F.(G.b) = (F*G).b & (id B).b = b by CAT_1:113,118;
id B is_transformable_to F*G by A8,NATTRA_1:def 7;
hence b, F.(G.b) are_isomorphic by A9,A24,Th9;
end;