:: Categorial Categories and Slice Categories
:: by Grzegorz Bancerek
::
:: Received October 24, 1994
:: Copyright (c) 1994-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, SUBSET_1, ZFMISC_1, MCART_1, CAT_1, STRUCT_0, RELAT_1,
GRAPH_1, FUNCT_1, CARD_1, TARSKI, PARTFUN1, CAT_2, REALSET1, GROUP_6,
SETFAM_1, GRCAT_1, FUNCT_3, CAT_5, MONOID_0, RELAT_2, BINOP_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, SETFAM_1, MCART_1,
DOMAIN_1, RELAT_1, REALSET1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2,
ORDINAL1, NUMBERS, BINOP_1, STRUCT_0, GRAPH_1, CAT_1, CAT_2;
constructors SETFAM_1, PARTFUN1, REALSET1, NATTRA_1, FUNCOP_1, RELSET_1,
XTUPLE_0, NUMBERS;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, REALSET1, CAT_1, CAT_2,
STRUCT_0, RELAT_1, XTUPLE_0;
requirements SUBSET, BOOLE;
definitions TARSKI, FUNCT_1, CAT_1, CAT_2, XBOOLE_0;
equalities CAT_1, CAT_2, REALSET1, BINOP_1, GRAPH_1;
expansions TARSKI, FUNCT_1, CAT_1, XBOOLE_0;
theorems TARSKI, ZFMISC_1, SETFAM_1, MCART_1, FUNCT_1, FUNCT_2, GRFUNC_1,
PARTFUN1, CAT_1, CAT_2, NATTRA_1, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1,
BINOP_1, XTUPLE_0;
schemes FUNCT_1, FUNCT_2, BINOP_1, XFAMILY;
begin :: Categories with Triple-like Morphisms
theorem Th1:
for C being Category,
D being non empty non void CatStr
st the CatStr of C = the CatStr of D holds
D is Category-like transitive associative reflexive with_identities
proof
let C be Category,
D be non empty non void CatStr such that
A1: the CatStr of C = the CatStr of D;
thus
A2: for f,g being Morphism of D
holds [g,f] in dom(the Comp of D) iff dom g=cod f
proof let f,g be Morphism of D;
reconsider ff=f, gg=g as Morphism of C by A1;
A3: [gg,ff] in dom(the Comp of D) iff dom gg=cod ff by A1,CAT_1:def 6;
thus [g,f] in dom(the Comp of D) implies dom g=cod f
proof
assume
A4: [g,f] in dom the Comp of D;
thus dom g = dom gg by A1
.= cod ff by A4,A1,CAT_1:def 6
.= cod f by A1;
end;
thus thesis by A1,A3;
end;
thus
A5: for f,g being Morphism of D
st dom g=cod f holds dom(g(*)f) = dom f & cod(g(*)f) = cod g
proof let f,g be Morphism of D;
reconsider ff=f, gg=g as Morphism of C by A1;
assume
A6: dom g = cod f;
A7: dom gg = cod ff by A1,A6;
then [gg,ff] in dom(the Comp of C) by CAT_1:def 6;
then
A8: (the Comp of C).(gg,ff) = gg(*)ff by CAT_1:def 1;
dom(gg(*)ff) = dom ff & cod(gg(*)ff) = cod gg by A7,CAT_1:def 7;
hence thesis by A1,A8,A6,A2,CAT_1:def 1;
end;
A9: for f,g being Morphism of D st cod g = dom f
for ff,gg being Morphism of C st ff=f & gg=g
holds f(*)g = ff(*)gg
proof let f,g be Morphism of D such that
A10: cod g = dom f;
let ff,gg be Morphism of C such that
A11: ff=f & gg=g;
A12: cod gg = dom ff by A10,A11,A1;
thus f(*)g
= (the Comp of D).(f,g) by A10,A2,CAT_1:def 1
.= (the Comp of C).(ff,gg) by A1,A11
.= ff(*)gg by A12,CAT_1:16;
end;
thus for f,g,h being Morphism of D
st dom h = cod g & dom g = cod f
holds h(*)(g(*)f) = (h(*)g)(*)f
proof let f,g,h being Morphism of D;
reconsider ff=f, gg=g, hh=h as Morphism of C by A1;
assume that
A13: dom h = cod g and
A14: dom g = cod f;
A15: dom hh = cod gg & dom gg = cod ff by A13,A14,A1;
A16: g(*)f = gg(*)ff by A14,A9;
A17: h(*)g = hh(*)gg by A13,A9;
A18: dom(h(*)g) = dom g by A13,A5;
cod(g(*)f) = cod g by A14,A5;
hence h(*)(g(*)f)
= hh(*)(gg(*)ff) by A9,A16,A13
.= hh(*)gg(*)ff by A15,CAT_1:def 8
.= (h(*)g)(*)f by A14,A9,A17,A18;
end;
thus
D is reflexive
proof
let b be Element of D;
reconsider bb = b as Element of C by A1;
reconsider ii = id bb as Morphism of D by A1;
A19: cod ii = cod id bb by A1
.= b;
dom ii = dom id bb by A1
.= b;
then id bb in Hom(b,b) by A19;
hence Hom(b,b)<>{};
end;
let a be Element of D;
reconsider aa = a as Element of C by A1;
reconsider ii = id aa as Morphism of D by A1;
A20: cod ii = cod id aa by A1
.= a;
dom ii = dom id aa by A1
.= a;
then reconsider ii as Morphism of a,a by A20,CAT_1:4;
take ii;
let b be Element of D;
reconsider bb = b as Element of C by A1;
thus Hom(a,b)<>{} implies for g being Morphism of a,b holds g(*)ii = g
proof assume
A21: Hom(a,b)<>{};
let g be Morphism of a,b;
reconsider gg = g as Morphism of C by A1;
A22: cod gg = cod g by A1
.= bb by A21,CAT_1:5;
A23: cod id aa = aa;
A24: dom gg = dom g by A1
.= aa by A21,CAT_1:5;
then
gg in Hom(aa,bb) by A22;
then reconsider gg as Morphism of aa,bb by CAT_1:def 5;
A25: dom g = dom gg by A1
.= a by A24;
cod ii = cod id aa by A1
.= a;
hence g(*)ii = (the Comp of D).(g,ii) by A25,A2,CAT_1:def 1
.= (the Comp of C).(gg,id aa) by A1
.= gg(*)id aa by A23,A24,CAT_1:16
.= g by A24,CAT_1:22;
end;
assume
A26: Hom(b,a)<>{};
let g be Morphism of b,a;
reconsider gg = g as Morphism of C by A1;
A27: dom gg = dom g by A1
.= bb by A26,CAT_1:5;
A28: dom id aa = aa;
A29: cod gg = cod g by A1
.= aa by A26,CAT_1:5;
then
gg in Hom(bb,aa) by A27;
then reconsider gg as Morphism of bb,aa by CAT_1:def 5;
A30: cod g = cod gg by A1
.= a by A29;
dom ii = dom id aa by A1
.= a;
hence ii(*)g = (the Comp of D).(ii,g) by A30,A2,CAT_1:def 1
.= (the Comp of C).(id aa,gg) by A1
.= (id aa)(*)gg by A28,A29,CAT_1:16
.= g by A29,CAT_1:21;
end;
Lm1:
for C,D being Category
st the CatStr of C = the CatStr of D holds
for c being Element of C, d being Element of D st c = d
holds id c = id d
proof let C,D be Category such that
A1: the CatStr of C = the CatStr of D;
let c be Element of C, d be Element of D such that
A2: c = d;
reconsider ii = id c as Morphism of D by A1;
A3: cod ii = cod id c by A1 .= d by A2;
A4: dom ii = dom id c by A1 .= d by A2;
then reconsider ii as Morphism of d,d by A3,CAT_1:4;
for b being Object of D holds
(Hom(d,b) <> {} implies
for f being Morphism of d,b holds f(*)ii = f)
& (Hom(b,d) <> {} implies
for f being Morphism of b,d holds ii(*)f = f)
proof let b be Object of D;
reconsider bb = b as Element of C by A1;
thus Hom(d,b) <> {} implies
for f being Morphism of d,b holds f(*)ii = f
proof assume
A5: Hom(d,b) <> {};
let f be Morphism of d,b;
reconsider ff=f as Morphism of C by A1;
A6: dom ff = dom f by A1 .= c by A2,A5,CAT_1:5;
A7: cod id c = c .= dom ff by A6;
cod ii = d by A3 .= dom f by A5,CAT_1:5;
hence f(*)ii = (the Comp of D).(f,ii) by CAT_1:16
.= (the Comp of C).(ff,id c) by A1
.= ff(*)id c by A7,CAT_1:16
.= f by A6,CAT_1:22;
end;
assume
A8: Hom(b,d) <> {};
let f be Morphism of b,d;
reconsider ff=f as Morphism of C by A1;
A9: cod ff = cod f by A1 .= c by A2,A8,CAT_1:5;
A10: dom id c = c .= cod ff by A9;
dom ii = d by A4 .= cod f by A8,CAT_1:5;
hence ii(*)f = (the Comp of D).(ii,f) by CAT_1:16
.= (the Comp of C).(id c,ff) by A1
.= (id c)(*)ff by A10,CAT_1:16
.= f by A9,CAT_1:21;
end;
hence id c = id d by CAT_1:def 12;
end;
definition
let IT be non void non empty CatStr;
attr IT is with_triple-like_morphisms means
:Def1:
for f being Morphism of IT ex x being set st f = [[dom f, cod f], x];
end;
registration
cluster with_triple-like_morphisms for strict Category;
existence
proof
take C = 1Cat(0, [[0,0], 1]);
let f be Morphism of C;
take 1;
dom f = 0 by TARSKI:def 1;
hence thesis by TARSKI:def 1;
end;
end;
theorem Th2:
for C being with_triple-like_morphisms non void non empty CatStr,
f being Morphism of C holds
dom f = f`11 & cod f = f`12 & f = [[dom f, cod f], f`2]
proof
let C be with_triple-like_morphisms non void non empty CatStr;
let f be Morphism of C;
ex x being set st ( f = [[dom f, cod f], x]) by Def1;
hence thesis by MCART_1:85;
end;
definition
let C be with_triple-like_morphisms non void non empty CatStr;
let f be Morphism of C;
redefine func f`11 -> Object of C; :: redefines `11 (MCART_1, definition)
coherence
proof f`11 = dom f by Th2;
hence thesis;
end;
redefine func f`12 -> Object of C; :: redefines `12 (MCART_1, definition)
coherence
proof f`12 = cod f by Th2;
hence thesis;
end;
end;
scheme CatEx { A, B() -> non empty set, P[set, set, set],
F(object,object) -> set }:
ex C being with_triple-like_morphisms strict Category st
the carrier of C = A() &
(for a,b being Element of A(), f being Element of B() st
P[a,b,f] holds [[a,b],f] is Morphism of C) &
(for m being Morphism of C
ex a,b being Element of A(), f being Element of B() st
m = [[a,b],f] & P[a,b,f]) &
for m1,m2 being (Morphism of C), a1,a2,a3 being Element of A(),
f1,f2 being Element of B() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2]
holds m2(*)m1 = [[a1,a3], F(f2,f1)]
provided
A1: for a,b,c being Element of A(), f,g being Element of B() st
P[a,b,f] & P[b,c,g] holds F(g,f) in B() & P[a,c,F(g,f)] and
A2: for a being Element of A()
ex f being Element of B() st P[a,a,f] &
for b being Element of A(), g being Element of B() holds
(P[a,b,g] implies F(g,f) = g) & (P[b,a,g] implies F(f,g) = g) and
A3: for a,b,c,d being Element of A(), f,g,h being Element of B() st
P[a,b,f] & P[b,c,g] & P[c,d,h] holds F(h, F(g,f)) = F(F(h,g), f)
proof
set M = {[[a,b],f] where a is Element of A(), b is Element of A(),
f is Element of B(): P[a,b,f]};
set a0 = the Element of A();
consider f0 being Element of B() such that
A4: P[a0,a0,f0]
and for b being Element of A(), g being Element of B() holds (P[a0,b,g]
implies F(g,f0) = g) & (P[b,a0,g] implies F(f0,g) = g)
by A2;
A5: [[a0,a0],f0] in M by A4;
M c= [:[:A(),A():],B():]
proof
let x be object;
assume x in M;
then ex a, b being Element of A(), f being Element of B() st
x = [[a,b],f] & P[a,b,f];
hence thesis;
end;
then reconsider M as non empty Subset of [:[:A(),A():],B():] by A5;
A6: now
let m be Element of M;
m in M;
then consider a,b being Element of A(), f being Element of B() such that
A7: m = [[a,b],f] and
A8: P[a,b,f];
A9: m`11 = a by A7,MCART_1:85;
m`12 = b by A7,MCART_1:85;
hence m = [[m`11,m`12],m`2] & P[m`11,m`12,m`2] by A7,A8,A9;
end;
deffunc f(Element of M) = $1`11;
consider DM being Function of M, A() such that
A10: for m being Element of M holds DM.m = f(m) from FUNCT_2:sch 4;
deffunc g(Element of M) = $1`12;
consider CM being Function of M, A() such that
A11: for m being Element of M holds CM.m = g(m) from FUNCT_2:sch 4;
deffunc f(object,object) = [[$2`11,$1`12],F($1`2,$2`2)];
defpred P[object,object] means $1`11 = $2`12 & $1 in M & $2 in M;
A12: now
let x,y be object;
assume
A13: P[x,y];
then consider ax, bx being Element of A(), fx being Element of B() such
that
A14: x = [[ax,bx],fx] and
A15: P[ax,bx,fx];
consider ay, b2 being Element of A(), fy being Element of B() such that
A16: y = [[ay,b2],fy] and
A17: P[ay,b2,fy] by A13;
A18: x`11 = ax by A14,MCART_1:85;
A19: x`12 = bx by A14,MCART_1:85;
A20: y`11 = ay by A16,MCART_1:85;
A21: y`12 = b2 by A16,MCART_1:85;
A22: x`2 = fx by A14;
A23: y`2 = fy by A16;
A24: F(fx,fy) in B() by A1,A13,A15,A17,A18,A21;
P[ay,bx,F(fx,fy)] by A1,A13,A15,A17,A18,A21;
hence f(x,y) in M by A19,A20,A22,A23,A24;
end;
consider CC being PartFunc of [:M,M:], M such that
A25: for x,y being object holds [x,y] in dom CC iff x in M & y in M & P[x,y]
and
A26: for x,y being object st [x,y] in dom CC holds
CC.(x,y) = f(x,y) from BINOP_1:sch 6(A12);
defpred II[Element of A(), set] means ex f being Element of B() st
$2 = [[$1,$1], f] & P[$1,$1,f] &
for b being Element of A(), g being Element of B() holds
(P[$1,b,g] implies F(g,f) = g) & (P[b,$1,g] implies F(f,g) = g);
A27: now
let a be Element of A();
consider f being Element of B() such that
A28: P[a,a,f] and
A29: for b being Element of A(), g being Element of B() holds (P[a,b,g]
implies F(g,f) = g) & (P[b,a,g] implies F(f,g) = g)
by A2;
[[a,a],f] in M by A28;
then reconsider y = [[a,a],f] as Element of M;
take y;
thus II[a,y] by A28,A29;
end;
consider I being Function of A(), M such that
A30: for o being Element of A() holds II[o,I.o] from FUNCT_2:sch 3(A27);
set C = CatStr (# A(),M,DM,CM,CC #);
A31: C is Category-like
proof
thus
now let f,g be Morphism of C;
A32: [g,f] in dom CC iff g in M & f in M & g`11 = f`12 & g in M & f in M
by A25;
DM.g = g`11 by A10;
hence [g,f] in dom(the Comp of C) iff dom g=cod f by A11,A32;
end;
end;
A33: for f,g be Morphism of C
holds [g,f] in dom(the Comp of C) iff dom g=cod f by A31;
A34: C is transitive
proof
let f,g be Morphism of C;
A35: (the Source of C).f = f`11 by A10;
A36: (the Source of C).g = g`11 by A10;
A37: (the Target of C).f = f`12 by A11;
A38: (the Target of C).g = g`12 by A11;
assume
A39: dom g=cod f;
then
A40: CC.(g,f) = [[f`11,g`12],F(g`2,f`2)] by A26,A25,A36,A37;
A41: (CC.[g,f])`11 = f`11 by A40,MCART_1:85;
A42: (the Comp of C).(g,f) = g(*)f by A39,A25,A36,A37,CAT_1:def 1;
(CC.[g,f])`12 = g`12 by A40,MCART_1:85;
hence dom(g(*)f) = dom f & cod(g(*)f) = cod g
by A10,A11,A35,A38,A41,A42;
end;
A43: C is associative
proof
let f,g,h be Morphism of C;
A44: (the Source of C).g = g`11 by A10;
A45: (the Source of C).h = h`11 by A10;
A46: (the Target of C).f = f`12 by A11;
A47: (the Target of C).g = g`12 by A11;
assume that
A48: dom h = cod g and
A49: dom g = cod f;
A50: [g,f] in dom CC by A25,A44,A46,A49;
A51: [h,g] in dom CC by A25,A45,A47,A48;
A52: CC.[g,f] in rng CC by A50,FUNCT_1:def 3;
CC.[h,g] in rng CC by A51,FUNCT_1:def 3;
then reconsider gf = CC.(g,f), hg = CC.(h,g) as Element of M by A52;
A53: gf = [[f`11,g`12],F(g`2,f`2)] by A26,A25,A44,A46,A49;
A54: hg = [[g`11,h`12],F(h`2,g`2)] by A26,A25,A45,A47,A48;
A55: DM.gf = gf`11 by A10;
A56: DM.hg = hg`11 by A10;
A57: CM.gf = gf`12 by A11;
A58: CM.hg = hg`12 by A11;
A59: DM.gf = f`11 by A53,A55,MCART_1:85;
A60: CM.gf = g`12 by A53,A57,MCART_1:85;
A61: CM.hg = h`12 by A54,A58,MCART_1:85;
A62: [h,gf] in dom CC by A25,A45,A11,A48,A57,A60;
A63: [hg,f] in dom CC by A25,A44,A46,A49,A56,A54,MCART_1:85;
reconsider f9 = f, g9 = g, h9 = h as Element of M;
A64: P[f9`11,f9`12,f9`2] by A6;
A65: P[g9`11,g9`12,g9`2] by A6;
A66: P[h9`11,h9`12,h9`2] by A6;
A67: (the Comp of C).(h,g) = h(*)g by A33,A48,CAT_1:def 1;
A68: dom(h(*)g) = dom g by A34,A48;
A69: (the Comp of C).(g,f) = g(*)f by A33,A49,CAT_1:def 1;
cod(g(*)f) = cod g by A34,A49;
hence h(*)(g(*)f)
= (the Comp of C).(h,(the Comp of C).(g,f)) by A69,A33,A48,CAT_1:def 1
.= [[f`11,h`12], F(h`2,gf`2)] by A26,A55,A59,A62
.= [[f`11,h`12], F(h9`2,F(g9`2,f9`2))] by A53
.= [[f`11,h`12], F(F(h9`2,g9`2),f9`2)] by A3,A44,A45,A46,A47,A48,A49
,A64,A65,A66
.= [[f`11,h`12], F(hg`2,f`2)] by A54
.= (the Comp of C).((the Comp of C).(h,g),f) by A26,A58,A61,A63
.= h(*)g(*)f by A67,A33,A49,A68,CAT_1:def 1;
end;
A70: C is reflexive
proof
let b be Object of C;
consider f being Element of B() such that
A71: I.b = [[b,b], f] and P[b,b,f] and
for c being Element of A(), g being Element of B()
holds (P[b,c,g] implies F(g,f) = g) & (P[c,b,g] implies F(f,g) = g)
by A30;
reconsider bb = b as Element of A();
reconsider Ib = I.bb as Element of M;
reconsider ii = I.bb as Morphism of C;
A72: cod ii = (I.b)`12 by A11
.= b by A71,MCART_1:85;
dom ii = (I.b)`11 by A10
.= b by A71,MCART_1:85;
then I.b in Hom(b,b) by A72;
hence Hom(b,b)<>{};
end;
C is with_identities
proof
let a be Object of C;
consider f being Element of B() such that
A73: I.a = [[a,a], f] and P[a,a,f] and
A74: for c being Element of A(), g being Element of B()
holds (P[a,c,g] implies F(g,f) = g) & (P[c,a,g] implies F(f,g) = g)
by A30;
reconsider aa = a as Element of A();
reconsider Ia = I.aa as Element of M;
reconsider ii = I.aa as Morphism of C;
A75: cod ii = (I.a)`12 by A11
.= a by A73,MCART_1:85;
dom ii = (I.a)`11 by A10
.= a by A73,MCART_1:85;
then reconsider ii as Morphism of a,a by A75,CAT_1:4;
take ii;
let b be Element of C;
thus Hom(a,b)<>{} implies for g being Morphism of a,b holds g(*)ii = g
proof assume
A76: Hom(a,b)<>{};
let g be Morphism of a,b;
reconsider bb = b as Element of A();
g in M;
then consider a1,b1 being Element of A(), f1 being Element of B()
such that
A77: g =[[a1,b1],f1] and
A78: P[a1,b1,f1];
A79: a = dom g by A76,CAT_1:5
.= DM.g
.= [[a1,b1],f1]`11 by A77,A10
.= a1 by MCART_1:85;
then
A80: F(f1,f) = f1 by A74,A78;
A81: [[a,a], f]`11 = a1 by A79,MCART_1:85;
A82: [[a1,b1],f1]`12 = b1 by MCART_1:85;
g`11 = [[a1,b1],f1]`11 by A77
.= a by A79,MCART_1:85
.= [[a,a], f]`12 by MCART_1:85
.= ii`12 by A73;
then
A83: [g,ii] in dom CC by A25;
hence g(*)ii = (the Comp of C).(g,ii) by CAT_1:def 1
.= CC.(g,ii)
.= [[ii`11,g`12],F(g`2,ii`2)] by A26,A83
.= [[a1,b1],f1] by A80,A81,A82,A77,A73
.= g by A77;
end;
thus Hom(b,a)<>{} implies for f being Morphism of b,a holds ii(*)f = f
proof assume
A84: Hom(b,a)<>{};
let g be Morphism of b,a;
reconsider bb = b as Element of A();
g in M;
then consider b1,a1 being Element of A(), f1 being Element of B()
such that
A85: g =[[b1,a1],f1] and
A86: P[b1,a1,f1];
A87: a = cod g by A84,CAT_1:5
.= CM.g
.= [[b1,a1],f1]`12 by A85,A11
.= a1 by MCART_1:85;
then
A88: F(f,f1) = f1 by A74,A86;
A89: [[a,a], f]`12 = a1 by A87,MCART_1:85;
A90: [[b1,a1],f1]`11 = b1 by MCART_1:85;
g`12 = [[b1,a1],f1]`12 by A85
.= a by A87,MCART_1:85
.= [[a,a], f]`11 by MCART_1:85
.= ii`11 by A73;
then
A91: [ii,g] in dom CC by A25;
hence ii(*)g = (the Comp of C).(ii,g) by CAT_1:def 1
.= CC.(ii,g)
.= [[g`11,ii`12],F(ii`2,g`2)] by A26,A91
.= [[b1,a1],f1] by A88,A89,A90,A85,A73
.= g by A85;
end;
end;
then reconsider C as strict Category by A31,A34,A43,A70;
C is with_triple-like_morphisms
proof
let f be Morphism of C;
f in M;
then consider a, b being Element of A(), g being Element of B() such that
A92: f = [[a,b],g] and P[a,b,g];
take g;
A93: dom f = f`11 by A10
.= a by A92,MCART_1:85;
cod f = f`12 by A11
.= b by A92,MCART_1:85;
hence thesis by A92,A93;
end;
then reconsider C as with_triple-like_morphisms strict Category;
take C;
thus the carrier of C = A();
hereby
let a,b be Element of A(), f be Element of B();
assume P[a,b,f];
then [[a,b],f] in M;
hence [[a,b],f] is Morphism of C;
end;
hereby
let m be Morphism of C;
m in M;
hence ex a,b being Element of A(), f being Element of B() st
m = [[a,b],f] & P[a,b,f];
end;
let m1,m2 be (Morphism of C), a1,a2,a3 be Element of A(),
f1,f2 be Element of B();
assume that
A94: m1 = [[a1,a2],f1] and
A95: m2 = [[a2,a3],f2];
A96: m1`11 = a1 by A94,MCART_1:85;
A97: m1`12 = a2 by A94,MCART_1:85;
A98: m2`11 = a2 by A95,MCART_1:85;
A99: m2`12 = a3 by A95,MCART_1:85;
thus m2(*)m1 = CC.(m2,m1) by A25,A97,A98,CAT_1:def 1
.= [[a1,a3],F(m2`2,m1`2)] by A26,A96,A99,A25,A97,A98
.= [[a1,a3],F(f2,m1`2)] by A95
.= [[a1,a3], F(f2,f1)] by A94;
end;
scheme CatUniq
{ A, B() -> non empty set, P[set, set, set], F(set,set) -> set }:
for C1, C2 being strict with_triple-like_morphisms Category st
the carrier of C1 = A() &
(for a,b being Element of A(), f being Element of B() st
P[a,b,f] holds [[a,b],f] is Morphism of C1) & (for m being Morphism of C1
ex a,b being Element of A(), f being Element of B() st
m = [[a,b],f] & P[a,b,f]) &
(for m1,m2 being (Morphism of C1), a1,a2,a3 being Element of A(),
f1,f2 being Element of B() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2]
holds m2(*)m1 = [[a1,a3], F(f2,f1)]) & the carrier of C2 = A() &
(for a,b being Element of A(), f being Element of B() st
P[a,b,f] holds [[a,b],f] is Morphism of C2) & (for m being Morphism of C2
ex a,b being Element of A(), f being Element of B() st
m = [[a,b],f] & P[a,b,f]) &
for m1,m2 being (Morphism of C2), a1,a2,a3 being Element of A(),
f1,f2 being Element of B() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2]
holds m2(*)m1 = [[a1,a3], F(f2,f1)] holds C1 = C2
provided
for a being Element of A() ex f being Element of B() st P[a,a,f] &
for b being Element of A(), g being Element of B() holds
(P[a,b,g] implies F(g,f) = g) & (P[b,a,g] implies F(f,g) = g)
proof
let C1, C2 be strict with_triple-like_morphisms Category such that
A1: the carrier of C1 = A() and
A2: for a,b being Element of A(), f being Element of B() st
P[a,b,f] holds [[a,b],f] is Morphism of C1 and
A3: for m being Morphism of C1
ex a,b being Element of A(), f being Element of B() st
m = [[a,b],f] & P[a,b,f] and
A4: for m1,m2 being (Morphism of C1), a1,a2,a3 being Element of A(),
f1,f2 being Element of B() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2]
holds m2(*)m1 = [[a1,a3], F(f2,f1)] and
A5: the carrier of C2 = A() and
A6: for a,b being Element of A(), f being Element of B() st
P[a,b,f] holds [[a,b],f] is Morphism of C2 and
A7: for m being Morphism of C2
ex a,b being Element of A(), f being Element of B() st
m = [[a,b],f] & P[a,b,f] and
A8: for m1,m2 being (Morphism of C2), a1,a2,a3 being Element of A(),
f1,f2 being Element of B() st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2]
holds m2(*)m1 = [[a1,a3], F(f2,f1)];
A9: the carrier' of C1 = the carrier' of C2
proof
hereby
let x be object;
assume x in the carrier' of C1;
then ex a,b being Element of A(), f being Element of B() st
x = [[a,b],f] & P[a,b,f] by A3;
then x is Morphism of C2 by A6;
hence x in the carrier' of C2;
end;
let x be object;
assume x in the carrier' of C2;
then ex a,b being Element of A(), f being Element of B() st
x = [[a,b],f] & P[a,b,f] by A7;
then x is Morphism of C1 by A2;
hence thesis;
end;
A10: dom the Source of C1 = the carrier' of C1 by FUNCT_2:def 1;
A11: dom the Source of C2 = the carrier' of C2 by FUNCT_2:def 1;
A12: dom the Target of C1 = the carrier' of C1 by FUNCT_2:def 1;
A13: dom the Target of C2 = the carrier' of C2 by FUNCT_2:def 1;
A14: now
let x be object;
assume x in the carrier' of C1;
then reconsider m1 = x as Morphism of C1;
reconsider m2 = m1 as Morphism of C2 by A9;
thus (the Source of C1).x = dom m1 .= m1`11 by Th2
.= dom m2 by Th2
.= (the Source of C2).x;
end;
then
A15: the Source of C1 = the Source of C2 by A9,A10,A11;
now
let x be object;
assume x in the carrier' of C1;
then reconsider m1 = x as Morphism of C1;
reconsider m2 = m1 as Morphism of C2 by A9;
thus (the Target of C1).x = cod m1 .= m1`12 by Th2
.= cod m2 by Th2
.= (the Target of C2).x;
end;
then
A16: the Target of C1 = the Target of C2 by A9,A12,A13;
A17: dom the Comp of C1 = dom the Comp of C2
proof
hereby
let x be object;
assume
A18: x in dom the Comp of C1;
then reconsider xx = x as
Element of [:the carrier' of C1, the carrier' of C1:];
reconsider y = xx as
Element of [:the carrier' of C2, the carrier' of C2:] by A9;
A19: y = [xx`1,xx`2] by MCART_1:21;
then dom(xx`1) = cod(xx`2) by A18,CAT_1:def 6;
then dom(y`1) = cod(y`2) by A14,A16;
hence x in dom the Comp of C2 by A19,CAT_1:def 6;
end;
let x be object;
assume
A20: x in dom the Comp of C2;
then reconsider xx = x as
Element of [:the carrier' of C1, the carrier' of C1:] by A9;
reconsider y = xx as
Element of [:the carrier' of C2, the carrier' of C2:] by A9;
A21: xx = [y`1,y`2] by MCART_1:21;
then dom(y`1) = cod(y`2) by A20,CAT_1:def 6;
then dom(xx`1) = cod(xx`2) by A14,A16;
hence thesis by A21,CAT_1:def 6;
end;
now
let x,y be object;
assume
A22: [x,y] in dom the Comp of C1;
then reconsider g1 = x, h1 = y as Morphism of C1 by ZFMISC_1:87;
reconsider g2 = g1, h2 = h1 as Morphism of C2 by A9;
consider a1,b1 being Element of A(), f1 being Element of B() such that
A23: g1 = [[a1,b1],f1] and P[a1,b1,f1] by A3;
consider c1,d1 being Element of A(), i1 being Element of B() such that
A24: h1 = [[c1,d1],i1] and P[c1,d1,i1] by A3;
A25: a1 = g1`11 by A23,MCART_1:85
.= dom g1 by Th2
.= cod h1 by A22,CAT_1:15
.= h1`12 by Th2
.= d1 by A24,MCART_1:85;
thus (the Comp of C1).(x,y) = g1(*)h1 by A22,CAT_1:def 1
.= [[c1,b1],F(f1,i1)] by A4,A23,A24,A25
.= g2(*)h2 by A8,A23,A24,A25
.= (the Comp of C2).(x,y) by A17,A22,CAT_1:def 1;
end;
hence thesis by A1,A5,A9,A15,A16,A17,BINOP_1:20;
end;
scheme FunctorEx { A,B() -> Category, O(set) -> Object of B(),
F(object) -> object }:
ex F being Functor of A(),B() st
for f being Morphism of A() holds F.f = F(f)
provided
A1: for f being Morphism of A() holds F(f) is Morphism of B() &
for g being Morphism of B() st g = F(f) holds
dom g = O(dom f) & cod g = O(cod f) and
A2: for a being Object of A() holds F(id a) = id O(a) and
A3: for f1,f2 being Morphism of A() for g1,g2 being Morphism of B() st
g1 = F(f1) & g2 = F(f2) & dom f2 = cod f1 holds F(f2(*)f1) = g2(*)g1
proof
consider F being Function such that
A4: dom F = the carrier' of A() and
A5: for x being object st x in the carrier' of A() holds F.x = F(x) from
FUNCT_1:sch 3;
rng F c= the carrier' of B()
proof
let x be object;
assume x in rng F;
then consider y being object such that
A6: y in dom F and
A7: x = F.y by FUNCT_1:def 3;
x = F(y) by A4,A5,A6,A7;
then x is Morphism of B() by A1,A4,A6;
hence thesis;
end;
then reconsider F as Function of the carrier' of A(), the carrier' of B()
by A4,FUNCT_2:def 1,RELSET_1:4;
A8: now
let c be Object of A();
take d = O(c);
thus F.(id c) = F(id c) by A5
.= id d by A2;
end;
A9: now
let f be Morphism of A();
reconsider g = F(f) as Morphism of B() by A1;
thus F.(id dom f) = F(id dom f) by A5
.= id O(dom f) by A2
.= id dom g by A1
.= id dom (F.f) by A5;
thus F.(id cod f) = F(id cod f) by A5
.= id O(cod f) by A2
.= id cod g by A1
.= id cod (F.f) by A5;
end;
now
let f,g be Morphism of A();
assume
A10: dom g = cod f;
A11: F.g = F(g) by A5;
A12: F.f = F(f) by A5;
F.(g(*)f) = F(g(*)f) by A5;
hence F.(g(*)f) = (F.g)(*)(F.f) by A3,A10,A11,A12;
end;
then reconsider F as Functor of A(), B() by A8,A9,CAT_1:61;
take F;
thus thesis by A5;
end;
theorem Th3:
for C1 being Category, C2 being Subcategory of C1 st C1 is Subcategory of C2
holds the CatStr of C1 = the CatStr of C2
proof
let C1 be Category, C2 be Subcategory of C1;
assume
A1: C1 is Subcategory of C2;
then
A2: the carrier of C1 c= the carrier of C2 by CAT_2:def 4;
the carrier of C2 c= the carrier of C1 by CAT_2:def 4;
then
A3: the carrier of C1 = the carrier of C2 by A2;
A4: the carrier' of C1 c= the carrier' of C2 by A1,CAT_2:7;
the carrier' of C2 c= the carrier' of C1 by CAT_2:7;
then
A5: the carrier' of C1 = the carrier' of C2 by A4;
A6: the Comp of C1 c= the Comp of C2 by A1,CAT_2:def 4;
the Comp of C2 c= the Comp of C1 by CAT_2:def 4;
then
A7: the Comp of C1 = the Comp of C2 by A6;
now
let m1 be Morphism of C1;
reconsider m2 = m1 as Morphism of C2 by A4;
thus (the Source of C1).m1 = dom m1 .= dom m2 by CAT_2:9
.= (the Source of C2).m1;
end;
then
A8: the Source of C1 = the Source of C2 by A3,A5,FUNCT_2:63;
now
let m1 be Morphism of C1;
reconsider m2 = m1 as Morphism of C2 by A4;
thus (the Target of C1).m1 = cod m1 .= cod m2 by CAT_2:9
.= (the Target of C2).m1;
end;
then
the Target of C1 = the Target of C2 by A3,A5,FUNCT_2:63;
hence thesis by A3,A5,A7,A8;
end;
theorem Th4:
for C being Category, D being Subcategory of C, E being Subcategory of D
holds E is Subcategory of C
proof
let C be Category, D be Subcategory of C, E be Subcategory of D;
A1: the carrier of D c= the carrier of C by CAT_2:def 4;
A2: the Comp of D c= the Comp of C by CAT_2:def 4;
A3: the carrier of E c= the carrier of D by CAT_2:def 4;
A4: the Comp of E c= the Comp of D by CAT_2:def 4;
thus the carrier of E c= the carrier of C by A1,A3;
hereby
let a,b be Object of E, a9,b9 be Object of C;
reconsider a1 = a, b1 = b as Object of D by CAT_2:6;
assume that
A5: a = a9 and
A6: b = b9;
A7: Hom(a,b) c= Hom(a1,b1) by CAT_2:def 4;
Hom(a1,b1) c= Hom(a9,b9) by A5,A6,CAT_2:def 4;
hence Hom(a,b) c= Hom(a9,b9) by A7;
end;
thus the Comp of E c= the Comp of C by A2,A4;
let a be Object of E, a9 be Object of C;
reconsider a1 = a as Object of D by CAT_2:6;
assume
A8: a = a9;
id a = id a1 by CAT_2:def 4;
hence thesis by A8,CAT_2:def 4;
end;
definition
let C1,C2 be Category;
given C being Category such that
A1: C1 is Subcategory of C and
A2: C2 is Subcategory of C;
given o1 being Object of C1 such that
A3: o1 is Object of C2;
func C1 /\ C2 -> strict Category means
:
Def2: the carrier of it = (the carrier of C1) /\ the carrier of C2 &
the carrier' of it = (the carrier' of C1) /\ the carrier' of C2 &
the Source of it = (the Source of C1)|the carrier' of C2 &
the Target of it = (the Target of C1)|the carrier' of C2 &
the Comp of it = (the Comp of C1)||the carrier' of C2;
existence
proof
set DD = (the Source of C1)|the carrier' of C2;
set CC = (the Target of C1)|the carrier' of C2;
set Cm = (the Comp of C1)||the carrier' of C2;
reconsider O = (the carrier of C1) /\ the carrier of C2
as non empty set by A3,XBOOLE_0:def 4;
reconsider o2 = o1 as Object of C2 by A3;
reconsider o = o1 as Object of C by A1,CAT_2:6;
A4: id o1 = id o by A1,CAT_2:def 4;
id o2 = id o by A2,CAT_2:def 4;
then reconsider M = (the carrier' of C1) /\ the carrier' of C2
as non empty set by A4,XBOOLE_0:def 4;
A5: dom the Source of C1 = the carrier' of C1 by FUNCT_2:def 1;
A6: dom the Target of C1 = the carrier' of C1 by FUNCT_2:def 1;
A7: dom DD = M by A5,RELAT_1:61;
A8: dom CC = M by A6,RELAT_1:61;
rng DD c= O
proof
let x be object;
assume x in rng DD;
then consider m being object such that
A9: m in dom DD and
A10: x = DD.m by FUNCT_1:def 3;
reconsider m1 = m as Morphism of C1 by A9;
reconsider m2 = m as Morphism of C2 by A7,A9,XBOOLE_0:def 4;
reconsider m = m1 as Morphism of C by A1,CAT_2:8;
A11: x = dom m1 by A9,A10,FUNCT_1:47;
A12: dom m1 = dom m by A1,CAT_2:9;
dom m = dom m2 by A2,CAT_2:9;
hence thesis by A11,A12,XBOOLE_0:def 4;
end;
then reconsider DD as Function of M,O by A7,FUNCT_2:def 1,RELSET_1:4;
rng CC c= O
proof
let x be object;
assume x in rng CC;
then consider m being object such that
A13: m in dom CC and
A14: x = CC.m by FUNCT_1:def 3;
reconsider m1 = m as Morphism of C1 by A13;
reconsider m2 = m as Morphism of C2 by A8,A13,XBOOLE_0:def 4;
reconsider m = m1 as Morphism of C by A1,CAT_2:8;
A15: x = cod m1 by A13,A14,FUNCT_1:47;
A16: cod m1 = cod m by A1,CAT_2:9;
cod m = cod m2 by A2,CAT_2:9;
hence thesis by A15,A16,XBOOLE_0:def 4;
end;
then reconsider CC as Function of M,O by A8,FUNCT_2:def 1,RELSET_1:4;
A17: dom Cm = (dom the Comp of C1) /\
[:the carrier' of C2,the carrier' of C2:] by RELAT_1:61;
then
dom Cm c= [:the carrier' of C1,the carrier' of C1:] /\
[:the carrier' of C2,the carrier' of C2:] by XBOOLE_1:26;
then
A18: dom Cm c= [:M,M:] by ZFMISC_1:100;
rng Cm c= M
proof
let x be object;
assume x in rng Cm;
then consider m being object such that
A19: m in dom Cm and
A20: x = Cm.m by FUNCT_1:def 3;
A21: m`1 in M by A18,A19,MCART_1:10;
A22: m`2 in M by A18,A19,MCART_1:10;
A23: m = [m`1,m`2] by A17,A19,MCART_1:21;
reconsider m1 = m`1, m2 = m`2 as Morphism of C1
by A21,A22,XBOOLE_0:def 4;
reconsider n1 = m`1, n2 = m`2 as Morphism of C2
by A21,A22,XBOOLE_0:def 4;
reconsider mm = m1, n = m2 as Morphism of C by A1,CAT_2:8;
A24: m in dom the Comp of C1 by A17,A19,XBOOLE_0:def 4;
then
A25: dom m1 = cod m2 by A23,CAT_1:15;
A26: x = (the Comp of C1).(m1,m2) by A19,A20,A23,FUNCT_1:47;
A27: dom m1 = dom mm by A1,CAT_2:9;
A28: dom n1 = dom mm by A2,CAT_2:9;
A29: cod m2 = cod n by A1,CAT_2:9;
A30: cod n2 = cod n by A2,CAT_2:9;
A31: x = m1(*)m2 by A23,A24,A26,CAT_1:def 1;
A32: m1(*)m2 = mm(*)n by A1,A25,CAT_2:11;
mm(*)n = n1(*)n2 by A2,A25,A27,A28,A29,A30,CAT_2:11;
hence thesis by A31,A32,XBOOLE_0:def 4;
end;
then reconsider Cm as PartFunc of [:M,M:], M by A18,RELSET_1:4;
set CAT = CatStr(#O,M,DD,CC,Cm#);
A33: CAT is Category-like
proof
let f,g be Morphism of CAT;
reconsider g9 = g, f9 = f as Morphism of C1 by XBOOLE_0:def 4;
A34: g in the carrier' of C2 by XBOOLE_0:def 4;
A35: f in the carrier' of C2 by XBOOLE_0:def 4;
hereby
assume [g,f] in dom the Comp of CAT;
then
A36: [g,f] in dom the Comp of C1 by A17,XBOOLE_0:def 4;
thus dom g = dom g9 by A34,FUNCT_1:49
.= cod f9 by A36,CAT_1:def 6
.= cod f by A35,FUNCT_1:49;
end;
assume
A37: dom g = cod f;
A38: dom g = dom g9 by A7,FUNCT_1:47;
A39: dom g = cod f9 by A8,A37,FUNCT_1:47;
A40: [g,f] in [:the carrier' of C2,the carrier' of C2:] by A34,A35,
ZFMISC_1:87;
[g,f] in dom the Comp of C1 by A38,A39,CAT_1:def 6;
hence [g,f] in dom(the Comp of CAT) by A17,A40,XBOOLE_0:def 4;
end;
A41: for f,g being Morphism of CAT holds
[g,f] in dom the Comp of CAT iff dom g = cod f by A33;
A42: CAT is transitive
proof let f,g be Morphism of CAT;
reconsider g9 = g, f9 = f as Morphism of C1 by XBOOLE_0:def 4;
assume
A43: dom g=cod f;
then
A44: [g,f] in dom the Comp of CAT by A41;
A45: dom the Comp of CAT c= dom the Comp of C1 by RELAT_1:60;
reconsider h = g(*)f as Morphism of CAT;
reconsider h9 = h as Morphism of C1 by XBOOLE_0:def 4;
A46: h = (the Comp of CAT).(g,f) by A44,CAT_1:def 1
.= (the Comp of C1).(g9,f9) by A44,FUNCT_1:47
.= g9(*)f9 by A45,A44,CAT_1:def 1;
A47: dom f = dom f9 by A7,FUNCT_1:47;
A48: dom g = dom g9 by A7,FUNCT_1:47;
A49: dom h = dom h9 by A7,FUNCT_1:47;
A50: cod f = cod f9 by A8,FUNCT_1:47;
A51: cod g = cod g9 by A8,FUNCT_1:47;
A52: cod h = cod h9 by A8,FUNCT_1:47;
thus dom(g(*)f) = dom f
by A43,A47,A48,A49,A50,A46,CAT_1:def 7;
thus cod(g(*)f) = cod g
by A43,A46,A48,A50,A51,A52,CAT_1:def 7;
end;
A53: for f,g being Morphism of CAT st dom g = cod f
holds dom(g(*)f) = dom f & cod(g(*)f) = cod g
by A42;
A54: CAT is associative
proof
let f,g,h be Morphism of CAT;
reconsider h9 = h, g9 = g, f9 = f as Morphism of C1 by XBOOLE_0:def 4;
assume that
A55: dom h = cod g and
A56: dom g = cod f;
A57: [h,g] in dom the Comp of CAT by A41,A55;
A58: [g,f] in dom the Comp of CAT by A41,A56;
then reconsider hg = (the Comp of CAT).(h,g),
gf = (the Comp of CAT).(g,f) as Morphism of CAT
by A57,PARTFUN1:4;
reconsider hg9 = hg, gf9 = gf as Morphism of C1 by XBOOLE_0:def 4;
A59: dom hg = dom(h(*)g) by A57,CAT_1:def 1
.= dom g by A53,A55;
A60: cod gf = cod(g(*)f) by A58,CAT_1:def 1
.= cod g by A53,A56;
A61: [hg,f] in dom the Comp of CAT by A41,A56,A59;
A62: [h,gf] in dom the Comp of CAT by A41,A55,A60;
A63: dom h9 = dom h by A7,FUNCT_1:47;
A64: cod g9 = cod g by A8,FUNCT_1:47;
then
A65: h9(*)g9 =(the Comp of C1).(h9,g9) by A63,A55,CAT_1:16;
A66: dom g9 = dom g by A7,FUNCT_1:47;
A67: cod f9 = cod f by A8,FUNCT_1:47;
then
A68: g9(*)f9 =(the Comp of C1).(g9,f9) by A66,A56,CAT_1:16;
A69: cod(g9(*)f9) = cod g9 by A56,A66,A67,CAT_1:def 7;
A70: dom(h9(*)g9) = dom g9 by A55,A63,A64,CAT_1:def 7;
A71: hg = h(*)g by A57,CAT_1:def 1;
gf = g(*)f by A58,CAT_1:def 1;
hence h(*)(g(*)f)
=(the Comp of CAT).(h,(the Comp of CAT).(g,f))
by A62,CAT_1:def 1
.= (the Comp of C1).[h9,gf9] by A62,FUNCT_1:47
.= (the Comp of C1).(h9,(the Comp of C1).(g9,f9)) by A58,FUNCT_1:47
.= h9(*)(g9(*)f9) by A69,A68,A55,A63,A64,CAT_1:16
.= h9(*)g9(*)f9 by A55,A56,A63,A64,A66,A67,CAT_1:def 8
.= (the Comp of C1).((the Comp of C1).(h9,g9),f9)
by A70,A65,A56,A66,A67,CAT_1:16
.= (the Comp of C1).[hg9,f9] by A57,FUNCT_1:47
.= (the Comp of CAT).((the Comp of CAT).(h,g),f) by A61,FUNCT_1:47
.= h(*)g(*)f by A71,A61,CAT_1:def 1;
end;
A72: CAT is reflexive
proof
let b be Object of CAT;
reconsider b1 = b as Object of C1 by XBOOLE_0:def 4;
reconsider b2 = b as Object of C2 by XBOOLE_0:def 4;
A73: the carrier of C1 c= the carrier of C by A1,CAT_2:def 4;
reconsider bb = b1 as Object of C by A73;
A74: id b1 = id bb by A1,CAT_2:def 4 .= id b2 by A2,CAT_2:def 4;
id b2 in (the carrier' of C1) /\ the carrier' of C2
by A74,XBOOLE_0:def 4;
then
id b2 in M;
then reconsider ii = id b2 as Morphism of CAT;
A75: dom ii = dom id b1 by A74,FUNCT_1:49
.= b;
cod ii = cod id b1 by A74,FUNCT_1:49
.= b;
then ii in Hom(b,b) by A75;
hence Hom(b,b)<>{};
end;
CAT is with_identities
proof let a be Element of CAT;
reconsider a1 = a as Object of C1 by XBOOLE_0:def 4;
reconsider a2 = a as Object of C2 by XBOOLE_0:def 4;
A76: the carrier of C1 c= the carrier of C by A1,CAT_2:def 4;
reconsider aa = a1 as Object of C by A76;
A77: id a1 = id aa by A1,CAT_2:def 4 .= id a2 by A2,CAT_2:def 4;
id a2 in (the carrier' of C1) /\ the carrier' of C2
by A77,XBOOLE_0:def 4;
then
id a2 in M;
then reconsider ii = id a2 as Morphism of CAT;
A78: dom ii = dom id a1 by A77,FUNCT_1:49
.= a;
cod ii = cod id a1 by A77,FUNCT_1:49
.= a;
then ii in Hom(a,a) by A78;
then reconsider ii as Morphism of a,a by CAT_1:def 5;
take ii;
let b be Element of CAT;
thus Hom(a,b)<>{} implies for g being Morphism of a,b holds g(*)ii = g
proof assume
A79: Hom(a,b)<>{};
let g be Morphism of a,b;
g in the carrier' of C1 by XBOOLE_0:def 4;
then reconsider gg = g as Morphism of C1;
A80: g in the carrier' of C2 by XBOOLE_0:def 4;
A81: dom gg = (the Source of C1).g
.= ((the Source of C1)|the carrier' of C2).g by A80,FUNCT_1:49
.= dom g
.= a1 by A79,CAT_1:5;
A82: cod id a1 = a1;
cod ii = cod id a1 by A77,FUNCT_1:49
.= dom g by A79,CAT_1:5;
then
A83: [g,ii] in dom the Comp of CAT by A33;
hence g(*)ii = Cm.(g,ii) by CAT_1:def 1
.= ((the Comp of C1)||the carrier' of C2).(g,ii)
.= ((the Comp of C1)).(gg,id a1) by A77,A83,FUNCT_1:47
.= gg(*)id a1 by A82,A81,CAT_1:16
.= g by A81,CAT_1:22;
end;
assume
A84: Hom(b,a)<>{};
let g be Morphism of b,a;
g in the carrier' of C1 by XBOOLE_0:def 4;
then reconsider gg = g as Morphism of C1;
A85: g in the carrier' of C2 by XBOOLE_0:def 4;
A86: cod gg = (the Target of C1).g
.= ((the Target of C1)|the carrier' of C2).g by A85,FUNCT_1:49
.= cod g
.= a1 by A84,CAT_1:5;
A87: dom id a1 = a1;
dom ii = dom id a1 by A77,FUNCT_1:49
.= cod g by A84,CAT_1:5;
then
A88: [ii,g] in dom the Comp of CAT by A33;
hence ii(*)g = Cm.(ii,g) by CAT_1:def 1
.= ((the Comp of C1)||the carrier' of C2).(ii,g)
.= ((the Comp of C1)).(id a1,gg) by A77,A88,FUNCT_1:47
.= (id a1)(*)gg by A87,A86,CAT_1:16
.= g by A86,CAT_1:21;
end;
hence thesis by A33,A42,A54,A72;
end;
uniqueness;
end;
reserve C for Category,
C1,C2 for Subcategory of C;
theorem Th5:
the carrier of C1 meets the carrier of C2 implies C1 /\ C2 = C2 /\ C1
proof
assume (the carrier of C1) /\ the carrier of C2 <> {};
then reconsider O = (the carrier of C1) /\ the carrier of C2 as non empty
set;
set o = the Element of O;
set C12 = C1 /\ C2, C21 = C2 /\ C1;
set M1 = the carrier' of C1, M2 = the carrier' of C2;
set O1 = the carrier of C1, O2 = the carrier of C2;
A1: o is Object of C1 by XBOOLE_0:def 4;
A2: o is Object of C2 by XBOOLE_0:def 4;
then
A3: the carrier of C12 = O by A1,Def2;
A4: the carrier of C21 = O by A1,A2,Def2;
A5: the carrier' of C12 = (the carrier' of C1) /\ the carrier' of C2 by A1,A2
,Def2;
A6: the Source of C21 = (the Source of C2)|M1 by A1,A2,Def2;
A7: the Source of C12 = (the Source of C1)|M2 by A1,A2,Def2;
A8: the Target of C21 = (the Target of C2)|M1 by A1,A2,Def2;
A9: the Target of C12 = (the Target of C1)|M2 by A1,A2,Def2;
A10: the Comp of C21 = (the Comp of C2)||M1 by A1,A2,Def2;
A11: the Comp of C12 = (the Comp of C1)||M2 by A1,A2,Def2;
A12: the Source of C1 = (the Source of C)|M1 by NATTRA_1:8;
A13: the Target of C1 = (the Target of C)|M1 by NATTRA_1:8;
A14: the Source of C2 = (the Source of C)|M2 by NATTRA_1:8;
A15: the Target of C2 = (the Target of C)|M2 by NATTRA_1:8;
A16: the Source of C12 = (the Source of C)|(M1 /\ M2) by A7,A12,RELAT_1:71
.= the Source of C21 by A6,A14,RELAT_1:71;
A17: the Target of C12 = (the Target of C)|(M1 /\ M2) by A9,A13,RELAT_1:71
.= the Target of C21 by A8,A15,RELAT_1:71;
the Comp of C12 = (the Comp of C)||M1||M2 by A11,NATTRA_1:8
.= (the Comp of C)|([:M1,M1:] /\ [:M2,M2:]) by RELAT_1:71
.= (the Comp of C)||M2||M1 by RELAT_1:71
.= the Comp of C21 by A10,NATTRA_1:8;
hence thesis by A1,A2,A3,A4,A5,A16,A17,Def2;
end;
theorem Th6:
the carrier of C1 meets the carrier of C2 implies
C1 /\ C2 is Subcategory of C1 & C1 /\ C2 is Subcategory of C2
proof
assume
A1: (the carrier of C1) meets the carrier of C2;
then
A2: (the carrier of C1) /\ the carrier of C2 <> {};
A3: C1 /\ C2 = C2 /\ C1 by A1,Th5;
now
let C1,C2 be Subcategory of C;
assume
A4: (the carrier of C1) /\ the carrier of C2 <> {};
A5: (the carrier of C1) /\ the carrier of C2 c= the carrier of C1 by
XBOOLE_1:17;
A6: (the carrier' of C1) /\ the carrier' of C2 c= the carrier' of C1 by
XBOOLE_1:17;
reconsider O = (the carrier of C1) /\ the carrier of C2 as non empty set
by A4;
set o = the Element of O;
A7: o is Object of C1 by XBOOLE_0:def 4;
A8: o is Object of C2 by XBOOLE_0:def 4;
then
A9: the carrier of C1/\C2 = (the carrier of C1) /\ the carrier of C2 by A7,Def2
;
A10: the carrier' of C1/\C2 = (the carrier' of C1) /\ the carrier' of C2 by A7
,A8,Def2;
A11: the Source of C1/\C2 = (the Source of C1)|the carrier' of C2 by A7,A8,Def2
;
A12: the Target of C1/\C2 = (the Target of C1)|the carrier' of C2 by A7,A8,Def2
;
A13: the Comp of C1/\C2 = (the Comp of C1)||the carrier' of C2 by A7,A8,Def2;
A14: the Source of C1 = (the Source of C1)|dom the Source of C1;
dom the Source of C1 = the carrier' of C1 by FUNCT_2:def 1;
then
A15: the Source of C1/\C2 = (the Source of C1)|the carrier' of C1/\C2
by A10,A11,A14,RELAT_1:71;
A16: the Target of C1 = (the Target of C1)|dom the Target of C1;
dom the Target of C1 = the carrier' of C1 by FUNCT_2:def 1;
then
A17: the Target of C1/\C2 = (the Target of C1)|the carrier' of C1/\C2
by A10,A12,A16,RELAT_1:71;
A18: for o being Element of C1 st o in O
holds id o in (the carrier' of C1) /\ the carrier' of C2
proof let o1 be Element of C1;
assume
o1 in O;
then reconsider o2 = o1 as Element of C2 by XBOOLE_0:def 4;
A19: the carrier of C1 c= the carrier of C by CAT_2:def 4;
reconsider o = o1 as Element of C by A19;
A20: id o1 = id o by CAT_2:def 4;
id o2 = id o by CAT_2:def 4;
hence id o1 in (the carrier' of C1) /\ the carrier' of C2
by A20,XBOOLE_0:def 4;
end;
the Comp of C1 = (the Comp of C1)||the carrier' of C1;
then the Comp of C1/\C2 = (the Comp of C1)|
([:the carrier' of C1,the carrier' of C1:] /\
[:the carrier' of C2,the carrier' of C2:]) by A13,RELAT_1:71;
then the Comp of C1/\C2 = (the Comp of C1)||the carrier' of C1/\C2
by A10,ZFMISC_1:100;
hence C1/\C2 is Subcategory of C1 by A5,A6,A9,A10,A15,A17,A18,NATTRA_1:9;
end;
hence thesis by A2,A3;
end;
definition
let C,D be Category;
let F be Functor of C,D;
func Image F -> strict Subcategory of D means
:Def3:
the carrier of it = rng Obj F & rng F c= the carrier' of it &
for E being Subcategory of D st
the carrier of E = rng Obj F & rng F c= the carrier' of E
holds it is Subcategory of E;
existence
proof set a = the Object of C;
A1: dom Obj F = the carrier of C by FUNCT_2:def 1;
then (Obj F).a in rng Obj F by FUNCT_1:def 3;
then reconsider O = rng Obj F as non empty set;
reconsider O as non empty Subset of the carrier of D;
set f = the Morphism of C;
A2: dom F = the carrier' of C by FUNCT_2:def 1;
A3: dom the Source of D = the carrier' of D by FUNCT_2:def 1;
A4: dom the Target of D = the carrier' of D by FUNCT_2:def 1;
defpred P[set] means
rng F c= $1 & ex E being Subcategory of D st the carrier of E = O &
the carrier' of E = $1;
consider MM being set such that
A5: for x being set holds x in MM iff x in bool the carrier' of D & P[x]
from XFAMILY:sch 1;
set HH = {Hom(a0,b) where a0 is Object of D, b is Object of D:
a0 in O & b in O};
reconsider M0 = union HH as non empty Subset of the carrier' of D
by CAT_2:19;
reconsider D0 = (the Source of D)|M0, C0 = (the Target of D)|M0
as Function of M0,O by CAT_2:20;
reconsider CC = (the Comp of D)||M0 as PartFunc of [:M0,M0:],M0
by CAT_2:20;
CatStr(#O,M0,D0,C0,CC#) is full Subcategory of D by CAT_2:21;
then
A6: CatStr(#O,M0,D0,C0,CC#) is Subcategory of D;
rng F c= M0
proof
let y be object;
assume y in rng F;
then consider x being object such that
A7: x in dom F and
A8: y = F.x by FUNCT_1:def 3;
reconsider x as Morphism of C by A7;
A9: (Obj F).dom x in O by A1,FUNCT_1:def 3;
A10: (Obj F).cod x in O by A1,FUNCT_1:def 3;
A11: dom (F.x) in O by A9,CAT_1:69;
A12: cod (F.x) in O by A10,CAT_1:69;
A13: y in Hom(dom (F.x), cod (F.x)) by A8;
Hom(dom (F.x), cod (F.x)) in HH by A11,A12;
hence thesis by A13,TARSKI:def 4;
end;
then
A14: M0 in MM by A5,A6;
set M = meet MM;
A15: for Z being set st Z in MM holds rng F c= Z by A5;
now
let X be set;
assume X in MM;
then
A16: rng F c= X by A5;
F.f in rng F by A2,FUNCT_1:def 3;
hence F.f in X by A16;
end;
then reconsider M as non empty set by A14,SETFAM_1:def 1;
M c= the carrier' of D
proof
let x be object;
assume x in M;
then x in M0 by A14,SETFAM_1:def 1;
hence thesis;
end;
then reconsider M as non empty Subset of the carrier' of D;
set DOM = (the Source of D)|M;
set COD = (the Target of D)|M;
set COMP = (the Comp of D)||M;
A17: dom DOM = M by A3,RELAT_1:62;
rng DOM c= O
proof
let y be object;
assume y in rng DOM;
then consider x being object such that
A18: x in M and
A19: y = DOM.x by A17,FUNCT_1:def 3;
reconsider x as Morphism of D by A18;
x in M0 by A14,A18,SETFAM_1:def 1;
then consider X being set such that
A20: x in X and
A21: X in HH by TARSKI:def 4;
consider a,b being Object of D such that
A22: X = Hom(a,b) and
A23: a in O and b in O by A21;
dom x = a by A20,A22,CAT_1:1;
hence thesis by A17,A18,A19,A23,FUNCT_1:47;
end;
then reconsider DOM as Function of M,O by A17,FUNCT_2:def 1,RELSET_1:4;
A24: dom COD = M by A4,RELAT_1:62;
rng COD c= O
proof
let y be object;
assume y in rng COD;
then consider x being object such that
A25: x in M and
A26: y = COD.x by A24,FUNCT_1:def 3;
reconsider x as Morphism of D by A25;
x in M0 by A14,A25,SETFAM_1:def 1;
then consider X being set such that
A27: x in X and
A28: X in HH by TARSKI:def 4;
consider a,b being Object of D such that
A29: X = Hom(a,b) and a in O and
A30: b in O by A28;
cod x = b by A27,A29,CAT_1:1;
hence thesis by A24,A25,A26,A30,FUNCT_1:47;
end;
then reconsider COD as Function of M,O by A24,FUNCT_2:def 1,RELSET_1:4;
A31: dom COMP c= [:M,M:] by RELAT_1:58;
rng COMP c= M
proof
let y be object;
assume y in rng COMP;
then consider x being object such that
A32: x in dom COMP and
A33: y = COMP.x by FUNCT_1:def 3;
reconsider x1 = x`1, x2 = x`2 as Element of M by A31,A32,MCART_1:10;
A34: x = [x1,x2] by A31,A32,MCART_1:21;
now
let X be set;
assume
A35: X in MM;
then consider E being Subcategory of D such that
the carrier of E = O and
A36: the carrier' of E = X by A5;
reconsider y1 = x1, y2 = x2 as Morphism of E by A35,A36,SETFAM_1:def 1;
dom COMP = (dom the Comp of D) /\ [:M,M:] by RELAT_1:61;
then x in dom the Comp of D by A32,XBOOLE_0:def 4;
then
A37: dom x1 = cod x2 by A34,CAT_1:15;
A38: dom y1 = dom x1 by CAT_2:9;
cod y2 = cod x2 by CAT_2:9;
then
A39: x in dom the Comp of E by A34,A37,A38,CAT_1:15;
the Comp of E c= the Comp of D by CAT_2:def 4;
then (the Comp of E).x = (the Comp of D).x by A39,GRFUNC_1:2
.= y
by A32,A33,FUNCT_1:47;
then y in rng the Comp of E by A39,FUNCT_1:def 3;
hence y in X by A36;
end;
hence thesis by A14,SETFAM_1:def 1;
end;
then reconsider COMP as PartFunc of [:M,M:], M by A31,RELSET_1:4;
for o being Element of D st o in O holds id o in M
proof let o be Element of D;
assume
A40: o in O;
for X being set st X in MM holds id o in X
proof let X be set;
assume X in MM;
then P[X] by A5;
then consider E being Subcategory of D such that
A41: the carrier of E = O and
A42: the carrier' of E = X;
o in the carrier of E by A40,A41;
then reconsider oo=o as Element of E;
id oo = id o by CAT_2:def 4;
hence id o in X by A42;
end;
hence id o in M by A14,SETFAM_1:def 1;
end;
then reconsider T = CatStr(#O,M, DOM, COD, COMP#)
as strict Subcategory of D by NATTRA_1:9;
take T;
thus the carrier of T = rng Obj F & rng F c= the carrier' of T by A14,A15,
SETFAM_1:5;
let E be Subcategory of D;
assume that
A43: the carrier of E = rng Obj F and
A44: rng F c= the carrier' of E;
thus the carrier of T c= the carrier of E by A43;
the carrier' of E c= the carrier' of D by CAT_2:7;
then the carrier' of E in MM by A5,A43,A44;
then
A45: M c= the carrier' of E by SETFAM_1:3;
hereby
let a,b be Object of T, a9,b9 be Object of E;
assume that
A46: a = a9 and
A47: b = b9;
thus Hom(a,b) c= Hom(a9,b9)
proof
let x be object;
assume x in Hom(a,b);
then consider f being Morphism of T such that
A48: x = f and
A49: dom f = a and
A50: cod f = b;
reconsider g = f as Morphism of D by TARSKI:def 3;
reconsider f as Morphism of E by A45;
A51: dom g = a by A49,CAT_2:9;
A52: cod g = b by A50,CAT_2:9;
A53: a9 = dom f by A46,A51,CAT_2:9;
b9 = cod f by A47,A52,CAT_2:9;
hence thesis by A48,A53;
end;
end;
A54: dom the Comp of T c= dom the Comp of E
proof
let x be object;
assume
A55: x in dom the Comp of T;
then reconsider x1 = x`1, x2 = x`2 as Element of M by MCART_1:10;
reconsider y1 = x1, y2 = x2 as Morphism of T;
reconsider z1 = x1, z2 = x2 as Morphism of E by A45;
A56: x = [x1,x2] by A55,MCART_1:21;
then
A57: dom y1 = cod y2 by A55,CAT_1:15;
A58: dom y1 = dom x1 by CAT_2:9;
A59: dom z1 = dom x1 by CAT_2:9;
A60: cod y2 = cod x2 by CAT_2:9;
cod z2 = cod x2 by CAT_2:9;
hence thesis by A56,A57,A58,A59,A60,CAT_1:15;
end;
now
let x be object;
assume
A61: x in dom the Comp of T;
A62: the Comp of T c= the Comp of D by CAT_2:def 4;
A63: the Comp of E c= the Comp of D by CAT_2:def 4;
thus (the Comp of T).x = (the Comp of D).x by A61,A62,GRFUNC_1:2
.= (the Comp of E).x by A54,A61,A63,GRFUNC_1:2;
end;
hence the Comp of T c= the Comp of E by A54,GRFUNC_1:2;
let a be Object of T, a9 be Object of E;
reconsider b = a as Object of D by TARSKI:def 3;
assume
A64: a = a9;
id a = id b by CAT_2:def 4;
hence thesis by A64,CAT_2:def 4;
end;
uniqueness
proof
let C1,C2 be strict Subcategory of D such that
A65: the carrier of C1 = rng Obj F and
A66: rng F c= the carrier' of C1 and
A67: for E being Subcategory of D st
the carrier of E = rng Obj F & rng F c= the carrier' of E
holds C1 is Subcategory of E and
A68: the carrier of C2 = rng Obj F and
A69: rng F c= the carrier' of C2 and
A70: for E being Subcategory of D st
the carrier of E = rng Obj F & rng F c= the carrier' of E
holds C2 is Subcategory of E;
A71: C1 is Subcategory of C2 by A67,A68,A69;
C2 is Subcategory of C1 by A65,A66,A70;
hence thesis by A71,Th3;
end;
end;
theorem Th7:
for C,D being Category, E be Subcategory of D, F being Functor of C,D st
rng F c= the carrier' of E holds F is Functor of C, E
proof
let C,D be Category, E be Subcategory of D, F be Functor of C,D;
assume
A1: rng F c= the carrier' of E;
A2: dom F = the carrier' of C by FUNCT_2:def 1;
A3: dom Obj F = the carrier of C by FUNCT_2:def 1;
reconsider G = F as Function of the carrier' of C, the carrier' of E
by A1,A2,FUNCT_2:def 1,RELSET_1:4;
A4: rng Obj F c= the carrier of E
proof
let y be object;
assume y in rng Obj F;
then consider x being object such that
A5: x in dom Obj F and
A6: y = (Obj F).x by FUNCT_1:def 3;
reconsider x as Object of C by A5;
F.id x = id ((Obj F).x) by CAT_1:68;
then id ((Obj F).x) in rng F by A2,FUNCT_1:def 3;
then reconsider f = id ((Obj F).x) as Morphism of E by A1;
A7: dom id ((Obj F).x) = y by A6;
dom id ((Obj F).x) = dom f by CAT_2:9;
hence thesis by A7;
end;
A8: now
let c be Object of C;
(Obj F).c in rng Obj F by A3,FUNCT_1:def 3;
then reconsider d = (Obj F).c as Object of E by A4;
take d;
thus G.id c = id ((Obj F).c) by CAT_1:68
.= id d by CAT_2:def 4;
end;
A9: now
let f be Morphism of C;
A10: dom (F.f) = dom (G.f) by CAT_2:9;
A11: cod (F.f) = cod (G.f) by CAT_2:9;
thus G.id dom f = id (F.dom f) by CAT_1:71
.= id dom (F.f) by CAT_1:72
.= id dom (G.f) by A10,CAT_2:def 4;
thus G.id cod f = id (F.cod f) by CAT_1:71
.= id cod (F.f) by CAT_1:72
.= id cod (G.f) by A11,CAT_2:def 4;
end;
now
let f,g be Morphism of C;
assume
A12: dom g = cod f;
then
A13: F.(g(*)f) = (F.g)(*)(F.f) by CAT_1:64;
A14: dom (F.g) = cod (F.f) by A12,CAT_1:64;
A15: dom (F.g) = dom (G. g) by CAT_2:9;
cod (F.f) = cod (G.f) by CAT_2:9;
hence G.(g(*)f) = (G.g)(*)(G.f) by A13,A14,A15,CAT_2:11;
end;
hence thesis by A8,A9,CAT_1:61;
end;
theorem
for C,D being Category, F being Functor of C,D holds
F is Functor of C, Image F
proof
let C,D be Category, F be Functor of C,D;
rng F c= the carrier' of Image F by Def3;
hence thesis by Th7;
end;
theorem Th9:
for C,D being Category, E being Subcategory of D, F being Functor of C,E
for G being Functor of C,D st F = G holds Image F = Image G
proof
let C,D be Category, E be Subcategory of D;
let F be Functor of C,E, G be Functor of C,D such that
A1: F = G;
reconsider S = Image F as strict Subcategory of D by Th4;
A2: now
thus dom Obj F = the carrier of C & dom Obj G = the carrier of C
by FUNCT_2:def 1;
let x be object;
assume x in the carrier of C;
then reconsider a = x as Object of C;
reconsider b = (Obj F).a as Object of D by CAT_2:6;
G.id a = id ((Obj F).a) by A1,CAT_1:68
.= id b by CAT_2:def 4;
hence (Obj G).x = (Obj F).x by CAT_1:67;
end;
then
A3: Obj F = Obj G;
then
A4: the carrier of S = rng Obj G by Def3;
A5: rng G c= the carrier' of S by A1,Def3;
now
let T be Subcategory of D;
assume that
A6: the carrier of T = rng Obj G and
A7: rng G c= the carrier' of T;
set x = the Object of C;
A8: (Obj G).x in rng Obj G by A2,FUNCT_1:def 3;
A9: (Obj G).x = (Obj F).x by A2;
then (Obj G).x in (the carrier of T) /\ the carrier of E
by A6,A8,XBOOLE_0:def 4;
then
A10: (the carrier of T) meets the carrier of E;
then reconsider E1 = T /\ E as Subcategory of E by Th6;
the carrier of E1 = (the carrier of T) /\ the carrier of E by A6,A8,A9,Def2
;
then
A11: the carrier of E1 = rng Obj F by A3,A6,XBOOLE_1:28;
the carrier' of E1 = (the carrier' of T) /\ the carrier' of E by A6,A8,A9
,Def2;
then rng F c= the carrier' of E1 by A1,A7,XBOOLE_1:19;
then
A12: Image F is Subcategory of E1 by A11,Def3;
E1 is Subcategory of T by A10,Th6;
hence S is Subcategory of T by A12,Th4;
end;
hence thesis by A4,A5,Def3;
end;
begin :: Categorial Categories
definition
let IT be set;
attr IT is categorial means
:Def4:
for x being set st x in IT holds x is Category;
end;
definition
let X be non empty set;
redefine attr X is categorial means :: redefines categorial (CAT_5, definition)
for x being Element of X holds x is Category;
compatibility;
end;
registration
cluster categorial for non empty set;
existence
proof
take X = {1Cat(0,{0})};
let x be Element of X;
thus thesis by TARSKI:def 1;
end;
end;
definition
let X be non empty categorial set;
redefine mode Element of X -> Category; :: redefines Element (SUBSET_1, definition)
coherence by Def4;
end;
definition
let C be Category;
attr C is Categorial means
:Def6:
the carrier of C is categorial &
(for a being Object of C, A being Category st a = A holds
id a = [[A,A], id A]) & (for m being Morphism of C
for A,B being Category st A = dom m & B = cod m
ex F being Functor of A,B st m = [[A,B], F]) & for m1,m2 being Morphism of C
for A,B,C being Category for F being Functor of A,B
for G being Functor of B,C st m1 = [[A,B],F] & m2 = [[B,C],G]
holds m2(*)m1 = [[A,C],G*F];
end;
registration
cluster Categorial -> with_triple-like_morphisms for Category;
coherence
proof
let C be Category;
assume
A1: C is Categorial;
then
A2: the carrier of C is categorial;
let f be Morphism of C;
reconsider A = dom f, B = cod f as Category by A2;
ex F being Functor of A,B st f = [[A,B], F] by A1;
hence thesis;
end;
end;
theorem Th10:
for C,D being Category st the CatStr of C = the CatStr of D holds
C is Categorial implies D is Categorial
proof
let C,D be Category;
assume
A1: the CatStr of C = the CatStr of D;
assume that
A2: the carrier of C is categorial and
A3: for a being Object of C, A being Category st a = A holds
id a = [[A,A], id A] and
A4: for m being Morphism of C for A,B being Category st A = dom m & B = cod m
ex F being Functor of A,B st m = [[A,B], F] and
A5: for m1,m2 being Morphism of C for A,B,C being Category
for F being Functor of A,B
for G being Functor of B,C st m1 = [[A,B],F] & m2 = [[B,C],G]
holds m2(*)m1 = [[A,C],G*F];
thus the carrier of D is categorial by A1,A2;
thus for a being Object of D, A being Category st a = A
holds id a = [[A,A], id A]
proof
let a be Object of D, A be Category;
reconsider b = a as Object of C by A1;
assume a = A;
then [[A,A], id A] = id b by A3;
hence id a = [[A,A], id A] by A1,Lm1;
end;
hereby
let m be Morphism of D;
reconsider m9 = m as Morphism of C by A1;
let A,B be Category;
assume that
A6: A = dom m and
A7: B = cod m;
A8: A = dom m9 by A1,A6;
B = cod m9 by A1,A7;
hence ex F being Functor of A,B st m = [[A,B], F] by A4,A8;
end;
let m1,m2 be Morphism of D;
reconsider f1 = m1, f2 = m2 as Morphism of C by A1;
let a,b,c be Category;
let F be Functor of a,b, G be Functor of b,c;
assume that
A9: m1 = [[a,b],F] and
A10: m2 = [[b,c],G];
reconsider a1 = dom f1, b1 = cod f1, a2 = dom f2, b2 = cod f2 as Category
by A2;
A11: ex F1 being Functor of a1,b1 st ( f1 = [[a1,b1], F1]) by A4;
ex F2 being Functor of a2,b2 st ( f2 = [[a2,b2], F2]) by A4;
then
A12: dom f2 = m2`11 by MCART_1:85;
A13: m2`11 = b by A10,MCART_1:85;
A14: cod f1 = m1`12 by A11,MCART_1:85;
m1`12 = b by A9,MCART_1:85;
then
A15: [f2,f1] in dom the Comp of C by A12,A13,A14,CAT_1:15;
hence m2(*)m1 = (the Comp of D).(m2,m1) by A1,CAT_1:def 1
.= f2(*)f1 by A1,A15,CAT_1:def 1
.= [[a,c],G*F] by A5,A9,A10;
end;
theorem Th11:
for C being Category holds 1Cat(C, [[C,C], id C]) is Categorial
proof
let A be Category;
set F = [[A,A], id A];
set C = 1Cat(A, F);
thus for x be Object of C holds x is Category by TARSKI:def 1;
hereby
let a be Object of C, D be Category;
assume a = D;
then D = A by TARSKI:def 1;
hence id a = [[D,D], id D] by TARSKI:def 1;
end;
hereby
let m be Morphism of C;
let C1,C2 be Category;
assume that
A1: C1 = dom m and
A2: C2 = cod m;
A3: C1 = A by A1,TARSKI:def 1;
A4: C2 = A by A2,TARSKI:def 1;
reconsider G = id A as Functor of C1,C2 by A2,A3,TARSKI:def 1;
take G;
thus m = [[C1,C2],G] by A3,A4,TARSKI:def 1;
end;
let m1,m2 be Morphism of C;
let A1,B,C be Category, F1 be Functor of A1,B, F2 be Functor of B,C;
assume that
A5: m1 = [[A1,B],F1] and
A6: m2 = [[B,C],F2];
A7: [[A1,B],F1] = F by A5,TARSKI:def 1;
A8: [[B,C],F2] = F by A6,TARSKI:def 1;
A9: [A1,B] = [A,A] by A7,XTUPLE_0:1;
A10: [A,A] = [B,C] by A8,XTUPLE_0:1;
A11: F1 = id A by A7,XTUPLE_0:1;
A12: F2 = id A by A8,XTUPLE_0:1;
A13: A1 = A by A9,XTUPLE_0:1;
A14: C = A by A10,XTUPLE_0:1;
F2*F1 = id A by A11,A12,FUNCT_2:17;
hence thesis by A13,A14,TARSKI:def 1;
end;
registration
cluster Categorial for strict Category;
existence
proof
set A = 1Cat(0,{0});
take 1Cat(A, [[A,A], id A]);
thus thesis by Th11;
end;
end;
theorem Th12:
for C being Categorial Category, a being Object of C holds a is Category
proof
let C be Categorial Category;
the carrier of C is categorial by Def6;
hence thesis;
end;
theorem Th13:
for C being Categorial Category, f being Morphism of C holds
dom f = f`11 & cod f = f`12
proof
let C be Categorial Category;
let f be Morphism of C;
reconsider A = dom f, B = cod f as Category by Th12;
ex F being Functor of A,B st f = [[A,B], F] by Def6;
hence thesis by MCART_1:85;
end;
definition
let C be Categorial Category;
let m be Morphism of C;
redefine func m`11 -> Category; :: redefines `11 (MCART_1, definition)
coherence
proof dom m = m`11 by Th13;
hence thesis by Th12;
end;
redefine func m`12 -> Category; :: redefines `12 (MCART_1, definition)
coherence
proof cod m = m`12 by Th13;
hence thesis by Th12;
end;
end;
theorem Th14:
for C1, C2 being Categorial Category st
the carrier of C1 = the carrier of C2 &
the carrier' of C1 = the carrier' of C2
holds the CatStr of C1 = the CatStr of C2
proof
let C1, C2 be Categorial Category;
assume that
A1: the carrier of C1 = the carrier of C2 and
A2: the carrier' of C1 = the carrier' of C2;
A3: dom the Source of C1 = the carrier' of C1 by FUNCT_2:def 1;
A4: dom the Source of C2 = the carrier' of C2 by FUNCT_2:def 1;
A5: dom the Target of C1 = the carrier' of C1 by FUNCT_2:def 1;
A6: dom the Target of C2 = the carrier' of C2 by FUNCT_2:def 1;
now
let x be object;
assume x in the carrier' of C1;
then reconsider m1 = x as Morphism of C1;
reconsider m2 = m1 as Morphism of C2 by A2;
thus (the Source of C1).x = dom m1 .= m1`11 by Th13
.= dom m2 by Th13
.= (the Source of C2).x;
end;
then
A7: the Source of C1 = the Source of C2 by A2,A3,A4;
A8: now
let x be object;
assume x in the carrier' of C1;
then reconsider m1 = x as Morphism of C1;
reconsider m2 = m1 as Morphism of C2 by A2;
thus (the Target of C1).x = cod m1 .= m1`12 by Th13
.= cod m2 by Th13
.= (the Target of C2).x;
end;
then
A9: the Target of C1 = the Target of C2 by A2,A5,A6;
A10: dom the Comp of C1 = dom the Comp of C2
proof
hereby
let x be object;
assume
A11: x in dom the Comp of C1;
then reconsider xx = x as
Element of [:the carrier' of C1, the carrier' of C1:];
reconsider y = xx as
Element of [:the carrier' of C2, the carrier' of C2:] by A2;
A12: y = [xx`1,xx`2] by MCART_1:21;
then dom(xx`1) = cod(xx`2) by A11,CAT_1:def 6;
then dom(y`1) = cod(y`2) by A8,A7;
hence x in dom the Comp of C2 by A12,CAT_1:def 6;
end;
let x be object;
assume
A13: x in dom the Comp of C2;
then reconsider xx = x as
Element of [:the carrier' of C1, the carrier' of C1:] by A2;
reconsider y = xx as
Element of [:the carrier' of C2, the carrier' of C2:] by A2;
A14: xx = [y`1,y`2] by MCART_1:21;
then dom(y`1) = cod(y`2) by A13,CAT_1:def 6;
then dom(xx`1) = cod(xx`2) by A8,A7;
hence thesis by A14,CAT_1:def 6;
end;
now
let x,y be object;
assume
A15: [x,y] in dom the Comp of C1;
then reconsider g1 = x, h1 = y as Morphism of C1 by ZFMISC_1:87;
reconsider g2 = g1, h2 = h1 as Morphism of C2 by A2;
reconsider a1 = dom g1, b1 = cod g1 as Category by Th12;
consider f1 being Functor of a1,b1 such that
A16: g1 = [[a1,b1],f1] by Def6;
reconsider c1 = dom h1, d1 = cod h1 as Category by Th12;
consider i1 being Functor of c1,d1 such that
A17: h1 = [[c1,d1],i1] by Def6;
A18: a1 = d1 by A15,CAT_1:15;
thus (the Comp of C1).(x,y) = g1(*)h1 by A15,CAT_1:def 1
.= [[c1,b1],f1*i1] by A16,A17,A18,Def6
.= g2(*)h2 by A16,A17,A18,Def6
.= (the Comp of C2).(x,y) by A10,A15,CAT_1:def 1;
end;
then the Comp of C1 = the Comp of C2 by A2,A10,BINOP_1:20;
hence thesis by A1,A2,A7,A9;
end;
registration
let C be Categorial Category;
cluster -> Categorial for Subcategory of C;
coherence
proof
let D be Subcategory of C;
A1: the carrier of C is categorial by Def6;
thus the carrier of D is categorial
proof
let x be Object of D;
x is Object of C by CAT_2:6;
hence thesis by A1;
end;
hereby
let a be Object of D, A be Category;
reconsider b = a as Object of C by CAT_2:6;
assume a = A;
then [[A,A], id A] = id b by Def6;
hence id a = [[A,A], id A] by CAT_2:def 4;
end;
hereby
let m be Morphism of D;
reconsider m9 = m as Morphism of C by CAT_2:8;
let a,b be Category;
assume that
A2: a = dom m and
A3: b = cod m;
A4: dom m9 = a by A2,CAT_2:9;
cod m9 = b by A3,CAT_2:9;
hence ex F being Functor of a,b st m = [[a,b], F] by A4,Def6;
end;
let m1,m2 be Morphism of D;
let a,b,c be Category;
reconsider m19 = m1, m29 = m2 as Morphism of C by CAT_2:8;
let f be Functor of a,b;
let g be Functor of b,c;
assume that
A5: m1 = [[a,b],f] and
A6: m2 = [[b,c],g];
A7: dom m2 = dom m29 by CAT_2:9;
A8: cod m1 = cod m19 by CAT_2:9;
A9: dom m29 = m2`11 by Th13;
A10: cod m19 = m1 `12 by Th13;
A11: dom m2 = b by A6,A7,A9,MCART_1:85;
cod m1 = b by A5,A8,A10,MCART_1:85;
hence m2(*)m1 = m29(*)m19 by A11,CAT_2:11
.= [[a,c],g*f] by A5,A6,Def6;
end;
end;
theorem Th15:
for C,D being Categorial Category st the carrier' of C c= the carrier' of D
holds C is Subcategory of D
proof
let C,D be Categorial Category;
assume
A1: the carrier' of C c= the carrier' of D;
thus the carrier of C c= the carrier of D
proof
let x be object;
assume x in the carrier of C;
then reconsider a = x as Object of C;
reconsider i = id a as Morphism of D by A1;
A2: dom i = i`11 by Th13;
dom id a = i`11 by Th13;
hence thesis by A2;
end;
hereby
let a,b be Object of C, a9,b9 be Object of D;
assume that
A3: a = a9 and
A4: b = b9;
thus Hom(a,b) c= Hom(a9,b9)
proof
let x be object;
assume x in Hom(a,b);
then consider f being Morphism of C such that
A5: x = f and
A6: dom f = a and
A7: cod f = b;
reconsider A = a, B = b as Category by Th12;
A8: ex F being Functor of A,B st ( f = [[A,B], F]) by A6,A7,Def6;
reconsider f as Morphism of D by A1;
A9: dom f = f`11 by Th13;
A10: cod f = f`12 by Th13;
A11: f`11 = A by A8,MCART_1:85;
f`12 = B by A8,MCART_1:85;
hence thesis by A3,A4,A5,A9,A10,A11;
end;
end;
A12: dom the Comp of C c= dom the Comp of D
proof
let x be object;
assume
A13: x in dom the Comp of C;
then reconsider g = x`1, f = x`2 as Morphism of C by MCART_1:10;
reconsider g9 = g, f9 = f as Morphism of D by A1;
A14: x = [g,f] by A13,MCART_1:21;
then
A15: dom g = cod f by A13,CAT_1:15;
A16: dom g = g`11 by Th13;
A17: dom g9 = g `11 by Th13;
A18: cod f = f`12 by Th13;
cod f9 = f`12 by Th13;
hence thesis by A14,A15,A16,A17,A18,CAT_1:15;
end;
now
let x be object;
assume
A19: x in dom the Comp of C;
then reconsider g = x`1, f = x`2 as Morphism of C by MCART_1:10;
reconsider g9 = g, f9 = f as Morphism of D by A1;
A20: x = [g,f] by A19,MCART_1:21;
A21: dom g = g`11 by Th13;
cod g = g`12 by Th13;
then consider G being Functor of g`11, g`12 such that
A22: g = [[g`11,g`12],G] by A21,Def6;
A23: dom f = f`11 by Th13;
cod f = dom g by A19,A20,CAT_1:15;
then consider F being Functor of f`11, g`11 such that
A24: f = [[f`11,g`11],F] by A21,A23,Def6;
thus (the Comp of C).x = (the Comp of C).(g,f) by A19,MCART_1:21
.= g(*)f by A19,A20,CAT_1:def 1
.= [[f`11,g`12],G*F] by A22,A24,Def6
.= g9(*)f9 by A22,A24,Def6
.= (the Comp of D).(g,f) by A12,A19,A20,CAT_1:def 1
.= (the Comp of D).x by A19,MCART_1:21;
end;
hence the Comp of C c= the Comp of D by A12,GRFUNC_1:2;
let a be Object of C, a9 be Object of D;
assume
A25: a = a9;
reconsider A = a as Category by Th12;
thus id a = [[A,A], id A] by Def6
.= id a9 by A25,Def6;
end;
definition
let a be object such that
A1: a is Category;
func cat a -> Category equals
: Def7:
a;
correctness by A1;
end;
theorem Th16:
for C being Categorial Category, c being Object of C holds cat c = c
proof
let C be Categorial Category, c be Object of C;
the carrier of C is categorial by Def6;
then c is Category;
hence thesis by Def7;
end;
definition
let C be Categorial Category;
let m be Morphism of C;
redefine func m`2 -> Functor of cat dom m, cat cod m; :: redefines `2 (XTUPLE_0, definition)
coherence
proof the carrier of C is categorial by Def6;
then reconsider A = dom m, B = cod m as Category;
consider F being Functor of A, B such that
A1: m = [[A,B], F] by Def6;
A2: m`2 = F by A1;
cat A = A by Def7;
hence thesis by A2,Def7;
end;
end;
theorem Th17:
for X being categorial non empty set, Y being non empty set st
(for A,B,C being Element of X
for F being Functor of A,B, G being Functor of B,C st
F in Y & G in Y holds G*F in Y) & (for A being Element of X holds id A in Y)
ex C being strict Categorial Category st the carrier of C = X &
for A,B being Element of X, F being Functor of A,B holds
[[A,B],F] is Morphism of C iff F in Y
proof
let X be categorial non empty set, Y be non empty set such that
A1: for A,B,C being Element of X
for F being Functor of A,B, G being Functor of B,C st
F in Y & G in Y holds G*F in Y and
A2: for A being Element of X holds id A in Y;
set B = {b where b is Element of Y: b is Function};
set a = the Element of X;
id a in Y by A2;
then id a in B;
then reconsider B as non empty set;
B is functional
proof
let x be object;
assume x in B;
then ex b being Element of Y st x = b & b is Function;
hence thesis;
end;
then reconsider B as non empty functional set;
reconsider A = X as non empty categorial set;
defpred P[Element of A, Element of A, set] means $3 is Functor of $1, $2;
deffunc F(Function,Function) = $1 * $2;
A3: for a,b,c being Element of A, f,g being Element of B st
P[a,b,f] & P[b,c,g] holds F(g,f) in B & P[a,c,F(g,f)]
proof
let a,b,c be Element of A, f,g be Element of B;
assume that
A4: P[a,b,f] and
A5: P[b,c,g];
reconsider f as Functor of a,b by A4;
reconsider g as Functor of b,c by A5;
A6: f in B;
A7: g in B;
A8: ex b being Element of Y st f = b & b is Function by A6;
ex b being Element of Y st g = b & b is Function by A7;
then g*f in Y by A1,A8;
hence thesis;
end;
A9: for a being Element of A ex f being Element of B st P[a,a,f] &
for b being Element of A, g being Element of B holds
(P[a,b,g] implies F(g,f) = g) & (P[b,a,g] implies F(f,g) = g)
proof
let a be Element of A;
reconsider f = id a as Element of Y by A2;
f in B;
then reconsider f as Element of B;
take f;
thus P[a,a,f];
let b be Element of A, g be Element of B;
thus P[a,b,g] implies g*f = g by FUNCT_2:17;
assume P[b,a,g];
then reconsider G = g as Functor of b,a;
(id a)*G = G by FUNCT_2:17;
hence thesis;
end;
A10: for a,b,c,d being Element of A, f,g,h being Element of B st
P[a,b,f] & P[b,c,g] & P[c,d,h] holds F(h, F(g,f)) = F(F(h,g), f)
by RELAT_1:36;
consider C being strict with_triple-like_morphisms Category such that
A11: the carrier of C = A &
(for a,b being Element of A, f being Element of B st
P[a,b,f] holds [[a,b],f] is Morphism of C) & (for m being Morphism of C
ex a,b being Element of A, f being Element of B st
m = [[a,b],f] & P[a,b,f]) &
for m1,m2 being (Morphism of C), a1,a2,a3 being Element of A,
f1,f2 being Element of B st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2]
holds m2(*)m1 = [[a1,a3], F(f2,f1)] from CatEx(A3,A9,A10);
C is Categorial
proof
thus the carrier of C is categorial by A11;
hereby
let a be Object of C, D be Category;
assume
A12: a = D;
then id D in Y by A2,A11;
then id D in B;
then reconsider f = id D as Element of B;
reconsider x = a as Element of A by A11;
reconsider F = [[x,x], f] as Morphism of C by A11,A12;
consider b,c being Element of A, g being Element of B such that
A13: id a = [[b,c],g] and
A14: P[b,c,g] by A11;
A15: dom id a = (id a)`11 by Th2;
A16: (id a)`11 = b by A13,MCART_1:85;
cod F = F`12 by Th2
.= x by MCART_1:85;
then F = (id a)(*)F by CAT_1:21
.= [[x,c], g*id the carrier' of D] by A11,A13,A15,A16
.= [[x,c], g] by A12,A14,A15,A16,FUNCT_2:17;
hence id a = [[D,D], id D] by A12,A13,A15,MCART_1:85;
end;
hereby
let m be Morphism of C;
consider a,b being Element of A, f being Element of B such that
A17: m = [[a,b],f] and
A18: P[a,b,f] by A11;
A19: dom m = m`11 by Th2;
A20: cod m = m`12 by Th2;
A21: dom m = a by A17,A19,MCART_1:85;
cod m = b by A17,A20,MCART_1:85;
hence for A,B being Category st A = dom m & B = cod m
ex F being Functor of A,B st m = [[A,B], F] by A17,A18,A21;
end;
let m1,m2 be Morphism of C;
consider a1,b1 being Element of A, f1 being Element of B such that
A22: m1 = [[a1,b1],f1] and P[a1,b1,f1] by A11;
consider a2,b2 being Element of A, f2 being Element of B such that
A23: m2 = [[a2,b2],f2] and P[a2,b2,f2] by A11;
let A,B,C be Category;
let F be Functor of A,B;
let G be Functor of B,C;
assume that
A24: m1 = [[A,B],F] and
A25: m2 = [[B,C],G];
A26: [A,B] = [a1,b1] by A22,A24,XTUPLE_0:1;
A27: [B,C] = [a2,b2] by A23,A25,XTUPLE_0:1;
A28: f1 = F by A22,A24,XTUPLE_0:1;
A29: f2 = G by A23,A25,XTUPLE_0:1;
A30: A = a1 by A26,XTUPLE_0:1;
A31: B = b1 by A26,XTUPLE_0:1;
C = b2 by A27,XTUPLE_0:1;
hence thesis by A11,A22,A25,A28,A29,A30,A31;
end;
then reconsider C as Categorial strict Category;
take C;
thus the carrier of C = X by A11;
let A9,B9 be Element of X, F be Functor of A9,B9;
hereby
assume [[A9,B9],F] is Morphism of C;
then reconsider m = [[A9,B9],F] as Morphism of C;
consider a,b being Element of A, f being Element of B such that
A32: m = [[a,b],f] and P[a,b,f] by A11;
m`2 = f by A32;
then F in B;
then ex b being Element of Y st F = b & b is Function;
hence F in Y;
end;
assume F in Y;
then F in B;
hence thesis by A11;
end;
theorem Th18:
for X being categorial non empty set, Y being non empty set
for C1, C2 being strict Categorial Category st the carrier of C1 = X &
(for A,B being Element of X, F being Functor of A,B holds
[[A,B],F] is Morphism of C1 iff F in Y) & the carrier of C2 = X &
(for A,B being Element of X, F being Functor of A,B holds
[[A,B],F] is Morphism of C2 iff F in Y) holds C1 = C2
proof
let X be categorial non empty set, Y be non empty set;
let C1, C2 be strict Categorial Category such that
A1: the carrier of C1 = X and
A2: for A,B being Element of X, F being Functor of A,B holds
[[A,B],F] is Morphism of C1 iff F in Y and
A3: the carrier of C2 = X and
A4: for A,B being Element of X, F being Functor of A,B holds
[[A,B],F] is Morphism of C2 iff F in Y;
the carrier' of C1 = the carrier' of C2
proof
hereby
let x be object;
assume x in the carrier' of C1;
then reconsider m = x as Morphism of C1;
reconsider a = dom m, b = cod m as Category by Th12;
consider f being Functor of a,b such that
A5: m = [[a,b],f] by Def6;
f in Y by A1,A2,A5;
then x is Morphism of C2 by A1,A4,A5;
hence x in the carrier' of C2;
end;
let x be object;
assume x in the carrier' of C2;
then reconsider m = x as Morphism of C2;
reconsider a = dom m, b = cod m as Category by Th12;
consider f being Functor of a,b such that
A6: m = [[a,b],f] by Def6;
f in Y by A3,A4,A6;
then x is Morphism of C1 by A2,A3,A6;
hence thesis;
end;
hence thesis by A1,A3,Th14;
end;
definition
let IT be Categorial Category;
attr IT is full means
:Def8:
for a,b being Category st a is Object of IT & b is Object of IT
for F being Functor of a, b holds [[a,b],F] is Morphism of IT;
end;
registration
cluster full for Categorial strict Category;
existence
proof
set A = 1Cat(0,{0});
reconsider C = 1Cat(A, [[A,A], id A]) as Categorial strict Category
by Th11;
take C;
let a,b be Category;
assume that
A1: a is Object of C and
A2: b is Object of C;
let F be Functor of a, b;
A3: a = A by A1,TARSKI:def 1;
A4: b = A by A2,TARSKI:def 1;
then id A = F by A3,FUNCT_2:51;
hence thesis by A3,A4,TARSKI:def 1;
end;
end;
theorem
for C1,C2 being full Categorial Category st
the carrier of C1 = the carrier of C2 holds
the CatStr of C1 = the CatStr of C2
proof
let C1, C2 be full Categorial Category;
assume
A1: the carrier of C1 = the carrier of C2;
reconsider A = the carrier of C1 as categorial non empty set by Def6;
set B = the set of all m`2 where m is Morphism of C1;
set m = the Morphism of C1;
m`2 in B;
then reconsider B as non empty set;
reconsider D1 = the CatStr of C1, D2 = the CatStr of C2 as strict Category
by Th1;
A2: D1 is Categorial by Th10;
A3: D2 is Categorial by Th10;
A4: now
let a,b be Element of A, F be Functor of a,b;
reconsider m = [[a,b], F] as Morphism of C1 by Def8;
m`2 = F;
hence [[a,b],F] is Morphism of the CatStr of C1 iff F in B;
end;
now
let a,b be Element of A, F be Functor of a,b;
reconsider a9 = a, b9 = b as Object of C2 by A1;
A5: cat a9 = a by Th16;
cat b9 = b by Th16;
then reconsider m2 = [[a,b], F] as Morphism of C2 by A5,Def8;
reconsider m = [[a,b], F] as Morphism of C1 by Def8;
A6: m`2 = F;
m2 = m2;
hence [[a,b],F] is Morphism of the CatStr of C2 iff F in B by A6;
end;
hence thesis by A1,A2,A3,A4,Th18;
end;
theorem Th20:
for A being categorial non empty set
ex C being full Categorial strict Category st the carrier of C = A
proof
let AA be categorial non empty set;
set dFF = the set of all
Funct(a,b) where a is Element of AA, b is Element of AA;
set a = the Element of AA,f = the Functor of a,a;
A1: f in Funct(a,a) by CAT_2:def 2;
Funct(a,a) in dFF;
then reconsider FF = union dFF as non empty set by A1,TARSKI:def 4;
A2: now
let A,B,C be Element of AA;
let F be Functor of A,B, G be Functor of B,C;
assume that F in FF and G in FF;
A3: G*F in Funct(A,C) by CAT_2:def 2;
Funct(A,C) in dFF;
hence G*F in FF by A3,TARSKI:def 4;
end;
now
let A be Element of AA;
A4: id A in Funct(A,A) by CAT_2:def 2;
Funct(A,A) in dFF;
hence id A in FF by A4,TARSKI:def 4;
end;
then consider C being strict Categorial Category such that
A5: the carrier of C = AA and
A6: for A,B being Element of AA, F being Functor of A,B holds [[A,B],F]
is Morphism of C iff F in FF
by A2,Th17;
C is full
proof
let a,b be Category;
assume that
A7: a is Object of C and
A8: b is Object of C;
reconsider A = a, B = b as Element of AA by A5,A7,A8;
let F be Functor of a, b;
A9: F in Funct(A,B) by CAT_2:def 2;
Funct(A,B) in dFF;
then F in FF by A9,TARSKI:def 4;
then [[A,B], F] is Morphism of C by A6;
hence thesis;
end;
hence thesis by A5;
end;
theorem Th21:
for C being Categorial Category, D being full Categorial Category st
the carrier of C c= the carrier of D holds C is Subcategory of D
proof
let C be Categorial Category;
let D be full Categorial Category;
assume
A1: the carrier of C c= the carrier of D;
the carrier' of C c= the carrier' of D
proof
let x be object;
assume x in the carrier' of C;
then reconsider x as Morphism of C;
reconsider y1 = dom x, y2 = cod x as Category by Th12;
consider F being Functor of y1,y2 such that
A2: x = [[y1,y2], F] by Def6;
A3: y1 is Object of D by A1;
y2 is Object of D by A1;
then [[y1,y2], F] is Morphism of D by A3,Def8;
hence thesis by A2;
end;
hence thesis by Th15;
end;
theorem
for C being Category, D1,D2 being Categorial Category
for F1 being Functor of C,D1 for F2 being Functor of C,D2 st
F1 = F2 holds Image F1 = Image F2
proof
let C be Category, D1,D2 be Categorial Category;
let F1 be Functor of C,D1;
let F2 be Functor of C,D2;
assume
A1: F1 = F2;
reconsider DD = (the carrier of D1) \/ the carrier of D2 as non empty set;
DD is categorial
proof
let d be Element of DD;
d is Object of D1 or d is Object of D2 by XBOOLE_0:def 3;
hence thesis by Th12;
end;
then reconsider DD = (the carrier of D1) \/ the carrier of D2 as
non empty categorial set;
consider D being full Categorial strict Category such that
A2: the carrier of D = DD by Th20;
reconsider D1, D2 as Subcategory of D by A2,Th21,XBOOLE_1:7;
reconsider F1 as Functor of C,D1;
reconsider F2 as Functor of C,D2;
rng F1 c= the carrier' of D1;
then F1 = (incl D1)*F1 by RELAT_1:53;
then reconsider G1 = F1 as Functor of C,D;
Image F1 = Image G1 by Th9
.= Image F2 by A1,Th9;
hence thesis;
end;
begin :: Slice category
definition
let C be Category;
let o be Object of C;
func Hom o -> Subset of the carrier' of C equals
(the Target of C)"{o};
coherence;
func o Hom -> Subset of the carrier' of C equals
(the Source of C)"{o};
coherence;
end;
registration
let C be Category;
let o be Object of C;
cluster Hom o -> non empty;
coherence
proof
A1: (the Target of C).id o = cod id o .= o;
A2: o in {o} by TARSKI:def 1;
dom the Target of C = the carrier' of C by FUNCT_2:def 1;
hence thesis by A1,A2,FUNCT_1:def 7;
end;
cluster o Hom -> non empty;
coherence
proof
A3: (the Source of C).id o = dom id o .= o;
A4: o in {o} by TARSKI:def 1;
dom the Source of C = the carrier' of C by FUNCT_2:def 1;
hence thesis by A3,A4,FUNCT_1:def 7;
end;
end;
theorem Th23:
for C being Category, a being Object of C, f being Morphism of C holds
f in Hom a iff cod f = a
proof
let C be Category, a be Object of C, f be Morphism of C;
cod f in {a} iff cod f = a by TARSKI:def 1;
hence thesis by FUNCT_2:38;
end;
theorem Th24:
for C being Category, a being Object of C, f being Morphism of C holds
f in a Hom iff dom f = a
proof
let C be Category, a be Object of C, f be Morphism of C;
dom f in {a} iff dom f = a by TARSKI:def 1;
hence thesis by FUNCT_2:38;
end;
theorem
for C being Category, a,b being Object of C holds
Hom(a,b) = (a Hom) /\ (Hom b)
proof
let C be Category, a,b be Object of C;
hereby
let x be object;
assume
A1: x in Hom(a,b);
then reconsider f = x as Morphism of C;
A2: dom f = a by A1,CAT_1:1;
A3: cod f = b by A1,CAT_1:1;
A4: f in a Hom by A2,Th24;
f in Hom b by A3,Th23;
hence x in (a Hom) /\ (Hom b) by A4,XBOOLE_0:def 4;
end;
let x be object;
assume
A5: x in (a Hom) /\ (Hom b);
then
A6: x in a Hom by XBOOLE_0:def 4;
A7: x in Hom b by A5,XBOOLE_0:def 4;
reconsider f = x as Morphism of C by A5;
A8: dom f = a by A6,Th24;
cod f = b by A7,Th23;
hence thesis by A8;
end;
theorem
for C being Category, f being Morphism of C holds
f in (dom f) Hom & f in Hom (cod f) by Th23,Th24;
theorem Th27:
for C being Category, f being (Morphism of C), g being Element of Hom dom f
holds f(*)g in Hom cod f
proof
let C be Category, f be (Morphism of C), g be Element of Hom dom f;
cod g = dom f by Th23;
then cod (f(*)g) = cod f by CAT_1:17;
hence thesis by Th23;
end;
theorem Th28:
for C being Category, f being (Morphism of C),
g being Element of (cod f) Hom holds g(*)f in (dom f) Hom
proof
let C be Category, f be (Morphism of C), g be Element of (cod f) Hom;
cod f = dom g by Th24;
then dom (g(*)f) = dom f by CAT_1:17;
hence thesis by Th24;
end;
definition
let C be Category, o be Object of C;
set A = Hom o;
set B = the carrier' of C;
defpred P[Element of A,Element of A,Element of B] means
dom $2 = cod $3 & $1 = $2(*)$3;
deffunc F((Morphism of C),Morphism of C) = $1(*)$2;
A1: for a,b,c being Element of A, f,g being Element of B st
P[a,b,f] & P[b,c,g] holds F(g,f) in B & P[a,c,F(g,f)]
proof
let a,b,c be Element of Hom o, f,g be Morphism of C;
assume that
A2: dom b = cod f and
A3: a = b(*)f and
A4: dom c = cod g and
A5: b = c(*)g;
dom g = cod f by A2,A4,A5,CAT_1:17;
hence thesis by A3,A4,A5,CAT_1:17,18;
end;
A6: for a being Element of A ex f being Element of B st P[a,a,f] &
for b being Element of A, g being Element of B holds
(P[a,b,g] implies F(g,f) = g) & (P[b,a,g] implies F(f,g) = g)
proof
let a be Element of Hom o;
take f = id dom a;
thus dom a = cod f & a = a(*)f by CAT_1:22;
let b be Element of Hom o, g be Morphism of C;
hereby
assume that
A7: dom b = cod g and
A8: a = b(*)g;
dom a = dom g by A7,A8,CAT_1:17;
hence g(*)f = g by CAT_1:22;
end;
thus thesis by CAT_1:21;
end;
A9: for a,b,c,d being Element of A, f,g,h being Element of B st
P[a,b,f] & P[b,c,g] & P[c,d,h] holds F(h, F(g,f)) = F(F(h,g), f)
proof
let a,b,c,d be Element of Hom o, f,g,h be Morphism of C;
assume that
A10: dom b = cod f and a = b(*)f and
A11: dom c = cod g and
A12: b = c(*)g and
A13: dom d = cod h and
A14: c = d(*)h;
A15: dom g = cod f by A10,A11,A12,CAT_1:17;
dom h = cod g by A11,A13,A14,CAT_1:17;
hence thesis by A15,CAT_1:18;
end;
func C-SliceCat(o) -> strict with_triple-like_morphisms Category means
:Def11: the carrier of it = Hom o &
(for a,b being Element of Hom o, f being Morphism of C st
dom b = cod f & a = b(*)f holds [[a,b],f] is Morphism of it) &
(for m being Morphism of it
ex a,b being Element of Hom o, f being Morphism of C st
m = [[a,b],f] & dom b = cod f & a = b(*)f) &
for m1,m2 being (Morphism of it), a1,a2,a3 being Element of Hom o,
f1,f2 being Morphism of C st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2]
holds m2(*)m1 = [[a1,a3], f2(*)f1];
existence
proof
thus ex F being with_triple-like_morphisms strict Category st
the carrier of F = A &
(for a,b being Element of A, f being Element of B st
P[a,b,f] holds [[a,b],f] is Morphism of F) & (for m being Morphism of F
ex a,b being Element of A, f being Element of B st
m = [[a,b],f] & P[a,b,f]) &
for m1,m2 being (Morphism of F), a1,a2,a3 being Element of A,
f1,f2 being Element of B st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2]
holds m2(*)m1 = [[a1,a3], F(f2,f1)] from CatEx(A1,A6,A9);
end;
uniqueness
proof
thus for C1, C2 being strict with_triple-like_morphisms Category st
the carrier of C1 = A &
(for a,b being Element of A, f being Element of B st
P[a,b,f] holds [[a,b],f] is Morphism of C1) & (for m being Morphism of C1
ex a,b being Element of A, f being Element of B st
m = [[a,b],f] & P[a,b,f]) &
(for m1,m2 being (Morphism of C1), a1,a2,a3 being Element of A,
f1,f2 being Element of B st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2]
holds m2(*)m1 = [[a1,a3], F(f2,f1)]) & the carrier of C2 = A &
(for a,b being Element of A, f being Element of B st
P[a,b,f] holds [[a,b],f] is Morphism of C2) & (for m being Morphism of C2
ex a,b being Element of A, f being Element of B st
m = [[a,b],f] & P[a,b,f]) &
for m1,m2 being (Morphism of C2), a1,a2,a3 being Element of A,
f1,f2 being Element of B st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2]
holds m2(*)m1 = [[a1,a3], F(f2,f1)] holds C1 = C2 from CatUniq(A6);
end;
set X = o Hom;
defpred R[Element of X,Element of X,Element of B] means
dom $3 = cod $1 & $2 = $3(*)$1;
A16: for a,b,c being Element of X, f,g being Element of B st
R[a,b,f] & R[b,c,g] holds F(g,f) in B & R[a,c,F(g,f)]
proof
let a,b,c be Element of o Hom, f,g be Morphism of C;
assume that
A17: dom f = cod a and
A18: f(*)a = b and
A19: dom g = cod b and
A20: g(*)b = c;
dom g = cod f by A17,A18,A19,CAT_1:17;
hence thesis by A17,A18,A20,CAT_1:17,18;
end;
A21: for a being Element of X ex f being Element of B st R[a,a,f] &
for b being Element of X, g being Element of B holds
(R[a,b,g] implies F(g,f) = g) & (R[b,a,g] implies F(f,g) = g)
proof
let a be Element of o Hom;
take f = id cod a;
thus dom f = cod a & f(*)a = a by CAT_1:21;
let b be Element of o Hom, g be Morphism of C;
thus dom g = cod a & g(*)a = b implies g(*)f = g by CAT_1:22;
assume that
A22: dom g = cod b and
A23: g(*)b = a;
cod g = cod a by A22,A23,CAT_1:17;
hence thesis by CAT_1:21;
end;
A24: for a,b,c,d being Element of X, f,g,h being Element of B st
R[a,b,f] & R[b,c,g] & R[c,d,h] holds F(h, F(g,f)) = F(F(h,g), f)
proof
let a,b,c,d be Element of o Hom, f,g,h be Morphism of C;
assume that
A25: dom f = cod a and
A26: f(*)a = b and
A27: dom g = cod b and
A28: g(*)b = c and
A29: dom h = cod c and h(*)c = d;
A30: dom g = cod f by A25,A26,A27,CAT_1:17;
dom h = cod g by A27,A28,A29,CAT_1:17;
hence thesis by A30,CAT_1:18;
end;
func o-SliceCat(C) -> strict with_triple-like_morphisms Category means
:
Def12: the carrier of it = o Hom &
(for a,b being Element of o Hom, f being Morphism of C st
dom f = cod a & f(*)a = b holds [[a,b],f] is Morphism of it) &
(for m being Morphism of it
ex a,b being Element of o Hom, f being Morphism of C st
m = [[a,b],f] & dom f = cod a & f(*)a = b) &
for m1,m2 being (Morphism of it), a1,a2,a3 being Element of o Hom,
f1,f2 being Morphism of C st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2]
holds m2(*)m1 = [[a1,a3], f2(*)f1];
existence
proof
thus ex F being with_triple-like_morphisms strict Category st
the carrier of F = X &
(for a,b being Element of X, f being Element of B st
R[a,b,f] holds [[a,b],f] is Morphism of F) & (for m being Morphism of F
ex a,b being Element of X, f being Element of B st
m = [[a,b],f] & R[a,b,f]) &
for m1,m2 being (Morphism of F), a1,a2,a3 being Element of X,
f1,f2 being Element of B st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2]
holds m2(*)m1 = [[a1,a3], F(f2,f1)] from CatEx(A16,A21,A24);
end;
uniqueness
proof
thus for C1, C2 being strict with_triple-like_morphisms Category st
the carrier of C1 = X &
(for a,b being Element of X, f being Element of B st
R[a,b,f] holds [[a,b],f] is Morphism of C1) & (for m being Morphism of C1
ex a,b being Element of X, f being Element of B st
m = [[a,b],f] & R[a,b,f]) &
(for m1,m2 being (Morphism of C1), a1,a2,a3 being Element of X,
f1,f2 being Element of B st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2]
holds m2(*)m1 = [[a1,a3], F(f2,f1)]) & the carrier of C2 = X &
(for a,b being Element of X, f being Element of B st
R[a,b,f] holds [[a,b],f] is Morphism of C2) & (for m being Morphism of C2
ex a,b being Element of X, f being Element of B st
m = [[a,b],f] & R[a,b,f]) &
for m1,m2 being (Morphism of C2), a1,a2,a3 being Element of X,
f1,f2 being Element of B st m1 = [[a1,a2],f1] & m2 = [[a2,a3],f2]
holds m2(*)m1 = [[a1,a3], F(f2,f1)] holds C1 = C2 from CatUniq(A21);
end;
end;
definition
let C be Category;
let o be Object of C;
let m be Morphism of C-SliceCat(o);
redefine func m`2 -> Morphism of C; :: redefines `2 (XTUPLE_0, definition)
coherence
proof
ex a,b being Element of Hom o, f being Morphism of C st ( m
= [[a,b],f])&( dom b = cod f)&( a = b(*)f) by Def11;
hence thesis;
end;
redefine func m`11 -> Element of Hom o; :: redefines `11 (MCART_1, definition)
coherence
proof
ex a,b being Element of Hom o, f being Morphism of C st ( m
= [[a,b],f])&( dom b = cod f)&( a = b(*)f) by Def11;
hence thesis by MCART_1:85;
end;
redefine func m`12 -> Element of Hom o; :: redefines `12 (MCART_1, definition)
coherence
proof
ex a,b being Element of Hom o, f being Morphism of C st ( m
= [[a,b],f])&( dom b = cod f)&( a = b(*)f) by Def11;
hence thesis by MCART_1:85;
end;
end;
theorem Th29:
for C being Category, a being Object of C, m being Morphism of C-SliceCat a
holds m = [[m`11,m`12],m`2] & dom m`12 = cod m`2 & m`11 = m`12(*)m`2 &
dom m = m`11 & cod m = m`12
proof
let C be Category, o be Object of C, m be Morphism of C-SliceCat o;
consider a,b being Element of Hom o, f being Morphism of C such that
A1: m = [[a,b],f] and
A2: dom b = cod f and
A3: a = b(*)f by Def11;
A4: m`11 = a by A1,MCART_1:85;
m`12 = b by A1,MCART_1:85;
hence thesis by A1,A2,A3,A4,Th2;
end;
theorem Th30:
for C being Category, o being Object of C, f being Element of Hom o
for a being Object of C-SliceCat o st a = f holds id a = [[a,a], id dom f]
proof
let C be Category, o be Object of C, f be Element of Hom o;
let a be Object of C-SliceCat o;
assume
A1: a = f;
consider b,c being Element of Hom o, g being Morphism of C such that
A2: id a = [[b,c], g] and
A3: dom c = cod g and b = c(*)g by Def11;
A4: cod id dom f = dom f;
f = f(*)id dom f by CAT_1:22;
then reconsider h = [[f,f], id dom f] as Morphism of C-SliceCat o by A4,Def11
;
A5: (id a)`11 = b by A2,MCART_1:85;
A6: (id a)`12 = c by A2,MCART_1:85;
A7: dom id a = b by A5,Th2;
A8: cod id a = c by A6,Th2;
A9: b = a by A7;
A10: c = a by A8;
dom h = h`11 by Th2
.= a by A1,MCART_1:85;
then h = h(*)id a by CAT_1:22
.= [[f,f], (id dom f)(*)g] by A1,A2,A9,A10,Def11
.= [[f,f], g] by A1,A3,A10,CAT_1:21;
hence thesis by A1,A2,A7,A10;
end;
definition
let C be Category;
let o be Object of C;
let m be Morphism of o-SliceCat(C);
redefine func m`2 -> Morphism of C; :: redefines `2 (XTUPLE_0, definition)
coherence
proof
ex a,b being Element of o Hom, f being Morphism of C st ( m
= [[a,b],f])&( dom f = cod a)&( f(*)a = b) by Def12;
hence thesis;
end;
redefine func m`11 -> Element of o Hom; :: redefines `11 (MCART_1, definition)
coherence
proof
ex a,b being Element of o Hom, f being Morphism of C st ( m
= [[a,b],f])&( dom f = cod a)&( f(*)a = b) by Def12;
hence thesis by MCART_1:85;
end;
redefine func m`12 -> Element of o Hom; :: redefines `12 (MCART_1, definition)
coherence
proof
ex a,b being Element of o Hom, f being Morphism of C st ( m
= [[a,b],f])&( dom f = cod a)&( f(*)a = b) by Def12;
hence thesis by MCART_1:85;
end;
end;
theorem Th31:
for C being Category, a being Object of C, m being Morphism of a-SliceCat C
holds m = [[m`11,m`12],m`2] & dom m`2 = cod m`11 & m`2(*)m`11 = m`12 &
dom m = m`11 & cod m = m`12
proof
let C be Category, o be Object of C, m be Morphism of o-SliceCat C;
consider a,b being Element of o Hom, f being Morphism of C such that
A1: m = [[a,b],f] and
A2: dom f = cod a and
A3: f(*)a = b by Def12;
A4: m`11 = a by A1,MCART_1:85;
m`12 = b by A1,MCART_1:85;
hence thesis by A1,A2,A3,A4,Th2;
end;
theorem Th32:
for C being Category, o being Object of C, f being Element of o Hom
for a being Object of o-SliceCat C st a = f holds id a = [[a,a], id cod f]
proof
let C be Category, o be Object of C, f be Element of o Hom;
let a be Object of o-SliceCat C;
assume
A1: a = f;
consider b,c being Element of o Hom, g being Morphism of C such that
A2: id a = [[b,c], g] and
A3: dom g = cod b and g(*)b = c by Def12;
A4: dom id cod f = cod f;
f = (id cod f)(*)f by CAT_1:21;
then reconsider h = [[f,f], id cod f] as Morphism of o-SliceCat C by A4,Def12
;
A5: (id a)`11 = b by A2,MCART_1:85;
A6: (id a)`12 = c by A2,MCART_1:85;
A7: dom id a = b by A5,Th2;
A8: cod id a = c by A6,Th2;
A9: b = a by A7;
A10: c = a by A8;
cod h = h`12 by Th2
.= a by A1,MCART_1:85;
then h = (id a)(*)h by CAT_1:21
.= [[f,f], g(*)id cod f] by A1,A2,A9,A10,Def12
.= [[f,f], g] by A1,A3,A9,CAT_1:22;
hence thesis by A1,A2,A8,A9;
end;
begin :: Functors Between Slice Categories
definition
let C be Category, f be Morphism of C;
func SliceFunctor f -> Functor of C-SliceCat dom f, C-SliceCat cod f means
:
Def13: for m being Morphism of C-SliceCat dom f holds
it.m = [[f(*)m`11, f(*)m`12], m`2];
existence
proof
set C1 = C-SliceCat dom f, C2 = C-SliceCat cod f;
deffunc f(Morphism of C1) = [[f(*)$1`11, f(*)$1`12], $1`2];
consider F being Function of
the carrier' of C1, the carrier' of [:[:C,C:],C:] such that
A1: for m being Morphism of C1 holds F.m = f(m) from FUNCT_2:sch 4;
A2: dom F = the carrier' of C1 by FUNCT_2:def 1;
rng F c= the carrier' of C2
proof
let x be object;
assume x in rng F;
then consider m being object such that
A3: m in dom F and
A4: x = F.m by FUNCT_1:def 3;
reconsider m as Morphism of C1 by A3;
A5: x = [[f(*)m`11, f(*)m`12], m`2] by A1,A4;
A6: dom m`12 = cod m`2 by Th29;
A7: m`11 = m`12(*)m`2 by Th29;
A8: cod m`12 = dom f by Th23;
A9: f(*)m`11 in Hom cod f by Th27;
A10: f(*)m`12 in Hom cod f by Th27;
A11: dom (f(*)m`12) = cod m`2 by A6,A8,CAT_1:17;
f(*)m`11 = f(*)m`12(*)m`2 by A6,A7,A8,CAT_1:18;
then x is Morphism of C2 by A5,A9,A10,A11,Def11;
hence thesis;
end;
then reconsider F as Function of the carrier' of C1, the carrier' of C2
by A2,FUNCT_2:def 1,RELSET_1:4;
A12: now
let c be Object of C1;
reconsider g = c as Element of Hom dom f by Def11;
reconsider h = f(*)g as Element of Hom cod f by Th27;
reconsider d = h as Object of C2 by Def11;
take d;
A13: id c = [[c,c], id dom g] by Th30;
A14: id d = [[d,d], id dom h] by Th30;
A15: (id c)`11 = c by A13,MCART_1:85;
A16: (id c)`12 = c by A13,MCART_1:85;
A17: (id c)`2 = id dom g by A13;
A18: cod g = dom f by Th23;
thus F.(id c) = [[h, h], (id c)`2] by A1,A15,A16
.= id d by A14,A17,A18,CAT_1:17;
end;
A19: now
let m be Morphism of C1;
reconsider g1 = f(*)m`11, g2 = f(*)m`12 as Element of Hom cod f by Th27;
A20: dom f = cod m`11 by Th23;
A21: dom f = cod m`12 by Th23;
F.m = [[g1,g2], m`2] by A1;
then dom (F.m) = [[g1,g2], m`2]`11 by Th29
.= g1 by MCART_1:85;
then
A22: id dom (F.m) = [[g1,g1], id dom g1] by Th30;
dom m = m`11 by Th29;
then
A23: id dom m = [[m`11,m`11], id dom m`11] by Th30;
then
A24: (id dom m)`11 = m`11 by MCART_1:85;
A25: (id dom m)`12 = m`11 by A23,MCART_1:85;
(id dom m)`2 = id dom m`11 by A23;
hence F.(id dom m) = [[g1,g1], id dom m`11] by A1,A24,A25
.= id dom (F.m) by A20,A22,CAT_1:17;
F.m = [[g1,g2], m`2] by A1;
then cod (F.m) = [[g1,g2], m`2]`12 by Th29
.= g2 by MCART_1:85;
then
A26: id cod (F.m) = [[g2,g2], id dom g2] by Th30;
cod m = m`12 by Th29;
then
A27: id cod m = [[m`12,m`12], id dom m`12] by Th30;
then
A28: (id cod m)`11 = m`12 by MCART_1:85;
A29: (id cod m)`12 = m`12 by A27,MCART_1:85;
(id cod m)`2 = id dom m`12 by A27;
hence F.(id cod m) = [[g2,g2], id dom m`12] by A1,A28,A29
.= id cod (F.m) by A21,A26,CAT_1:17;
end;
now
let f1,f2 be Morphism of C1;
consider a1,b1 being Element of Hom dom f, g1 being Morphism of C such
that
A30: f1 = [[a1,b1], g1] and dom b1 = cod g1
and a1 = b1(*)g1 by Def11;
consider a2,b2 being Element of Hom dom f, g2 being Morphism of C such
that
A31: f2 = [[a2,b2], g2] and dom b2 = cod g2
and a2 = b2(*)g2 by Def11;
A32: dom f2 = f2`11 by Th2;
A33: cod f1 = f1`12 by Th2;
A34: dom f2 = a2 by A31,A32,MCART_1:85;
A35: cod f1 = b1 by A30,A33,MCART_1:85;
reconsider ha1 = f(*)a1, ha2 = f(*)a2, hb1 = f(*)b1, hb2 = f(*)b2 as
Element of Hom cod f by Th27;
A36: f1`11 = a1 by A30,MCART_1:85;
A37: f1`12 = b1 by A30,MCART_1:85;
A38: f1`2 = g1 by A30;
A39: f2`11 = a2 by A31,MCART_1:85;
A40: f2`12 = b2 by A31,MCART_1:85;
A41: f2`2 = g2 by A31;
A42: F.f1 = [[ha1, hb1], g1] by A1,A36,A37,A38;
A43: F.f2 = [[ha2, hb2], g2] by A1,A39,A40,A41;
assume
A44: dom f2 = cod f1;
then
A45: f2(*)f1 = [[a1,b2], g2(*)g1] by A30,A31,A34,A35,Def11;
A46: (F.f2)(*)(F.f1) = [[ha1,hb2], g2(*)g1] by A34,A35,A42,A43,A44,Def11;
A47: (f2(*)f1)`11 = a1 by A45,MCART_1:85;
A48: (f2(*)f1)`12 = b2 by A45,MCART_1:85;
(f2(*)f1)`2 = g2(*)g1 by A45;
hence F.(f2(*)f1) = (F.f2)(*)(F.f1) by A1,A46,A47,A48;
end;
then reconsider F as Functor of C1, C2 by A12,A19,CAT_1:61;
take F;
thus thesis by A1;
end;
uniqueness
proof
let F1,F2 be Functor of C-SliceCat dom f, C-SliceCat cod f such that
A49: for m being Morphism of C-SliceCat dom f holds
F1.m = [[f(*)m`11, f(*)m`12], m`2] and
A50: for m being Morphism of C-SliceCat dom f holds
F2.m = [[f(*)m`11, f(*)m`12], m`2];
now
let m be Morphism of C-SliceCat dom f;
thus F1.m = [[f(*)m`11, f(*)m`12], m`2] by A49
.= F2.m by A50;
end;
hence thesis by FUNCT_2:63;
end;
func SliceContraFunctor f ->
Functor of (cod f)-SliceCat C, (dom f)-SliceCat C means
:
Def14: for m being Morphism of (cod f)-SliceCat C holds
it.m = [[m`11(*)f, m`12(*)f], m`2];
existence
proof
set C1 = (cod f)-SliceCat C, C2 = (dom f)-SliceCat C;
deffunc f(Morphism of C1) = [[$1`11(*)f, $1`12(*)f], $1`2];
consider F being Function of
the carrier' of C1, the carrier' of [:[:C,C:],C:] such that
A51: for m being Morphism of C1 holds F.m = f(m) from FUNCT_2:sch 4;
A52: dom F = the carrier' of C1 by FUNCT_2:def 1;
rng F c= the carrier' of C2
proof
let x be object;
assume x in rng F;
then consider m being object such that
A53: m in dom F and
A54: x = F.m by FUNCT_1:def 3;
reconsider m as Morphism of C1 by A53;
A55: x = [[m`11(*)f, m`12(*)f], m`2] by A51,A54;
A56: dom m`2 = cod m`11 by Th31;
A57: m`12 = m`2(*)m`11 by Th31;
A58: dom m`11 = cod f by Th24;
A59: m`11(*)f in (dom f)Hom by Th28;
A60: m`12(*)f in (dom f)Hom by Th28;
A61: cod (m`11(*)f) = dom m`2 by A56,A58,CAT_1:17;
m`12(*)f = m`2(*)(m`11(*)f) by A56,A57,A58,CAT_1:18;
then x is Morphism of C2 by A55,A59,A60,A61,Def12;
hence thesis;
end;
then reconsider F as Function of the carrier' of C1, the carrier' of C2
by A52,FUNCT_2:def 1,RELSET_1:4;
A62: now
let c be Object of C1;
reconsider g = c as Element of (cod f) Hom by Def12;
reconsider h = g(*)f as Element of (dom f) Hom by Th28;
reconsider d = h as Object of C2 by Def12;
take d;
A63: id c = [[c,c], id cod g] by Th32;
A64: id d = [[d,d], id cod h] by Th32;
A65: (id c)`11 = c by A63,MCART_1:85;
A66: (id c)`12 = c by A63,MCART_1:85;
A67: (id c)`2 = id cod g by A63;
A68: dom g = cod f by Th24;
thus F.(id c) = [[h, h], (id c)`2] by A51,A65,A66
.= id d by A64,A67,A68,CAT_1:17;
end;
A69: now
let m be Morphism of C1;
reconsider g1 = m`11(*)f, g2 = m`12(*)f as Element of (dom f) Hom
by Th28;
A70: cod f = dom m`11 by Th24;
A71: cod f = dom m`12 by Th24;
F.m = [[g1,g2], m`2] by A51;
then dom (F.m) = [[g1,g2], m`2]`11 by Th31
.= g1 by MCART_1:85;
then
A72: id dom (F.m) = [[g1,g1], id cod g1] by Th32;
dom m = m`11 by Th31;
then
A73: id dom m = [[m`11,m`11], id cod m`11] by Th32;
then
A74: (id dom m)`11 = m`11 by MCART_1:85;
A75: (id dom m)`12 = m`11 by A73,MCART_1:85;
(id dom m)`2 = id cod m`11 by A73;
hence F.(id dom m) = [[g1,g1], id cod m`11] by A51,A74,A75
.= id dom (F.m) by A70,A72,CAT_1:17;
F.m = [[g1,g2], m`2] by A51;
then cod (F.m) = [[g1,g2], m`2]`12 by Th31
.= g2 by MCART_1:85;
then
A76: id cod (F.m) = [[g2,g2], id cod g2] by Th32;
cod m = m`12 by Th31;
then
A77: id cod m = [[m`12,m`12], id cod m`12] by Th32;
then
A78: (id cod m)`11 = m`12 by MCART_1:85;
A79: (id cod m)`12 = m`12 by A77,MCART_1:85;
(id cod m)`2 = id cod m`12 by A77;
hence F.(id cod m) = [[g2,g2], id cod m`12] by A51,A78,A79
.= id cod (F.m) by A71,A76,CAT_1:17;
end;
now
let f1,f2 be Morphism of C1;
consider a1,b1 being Element of (cod f) Hom, g1 being Morphism of C such
that
A80: f1 = [[a1,b1], g1] and dom g1 = cod a1
and g1(*)a1 = b1 by Def12;
consider a2,b2 being Element of (cod f) Hom, g2 being Morphism of C such
that
A81: f2 = [[a2,b2], g2] and dom g2 = cod a2
and g2(*)a2 = b2 by Def12;
A82: dom f2 = f2`11 by Th2;
A83: cod f1 = f1`12 by Th2;
A84: dom f2 = a2 by A81,A82,MCART_1:85;
A85: cod f1 = b1 by A80,A83,MCART_1:85;
reconsider ha1 = a1(*)f, ha2 = a2(*)f, hb1 = b1(*)f, hb2 = b2(*)f as
Element of (dom f) Hom by Th28;
A86: f1`11 = a1 by A80,MCART_1:85;
A87: f1`12 = b1 by A80,MCART_1:85;
A88: f1`2 = g1 by A80;
A89: f2`11 = a2 by A81,MCART_1:85;
A90: f2`12 = b2 by A81,MCART_1:85;
A91: f2`2 = g2 by A81;
A92: F.f1 = [[ha1, hb1], g1] by A51,A86,A87,A88;
A93: F.f2 = [[ha2, hb2], g2] by A51,A89,A90,A91;
assume
A94: dom f2 = cod f1;
then
A95: f2(*)f1 = [[a1,b2], g2(*)g1] by A80,A81,A84,A85,Def12;
A96: (F.f2)(*)(F.f1) = [[ha1,hb2], g2(*)g1] by A84,A85,A92,A93,A94,Def12;
A97: (f2(*)f1)`11 = a1 by A95,MCART_1:85;
A98: (f2(*)f1)`12 = b2 by A95,MCART_1:85;
(f2(*)f1)`2 = g2(*)g1 by A95;
hence F.(f2(*)f1) = (F.f2)(*)(F.f1) by A51,A96,A97,A98;
end;
then reconsider F as Functor of C1, C2 by A62,A69,CAT_1:61;
take F;
thus thesis by A51;
end;
uniqueness
proof
let F1,F2 be Functor of (cod f)-SliceCat C, (dom f)-SliceCat C such that
A99: for m being Morphism of (cod f)-SliceCat C holds
F1.m = [[m`11(*)f, m`12(*)f], m`2] and
A100: for m being Morphism of (cod f)-SliceCat C holds
F2.m = [[m`11(*)f, m`12(*)f], m`2];
now
let m be Morphism of (cod f)-SliceCat C;
thus F1.m = [[m`11(*)f, m`12(*)f], m`2] by A99
.= F2.m by A100;
end;
hence thesis by FUNCT_2:63;
end;
end;
theorem
for C being Category, f,g being Morphism of C st dom g = cod f holds
SliceFunctor (g(*)f) = (SliceFunctor g)*(SliceFunctor f)
proof
let C be Category, f,g be Morphism of C;
assume
A1: dom g = cod f;
then
A2: dom (g(*)f) = dom f by CAT_1:17;
set A1 = C-SliceCat dom f, A3 = C-SliceCat cod g;
set F = SliceFunctor f;
reconsider G = SliceFunctor g as Functor of C-SliceCat cod f,A3 by A1;
reconsider GF = SliceFunctor (g(*)f) as Functor of A1,A3 by A1,A2,CAT_1:17;
now
let m be Morphism of A1;
A3: F.m = [[f(*)m`11, f(*)m`12], m`2] by Def13;
then
A4: (F.m)`11 = f(*)m`11 by MCART_1:85;
A5: (F.m)`12 = f(*)m`12 by A3,MCART_1:85;
A6: (F.m)`2 = m`2 by A3;
A7: dom f = cod m`11 by Th23;
A8: dom f = cod m`12 by Th23;
A9: g(*)(f(*)m`11) = g(*)f(*)m`11 by A1,A7,CAT_1:18;
A10: g(*)(f(*)m`12) = g(*)f(*)m`12 by A1,A8,CAT_1:18;
thus (G*F).m = G.(F.m) by FUNCT_2:15
.= [[g(*)(f(*)m`11), g(*)(f(*)m`12)], m`2] by A1,A4,A5,A6,Def13
.= GF.m by A2,A9,A10,Def13;
end;
hence thesis by FUNCT_2:63;
end;
theorem
for C being Category, f,g being Morphism of C st dom g = cod f holds
SliceContraFunctor (g(*)f) = (SliceContraFunctor f)*(SliceContraFunctor g)
proof
let C be Category, f,g be Morphism of C;
assume
A1: dom g = cod f;
then
A2: cod (g(*)f) = cod g by CAT_1:17;
set A1 = (dom f)-SliceCat C, A2 = (cod f)-SliceCat C;
set A3 = (cod g)-SliceCat C;
reconsider F=SliceContraFunctor f as Functor of A2,A1;
reconsider G = SliceContraFunctor g as Functor of A3,A2 by A1;
reconsider FG = SliceContraFunctor (g(*)f) as Functor of A3,A1 by A1,A2,
CAT_1:17;
now
let m be Morphism of A3;
A3: G.m = [[m`11(*)g, m`12(*)g], m`2] by Def14;
then
A4: (G.m)`11 = m`11(*)g by MCART_1:85;
A5: (G.m)`12 = m`12(*)g by A3,MCART_1:85;
A6: (G.m)`2 = m`2 by A3;
A7: cod g = dom m`11 by Th24;
A8: cod g = dom m`12 by Th24;
A9: m`11(*)(g(*)f) = m`11(*)g(*)f by A1,A7,CAT_1:18;
A10: m`12(*)(g(*)f) = m`12(*)g(*)f by A1,A8,CAT_1:18;
thus (F*G).m = F.(G.m) by FUNCT_2:15
.= [[m`11(*)g(*)f, m`12(*)g(*)f], m`2] by A4,A5,A6,Def14
.= FG.m by A2,A9,A10,Def14;
end;
hence thesis by FUNCT_2:63;
end;