:: Natural Transformations. Discrete Categories
:: by Andrzej Trybulec
::
:: Received May 15, 1991
:: Copyright (c) 1991-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, FUNCT_1, SUBSET_1, RELAT_1, ZFMISC_1, PARTFUN1,
FUNCT_4, REALSET1, TARSKI, CAT_1, GRAPH_1, STRUCT_0, CAT_2, MCART_1,
PZFMISC1, ALGSTR_0, FUNCT_2, NATTRA_1, MONOID_0, RELAT_2, BINOP_1,
ALTCAT_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, MCART_1, REALSET1,
PARTFUN1, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_3, BINOP_1, FUNCT_4, STRUCT_0,
GRAPH_1, CAT_1, CAT_2, CAT_3;
constructors PARTFUN1, REALSET1, CAT_2, FUNCOP_1, RELSET_1, CAT_3, XTUPLE_0,
FUNCT_4;
registrations XBOOLE_0, SUBSET_1, RELSET_1, REALSET1, CAT_1, CAT_2, STRUCT_0,
ZFMISC_1, RELAT_1, XTUPLE_0;
requirements SUBSET, BOOLE;
definitions CAT_2, TARSKI, CAT_1, XBOOLE_0, FUNCT_2, ZFMISC_1;
equalities CAT_2, TARSKI, CAT_1, REALSET1, BINOP_1, GRAPH_1;
expansions TARSKI, CAT_1, XBOOLE_0, FUNCT_2;
theorems SUBSET_1, FUNCT_2, CAT_1, TARSKI, MCART_1, ZFMISC_1, PARTFUN1,
FUNCT_1, DOMAIN_1, CAT_2, FUNCT_3, FUNCT_4, GRFUNC_1, RELAT_1, RELSET_1,
XBOOLE_0, XBOOLE_1, CAT_3, XTUPLE_0;
schemes FUNCT_2, BINOP_1, FRAENKEL, XBOOLE_0;
begin
:: Preliminaries
reserve A,B,C for Category,
F,F1,F2,F3 for Functor of A,B,
G for Functor of B, C;
reserve m,o for set;
::$CT 4
theorem Th1:
for a being Object of A holds [[id a,id a],id a] in the Comp of A
proof
let a be Object of A;
A1: dom id a = a;
A2: cod id a = a;
then
A3: [id a,id a] in dom the Comp of A by A1,CAT_1:15;
(id a)(*)(id a) = id a by A1,CAT_1:22;
then (the Comp of A).(id a,id a) = id a by A1,A2,CAT_1:16;
hence thesis by A3,FUNCT_1:def 2;
end;
theorem Th2:
the Comp of 1Cat(o,m) = {[[m,m],m]}
proof
set A = 1Cat(o,m);
reconsider f = m as Morphism of A by TARSKI:def 1;
set a = the Object of A;
thus the Comp of A c= {[[m,m],m]}
proof
set o9 = the Object of A;
let x be object;
A1: dom id o9 = o9;
A2: cod id o9 = o9;
assume
A3: x in the Comp of A;
then consider x1,x2 being object such that
A4: x = [x1,x2] by RELAT_1:def 1;
A5: x1 in dom the Comp of A by A3,A4,XTUPLE_0:def 12;
dom the Comp of A c= [:the carrier' of A, the carrier' of A:] by
RELAT_1:def 18;
then consider x11,x12 being object such that
A6: x11 in the carrier' of A and
A7: x12 in the carrier' of A and
A8: x1 = [x11,x12] by A5,ZFMISC_1:def 2;
A9: x12 = id o9 by A7,ZFMISC_1:def 10;
A10: x2 is set by TARSKI:1;
x11 = id o9 by A6,ZFMISC_1:def 10;
then x2 = (the Comp of A).(id o9,id o9) by A3,A4,A5,A8,A9,FUNCT_1:def 2,A10
;
then x2 = id o9(*)(id o9 qua Morphism of A) by A1,A2,CAT_1:16;
then
A11: x2 = m by TARSKI:def 1;
A12: x12 = m by A7,TARSKI:def 1;
x11 = m by A6,TARSKI:def 1;
hence thesis by A4,A8,A12,A11,TARSKI:def 1;
end;
let x be object;
assume x in {[[m,m],m]};
then
A13: x = [[m,m],m] by TARSKI:def 1;
f = id a by TARSKI:def 1;
hence thesis by A13,Th1;
end;
theorem Th3:
for a being Object of A holds 1Cat(a,id a) is Subcategory of A
proof
let d be Object of A;
thus the carrier of 1Cat(d,id d) c= the carrier of A
proof
let b be object;
assume b in the carrier of 1Cat(d,id d);
then b = d by TARSKI:def 1;
hence thesis;
end;
thus for a,b being Object of 1Cat(d,id d), a9,b9 being Object of A st a = a9
& b = b9 holds Hom(a,b) c= Hom(a9,b9)
proof
let a,b be Object of 1Cat(d,id d), a9,b9 be Object of A;
assume that
A1: a = a9 and
A2: b = b9;
A3: b9 = d by A2,TARSKI:def 1;
let x be object;
assume x in Hom(a,b);
then
A4: x = id d by TARSKI:def 1;
a9 = d by A1,TARSKI:def 1;
hence thesis by A3,A4,CAT_1:27;
end;
thus the Comp of 1Cat(d,id d) c= the Comp of A
proof
let x be object;
assume x in the Comp of 1Cat(d,id d);
then x in {[[id d,id d],id d]} by Th2;
then x = [[id d,id d],id d] by TARSKI:def 1;
hence thesis by Th1;
end;
let a be Object of 1Cat(d,id d), a9 be Object of A;
assume a = a9;
then a9 = d by TARSKI:def 1;
hence thesis by TARSKI:def 1;
end;
theorem Th4:
for C being Subcategory of A holds the Source of C = (the Source
of A)|the carrier' of C & the Target of C = (the Target of A)|the carrier' of C
& the Comp of C = (the Comp of A)||the carrier' of C
proof
let C be Subcategory of A;
A1: dom the Source of A = the carrier' of A by FUNCT_2:def 1;
A2: now
let x be object;
assume x in dom the Source of C;
then reconsider m = x as Morphism of C by FUNCT_2:def 1;
reconsider m9=m as Morphism of A by CAT_2:8;
thus (the Source of C).x = dom m .= dom m9 by CAT_2:9
.= (the Source of A).x;
end;
A3: now
let x be object;
assume x in dom the Target of C;
then reconsider m = x as Morphism of C by FUNCT_2:def 1;
reconsider m9=m as Morphism of A by CAT_2:8;
thus (the Target of C).x = cod m .= cod m9 by CAT_2:9
.= (the Target of A).x;
end;
dom the Source of C = the carrier' of C by FUNCT_2:def 1;
then dom the Source of C = (dom the Source of A) /\ the carrier' of C by A1,
CAT_2:7,XBOOLE_1:28;
hence the Source of C = (the Source of A)|the carrier' of C by A2,FUNCT_1:46;
A4: dom the Target of A = the carrier' of A by FUNCT_2:def 1;
dom the Target of C = the carrier' of C by FUNCT_2:def 1;
then dom the Target of C = (dom the Target of A) /\ the carrier' of C by A4,
CAT_2:7,XBOOLE_1:28;
hence the Target of C = (the Target of A)|the carrier' of C by A3,FUNCT_1:46;
A5: dom the Comp of C = (dom the Comp of A) /\ [:the carrier' of C, the
carrier' of C:]
proof
the Comp of C c= the Comp of A by CAT_2:def 4;
then
A6: dom the Comp of C c= dom the Comp of A by RELAT_1:11;
dom the Comp of C c= [:the carrier' of C, the carrier' of C:] by
RELAT_1:def 18;
hence dom the Comp of C c= (dom the Comp of A) /\ [:the carrier' of C, the
carrier' of C:] by A6,XBOOLE_1:19;
let x be object;
assume
A7: x in(dom the Comp of A) /\ [:the carrier' of C, the carrier' of C :];
then x in [:the carrier' of C, the carrier' of C:] by XBOOLE_0:def 4;
then reconsider f=x`1, g=x`2 as Morphism of C by MCART_1:10;
reconsider f9=f, g9=g as Morphism of A by CAT_2:8;
x in dom the Comp of A by A7,XBOOLE_0:def 4;
then
A8: [f9,g9] in dom the Comp of A by MCART_1:21;
dom f = dom f9 by CAT_2:9
.= cod g9 by A8,CAT_1:15
.= cod g by CAT_2:9;
then [f,g] in dom the Comp of C by CAT_1:15;
hence thesis by A7,MCART_1:21;
end;
the Comp of C c= the Comp of A by CAT_2:def 4;
hence
the Comp of C = (the Comp of A)| ((dom the Comp of A) /\ [:the carrier'
of C, the carrier' of C:] qua set) by A5,GRFUNC_1:23
.= ((the Comp of A) qua Relation)| (dom(the Comp of A) qua set)| ([:the
carrier' of C, the carrier' of C:] qua set) by RELAT_1:71
.= (the Comp of A)||the carrier' of C;
end;
theorem Th5:
for O being non empty Subset of the carrier of A,
M being non empty Subset of the carrier' of A st
for o being Element of A st o in O holds id o in M
for DOM,COD being Function of M,O st DOM = (the Source of A) |M &
COD = (the Target of A)|M
for COMP being PartFunc of [:M,M qua non empty set:], M
st COMP = (the Comp of A)||M
holds CatStr(#O,M,DOM,COD,COMP#) is Subcategory of A
proof
let O be non empty Subset of the carrier of A,
M be non empty Subset of the carrier' of A such that
A1: for o being Element of A st o in O holds id o in M;
let DOM,COD be Function of M,O such that
A2: DOM = (the Source of A) |M and
A3: COD = (the Target of A)|M;
let COMP be PartFunc of [:M,M qua non empty set:], M such that
A4: COMP = (the Comp of A)||M;
set C = CatStr(#O,M,DOM,COD,COMP#);
A5: now
let f be (Morphism of A), g be Morphism of C such that
A6: f = g;
dom the Source of C = the carrier' of C by FUNCT_2:def 1;
hence dom f = dom g by A2,A6,FUNCT_1:47;
dom the Target of C = the carrier' of C by FUNCT_2:def 1;
hence cod f = cod g by A3,A6,FUNCT_1:47;
end;
A7: dom the Comp of C = (dom the Comp of A) /\ [:the carrier' of C, the
carrier' of C:] by A4,RELAT_1:61;
A8: now
let f,g be Morphism of C;
reconsider g9=g, f9=f as Morphism of A by TARSKI:def 3;
assume dom g = cod f;
then dom g9 = cod f by A5
.= cod f9 by A5;
then
A9: [g9,f9] in dom the Comp of A by CAT_1:def 6;
[g,f] in [:the carrier' of C, the carrier' of C:] by ZFMISC_1:87;
hence [g,f] in dom the Comp of C by A7,A9,XBOOLE_0:def 4;
end;
A10: dom the Comp of C c= dom the Comp of A by A4,RELAT_1:60;
A11: C is Category-like
proof
let f,g be Morphism of C;
reconsider g9=g, f9=f as Morphism of A by TARSKI:def 3;
thus [g,f] in dom(the Comp of C) implies dom g=cod f
proof
assume
A12: [g,f] in dom the Comp of C;
thus dom g = dom g9 by A5
.= cod f9 by A10,A12,CAT_1:def 6
.= cod f by A5;
end;
thus thesis by A8;
end;
A13: C is transitive
proof
let f,g be Morphism of C;
reconsider g9=g, f9=f as Morphism of A by TARSKI:def 3;
assume
A14: dom g=cod f;
[g,f] in dom the Comp of C by A14,A11;
then
A15: (the Comp of C).(g,f) = g(*)f by CAT_1:def 1;
A16: dom g9 = cod f by A5,A14
.= cod f9 by A5;
then [g9,f9] in dom the Comp of A by CAT_1:def 6;
then
A17: (the Comp of A).(g9,f9) = g9(*)f9 by CAT_1:def 1;
A18: (the Comp of C).(g,f) = (the Comp of A).(g9,f9) by A4,A8,A14,FUNCT_1:47;
thus dom(g(*)f) =
dom(g9(*)f9) by A5,A18,A15,A17
.= dom f9 by A16,CAT_1:def 7
.= dom f by A5;
thus cod(g(*)f)
= cod(g9(*)f9) by A5,A18,A15,A17
.= cod g9 by A16,CAT_1:def 7
.= cod g by A5;
end;
A19: for f,g being Morphism of C st cod g = dom f
for ff,gg being Morphism of A st ff=f & gg=g
holds f(*)g = ff(*)gg
proof let f,g be Morphism of C such that
A20: cod g = dom f;
let ff,gg be Morphism of A such that
A21: ff=f & gg=g;
A22: cod gg = dom f by A20,A5,A21
.= dom ff by A5,A21;
[f,g] in dom the Comp of C by A20,A11;
hence f(*)g = (the Comp of C).(f,g) by CAT_1:def 1
.= (the Comp of A).(ff,gg) by A21,A4,A8,A20,FUNCT_1:47
.= ff(*)gg by A22,CAT_1:16;
end;
A23: C is associative
proof
let f,g,h be Morphism of C;
reconsider g9=g, f9=f, h9=h as Morphism of A by TARSKI:def 3;
assume that
A24: dom h = cod g and
A25: dom g = cod f;
reconsider gf = (the Comp of C).(g,f), hg = (the Comp of C).[h,g] as
Morphism of C by A8,A24,A25,PARTFUN1:4;
A26: dom h9 = cod g by A5,A24
.= cod g9 by A5;
then
A27: [h9,g9] in dom the Comp of A by CAT_1:def 6;
A28: dom g9 = cod f by A5,A25
.= cod f9 by A5;
then
A29: [g9,f9] in dom the Comp of A by CAT_1:def 6;
reconsider gf9 = g9(*)f9, hg9 = h9(*)g9 as Morphism of A;
(the Comp of C).(h,g) = (the Comp of A).(h9,g9) by A4,A8,A24,FUNCT_1:47;
then
A30: hg = h9(*)g9 by A27,CAT_1:def 1;
then
A31: dom hg = dom hg9 by A5
.= dom g9 by A26,CAT_1:def 7
.= cod f by A5,A25;
(the Comp of C).(g,f) = (the Comp of A).(g9,f9) by A4,A8,A25,FUNCT_1:47;
then
A32: gf = gf9 by A29,CAT_1:def 1;
A33: dom h = cod g9 by A5,A24
.= cod gf9 by A28,CAT_1:def 7
.= cod gf by A5,A32;
A34: h(*)g = h9(*)g9 by A19,A24;
g(*)f = g9(*)f9 by A19,A25;
hence h(*)(g(*)f)
= h9(*)(g9(*)f9) by A19,A33,A32
.= h9(*)g9(*)f9 by A26,A28,CAT_1:def 8
.= h(*)g(*)f by A19,A34,A30,A31;
end;
A35: C is reflexive
proof
let b be Object of C;
reconsider b9 = b as Object of A by TARSKI:def 3;
reconsider ii = id b9 as Morphism of C by A1;
A36: cod ii = cod id b9 by A5 .= b;
dom ii = dom id b9 by A5 .= b;
then ii in Hom(b,b) by A36;
hence Hom(b,b)<>{};
end;
A37: for a be Object of C, aa being Element of A st a = aa
for m being Morphism of C st m = id aa
for b being Object of C holds
(Hom(a,b) <> {} implies
for f being Morphism of a,b holds f(*)m = f)
& (Hom(b,a) <> {} implies
for f being Morphism of b,a holds m(*)f = f)
proof let a be Object of C, aa be Element of A such that
A38: a = aa;
let m be Morphism of C such that
A39: m = id aa;
let b be Object of C;
reconsider bb = b as Object of A by TARSKI:def 3;
thus Hom(a,b) <> {} implies
for f being Morphism of a,b holds f(*)m = f
proof assume
A40: Hom(a,b) <> {};
let f be Morphism of a,b;
reconsider ff = f as Morphism of A by TARSKI:def 3;
dom f = a by A40,CAT_1:5;
then
A41: dom ff = aa by A38,A5;
dom f = cod id aa by A38,A40,CAT_1:5 .= cod m by A39,A5;
hence f(*)m = ff(*)id aa by A19,A39
.= f by A41,CAT_1:22;
end;
thus Hom(b,a) <> {} implies
for f being Morphism of b,a holds m(*)f = f
proof assume
A42: Hom(b,a) <> {};
let f be Morphism of b,a;
reconsider ff = f as Morphism of A by TARSKI:def 3;
cod f = a by A42,CAT_1:5;
then
A43: cod ff = aa by A38,A5;
dom f = b by A42,CAT_1:5;
then dom ff = bb by A5;
then
A44: ff in Hom(bb,aa) by A43;
then reconsider ff as Morphism of bb,aa by CAT_1:def 5;
A45: Hom(aa,aa) <> {};
cod f = dom id aa by A38,A42,CAT_1:5 .= dom m by A39,A5;
hence m(*)f = (id aa)(*)ff by A19,A39
.= (id aa)*ff by A44,A45,CAT_1:def 13
.= f by A44,CAT_1:28;
end;
end;
C is with_identities
proof
let a be Element of C;
reconsider aa = a as Element of A by TARSKI:def 3;
reconsider m = id aa as Morphism of C by A1;
A46: cod m = cod id aa by A5 .= a;
dom m = dom id aa by A5 .= a;
then m in Hom(a,a) by A46;
then reconsider m as Morphism of a,a by CAT_1:def 5;
take m;
thus thesis by A37;
end;
then reconsider C as Category by A11,A13,A23,A35;
C is Subcategory of A
proof
thus the carrier of C c= the carrier of A;
thus for a,b being Object of C, a9,b9 being Object of A st a = a9 & b = b9
holds Hom(a,b) c= Hom(a9,b9)
proof
let a,b be Object of C, a9,b9 be Object of A such that
A47: a = a9 and
A48: b = b9;
let x be object;
assume x in Hom(a,b);
then consider f being Morphism of C such that
A49: x = f and
A50: dom f = a and
A51: cod f = b;
reconsider f9 = f as Morphism of A by TARSKI:def 3;
A52: cod f9 = b9 by A5,A48,A51;
dom f9 = a9 by A5,A47,A50;
hence thesis by A49,A52;
end;
thus the Comp of C c= the Comp of A by A4,RELAT_1:59;
let a be Object of C, a9 be Object of A;
assume
A53: a = a9;
reconsider m = id a9 as Morphism of C by A1,A53;
A54: cod m = cod id a9 by A5 .= a by A53;
dom m = dom id a9 by A5 .= a by A53;
then m in Hom(a,a) by A54;
then reconsider m as Morphism of a,a by CAT_1:def 5;
for b being Object of C holds
(Hom(a,b) <> {} implies
for f being Morphism of a,b holds f(*)m = f)
& (Hom(b,a) <> {} implies
for f being Morphism of b,a holds m(*)f = f) by A53,A37;
hence id a = id a9 by CAT_1:def 12;
end;
hence thesis;
end;
theorem Th6:
for C being strict Category, A being strict Subcategory of C st
the carrier of A = the carrier of C & the carrier' of A = the carrier' of C
holds A = C
proof
let C be strict Category, A be strict Subcategory of C such that
A1: the carrier of A = the carrier of C and
A2: the carrier' of A = the carrier' of C;
A3: the Target of A = (the Target of C)|the carrier' of A by Th4
.= the Target of C by A2;
A4: the Comp of A = (the Comp of C)||the carrier' of A by Th4
.= the Comp of C by A2;
the Source of A = (the Source of C)|the carrier' of A by Th4
.= the Source of C by A2;
hence thesis by A1,A3,A4;
end;
begin :: Application of a functor to a morphism
definition
::$CD
end;
theorem
for a,b being Object of A st Hom(a,b) <> {} for f being Morphism of a,
b holds (G*F)/.f = G/.(F/.f)
proof
let a,b be Object of A;
assume
A1: Hom(a,b) <> {};
then
A2: Hom(F.a,F.b) <> {} by CAT_1:84;
let f be Morphism of a,b;
thus (G*F)/.f = (G*F).(f qua Morphism of A) by A1,CAT_3:def 10
.= G.(F.(f qua Morphism of A)) by FUNCT_2:15
.= G.(F/.f qua Morphism of B) by A1,CAT_3:def 10
.= G/.(F/.f) by A2,CAT_3:def 10;
end;
:: The following theorems are analogues of theorems from CAT_1, with
:: the new concept of the application of a functor to a morphism
theorem
for F1,F2 being Functor of A,B
st for a,b being Object of A st Hom(a,b) <> {}
for f being Morphism of a,b holds F1.f = F2.f
holds F1 = F2
proof
let F1,F2 be Functor of A,B such that
A1: for a,b being Object of A st Hom(a,b) <> {} for f being Morphism of
a,b holds F1.f = F2.f;
now
let f be Morphism of A;
reconsider f9 = f as Morphism of dom f, cod f by CAT_1:4;
set a = dom f, b = cod f;
Hom(dom f, cod f) <> {} by CAT_1:2;
hence F1.f = F2.f9 by A1
.= F2.f;
end;
hence thesis;
end;
theorem Th9:
for a,b,c being Object of A st Hom(a,b) <> {} & Hom(b,c) <> {}
for f being Morphism of a,b, g being Morphism of b,c
holds F/.(g*f) = (F/.g)*(F/.f)
proof
let a,b,c be Object of A;
assume that
A1: Hom(a,b) <> {} and
A2: Hom(b,c) <> {};
let f be Morphism of a,b, g be Morphism of b,c;
A3: dom g = b by A2,CAT_1:5;
A4: cod f = b by A1,CAT_1:5;
A5: F/.g = F.(g qua Morphism of A) by A2,CAT_3:def 10;
A6: Hom(F.a,F.b) <> {} by A1,CAT_1:84;
A7: F/.f = F.(f qua Morphism of A) by A1,CAT_3:def 10;
A8: Hom(F.b,F.c) <> {} by A2,CAT_1:84;
Hom(a,c) <> {} by A1,A2,CAT_1:24;
hence F/.(g*f) = F.(g*f qua Morphism of A) by CAT_3:def 10
.= F.((g qua Morphism of A)(*)(f qua Morphism of A)) by A1,A2,CAT_1:def 13
.= (F.(g qua Morphism of A))(*)(F.(f qua Morphism of A)) by A3,A4,CAT_1:64
.= (F/.g)*(F/.f) by A6,A8,A5,A7,CAT_1:def 13;
end;
theorem
for c being Object of A, d being Object of B st F/.(id c) = id d
holds F.c = d
proof
let c be Object of A, d be Object of B;
A1: Hom(c,c) <> {};
assume F/.(id c) = id d;
then F.(id c qua Morphism of A) = id d by A1,CAT_3:def 10;
hence thesis by CAT_1:70;
end;
theorem Th11:
for a being Object of A holds F/.id a = id (F.a)
proof
let a be Object of A;
Hom(a,a) <> {};
hence F/.id a = F.((id a) qua Morphism of A) by CAT_3:def 10
.= id (F.a) by CAT_1:71;
end;
theorem
for a,b being Object of A st Hom(a,b) <> {} for f being Morphism of a,
b holds (id A)/.f = f
proof
let a,b be Object of A such that
A1: Hom(a,b) <> {};
let f be Morphism of a,b;
thus (id A)/.f = (id A).(f qua Morphism of A) by A1,CAT_3:def 10
.= f by FUNCT_1:18;
end;
theorem
for a,b,c,d being Object of A st Hom(a,b) meets Hom(c,d) holds a = c & b = d
proof
let a,b,c,d be Object of A;
assume Hom(a,b) meets Hom(c,d);
then consider x being object such that
A1: x in Hom(a,b) and
A2: x in Hom(c,d) by XBOOLE_0:3;
reconsider x as Morphism of A by A1;
A3: cod x = b by A1,CAT_1:1;
dom x = a by A1,CAT_1:1;
hence thesis by A2,A3,CAT_1:1;
end;
begin :: Transformations
definition
let A,B,F1,F2;
pred F1 is_transformable_to F2 means
:Def1:
for a being Object of A holds Hom(F1.a,F2.a) <> {};
reflexivity;
end;
theorem Th14:
F is_transformable_to F1 & F1 is_transformable_to F2 implies F
is_transformable_to F2
proof
assume that
A1: F is_transformable_to F1 and
A2: F1 is_transformable_to F2;
let a be Object of A;
A3: Hom(F1.a,F2.a) <> {} by A2;
Hom(F.a,F1.a) <> {} by A1;
hence thesis by A3,CAT_1:24;
end;
definition
let A,B,F1,F2;
assume
A1: F1 is_transformable_to F2;
mode transformation of F1,F2 -> Function of the carrier of A, the carrier'
of B means
:Def2:
for a being Object of A holds it.a is Morphism of F1.a,F2.a;
existence
proof
deffunc F(Object of A) = Hom(F1.$1,F2.$1);
A2: for a being Object of A holds the carrier' of B meets F(a)
proof
let a be Object of A;
set x = the Element of Hom(F1.a,F2.a);
A3: Hom(F1.a,F2.a) <> {} by A1;
now
take x;
thus x in the carrier' of B & x in Hom(F1.a,F2.a) by A3,TARSKI:def 3;
end;
hence thesis by XBOOLE_0:3;
end;
consider t being Function of the carrier of A, the carrier' of B such that
A4: for a being Object of A holds t.a in F(a) from FUNCT_2:sch 10(A2);
take t;
let a be Object of A;
t.a in Hom(F1.a,F2.a) by A4;
hence thesis by CAT_1:def 5;
end;
end;
definition
let A,B;
let F be Functor of A,B;
func id F ->transformation of F,F means
:Def3:
for a being Object of A holds it.a = id (F.a);
existence
proof
deffunc F(Object of A) = id (F.$1);
consider t being Function of the carrier of A, the carrier' of B such that
A1: for a being Object of A holds t.a = F(a) from FUNCT_2:sch 4;
for a being Object of A holds t.a is Morphism of F.a,F.a
proof
let a be Object of A;
t.a = id (F.a) by A1;
hence thesis;
end;
then reconsider t as transformation of F,F by Def2;
take t;
let a be Object of A;
thus thesis by A1;
end;
uniqueness
proof
let it1,it2 be transformation of F,F such that
A2: for a being Object of A holds it1.a = id (F.a) and
A3: for a being Object of A holds it2.a = id (F.a);
now
let a be Object of A;
thus it1.a = id (F.a) by A2
.= it2.a by A3;
end;
hence it1 = it2;
end;
end;
definition
let A,B,F1,F2;
assume
A1: F1 is_transformable_to F2;
let t be transformation of F1,F2;
let a be Object of A;
func t.a -> Morphism of F1.a, F2.a equals
:Def4:
t.a;
coherence by A1,Def2;
end;
definition
let A,B,F,F1,F2;
assume that
A1: F is_transformable_to F1 and
A2: F1 is_transformable_to F2;
let t1 be transformation of F,F1;
let t2 be transformation of F1,F2;
func t2`*`t1 -> transformation of F,F2 means
:Def5:
for a being Object of A holds it.a = (t2.a)*(t1.a);
existence
proof
deffunc F(Object of A) = (t2.$1)*(t1.$1);
consider t being Function of the carrier of A, the carrier' of B such that
A3: for a being Object of A holds t.a = F(a) from FUNCT_2:sch 4;
A4: for a being Object of A holds t.a is Morphism of F.a,F2.a
proof
let a be Object of A;
t.a = (t2.a)*(t1.a) by A3;
hence thesis;
end;
F is_transformable_to F2 by A1,A2,Th14;
then reconsider t9 = t as transformation of F,F2 by A4,Def2;
take t9;
let a be Object of A;
thus t9.a = t.a by A1,A2,Def4,Th14
.= (t2.a)*(t1.a) by A3;
end;
uniqueness
proof
let it1,it2 be transformation of F,F2 such that
A5: for a being Object of A holds it1.a = (t2.a)*(t1.a) and
A6: for a being Object of A holds it2.a = (t2.a)*(t1.a);
now
let a be Object of A;
thus (it1 qua Function of the carrier of A, the carrier' of B).a = it1.a
by A1,A2,Def4,Th14
.= (t2.a)*(t1.a) by A5
.= it2.a by A6
.= (it2 qua Function of the carrier of A, the carrier' of B).a by A1,A2
,Def4,Th14;
end;
hence it1 = it2;
end;
end;
theorem Th15:
F1 is_transformable_to F2 implies for t1,t2 being transformation
of F1,F2 st for a being Object of A holds t1.a = t2.a holds t1 = t2
proof
assume
A1: F1 is_transformable_to F2;
let t1,t2 be transformation of F1,F2;
assume
A2: for a being Object of A holds t1.a = t2.a;
now
let a be Object of A;
thus (t1 qua Function of the carrier of A, the carrier' of B).a = t1.a by
A1,Def4
.= t2.a by A2
.= (t2 qua Function of the carrier of A, the carrier' of B).a by A1,Def4;
end;
hence thesis;
end;
theorem Th16:
for a being Object of A holds id F.a = id(F.a)
proof
let a be Object of A;
thus id F.a = (id F qua Function of the carrier of A, the carrier' of B).a
by Def4
.= id (F.a) by Def3;
end;
theorem Th17:
F1 is_transformable_to F2 implies for t being transformation of
F1,F2 holds (id F2)`*`t = t & t`*`(id F1) = t
proof
assume
A1: F1 is_transformable_to F2;
let t be transformation of F1,F2;
now
let a be Object of A;
A2: Hom(F1.a,F2.a) <> {} by A1;
thus ((id F2)`*`t).a = ((id F2).a)*(t.a) by A1,Def5
.= (id(F2.a))*(t.a) by Th16
.= t.a by A2,CAT_1:28;
end;
hence (id F2)`*`t = t by A1,Th15;
now
let a be Object of A;
A3: Hom(F1.a,F2.a) <> {} by A1;
thus (t`*`(id F1)).a = (t.a)*((id F1).a) by A1,Def5
.= (t.a)*(id(F1.a)) by Th16
.= t.a by A3,CAT_1:29;
end;
hence thesis by A1,Th15;
end;
theorem Th18:
F is_transformable_to F1 & F1 is_transformable_to F2 & F2
is_transformable_to F3 implies for t1 being transformation of F,F1, t2 being
transformation of F1,F2, t3 being transformation of F2,F3 holds t3`*`t2`*`t1 =
t3`*`(t2`*`t1)
proof
assume that
A1: F is_transformable_to F1 and
A2: F1 is_transformable_to F2 and
A3: F2 is_transformable_to F3;
let t1 be transformation of F,F1, t2 be transformation of F1,F2, t3 be
transformation of F2,F3;
A4: F1 is_transformable_to F3 by A2,A3,Th14;
A5: F is_transformable_to F2 by A1,A2,Th14;
now
let a be Object of A;
A6: Hom(F.a,F1.a) <> {} by A1;
A7: Hom(F1.a,F2.a) <> {} by A2;
A8: Hom(F2.a,F3.a) <> {} by A3;
thus (t3`*`t2`*`t1).a = ((t3`*`t2).a)*(t1.a) by A1,A4,Def5
.= (t3.a)*(t2.a)*(t1.a) by A2,A3,Def5
.= (t3.a)*((t2.a)*(t1.a)) by A6,A7,A8,CAT_1:25
.= (t3.a)*((t2`*`t1).a) by A1,A2,Def5
.= (t3`*`(t2`*`t1)).a by A3,A5,Def5;
end;
hence thesis by A1,A4,Th14,Th15;
end;
begin :: Natural transformations
Lm1: for a,b being Object of A st Hom(a,b) <> {} for f being Morphism of a,b
holds (id F.b)*(F/.f) = F/.f*id F.a
proof
let a,b be Object of A such that
A1: Hom(a,b) <> {};
let f be Morphism of a,b;
A2: Hom(a,a) <> {};
A3: Hom(b,b) <> {};
thus id F.b*(F/.f) = id(F.b)*F/.f by Th16
.= F/.id b*F/.f by Th11
.= F/.(id b*f) by A1,A3,Th9
.= F/.f by A1,CAT_1:28
.= F/.(f*id a) by A1,CAT_1:29
.= F/.f*F/.id a by A1,A2,Th9
.= F/.f*id(F.a) by Th11
.= F/.f*id F.a by Th16;
end;
definition
let A,B,F1,F2;
pred F1 is_naturally_transformable_to F2 means
F1 is_transformable_to
F2 & ex t being transformation of F1,F2 st for a,b being Object of A st Hom(a,b
) <> {} for f being Morphism of a,b holds t.b*F1/.f = F2/.f*t.a;
reflexivity
proof
let F;
ex t being transformation of F,F st for a,b being Object of A st Hom(a
,b) <> {} for f being Morphism of a,b holds t.b*F/.f = F/.f*t.a
proof
take id F;
thus thesis by Lm1;
end;
hence thesis;
end;
end;
Lm2: F is_transformable_to F1 & F1 is_transformable_to F2 implies for t1 being
transformation of F,F1 st for a,b being Object of A st Hom(a,b) <> {} for f
being Morphism of a,b holds t1.b*F/.f = F1/.f*t1.a
for t2 being transformation of
F1,F2 st for a,b being Object of A st Hom(a,b) <> {} for f being Morphism of a,
b holds t2.b*F1/.f = F2/.f*t2.a
for a,b being Object of A st Hom(a,b)<>{} for f
being Morphism of a,b holds (t2`*`t1).b*F/.f = F2/.f*(t2`*`t1).a
proof
assume that
A1: F is_transformable_to F1 and
A2: F1 is_transformable_to F2;
let t1 be transformation of F,F1 such that
A3: for a,b being Object of A st Hom(a,b) <> {} for f being Morphism of
a,b holds t1.b*F/.f = F1/.f*t1.a;
let t2 be transformation of F1,F2 such that
A4: for a,b being Object of A st Hom(a,b) <> {} for f being Morphism of
a,b holds t2.b*F1/.f = F2/.f*t2.a;
let a,b be Object of A;
A5: Hom(F.b,F1.b) <> {} by A1;
A6: Hom(F.a,F1.a) <> {} by A1;
A7: Hom(F1.b,F2.b) <> {} by A2;
A8: Hom(F1.a,F2.a) <> {} by A2;
assume
A9: Hom(a,b)<>{};
then
A10: Hom(F.a,F.b) <> {} by CAT_1:84;
let f be Morphism of a,b;
A11: Hom(F2.a,F2.b) <> {} by A9,CAT_1:84;
A12: Hom(F1.a,F1.b) <> {} by A9,CAT_1:84;
thus (t2`*`t1).b*F/.f = t2.b*t1.b*F/.f by A1,A2,Def5
.= t2.b*(t1.b*F/.f) by A10,A5,A7,CAT_1:25
.= t2.b*(F1/.f*t1.a) by A3,A9
.= t2.b*F1/.f*t1.a by A6,A7,A12,CAT_1:25
.= F2/.f*t2.a*t1.a by A4,A9
.= F2/.f*(t2.a*t1.a) by A6,A8,A11,CAT_1:25
.= F2/.f*(t2`*`t1).a by A1,A2,Def5;
end;
theorem Th19:
F is_naturally_transformable_to F1 & F1
is_naturally_transformable_to F2 implies F is_naturally_transformable_to F2
proof
assume
A1: F is_transformable_to F1;
given t1 being transformation of F,F1 such that
A2: for a,b being Object of A st Hom(a,b) <> {} for f being Morphism of
a,b holds t1.b*F/.f = F1/.f*t1.a;
assume
A3: F1 is_transformable_to F2;
given t2 being transformation of F1,F2 such that
A4: for a,b being Object of A st Hom(a,b) <> {} for f being Morphism of
a,b holds t2.b*F1/.f = F2/.f*t2.a;
thus F is_transformable_to F2 by A1,A3,Th14;
take t2`*`t1;
thus thesis by A1,A2,A3,A4,Lm2;
end;
definition
let A,B,F1,F2;
assume
A1: F1 is_naturally_transformable_to F2;
mode natural_transformation of F1,F2 -> transformation of F1,F2 means
:Def7:
for a,b being Object of A st Hom(a,b) <> {} for f being Morphism of a,b holds
it.b*F1/.f = F2/.f*it.a;
existence by A1;
end;
definition
let A,B,F;
redefine func id F -> natural_transformation of F,F; :: redefines id (NATTRA_1, definition)
coherence
proof
thus F is_naturally_transformable_to F;
thus thesis by Lm1;
end;
end;
definition
let A,B,F,F1,F2 such that
A1: F is_naturally_transformable_to F1 and
A2: F1 is_naturally_transformable_to F2;
let t1 be natural_transformation of F,F1;
let t2 be natural_transformation of F1,F2;
func t2`*`t1 -> natural_transformation of F,F2 equals
:Def8:
t2`*`t1;
coherence
proof
A3: F is_naturally_transformable_to F2 by A1,A2,Th19;
A4: F1 is_transformable_to F2 by A2;
A5: for a,b being Object of A st Hom(a,b) <> {} for f being Morphism of a,
b holds t2.b*F1/.f = F2/.f*t2.a by A2,Def7;
A6: for a,b being Object of A st Hom(a,b) <> {} for f being Morphism of a,
b holds t1.b*F/.f = F1/.f*t1.a by A1,Def7;
F is_transformable_to F1 by A1;
then for a,b being Object of A st Hom(a,b)<>{} for f being Morphism of a,b
holds (t2`*`t1).b*F/.f = F2/.f*(t2`*`t1).a by A4,A6,A5,Lm2;
hence thesis by A3,Def7;
end;
end;
theorem Th20:
F1 is_naturally_transformable_to F2 implies for t being
natural_transformation of F1,F2 holds (id F2)`*`t = t & t`*`(id F1) = t
proof
assume
A1: F1 is_naturally_transformable_to F2;
then
A2: F1 is_transformable_to F2;
let t be natural_transformation of F1,F2;
thus (id F2)`*`t = (id F2)`*`(t qua transformation of F1,F2) by A1,Def8
.= t by A2,Th17;
thus t`*`(id F1) = (t qua transformation of F1,F2)`*`(id F1) by A1,Def8
.= t by A2,Th17;
end;
reserve t for natural_transformation of F,F1,
t1 for natural_transformation of F1,F2;
theorem Th21:
F is_naturally_transformable_to F1 & F1
is_naturally_transformable_to F2 implies for t1 being natural_transformation of
F,F1 for t2 being natural_transformation of F1,F2 for a being Object of A holds
(t2`*`t1).a = (t2.a)*(t1.a)
proof
assume that
A1: F is_naturally_transformable_to F1 and
A2: F1 is_naturally_transformable_to F2;
A3: F1 is_transformable_to F2 by A2;
let t1 be natural_transformation of F,F1;
let t2 be natural_transformation of F1,F2;
let a be Object of A;
reconsider t19 = t1 as transformation of F,F1;
reconsider t29 = t2 as transformation of F1,F2;
A4: F is_transformable_to F1 by A1;
thus (t2`*`t1).a = (t29`*`t19).a by A1,A2,Def8
.= (t2.a)*(t1.a) by A4,A3,Def5;
end;
theorem Th22:
F is_naturally_transformable_to F1 & F1
is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 implies
for t3 being natural_transformation of F2,F3 holds t3`*`t1`*`t = t3`*`(t1`*`t)
proof
assume that
A1: F is_naturally_transformable_to F1 and
A2: F1 is_naturally_transformable_to F2 and
A3: F2 is_naturally_transformable_to F3;
A4: F is_naturally_transformable_to F2 by A1,A2,Th19;
A5: F2 is_transformable_to F3 by A3;
A6: F1 is_transformable_to F2 by A2;
let t3 be natural_transformation of F2,F3;
A7: F is_transformable_to F1 by A1;
F1 is_naturally_transformable_to F3 by A2,A3,Th19;
hence t3`*`t1`*`t = t3`*`t1`*`(t qua transformation of F,F1) by A1,Def8
.= (t3 qua transformation of F2,F3)`*`t1`*`t by A2,A3,Def8
.= t3`*`(t1`*`(t qua transformation of F,F1)) by A7,A6,A5,Th18
.= (t3 qua transformation of F2,F3)`*`(t1`*`t) by A1,A2,Def8
.= t3 `*`(t1`*`t) by A3,A4,Def8;
end;
:: Natural equivalences
definition
let A,B,F1,F2;
let IT be transformation of F1,F2;
attr IT is invertible means
for a being Object of A holds IT.a is invertible;
end;
definition
let A,B,F1,F2;
pred F1,F2 are_naturally_equivalent means
F1
is_naturally_transformable_to F2 & ex t being natural_transformation of F1,F2
st t is invertible;
reflexivity
proof
let F;
thus F is_naturally_transformable_to F;
take id F;
let a be Object of A;
(id F).a = id(F.a) by Th16;
hence thesis by CAT_1:44;
end;
end;
notation
let A,B,F1,F2;
synonym F1 ~= F2 for F1,F2 are_naturally_equivalent;
end;
Lm3: for t being transformation of F1,F2 st F1 is_transformable_to F2 & t is
invertible holds F2 is_transformable_to F1
proof
let t be transformation of F1,F2 such that
F1 is_transformable_to F2 and
A1: for a being Object of A holds t.a is invertible;
let a be Object of A;
A2: t.a is invertible by A1;
thus thesis by A2;
end;
definition
let A,B,F1,F2 such that
A1: F1 is_transformable_to F2;
let t1 be transformation of F1,F2 such that
A2: t1 is invertible;
func t1" -> transformation of F2,F1 means
:Def11:
for a being Object of A holds it.a = (t1.a)";
existence
proof
deffunc F(Object of A) = (t1.$1)";
consider t being Function of the carrier of A, the carrier' of B such that
A3: for a being Object of A holds t.a = F(a) from FUNCT_2:sch 4;
A4: now
let a be Object of A;
t.a = (t1.a)" by A3;
hence t.a is Morphism of F2.a,F1.a;
end;
F2 is_transformable_to F1 by A1,A2,Lm3;
then reconsider t as transformation of F2,F1 by A4,Def2;
take t;
let a be Object of A;
thus t.a = (t qua Function of the carrier of A, the carrier' of B).a
by A1,A2,Def4,Lm3
.= (t1.a)" by A3;
end;
uniqueness
proof
let t,t9 be transformation of F2,F1 such that
A5: for a being Object of A holds t.a = (t1.a)" and
A6: for a being Object of A holds t9.a = (t1.a)";
now
let a be Object of A;
thus t.a = (t1.a)" by A5
.= t9.a by A6;
end;
hence thesis by A1,A2,Lm3,Th15;
end;
end;
Lm4: now
let A,B,F1,F2,t1 such that
A1: F1 is_naturally_transformable_to F2 and
A2: t1 is invertible;
let a,b be Object of A such that
A3: Hom(a,b) <> {};
A4: Hom(F1.a,F1.b) <> {} by A3,CAT_1:84;
let f be Morphism of a,b;
A5: Hom(F2.a,F2.b) <> {} by A3,CAT_1:84;
A6: F1 is_transformable_to F2 by A1;
A7: Hom(F1.b,F2.b) <> {} by Def1,A1;
A8: t1.b is invertible by A2;
then
A9: Hom(F2.b,F1.b) <> {};
A10: Hom(F1.a,F2.a) <> {} by A1,Def1;
F2/.f*t1.a = t1.b*F1/.f by A1,A3,Def7;
then
A11: (t1.b)"*F2/.f*t1.a = (t1.b)"*(t1.b*F1/.f) by A10,A9,A5,CAT_1:25
.= (t1.b)"*t1.b*F1/.f by A4,A7,A9,CAT_1:25
.= id(F1.b)*F1/.f by A8,CAT_1:def 17
.= F1/.f by A4,CAT_1:28;
A12: t1.a is invertible by A2;
then
A13: Hom(F2.a,F1.a) <> {};
then
A14: Hom(F2.a,F1.b) <> {} by A4,CAT_1:24;
then (t1.b)"*F2/.f = (t1.b)"*F2/.f*id(F2.a) by CAT_1:29
.= (t1.b)"*F2/.f*(t1.a*(t1.a)") by A12,CAT_1:def 17
.= F1/.f*(t1.a)" by A10,A13,A14,A11,CAT_1:25;
hence t1".b*F2/.f = F1/.f*(t1.a)" by A2,A6,Def11
.= F1/.f*t1".a by A2,A6,Def11;
end;
Lm5: F1 is_naturally_transformable_to F2 & t1 is invertible implies F2
is_naturally_transformable_to F1
proof
assume
A1: F1 is_naturally_transformable_to F2;
assume
A2: t1 is invertible;
hence F2 is_transformable_to F1 by A1,Lm3;
take t1";
thus thesis by A1,A2,Lm4;
end;
definition
let A,B,F1,F2,t1 such that
A1: F1 is_naturally_transformable_to F2 and
A2: t1 is invertible;
func t1" -> natural_transformation of F2,F1 equals
:Def12:
(t1 qua
transformation of F1,F2)";
coherence
proof
A3: for a,b be Object of A st Hom(a,b) <> {} for f be Morphism of a,b
holds t1".b*F2/.f = F1/.f*t1".a by A1,A2,Lm4;
F2 is_naturally_transformable_to F1 by A1,A2,Lm5;
hence thesis by A3,Def7;
end;
end;
theorem Th23:
for A,B,F1,F2,t1 st F1 is_naturally_transformable_to F2 & t1 is
invertible for a being Object of A holds t1".a = (t1.a)"
proof
let A,B,F1,F2,t1 such that
A1: F1 is_naturally_transformable_to F2 and
A2: t1 is invertible;
let a be Object of A;
A3: F1 is_transformable_to F2 by A1;
thus t1".a = (t1 qua transformation of F1,F2)".a by A1,A2,Def12
.= ((t1 qua transformation of F1,F2).a)" by A2,A3,Def11;
end;
theorem
F1 ~= F2 implies F2 ~= F1
proof
assume
A1: F1 is_naturally_transformable_to F2;
given t being natural_transformation of F1,F2 such that
A2: t is invertible;
thus F2 is_naturally_transformable_to F1 by A1,A2,Lm5;
take t";
let a be Object of A;
t".a = (t.a)" by A1,A2,Th23;
hence thesis by A2,CAT_1:46;
end;
theorem Th25:
F1 ~= F2 & F2 ~= F3 implies F1 ~= F3
proof
assume
A1: F1 is_naturally_transformable_to F2;
given t being natural_transformation of F1,F2 such that
A2: t is invertible;
assume
A3: F2 is_naturally_transformable_to F3;
given t9 being natural_transformation of F2,F3 such that
A4: t9 is invertible;
thus F1 is_naturally_transformable_to F3 by A1,A3,Th19;
take t9`*`t;
let a be Object of A;
A5: t9.a is invertible by A4;
A6: t.a is invertible by A2;
(t9`*`t).a = (t9.a)*(t.a) by A1,A3,Th21;
hence thesis by A5,A6,CAT_1:45;
end;
definition
let A,B,F1,F2;
assume
A1: F1,F2 are_naturally_equivalent;
mode natural_equivalence of F1,F2 -> natural_transformation of F1,F2 means
:
Def13: it is invertible;
existence by A1;
end;
theorem
id F is natural_equivalence of F,F
proof
thus F ~= F;
let a be Object of A;
(id F).a = id(F.a) by Th16;
hence thesis by CAT_1:44;
end;
theorem
F1 ~= F2 & F2 ~= F3 implies for t being natural_equivalence of F1,F2,
t9 being natural_equivalence of F2,F3 holds t9`*`t is natural_equivalence of F1
,F3
proof
assume that
A1: F1,F2 are_naturally_equivalent and
A2: F2,F3 are_naturally_equivalent;
let t be natural_equivalence of F1,F2, t9 be natural_equivalence of F2,F3;
thus F1,F3 are_naturally_equivalent by A1,A2,Th25;
let a be Object of A;
t9 is invertible by A2,Def13;
then
A3: t9.a is invertible;
t is invertible by A1,Def13;
then
A4: t.a is invertible;
A5: F1 is_naturally_transformable_to F2 by A1;
A6: F2 is_naturally_transformable_to F3 by A2;
(t9`*`t).a = (t9.a)*(t.a) by A5,A6,Th21;
hence thesis by A3,A4,CAT_1:45;
end;
begin :: Functor category
definition
let A,B;
mode NatTrans-DOMAIN of A,B -> non empty set means
:Def14:
for x being set
holds x in it implies ex F1,F2 being Functor of A,B, t being
natural_transformation of F1,F2 st x = [[F1,F2],t] & F1
is_naturally_transformable_to F2;
existence
proof
set F = the Functor of A,B;
take {[[F,F],id F]};
let x be set such that
A1: x in {[[F,F],id F]};
take F,F, id F;
thus thesis by A1,TARSKI:def 1;
end;
end;
definition
let A,B;
func NatTrans(A,B) -> NatTrans-DOMAIN of A,B means
:Def15:
for x being set
holds x in it iff ex F1,F2 being Functor of A,B, t being natural_transformation
of F1,F2 st x = [[F1,F2],t] & F1 is_naturally_transformable_to F2;
existence
proof
set F = the Functor of A,B;
defpred P[object] means ex F1,F2 being Functor of A,B, t being
natural_transformation of F1,F2 st $1 = [[F1,F2],t] & F1
is_naturally_transformable_to F2;
consider T being set such that
A1: for x being object holds x in T iff x in [:[:Funct(A,B),Funct(A,B):],
Funcs(the carrier of A, the carrier' of B):] & P[x] from XBOOLE_0:sch 1;
F in Funct(A,B) by CAT_2:def 2;
then
A2: [F,F] in [:Funct(A,B),Funct(A,B):] by ZFMISC_1:87;
id F in Funcs(the carrier of A, the carrier' of B) by FUNCT_2:8;
then [[F,F],id F] in [:[:Funct(A,B),Funct(A,B):], Funcs(the carrier of A,
the carrier' of B):] by A2,ZFMISC_1:87;
then reconsider T as non empty set by A1;
for x being set st x in T holds ex F1,F2 being Functor of A,B, t being
natural_transformation of F1,F2 st x = [[F1,F2],t] & F1
is_naturally_transformable_to F2 by A1;
then reconsider T as NatTrans-DOMAIN of A,B by Def14;
take T;
let x be set;
thus x in T implies ex F1,F2 being Functor of A,B, t being
natural_transformation of F1,F2 st x = [[F1,F2],t] & F1
is_naturally_transformable_to F2 by A1;
given F1,F2 being Functor of A,B, t being natural_transformation of F1,F2
such that
A3: x = [[F1,F2],t] and
A4: F1 is_naturally_transformable_to F2;
A5: F2 in Funct(A,B) by CAT_2:def 2;
A6: t in Funcs(the carrier of A, the carrier' of B) by FUNCT_2:8;
F1 in Funct(A,B) by CAT_2:def 2;
then [F1,F2] in [:Funct(A,B),Funct(A,B):] by A5,ZFMISC_1:87;
then x in [:[:Funct(A,B),Funct(A,B):], Funcs(the carrier of A, the
carrier' of B):] by A3,A6,ZFMISC_1:87;
hence thesis by A1,A3,A4;
end;
uniqueness
proof
let S,T be NatTrans-DOMAIN of A,B such that
A7: for x being set holds x in S iff ex F1,F2 being Functor of A,B, t
being natural_transformation of F1,F2 st x = [[F1,F2],t] & F1
is_naturally_transformable_to F2 and
A8: for x being set holds x in T iff ex F1,F2 being Functor of A,B, t
being natural_transformation of F1,F2 st x = [[F1,F2],t] & F1
is_naturally_transformable_to F2;
now
let x be object;
x in S iff ex F1,F2 being Functor of A,B, t being
natural_transformation of F1,F2 st x = [[F1,F2],t] & F1
is_naturally_transformable_to F2 by A7;
hence x in S iff x in T by A8;
end;
hence thesis by TARSKI:2;
end;
end;
theorem Th28:
F1 is_naturally_transformable_to F2 iff [[F1,F2],t1] in NatTrans (A,B)
proof
thus F1 is_naturally_transformable_to F2 implies [[F1,F2],t1] in NatTrans(A,
B) by Def15;
assume [[F1,F2],t1] in NatTrans(A,B);
then consider
F19,F29 being Functor of A,B, t being natural_transformation of F19
,F29 such that
A1: [[F1,F2],t1] = [[F19,F29],t] and
A2: F19 is_naturally_transformable_to F29 by Def15;
A3: [F1,F2] = [F19,F29] by A1,XTUPLE_0:1;
then F1 = F19 by XTUPLE_0:1;
hence thesis by A2,A3,XTUPLE_0:1;
end;
definition
let A,B;
func Functors(A,B) -> strict Category means
:Def16:
the carrier of it =
Funct(A,B) & the carrier' of it = NatTrans(A,B) & (for f being Morphism of it
holds dom f = f`1`1 & cod f = f`1`2) & (for f,g being Morphism of it st dom g =
cod f holds [g,f] in dom the Comp of it) & (for f,g being Morphism of it st [g,
f] in dom (the Comp of it) ex F,F1,F2,t,t1 st f = [[F,F1],t] & g = [[F1,F2],t1]
& (the Comp of it).[g,f] = [[F,F2],t1`*`t])
& for a being Object of it, F st F
= a holds id a = [[F,F],id F];
existence
proof
defpred P[object,object,object] means
ex F,F1,F2,t,t1 st $2 = [[F,F1],t] & $1 = [[
F1,F2],t1] & $3 = [[F,F2],t1`*`t];
deffunc F(object) = $1`1`1;
A1: now
let x,y,z1,z2 be object;
assume that
x in NatTrans(A,B) and
y in NatTrans(A,B);
assume P[x,y,z1];
then consider F,F1,F2,t,t1 such that
A2: y = [[F,F1],t] and
A3: x = [[F1,F2],t1] and
A4: z1 = [[F,F2],t1`*`t];
assume P[x,y,z2];
then consider F9,F19,F29 being Functor of A,B, t9 being
natural_transformation of F9,F19, t19 being natural_transformation of F19,F29
such that
A5: y = [[F9,F19],t9] and
A6: x = [[F19,F29],t19] and
A7: z2 = [[F9,F29],t19`*`t9];
A8: t=t9 by A2,A5,XTUPLE_0:1;
[F1,F2]=[F19,F29] by A3,A6,XTUPLE_0:1;
then
A9: F2 = F29 by XTUPLE_0:1;
A10: t1=t19 by A3,A6,XTUPLE_0:1;
A11: [F,F1]=[F9,F19] by A2,A5,XTUPLE_0:1;
then F = F9 by XTUPLE_0:1;
hence z1 = z2 by A4,A7,A11,A8,A10,A9,XTUPLE_0:1;
end;
A12: now
let x,y,z be object;
assume that
A13: x in NatTrans(A,B) and
A14: y in NatTrans(A,B);
assume P[x,y,z];
then consider F,F1,F2,t,t1 such that
A15: y = [[F,F1],t] and
A16: x = [[F1,F2],t1] and
A17: z = [[F,F2],t1`*`t];
A18: F1 is_naturally_transformable_to F2 by A13,A16,Th28;
F is_naturally_transformable_to F1 by A14,A15,Th28;
hence z in NatTrans(A,B) by A17,Th28,A18,Th19;
end;
consider m being PartFunc of [:NatTrans(A,B),NatTrans(A,B):],NatTrans(A,B)
such that
A19: for x,y being object holds [x,y] in dom m iff x in NatTrans(A,B) & y
in NatTrans(A,B) & ex z being object st P[x,y,z] and
A20: for x,y being object st [x,y] in dom m holds P[x,y,m.(x,y)] from
BINOP_1:sch 5(A12,A1);
A21: now
let t be Element of NatTrans(A,B);
consider F1,F2 being Functor of A,B, s being natural_transformation of
F1,F2 such that
A22: t = [[F1,F2],s] and
F1 is_naturally_transformable_to F2 by Def15;
t`1`1 = [F1,F2]`1 by A22
.= F1;
hence F(t) in Funct(A,B) by CAT_2:def 2;
end;
consider d being Function of NatTrans(A,B), Funct(A,B) such that
A23: for t being Element of NatTrans(A,B) holds d.t = F(t) from FUNCT_2
:sch 8(A21);
deffunc F(set) = $1`1`2;
A24: now
let t be Element of NatTrans(A,B);
consider F1,F2 being Functor of A,B, s being natural_transformation of
F1,F2 such that
A25: t = [[F1,F2],s] and
F1 is_naturally_transformable_to F2 by Def15;
t`1`2 = [F1,F2]`2 by A25
.= F2;
hence F(t) in Funct(A,B) by CAT_2:def 2;
end;
consider c being Function of NatTrans(A,B), Funct(A,B) such that
A26: for t being Element of NatTrans(A,B) holds c.t = F(t) from FUNCT_2
:sch 8(A24);
deffunc F(Element of Funct(A,B)) = [[$1,$1],id $1];
A27: for F be Element of Funct(A,B) holds F(F) in NatTrans(A,B) by Def15;
consider i being Function of Funct(A,B), NatTrans(A,B) such that
A28: for F being Element of Funct(A,B) holds i.F = F(F) from FUNCT_2:
sch 8(A27);
set C = CatStr(#Funct(A,B),NatTrans(A,B),d,c,m#);
A29: now
let F,F1,F2,t,t1;
assume that
A30: F1 is_naturally_transformable_to F2 and
A31: F is_naturally_transformable_to F1;
A32: [[F,F1],t] in NatTrans(A,B) by A31,Th28;
A33: P[[[F1,F2],t1],[[F,F1],t],[[F,F2],t1`*`t]];
[[F1,F2],t1] in NatTrans(A,B) by A30,Th28;
then consider F9,F19,F29 being Functor of A,B, t9 being
natural_transformation of F9,F19, t19 being natural_transformation of F19,F29
such that
A34: [[F,F1],t] = [[F9,F19],t9] and
A35: [[F1,F2],t1] = [[F19,F29],t19] and
A36: m.([[F1,F2],t1],[[F,F1],t]) = [[F9,F29],t19`*`t9] by A20,A19,A32,A33;
A37: t = t9 by A34,XTUPLE_0:1;
[F1,F2] = [F19,F29] by A35,XTUPLE_0:1;
then
A38: F2 = F29 by XTUPLE_0:1;
A39: t1 = t19 by A35,XTUPLE_0:1;
A40: [F,F1] = [F9,F19] by A34,XTUPLE_0:1;
then F = F9 by XTUPLE_0:1;
hence m.[[[F1,F2],t1],[[F,F1],t]] = [[F,F2],t1`*`t] by A36,A40,A37,A39
,A38,XTUPLE_0:1;
end;
A41: C is Category-like
proof
let f,g be Element of the carrier' of C;
consider F19,F29 being Functor of A,B, t9 being natural_transformation
of F19,F29 such that
A42: f = [[F19,F29],t9] and
A43: F19 is_naturally_transformable_to F29 by Def15;
thus [g,f] in dom(the Comp of C) implies dom g=cod f
proof
assume [g,f] in dom(the Comp of C);
then consider F,F1,F2,t,t1 such that
A44: f = [[F,F1],t] and
A45: g = [[F1,F2],t1] and
m.(g,f) = [[F,F2],t1`*`t] by A20;
thus dom g= g`1`1 by A23
.= [F1,F2]`1 by A45
.= [F,F1]`2
.= f`1`2 by A44
.= cod f by A26;
end;
assume
A46: dom g=cod f;
consider F1,F2 being Functor of A,B, t being natural_transformation of
F1,F2 such that
A47: g = [[F1,F2],t] and
A48: F1 is_naturally_transformable_to F2 by Def15;
A49: F1 = [F1,F2]`1
.= g`1`1 by A47
.= c.f by A23,A46
.= f`1`2 by A26
.= [F19,F29]`2 by A42
.= F29;
then reconsider t as natural_transformation of F29,F2;
m.[g,f] = [[F19,F2],t`*`t9] by A29,A47,A48,A42,A43,A49;
hence thesis by A19,A47,A42,A49;
end;
A50: C is transitive
proof
let f,g be Element of the carrier' of C;
consider F19,F29 being Functor of A,B, t9 being natural_transformation
of F19,F29 such that
A51: f = [[F19,F29],t9] and
A52: F19 is_naturally_transformable_to F29 by Def15;
assume dom g=cod f;
then
A53: [g,f] in dom m by A41;
then consider F,F1,F2,t,t1 such that
A54: f = [[F,F1],t] and
A55: g = [[F1,F2],t1] and
A56: m.(g,f) = [[F,F2],t1`*`t] by A20;
A57: m.(g,f) = g(*)f by A53,CAT_1:def 1;
A58: [F,F1] = [F19,F29] by A54,A51,XTUPLE_0:1;
then
A59: F = F19 by XTUPLE_0:1;
A60: F1 = F29 by A58,XTUPLE_0:1;
consider F19,F29 being Functor of A,B, t9 being natural_transformation
of F19,F29 such that
A61: g = [[F19,F29],t9] and
A62: F19 is_naturally_transformable_to F29 by Def15;
A63: [F1,F2] = [F19,F29] by A55,A61,XTUPLE_0:1;
then
A64: F2 = F29 by XTUPLE_0:1;
F1 = F19 by A63,XTUPLE_0:1;
then reconsider x = [[F,F2],t1`*`t] as Element of NatTrans(A,B)
by Th28,A52,A59,A60,A62,A64,Th19;
thus dom(g(*)f) = x`1`1 by A23,A56,A57
.= [F,F2]`1
.= [[F,F1],t]`1`1
.= dom f by A23,A54;
thus cod(g(*)f) = x`1`2 by A26,A56,A57
.= [F,F2]`2
.= [[F1,F2],t1]`1`2
.= cod g by A26,A55;
end;
A65: C is associative
proof
A66: for f,g being Element of the carrier' of C holds [g,f] in dom(
the Comp of C) iff dom g=cod f by A41;
let f,g,h be Element of the carrier' of C;
reconsider f9=f, g9=g, h9=h as Element of NatTrans(A,B);
assume that
A67: dom h = cod g and
A68: dom g = cod f;
[g9,f9] in dom m by A41,A68;
then consider F1,F19,F2 being Functor of A,B, t1 being
natural_transformation of F1,F19, t2 being natural_transformation of F19,F2
such that
A69: f9 = [[F1,F19],t1] and
A70: g9 = [[F19,F2],t2] and
A71: m.(g9,f9) = [[F1,F2],t2`*`t1] by A20;
[h9,g9] in dom m by A41,A67;
then consider F29,F3,F39 being Functor of A,B, t29 being
natural_transformation of F29,F3, t3 being natural_transformation of F3,F39
such that
A72: g9 = [[F29,F3],t29] and
A73: h9 = [[F3,F39],t3] and
m.(h9,g9) = [[F29,F39],t3`*`t29] by A20;
A74: [F29,F3] = [F19,F2] by A70,A72,XTUPLE_0:1;
then
A75: g9 = [[F19,F3],t2] by A70,XTUPLE_0:1;
reconsider t2 as natural_transformation of F19,F3 by A74,XTUPLE_0:1;
A76: F2 = F3 by A74,XTUPLE_0:1;
then
A77: F19 is_naturally_transformable_to F3 by A70,Th28;
A78: F3 is_naturally_transformable_to F39 by A73,Th28;
then
A79: F19 is_naturally_transformable_to F39 by A77,Th19;
A80: F1 is_naturally_transformable_to F19 by A69,Th28;
then
A81: F1 is_naturally_transformable_to F3 by A77,Th19;
A82: h(*)g =(the Comp of C).(h,g) by A66,A67,CAT_1:def 1;
A83: dom(h(*)g) = dom g by A50,A67;
A84: g(*)f =(the Comp of C).(g,f) by A66,A68,CAT_1:def 1;
cod(g(*)f) = cod g by A50,A68;
hence h(*)(g(*)f)
= (the Comp of C).(h,(the Comp of C).(g,f))
by A84,A66,A67,CAT_1:def 1
.= [[F1,F39],t3`*`(t2`*` t1)] by A29,A71,A73,A76,A78,A81
.= [[F1,F39],t3`*`t2`*`t1] by A80,A77,A78,Th22
.= m.[[[F19,F39],t3`*`t2],f9] by A29,A69,A80,A79
.= (the Comp of C).((the Comp of C).(h,g),f) by A29,A73,A75,A77,A78
.= h(*)g(*)f by A83,A82,A66,A68,CAT_1:def 1;
end;
A85: C is reflexive
proof
let b be Element of C;
reconsider F = b as Functor of A,B by CAT_2:def 2;
reconsider s = [[F,F], id F] as Element of NatTrans(A,B) by Def15;
reconsider s as Morphism of C;
A86: dom s = [[F,F], id F]`1`1 by A23
.= F;
cod s = [[F,F], id F]`1`2 by A26 .= F;
then s in Hom(b,b) by A86;
hence Hom(b,b)<>{};
end;
A87: for a be Object of C, F being Functor of A,B st a = F
for m being Morphism of C st m = [[F,F], id F]
for b being Object of C holds
(Hom(a,b) <> {} implies
for f being Morphism of a,b holds f(*)m = f)
& (Hom(b,a) <> {} implies
for f being Morphism of b,a holds m(*)f = f)
proof
let a be Object of C, F be Functor of A,B such that
A88: a = F;
let ii being Morphism of C such that
A89: ii = [[F,F], id F];
let b be Object of C;
reconsider s = [[F,F], id F] as Element of NatTrans(A,B) by Def15;
A90: F in Funct(A,B) by CAT_2:def 2;
then
A91: i.F = [[F,F], id F] by A28;
thus Hom(a,b) <> {} implies
for f being Morphism of a,b holds f(*)ii = f
proof assume
A92: Hom(a,b)<>{};
let f be Morphism of a,b;
reconsider f9 = f as Element of NatTrans(A,B);
A93: dom f = a by A92,CAT_1:5;
consider F1,F2 being Functor of A,B, t being natural_transformation of
F1,F2 such that
A94: f9 = [[F1,F2],t] and
F1 is_naturally_transformable_to F2 by Def15;
A95: F1 = [F1,F2]`1
.= f9`1`1 by A94
.= dom f by A23
.= F by A92,A88,CAT_1:5;
then reconsider t as natural_transformation of F,F2;
P[f9,s,[[F,F2],t`*`id F]] by A94,A95;
then consider F9,F19,F29 being Functor of A,B, t9 being
natural_transformation of F9,F19, t19 being natural_transformation of F19,F29
such that
A96: i.F = [[F9,F19],t9] and
A97: f9 = [[F19,F29],t19] and
A98: m.(f9,i.F) = [[F9,F29],t19`*`t9] by A20,A91,A19;
A99: [F9,F19] = [F,F] by A96,A91,XTUPLE_0:1;
then
A100: F9 = F by XTUPLE_0:1;
A101: F19 = F by A99,XTUPLE_0:1;
A102: F19 is_naturally_transformable_to F29 by A97,Th28;
A103: F29 = [[F19,F29],t19]`1`2
.= [[F1,F2],t]`1`2 by A97,A94
.= F2;
A104: t19 = [[F19,F29],t19]`2
.= [[F1,F2],t]`2 by A97,A94
.= t;
A105: t19`*`(id F19) = t19 by Th20,A102;
cod ii = [[F,F], id F]`1`2 by A89,A26
.= a by A88;
then [f,ii] in dom the Comp of C by A41,A93;
hence f(*)ii = m.(f,ii) by CAT_1:def 1
.= f by A104,A105,A95,A103,A96,A91,A100,A101,A98,A89,A94,XTUPLE_0:1;
end;
assume
A106: Hom(b,a)<>{};
let f be Morphism of b,a;
reconsider f9 = f as Element of NatTrans(A,B);
A107: cod f = a by A106,CAT_1:5;
consider F1,F2 being Functor of A,B, t being natural_transformation of
F1,F2 such that
A108: f9 = [[F1,F2],t] and
F1 is_naturally_transformable_to F2 by Def15;
A109: F2 = [F1,F2]`2
.= f9`1`2 by A108
.= cod f by A26
.= F by A106,A88,CAT_1:5;
then reconsider t as natural_transformation of F1,F;
P[s,f9,[[F1,F],(id F)`*`t]] by A108,A109;
then consider F9,F19,F29 being Functor of A,B, t9 being
natural_transformation of F9,F19, t19 being natural_transformation of F19,F29
such that
A110: f9 = [[F9,F19],t9] and
A111: i.F = [[F19,F29],t19] and
A112: m.(i.F,f9) = [[F9,F29],t19`*`t9] by A20,A91,A19;
A113: t19 = id F by A111,A91,XTUPLE_0:1;
A114: [F19,F29] = [F,F] by A111,A91,XTUPLE_0:1;
then
A115: F19 = F by XTUPLE_0:1;
A116: F9 is_naturally_transformable_to F19 by A110,Th28;
A117: F9 = [[F9,F19],t9]`1`1
.= [[F1,F2],t]`1`1 by A110,A108
.= F1;
A118: t9 = [[F9,F19],t9]`2
.= [[F1,F2],t]`2 by A110,A108
.= t;
A119: (id F19)`*` t9 = t9 by Th20,A116;
dom ii = [[F,F], id F]`1`1 by A89,A23
.= a by A88;
then [ii,f] in dom the Comp of C by A41,A107;
hence ii(*)f
= m.(ii,f) by CAT_1:def 1
.= m.(i.F,f9) by A89,A90,A28
.= [[F9,F29],(id F19)`*`t9] by A113,A115,A114,A112,XTUPLE_0:1
.= f by A108,A118,A119,A114,A109,A117,XTUPLE_0:1;
end;
C is with_identities
proof let a be Element of C;
reconsider F = a as Functor of A,B by CAT_2:def 2;
reconsider s = [[F,F], id F] as Element of NatTrans(A,B) by Def15;
reconsider s as Morphism of C;
A120: dom s = [[F,F], id F]`1`1 by A23 .= F;
cod s = [[F,F], id F]`1`2 by A26 .= F;
then s in Hom(a,a) by A120;
then reconsider s as Morphism of a,a by CAT_1:def 5;
take s;
thus thesis by A87;
end;
then reconsider C as strict Category by A41,A50,A65,A85;
take C;
thus the carrier of C = Funct(A,B) & the carrier' of C = NatTrans(A,B);
thus for f being Morphism of C holds dom f = f`1`1 & cod f = f`1`2 by A23
,A26;
thus for f,g being Morphism of C st dom g = cod f holds [g,f] in dom the
Comp of C
proof
let f,g be Morphism of C;
assume
A121: dom g = cod f;
consider F19,F29 being Functor of A,B, t9 being natural_transformation
of F19,F29 such that
A122: g = [[F19,F29],t9] and
F19 is_naturally_transformable_to F29 by Def15;
consider F1,F2 being Functor of A,B, t being natural_transformation of
F1,F2 such that
A123: f = [[F1,F2],t] and
F1 is_naturally_transformable_to F2 by Def15;
A124: F2 = [[F1,F2],t]`1`2
.= cod f by A26,A123
.= [[F19,F29],t9]`1`1 by A23,A122,A121
.= F19;
then reconsider t9 as natural_transformation of F2,F29;
P[g,f,[[F1,F29],t9`*`t]] by A123,A122,A124;
hence thesis by A19;
end;
thus for f,g being Morphism of C st [g,f] in dom (the Comp of C) ex F,F1,
F2,t,t1 st f = [[F,F1],t] & g = [[F1,F2],t1] & (the Comp of C).[g,f] = [[F,F2],
t1`*`t]
proof
let f,g be Morphism of C;
assume [g,f] in dom (the Comp of C);
then ex F,F1,F2,t,t1 st f = [[F,F1],t] & g = [[F1,F2],t1] & (the Comp
of C).(g,f) = [[F,F2],t1`*`t] by A20;
hence thesis;
end;
let a be Object of C, F such that
A125: a = F;
reconsider m = [[F,F], id F] as Element of NatTrans(A,B) by Def15;
reconsider m as Morphism of C;
A126: dom m = [[F,F], id F]`1`1 by A23 .= F;
cod m = [[F,F], id F]`1`2 by A26 .= F;
then m in Hom(a,a) by A125,A126;
then reconsider m as Morphism of a,a by CAT_1:def 5;
for b being Object of C holds
(Hom(a,b) <> {} implies
for f being Morphism of a,b holds f(*)m = f)
& (Hom(b,a) <> {} implies
for f being Morphism of b,a holds m(*)f = f) by A125,A87;
hence id a = [[F,F],id F] by CAT_1:def 12;
end;
uniqueness
proof
let C1,C2 be strict Category such that
A127: the carrier of C1 = Funct(A,B) and
A128: the carrier' of C1 = NatTrans(A,B) and
A129: for f being Morphism of C1 holds dom f = f`1`1 & cod f = f`1`2 and
A130: for f,g being Morphism of C1 st dom g = cod f holds [g,f] in dom
the Comp of C1 and
A131: for f,g being Morphism of C1 st [g,f] in dom (the Comp of C1) ex
F,F1,F2,t,t1 st f = [[F,F1],t] & g = [[F1,F2],t1] & (the Comp of C1).[g,f] = [[
F,F2],t1`*`t] and
for a being Object of C1, F st F = a holds id a = [[F,F],id F] and
A132: the carrier of C2 = Funct(A,B) and
A133: the carrier' of C2 = NatTrans(A,B) and
A134: for f being Morphism of C2 holds dom f = f`1`1 & cod f = f`1`2 and
A135: for f,g being Morphism of C2 st dom g = cod f holds [g,f] in dom
the Comp of C2 and
A136: for f,g being Morphism of C2 st [g,f] in dom (the Comp of C2) ex
F,F1,F2,t,t1 st f = [[F,F1],t] & g = [[F1,F2],t1] & (the Comp of C2).[g,f] = [[
F,F2],t1`*`t] and
for a being Object of C2, F st F = a holds id a = [[F,F],id F];
A137: the Target of C1 = the Target of C2
proof
thus the carrier' of C1 = the carrier' of C2 by A128,A133;
let a be Morphism of C1;
reconsider b = a as Morphism of C2 by A128,A133;
thus (the Target of C1).a = cod a .= a`1`2 by A129
.= cod b by A134
.= (the Target of C2).a;
end;
A138: now
reconsider S1 = dom the Comp of C1, S2 = dom the Comp of C2 as Subset of
[:the carrier' of C1, the carrier' of C1:] by A128,A133,RELAT_1:def 18;
A139: now
let x be Element of [:the carrier' of C1, the carrier' of C1 :];
A140: x = [x`1,x`2] by MCART_1:21;
then reconsider f1 = x`2, g1 = x`1 as Morphism of C1 by ZFMISC_1:87;
reconsider f2 = x`2, g2 = x`1 as Morphism of C2 by A128,A133,A140,
ZFMISC_1:87;
A141: now
assume [g2,f2] in S2;
then consider F,F1,F2,t,t1 such that
A142: f2 = [[F,F1],t] and
A143: g2 = [[F1,F2],t1] and
(the Comp of C2).[g2,f2] = [[F,F2],t1`*`t] by A136;
dom g1 = g1`1`1 by A129
.= [F1,F2]`1 by A143
.= [F,F1]`2
.= f2`1`2 by A142
.= cod f1 by A129;
hence [g1,f1] in S1 by A130;
end;
now
assume [g1,f1] in S1;
then consider F,F1,F2,t,t1 such that
A144: f1 = [[F,F1],t] and
A145: g1 = [[F1,F2],t1] and
(the Comp of C1).[g1,f1] = [[F,F2],t1`*`t] by A131;
dom g2 = g2`1`1 by A134
.= [F1,F2]`1 by A145
.= [F,F1]`2
.= f1`1`2 by A144
.= cod f2 by A134;
hence [g2,f2] in S2 by A135;
end;
hence x in S1 iff x in S2 by A141,MCART_1:21;
end;
hence
dom the Comp of C1 = dom the Comp of C2 by SUBSET_1:3;
let x be object;
assume
A146: x in dom the Comp of C1;
dom the Comp of C1 c= [:the carrier' of C1, the carrier' of C1:]
by RELAT_1:def 18;
then reconsider f=x`2, g=x`1 as Morphism of C1 by A146,MCART_1:10;
A147: [g,f] = x by A146,MCART_1:21;
then consider F9,F19,F29 being Functor of A,B, t9 being
natural_transformation of F9,F19, t19 being natural_transformation of F19,F29
such that
A148: f = [[F9,F19],t9] and
A149: g = [[F19,F29],t19] and
A150: (the Comp of C2).[g,f] = [[F9,F29],t19`*`t9]
by A128,A133,A136,A139,A146;
consider F,F1,F2,t,t1 such that
A151: f = [[F,F1],t] and
A152: g = [[F1,F2],t1] and
A153: (the Comp of C1).[g,f] = [[F,F2],t1`*`t] by A131,A146,A147;
A154: [F,F1] = [F9,F19] by A151,A148,XTUPLE_0:1;
then
A155: F = F9 by XTUPLE_0:1;
[F1,F2] = [F19,F29] by A152,A149,XTUPLE_0:1;
then
A156: F2 = F29 by XTUPLE_0:1;
A157: F1 = F19 by A154,XTUPLE_0:1;
t = t9 by A151,A148,XTUPLE_0:1;
hence (the Comp of C1).x = (the Comp of C2).x by A147,A152,A153,A149,A150
,A155,A157,A156,XTUPLE_0:1;
end;
the Source of C1 = the Source of C2
proof
thus the carrier' of C1 = the carrier' of C2 by A128,A133;
let a be Morphism of C1;
reconsider b = a as Morphism of C2 by A128,A133;
thus (the Source of C1).a = dom a .= a`1`1 by A129
.= dom b by A134
.= (the Source of C2).a;
end;
hence thesis by A127,A132,A137,A138,FUNCT_1:2;
end;
end;
:: As immediate consequences of the definition we get
theorem Th29:
for f being Morphism of Functors(A,B) st f = [[F,F1],t] holds
dom f = F & cod f = F1
proof
let f be Morphism of Functors(A,B) such that
A1: f = [[F,F1],t];
thus dom f = f`1`1 by Def16
.= [F,F1]`1 by A1
.= F;
thus cod f = f`1`2 by Def16
.= [F,F1]`2 by A1
.= F1;
end;
theorem
for a,b being Object of Functors(A,B), f being Morphism of a,b st Hom(
a,b) <> {} ex F,F1,t st a = F & b = F1 & f = [[F,F1],t]
proof
let a,b be Object of Functors(A,B), f be Morphism of a,b such that
A1: Hom(a,b) <> {};
the carrier' of Functors(A,B) = NatTrans(A,B) by Def16;
then consider
F1,F2 being Functor of A,B, t being natural_transformation of F1,F2
such that
A2: f = [[F1,F2],t] and
F1 is_naturally_transformable_to F2 by Def14;
take F1,F2,t;
thus a = dom f by A1,CAT_1:5
.= F1 by A2,Th29;
thus b = cod f by A1,CAT_1:5
.= F2 by A2,Th29;
thus thesis by A2;
end;
theorem Th31:
for t9 being natural_transformation of F2,F3 for f,g being
Morphism of Functors(A,B) st f = [[F,F1],t] & g = [[F2,F3],t9] holds [g,f] in
dom the Comp of Functors(A,B) iff F1 = F2
proof
let t9 be natural_transformation of F2,F3;
let f,g be Morphism of Functors(A,B);
assume that
A1: f = [[F,F1],t] and
A2: g = [[F2,F3],t9];
thus [g,f] in dom the Comp of Functors(A,B) implies F1 = F2
proof
assume [g,f] in dom the Comp of Functors(A,B);
then consider
F9,F19,F29 being Functor of A,B, t9 being natural_transformation
of F9,F19, t19 being natural_transformation of F19,F29 such that
A3: f = [[F9,F19],t9] and
A4: g = [[F19,F29],t19] and
(the Comp of Functors(A,B)).[g,f] = [[F9,F29],t19`*`t9] by Def16;
thus F1 = [[F,F1],t]`1`2
.= [[F9,F19],t9]`1`2 by A1,A3
.= [F9,F19]`2
.= [[F19,F29],t19]`1`1
.= [F2,F3]`1 by A2,A4
.= F2;
end;
A5: cod f = F1 by A1,Th29;
dom g = F2 by A2,Th29;
hence thesis by A5,Def16;
end;
theorem
for f,g being Morphism of Functors(A,B) st f = [[F,F1],t] & g = [[F1,
F2],t1] holds g(*)f = [[F,F2],t1`*`t]
proof
let f,g be Morphism of Functors(A,B);
assume that
A1: f = [[F,F1],t] and
A2: g = [[F1,F2],t1];
A3: [g,f] in dom the Comp of Functors(A,B) by A1,A2,Th31;
then consider
F9,F19,F29 being Functor of A,B, t9 being natural_transformation of
F9,F19, t19 being natural_transformation of F19,F29 such that
A4: f = [[F9,F19],t9] and
A5: g = [[F19,F29],t19] and
A6: (the Comp of Functors(A,B)).(g,f) = [[F9,F29],t19`*`t9] by Def16;
A7: t1 = t19 by A2,A5,XTUPLE_0:1;
A8: [F9,F19] = [F,F1] by A1,A4,XTUPLE_0:1;
then
A9: F = F9 by XTUPLE_0:1;
[F19,F29] = [F1,F2] by A2,A5,XTUPLE_0:1;
then
A10: F2 = F29 by XTUPLE_0:1;
A11: F1 = F19 by A8,XTUPLE_0:1;
t = t9 by A1,A4,XTUPLE_0:1;
hence thesis by A3,A6,A7,A9,A11,A10,CAT_1:def 1;
end;
begin :: Discrete categories
definition
let C be Category;
attr C is quasi-discrete means
:Def17: for a,b being Element of C st Hom(a,b)<>{} holds a=b;
attr C is pseudo-discrete means
:Def18: for a being Element of C holds Hom(a,a) is trivial;
end;
reserve a,b for Element of C;
Lm6:
C is quasi-discrete implies
the carrier' of C = union the set of all Hom(a,a)
proof assume
A1: C is quasi-discrete;
set A = the set of all Hom(a,b), N = union A,
B = the set of all Hom(a,a), M = union B;
A2: the carrier' of C = N by CAT_1:92;
thus the carrier' of C c= M
proof let e be object;
assume e in the carrier' of C;
then consider X being set such that
A3: e in X and
A4: X in A by A2,TARSKI:def 4;
consider a,b such that
A5: X = Hom(a,b) by A4;
a = b by A1,A3,A5;
then X in B by A5;
hence e in M by A3,TARSKI:def 4;
end;
let e be object;
assume e in M;
then consider X being set such that
A6: e in X and
A7: X in B by TARSKI:def 4;
ex a st X = Hom(a,a) by A7;
hence e in the carrier' of C by A6;
end;
Lm7:
C is pseudo-discrete implies Hom(a,a) = { id a }
proof
assume C is pseudo-discrete;
then Hom(a,a) is trivial non empty;
then consider m being object such that
A1: Hom(a,a) = { m } by ZFMISC_1:131;
id a in Hom(a,a) by CAT_1:27;
hence Hom(a,a) = { id a } by A1,TARSKI:def 1;
end;
definition
let C be Category;
attr C is discrete means
C is quasi-discrete pseudo-discrete;
end;
registration
cluster discrete -> quasi-discrete pseudo-discrete for Category;
coherence;
cluster quasi-discrete pseudo-discrete -> discrete for Category;
coherence;
end;
Lm8:
C is discrete implies
the carrier' of C c= the set of all id a
proof assume
A1: C is discrete;
let e be object;
assume e in the carrier' of C;
then e in union the set of all Hom(a,a) by A1,Lm6;
then consider X being set such that
A2: e in X and
A3: X in the set of all Hom(a,a) by TARSKI:def 4;
consider a such that
A4: X = Hom(a,a) by A3;
X = { id a } by A4,A1,Lm7;
then e = id a by A2,TARSKI:def 1;
hence e in the set of all id b;
end;
registration let o,m be set;
cluster 1Cat(o,m) -> discrete;
coherence
proof
thus 1Cat(o,m) is quasi-discrete
by ZFMISC_1:def 10;
let a be Object of 1Cat(o,m);
thus Hom(a,a) is trivial;
end;
end;
registration
cluster discrete for Category;
existence
proof
take 1Cat({},{});
thus thesis;
end;
end;
registration let C be discrete Category;
let a be Element of C;
cluster Hom(a,a) -> trivial;
coherence by Def18;
end;
theorem Th33:
for A being discrete Category, a being Object of A holds Hom(a,a ) = { id a}
proof
let A be discrete Category, a be Object of A;
now
let g be Morphism of a,a;
id a in Hom(a,a) & g in Hom(a,a) by CAT_1:def 5;
hence g = id a by ZFMISC_1:def 10;
end;
hence thesis by CAT_1:8;
end;
registration let A be discrete Category;
cluster -> discrete for Subcategory of A;
coherence
proof let C be Subcategory of A;
A1: the carrier of C c= the carrier of A by CAT_2:def 4;
thus C is quasi-discrete
proof let a,b be Element of C;
reconsider aa=a, bb=b as Element of A by A1;
assume
A2: Hom(a,b)<>{};
Hom(a,b) c= Hom(aa,bb) by CAT_2:def 4;
then Hom(aa,bb)<>{} by A2;
hence thesis by Def17;
end;
let a be Element of C;
reconsider aa=a as Element of A by A1;
Hom(a,a) c= Hom(aa,aa) by CAT_2:def 4;
hence thesis;
end;
end;
registration let A,B be discrete Category;
cluster [:A,B:] -> discrete;
coherence
proof
thus [:A,B:] is quasi-discrete
proof let a,b be Element of [:A,B:] such that
A1: Hom(a,b)<>{};
consider a1 being Element of A, b1 being Element of B such that
A2: a = [a1,b1] by DOMAIN_1:1;
consider a2 being Element of A, b2 being Element of B such that
A3: b = [a2,b2] by DOMAIN_1:1;
Hom(a,b) = [:Hom(a1,a2),Hom(b1,b2):] by A2,A3,CAT_2:32;
then Hom(a1,a2)<>{} & Hom(b1,b2)<>{} by A1;
then a1 = a2 & b1 = b2 by Def17;
hence a = b by A2,A3;
end;
let a be Element of [:A,B:];
consider a1 being Element of A, b1 being Element of B such that
A4: a = [a1,b1] by DOMAIN_1:1;
Hom(a,a) = [:Hom(a1,a1),Hom(b1,b1):] by A4,CAT_2:32;
hence Hom(a,a) is trivial;
end;
end;
::$CT 3
theorem Th34:
for A being discrete Category, B being Category, F1,F2 being
Functor of B,A st F1 is_transformable_to F2 holds F1 = F2
proof
let A be discrete Category, B be Category, F1,F2 be Functor of B,A;
assume
A1: F1 is_transformable_to F2;
now
let m be Morphism of B;
Hom(F1.dom m,F2.dom m) <> {} by A1;
then
A2: F1.dom m = F2.dom m by Def17;
A3: m in Hom(dom m,cod m);
then Hom(F1.dom m, F1.cod m) <> {} by CAT_1:81;
then F1.dom m = F1.cod m by Def17;
then
A4: Hom(F1.dom m, F1.cod m) = { id(F1.dom m) } by Th33;
Hom(F2.dom m, F2.cod m) <> {} by A3,CAT_1:81;
then F2.dom m = F2.cod m by Def17;
then
A5: Hom(F2.dom m, F2.cod m) = { id(F2.dom m) } by Th33;
F1.m in Hom(F1.dom m, F1.cod m) by A3,CAT_1:81;
then
A6: F1.m = id(F1.dom m) by A4,TARSKI:def 1;
F2.m in Hom(F2.dom m,F2.cod m) by A3,CAT_1:81;
hence F1.m = F2.m by A2,A6,A5,TARSKI:def 1;
end;
hence thesis;
end;
theorem Th35:
for A being discrete Category, B being Category, F being Functor
of B,A, t being transformation of F,F holds t = id F
proof
let A be discrete Category, B be Category, F be Functor of B,A, t be
transformation of F,F;
now
let a be Object of B;
A1: Hom(F.a,F.a) = { id(F.a) } by Th33;
t.a in Hom(F.a, F.a) by CAT_1:def 5;
hence t.a = id(F.a) by A1,TARSKI:def 1
.= (id F).a by Th16;
end;
hence thesis by Th15;
end;
registration let B be Category, A be discrete Category;
cluster Functors(B,A) -> discrete;
coherence
proof
thus Functors(B,A) is quasi-discrete
proof let a,b be Element of Functors(B,A);
assume Hom(a,b)<>{};
then consider f being Morphism of a,b such that
A1: f in Hom(a,b) by CAT_1:91;
f in the carrier' of Functors(B,A);
then f in NatTrans(B,A) by Def16;
then consider F1,F2 being Functor of B,A,
t being natural_transformation of F1,F2 such that
A2: f = [[F1,F2],t] and
A3: F1 is_naturally_transformable_to F2 by Def15;
A4: F1 = dom f by A2,Th29
.= a by A1,CAT_1:1;
F2 = cod f by A2,Th29
.= b by A1,CAT_1:1;
hence a = b by A4,Th34,A3;
end;
let a be Element of Functors(B,A);
A5: now let f be set such that
A6: f in Hom(a,a);
f in the carrier' of Functors(B,A) by A6;
then
f in NatTrans(B,A) by Def16;
then consider F1,F2 being Functor of B,A,
t being natural_transformation of F1,F2 such that
A7: f = [[F1,F2],t] and
A8: F1 is_naturally_transformable_to F2 by Def15;
reconsider ff =f as Morphism of Functors(B,A) by A6;
A9: F1 = dom ff by A7,Th29
.= a by A6,CAT_1:1;
A10: F1 = F2 by Th34,A8;
then t = id F1 by Th35;
hence f = id a by A9,Def16,A7,A10;
end;
let x,y be object;
assume x in Hom(a,a) & y in Hom(a,a);
then x = id a & y = id a by A5;
hence thesis;
end;
end;
registration
let C be Category;
cluster strict discrete for Subcategory of C;
existence
proof
set c = the Object of C;
reconsider A =1Cat(c,id c) as Subcategory of C by Th3;
take A;
thus thesis;
end;
end;
definition
let C;
func IdCat(C) -> strict Subcategory of C means
:Def20:
the carrier of it = the carrier of C &
the carrier' of it = the set of all id a where a is Object of C;
existence
proof
defpred P[Object of C] means not contradiction;
deffunc F(Object of C) = id $1;
defpred Q[Object of C] means F($1) in the carrier' of C;
set M = { F(a) where a is Object of C: P[a]};
set N = { F(a) where a is Object of C: Q[a]};
set N9 = { F(a) where a is Object of C: F(a) in the carrier' of C & P[a]};
defpred R[Object of C] means F($1) in the carrier' of C & P[$1];
set N99 = { F(a) where a is Object of C: R[a]};
set a = the Object of C;
A1: id a in M;
A2: for a being Object of C holds Q[a] iff P[a];
A3: N = M from FRAENKEL:sch 3(A2);
A4: for a being Object of C holds Q[a] iff R[a];
A5: N = N99 from FRAENKEL:sch 3(A4);
N9 c= the carrier' of C from FRAENKEL:sch 17;
then reconsider M as non empty Subset of the carrier' of C by A3,A5,A1;
A6: rng ((the Comp of C)||M) c= M
proof
let x be object;
assume x in rng ((the Comp of C)||M);
then consider y being object such that
A7: y in dom ((the Comp of C)||M) and
A8: x = ((the Comp of C)||M).y by FUNCT_1:def 3;
A9: y in dom (the Comp of C) /\ [:M,M:] by A7,RELAT_1:61;
then
A10: y in dom (the Comp of C) by XBOOLE_0:def 4;
y in [:M,M:] by A9,XBOOLE_0:def 4;
then consider y1,y2 being object such that
A11: y1 in M and
A12: y2 in M and
A13: y = [y1,y2] by ZFMISC_1:84;
consider a1 being Object of C such that
A14: y1 = id a1 by A11;
A15: Hom(a1,a1) <> {};
consider a2 being Object of C such that
A16: y2 = id a2 by A12;
A17: a1 = dom id a1
.= cod id a2 by A13,A14,A16,A10,CAT_1:15
.= a2;
id a1 = (id a1)*(id a1)
.= id a1 (*)(id a2) by A15,A17,CAT_1:def 13
.= (the Comp of C).(id a1, id a2) by A13,A14,A16,A10,CAT_1:def 1
.= x by A8,A9,A13,A14,A16,FUNCT_1:48;
hence thesis;
end;
(the Comp of C)||M is PartFunc of [:M,M qua non empty set:], the
carrier' of C by PARTFUN1:10;
then reconsider
COMP = (the Comp of C)||M as PartFunc of [:M,M qua non empty
set:],M by A6,RELSET_1:6;
A18: the carrier of C c= the carrier of C;
for o being Element of C st o in the carrier of C holds id o in M;
then reconsider
A = CatStr(#the carrier of C,M,((the Source of C)|M), ((the
Target of C)|M),COMP#) as Subcategory of C by Th5,A18;
reconsider A as strict Subcategory of C;
take A;
thus thesis;
end;
uniqueness
proof
let It1,It2 be strict Subcategory of C such that
A19: the carrier of It1 = the carrier of C and
A20: the carrier' of It1 = the set of all id a where a is Object of C and
A21: the carrier of It2 = the carrier of C and
A22: the carrier' of It2 = the set of all id a where a is Object of C;
set M = the carrier' of It1;
A23: the Target of It2 = (the Target of C)|M by A20,A22,Th4;
A24: the Comp of It2 = (the Comp of C)||M by A20,A22,Th4;
A25: the Source of It1 = (the Source of C)|M by Th4;
A26: the Comp of It1 = (the Comp of C)||M by Th4;
the Target of It1 = (the Target of C)|M by Th4;
hence thesis by A19,A20,A21,A22,A25,A23,A26,A24,Th4;
end;
end;
registration
let C;
cluster IdCat C -> discrete;
coherence
proof
A1: the carrier' of IdCat C
= the set of all id a where a is Object of C
by Def20;
thus IdCat C is quasi-discrete
proof let a,b be Element of IdCat C;
assume Hom(a,b)<> {};
then consider m being object such that
A2: m in Hom(a,b) by XBOOLE_0:def 1;
reconsider m as Morphism of IdCat C by A2;
m in the carrier' of IdCat C;
then consider cc being Element of C such that
A3: m = id cc by A1;
reconsider c = cc as Element of IdCat C by Def20;
A4: id c in Hom(a,b) by A3,A2,CAT_2:def 4;
hence a = dom id c by CAT_1:1
.= cod id c
.= b by A4,CAT_1:1;
end;
let c be Element of IdCat C;
let x,y be object;
assume
A5: x in Hom(c,c) & y in Hom(c,c);
then reconsider a=x, b=y as Morphism of IdCat C;
set M = the set of all id o where o is Object of C;
a in the carrier' of IdCat C;
then a in M by Def20;
then consider ox being Element of C such that
A6: a = id ox;
b in the carrier' of IdCat C;
then b in M by Def20;
then consider oy being Element of C such that
A7: b = id oy;
reconsider cc = c as Element of C by Def20;
A8: Hom(c,c) c= Hom(cc,cc) by CAT_2:def 4;
ox = dom id ox
.= cc by A8,A5,A6,CAT_1:1
.= dom id oy by A8,A5,A7,CAT_1:1
.= oy;
hence x = y by A6,A7;
end;
end;
registration
cluster strict discrete for Category;
existence
proof
take IdCat the Category;
thus thesis;
end;
end;
registration let C be strict discrete Category;
reduce IdCat C to C;
reducibility
proof
the carrier' of C c= the set of all id a where a is Object of C
by Lm8;
then
A1: the carrier' of C c= the carrier' of IdCat(C) by Def20;
the carrier' of IdCat(C) c= the carrier' of C by CAT_2:7;
then the carrier' of IdCat(C) = the carrier' of C by A1;
hence thesis by Def20,Th6;
end;
end;
::$CT 4
theorem
IdCat([:A,B:]) = [:IdCat(A), IdCat(B):]
proof
now
reconsider OA = the carrier of IdCat A as non empty Subset of the carrier
of A by CAT_2:def 4;
set AB = the set of all id c where c is Object of [:A,B:];
set MA = the set of all id a where a is Object of A;
set MB = the set of all id b where b is Object of B;
A1: AB = [:MA,MB:]
proof
thus AB c= [:MA,MB:]
proof
let x be object;
assume x in AB;
then consider c being Object of [:A,B:] such that
A2: x = id c;
consider c1 being Object of A, c2 being Object of B such that
A3: c = [c1,c2] by DOMAIN_1:1;
A4: id c2 in MB;
A5: id c1 in MA;
id c = [id c1, id c2] by A3,CAT_2:31;
hence thesis by A2,A5,A4,ZFMISC_1:87;
end;
let x be object;
assume x in [:MA,MB:];
then consider x1,x2 being object such that
A6: x1 in MA and
A7: x2 in MB and
A8: x = [x1,x2] by ZFMISC_1:84;
consider a being Object of A such that
A9: x1 = id a by A6;
consider b being Object of B such that
A10: x2 = id b by A7;
id [a,b] = [id a, id b] by CAT_2:31;
hence thesis by A8,A9,A10;
end;
reconsider OB = the carrier of IdCat B as non empty Subset of the carrier
of B by CAT_2:def 4;
reconsider MB = the carrier' of IdCat B as non empty Subset of the
carrier' of B by CAT_2:7;
reconsider MA = the carrier' of IdCat A as non empty Subset of the
carrier' of A by CAT_2:7;
A11: the carrier of IdCat B = the carrier of B by Def20;
the carrier of IdCat A = the carrier of A by Def20;
hence
[:the carrier of IdCat A,the carrier of IdCat B:] = the carrier
of IdCat [:A,B:] by A11,Def20;
A12: the Target of IdCat B = (the Target of B)|the carrier' of IdCat B by Th4;
A13: the Source of IdCat B = (the Source of B)|the carrier' of IdCat B by Th4;
A14: the carrier' of IdCat B = the set of all id b where b is Object of B
by Def20;
the carrier' of IdCat A = the set of all id a where a is Object of A
by Def20;
hence
A15: the carrier' of IdCat [:A,B:] = [:the carrier' of IdCat A,the
carrier' of IdCat B:] by A1,A14,Def20;
the Source of IdCat A = (the Source of A)|the carrier' of IdCat A by Th4;
hence [:the Source of IdCat A,the Source of IdCat B:] = [:the Source of A,
the Source of B:]|[:MA,MB:] by A13,FUNCT_3:81
.= the Source of IdCat [:A,B:] by A15,Th4;
the Target of IdCat A = (the Target of A)|the carrier' of IdCat A by Th4;
hence [:the Target of IdCat A,the Target of IdCat B:] = [:the Target of A,
the Target of B:]|[:MA,MB:] by A12,FUNCT_3:81
.= the Target of IdCat [:A,B:] by A15,Th4;
A16: the Comp of IdCat A = (the Comp of A)||MA by Th4;
the Comp of IdCat B = (the Comp of B)||MB by Th4;
hence |:the Comp of IdCat A,the Comp of IdCat B:|
= |:the Comp of A,the Comp of B:| ||[:MA,MB:] by A16,FUNCT_4:126
.= the Comp of IdCat [:A,B:] by A15,Th4;
end;
hence thesis;
end;