:: Comma Category
:: by Grzegorz Bancerek and Agata Darmochwa\l
::
:: Received February 20, 1992
:: Copyright (c) 1992-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies CAT_1, STRUCT_0, FUNCT_1, XBOOLE_0, SUBSET_1, ZFMISC_1, TARSKI,
MCART_1, RELAT_1, GRAPH_1, PARTFUN1, CAT_2, FUNCOP_1, FUNCT_3, COMMACAT,
MONOID_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1,
FUNCT_2, BINOP_1, FUNCOP_1, STRUCT_0, GRAPH_1, CAT_1, CAT_2, MCART_1,
DOMAIN_1;
constructors DOMAIN_1, CAT_2, FUNCOP_1, RELSET_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, CAT_1, CAT_2, STRUCT_0, XTUPLE_0;
requirements SUBSET, BOOLE;
definitions TARSKI, XBOOLE_0;
equalities CAT_1, BINOP_1, FUNCOP_1, GRAPH_1;
theorems TARSKI, ZFMISC_1, MCART_1, FUNCT_1, FUNCT_2, CAT_1, CAT_2, GRFUNC_1,
RELSET_1, FUNCOP_1, XTUPLE_0;
schemes FUNCT_2, CLASSES1;
begin
deffunc obj(CatStr) = the carrier of $1;
deffunc morph(CatStr) = the carrier' of $1;
reserve y for set;
reserve C,D,E for Category,
c,c1,c2 for Object of C,
d,d1 for Object of D,
x for set,
f,f1 for (Morphism of E),
g,g1 for (Morphism of C),
h,h1 for (Morphism of D) ,
F for Functor of C,E,
G for Functor of D,E;
definition
let C,D,E;
let F be Functor of C,E, G be Functor of D,E;
given c1,d1,f1 such that
A1: f1 in Hom(F.c1,G.d1);
func commaObjs(F,G) -> non empty Subset of [:[:the carrier of C, the carrier
of D:], the carrier' of E:] equals
:Def1:
{[[c,d],f] : f in Hom(F.c,G.d)};
coherence
proof
A2: {[[c,d],f] : f in Hom(F.c,G.d)} c= [:[:the carrier of C, the carrier
of D:], the carrier' of E:]
proof
let x be object;
assume x in {[[c,d],f] : f in Hom(F.c,G.d)};
then ex c,d,f st x = [[c,d],f] & f in Hom(F.c,G.d);
hence thesis;
end;
[[c1,d1],f1] in {[[c,d],f] : f in Hom(F.c,G.d)} by A1;
hence thesis by A2;
end;
end;
reserve o,o1,o2 for Element of commaObjs(F,G);
theorem Th1:
(ex c,d,f st f in Hom(F.c,G.d)) implies o = [[o`11,o`12],o`2] & o
`2 in Hom(F.o`11,G.o`12) & dom o`2 = F.o`11 & cod o`2 = G.o`12
proof
assume ex c,d,f st f in Hom(F.c,G.d);
then
A1: commaObjs(F,G) = {[[c,d],f]: f in Hom(F.c,G.d)} by Def1;
o in commaObjs(F,G);
then consider c,d,f such that
A2: o = [[c,d],f] and
A3: f in Hom(F.c,G.d) by A1;
o`11 = c & o`12 = d by A2,MCART_1:85;
hence thesis by A2,A3,CAT_1:1;
end;
definition
let C,D,E,F,G;
given c1,d1,f1 such that
A1: f1 in Hom(F.c1,G.d1);
func commaMorphs(F,G) -> non empty Subset of [:[:commaObjs(F,G), commaObjs(F
,G):], [:the carrier' of C, the carrier' of D:]:] equals
:Def2:
{[[o1,o2], [g,h]] :
dom g = o1`11 & cod g = o2`11 & dom h = o1`12 & cod h = o2`12 &
(o2`2)(*)(F.g) = (G.h)(*)(o1`2)};
coherence
proof
commaObjs(F,G) = {[[c,d],f] : f in Hom(F.c,G.d)} by A1,Def1;
then [[c1,d1],f1] in commaObjs(F,G) by A1;
then reconsider o = [[c1,d1],f1] as Element of commaObjs(F,G);
set X = {[[o1,o2], [g,h]] : dom g = o1`11 & cod g = o2`11 & dom h = o1`12
& cod h = o2`12 & (o2`2)(*)(F.g) = (G.h)(*)(o1`2)};
A2: dom id d1 = d1 & cod id d1 = d1;
A3: o`1`1 = o`11 & o`1`2 = o`12 by MCART_1:def 14,def 15;
A4: X c= [:[:commaObjs(F,G), commaObjs(F,G):], [:the carrier' of C, the
carrier' of D:]:]
proof
let x be object;
assume x in X;
then ex g,h,o1,o2 st x = [[o1,o2], [g,h]] & dom g = o1`11 & cod g = o2
`11 & dom h = o1`12 & cod h = o2`12 & (o2`2)(*)(F.g) = (G.h)(*)(o1`2);
hence thesis;
end;
A5: [c1,d1]`2 = d1 & o`2 = f1;
cod f1 = G.d1 by A1,CAT_1:1;
then
A6: id(G.d1)(*)f1 = f1 by CAT_1:21;
dom f1 = F.c1 by A1,CAT_1:1;
then
A7: f1(*)id(F.c1) = f1 by CAT_1:22;
A8: F.id c1 = id(F.c1) & G.id d1 = id(G.d1) by CAT_1:71;
dom id c1 = c1 & cod id c1 = c1;
then [[o,o],[id c1,id d1]] in X by A2,A3,A5,A7,A6,A8;
hence thesis by A4;
end;
end;
reserve k,k1,k2,k9 for Element of commaMorphs(F,G);
definition
let C,D,E,F,G,k;
redefine func k`11 -> Element of commaObjs(F,G); :: redefines `11 (MCART_1, definition)
coherence
proof
thus k`11 is Element of commaObjs(F,G);
end;
redefine func k`12 -> Element of commaObjs(F,G); :: redefines `12 (MCART_1, definition)
coherence
proof
thus k`12 is Element of commaObjs(F,G);
end;
end;
theorem Th2:
(ex c,d,f st f in Hom(F.c,G.d)) implies k = [[k`11,k`12], [k`21,k
`22]] & dom k`21 = k`11`11 & cod k`21 = k`12`11 & dom k`22 = k`11`12 & cod k`22
= k`12`12 & (k`12`2)(*)(F.k`21) = (G.k`22)(*)(k`11`2)
proof
assume ex c,d,f st f in Hom(F.c,G.d);
then
A1: commaMorphs(F,G) = {[[o1,o2], [g,h]] : dom g = o1`11 & cod g = o2`11 &
dom h = o1`12 & cod h = o2`12 & (o2`2)(*)(F.g) = (G.h)(*)(o1`2)} by Def2;
k in commaMorphs(F,G);
then consider g,h,o1,o2 such that
A2: k = [[o1,o2], [g,h]] and
A3: dom g = o1`11 & cod g = o2`11 & dom h = o1`12 & cod h = o2`12 & (o2
`2)(*)(F.g) = (G.h)(*)(o1`2) by A1;
A4: k`21 = g by A2,MCART_1:85;
k`11 = o1 & k`12 = o2 by A2,MCART_1:85;
hence thesis by A2,A3,A4,MCART_1:85;
end;
definition
let C,D,E,F,G,k1,k2;
given c1,d1,f1 such that
A1: f1 in Hom(F.c1,G.d1);
assume
A2: k1`12 = k2`11;
func k2*k1 -> Element of commaMorphs(F,G) equals
:Def3:
[[k1`11,k2`12],[k2`21(*)k1`21,k2`22(*)k1`22]];
coherence
proof
set k22 = k2`22(*)k1`22;
set k21 = k2`21(*)k1`21;
A3: F.cod k2`21 = cod (F.k2`21) & dom (F.k2`21) = F.dom k2`21 by CAT_1:72;
A4: cod (F.k1`21) = F.cod k1`21 by CAT_1:72;
A5: cod k1`12`2 = G.k1`12`12 by A1,Th1;
A6: dom k1`22 = k1`11`12 by A1,Th2;
A7: (k2`12`2)(*)(F.k2`21) = (G.k2`22)(*)(k2`11`2) & dom k2`12`2 = F.k2`12`11
by A1,Th1,Th2;
A8: cod (G.k1`22) = G.cod k1`22 by CAT_1:72;
A9: (k1`12`2)(*)(F.k1`21) = (G.k1`22)(*)(k1`11`2) & dom k1`12`2 = F.k1`12`11
by A1,Th1,Th2;
A10: dom (G.k2`22) = G.dom k2`22 by CAT_1:72;
A11: cod k1`11`2 = G.k1`11`12 & dom (G.k1`22) = G.dom k1`22 by A1,Th1,CAT_1:72;
A12: cod k2`21 = k2`12`11 by A1,Th2;
A13: commaMorphs(F,G) = {[[o1,o2], [g,h]] : dom g = o1`11 & cod g = o2`11
& dom h = o1`12 & cod h = o2`12 & (o2`2)(*)(F.g) = (G.h)(*)(o1`2)}
by A1,Def2;
A14: dom k2`22 = k2`11`12 by A1,Th2;
A15: cod k1`22 = k1`12`12 by A1,Th2;
then
A16: dom k22 = dom k1`22 & cod k22 = cod k2`22 by A2,A14,CAT_1:17;
A17: dom k1`21 = k1`11`11 & cod k2`22 = k2`12`12 by A1,Th2;
A18: cod k1`21 = k1`12`11 by A1,Th2;
A19: dom k2`21 = k2`11`11 by A1,Th2;
then
A20: dom k21 = dom k1`21 & cod k21 = cod k2`21 by A2,A18,CAT_1:17;
((k2`12)`2)(*)(F.k21) = (k2`12`2)(*)((F.k2`21)(*)(F.k1`21)) by A2,A18,A19,
CAT_1:64
.= (G.k2`22)(*)(k2`11`2)(*)(F.k1`21) by A2,A18,A19,A12,A7,A3,A4,CAT_1:18
.= (G.k2`22)(*)((G.k1`22)(*)(k1`11`2))
by A2,A18,A14,A9,A5,A4,A10,CAT_1:18
.= (G.k2`22)(*)(G.k1`22)(*)(k1`11`2) by A2,A6,A15,A14,A10,A11,A8,CAT_1:18
.= (G.k22)(*)((k1`11)`2) by A2,A15,A14,CAT_1:64;
then
([[k1`11,k2`12],[k2`21(*)k1`21,k2`22(*)k1`22]]) in commaMorphs(F,G)
by A6,A12,A17,A13,A20,A16;
hence thesis;
end;
end;
definition
let C,D,E,F,G;
func commaComp(F,G) -> PartFunc of [:commaMorphs(F,G),commaMorphs(F,G):],
commaMorphs(F,G) means
: Def4:
dom it = { [k1,k2]: k1`11 = k2`12 } & for k,k9
st [k,k9] in dom it holds it.[k,k9] = k*k9;
existence
proof
defpred P[object,object] means
ex k1,k2 st $1 = [k1,k2] & $2 = k1*k2;
set X = {[k1,k2]: k1`11 = k2`12};
A1: for x being object st x in X ex y being object st P[x,y]
proof
let x be object;
assume x in X;
then consider k1,k2 such that
A2: x = [k1,k2] and
k1`11 = k2`12;
reconsider y = k1*k2 as set;
take y,k1,k2;
thus thesis by A2;
end;
consider f being Function such that
A3: dom f = X &
for x being object st x in X holds P[x,f.x] from CLASSES1:sch 1(A1);
A4: rng f c= commaMorphs(F,G)
proof
let x be object;
assume x in rng f;
then consider y being object such that
A5: y in dom f and
A6: x = f.y by FUNCT_1:def 3;
ex k1,k2 st y = [k1,k2] & f.y = k1*k2 by A3,A5;
hence thesis by A6;
end;
dom f c= [:commaMorphs(F,G),commaMorphs(F,G):]
proof
let x be object;
assume x in dom f;
then ex k1,k2 st x = [k1,k2] & k1`11 = k2`12 by A3;
hence thesis;
end;
then reconsider f as PartFunc of [:commaMorphs(F,G),commaMorphs(F,G):],
commaMorphs(F,G) by A4,RELSET_1:4;
take f;
thus dom f = X by A3;
let k1,k2;
assume [k1,k2] in dom f;
then consider k,k9 such that
A7: [k1,k2] = [k,k9] and
A8: f.[k1,k2] = k*k9 by A3;
k1 = k by A7,XTUPLE_0:1;
hence thesis by A7,A8,XTUPLE_0:1;
end;
uniqueness
proof
let f1,f2 be PartFunc of [:commaMorphs(F,G),commaMorphs(F,G):],
commaMorphs(F,G) such that
A9: dom f1 = { [k1,k2]: k1`11 = k2`12 } & for k,k9 st [k,k9] in dom
f1 holds f1.[k,k9] = k*k9 and
A10: dom f2 = { [k1,k2]: k1`11 = k2`12 } & for k,k9 st [k,k9] in dom
f2 holds f2.[k,k9] = k*k9;
now
let x be object;
assume
A11: x in { [k1,k2]: k1`11 = k2`12 };
then consider k1,k2 such that
A12: x = [k1,k2] and
k1`11 = k2`12;
thus f1.x = k1*k2 by A9,A11,A12
.= f2.x by A10,A11,A12;
end;
hence thesis by A9,A10,FUNCT_1:2;
end;
end;
definition
let C,D,E,F,G;
given c1,d1,f1 such that
A1: f1 in Hom(F.c1,G.d1);
func F comma G -> strict Category means
the carrier of it = commaObjs(F,G) &
the carrier' of it = commaMorphs(F,G) & (for k holds (the Source of it).k = k
`11) & (for k holds (the Target of it).k = k`12) &
the Comp of it = commaComp(F,G);
existence
proof
reconsider O = commaObjs(F,G), M = commaMorphs(F,G) as non empty set;
defpred P[Element of commaObjs(F,G),set] means $2 = [[$1,$1],[id $1`11, id
$1`12]];
deffunc G(Element of commaMorphs(F,G)) = $1`12;
deffunc F(Element of commaMorphs(F,G)) = $1`11;
consider D9 being Function of commaMorphs(F,G),commaObjs(F,G) such that
A2: D9.k = F(k) from FUNCT_2:sch 4;
set I = the Function of commaObjs(F,G),commaMorphs(F,G);
reconsider I as Function of O,M;
reconsider a9 = commaComp(F,G) as PartFunc of [:M,M:],M;
consider C9 being Function of commaMorphs(F,G),commaObjs(F,G) such that
A3: C9.k = G(k) from FUNCT_2:sch 4;
reconsider D9, C9 as Function of M,O;
set FG = CatStr(#O, M, D9, C9, a9#);
A4: dom the Comp of FG = { [k1,k2]: k1`11 = k2`12} by Def4;
A5: for f,g being Morphism of FG for k1,k2 st f = k1 & g = k2 & dom g =
cod f holds g(*)f = [[k1`11,k2`12],[k2`21(*)k1`21,k2`22(*)k1`22]]
proof
let f,g be Morphism of FG;
let k1,k2;
assume that
A6: f = k1 & g = k2 and
A7: dom g = cod f;
A8: dom g = k2`11 & cod f = k1`12 by A2,A3,A6;
then
A9: [k2,k1] in dom a9 by A4,A7;
then
A10: a9.(k2,k1) = k2*k1 by Def4;
g(*)f = a9.(g,f) by A6,A9,CAT_1:def 1;
hence thesis by A1,A6,A7,A8,A10,Def3;
end;
A11: for b being Element of FG holds Hom(b,b) <> {}
proof let b be Element of FG;
reconsider o = b as Element of commaObjs(F,G);
set i = [[o,o], [id o`11,id o`12]];
reconsider g = id o`11 as Morphism of C;
reconsider h = id o`12 as Morphism of D;
A12: dom g = o`11;
A13: cod g = o`11;
A14: dom h = o`12;
A15: cod h = o`12;
o in commaObjs(F,G);
then o in {[[c,d],f] : f in Hom(F.c,G.d)} by A1,Def1;
then consider c,d,f such that
A16: o = [[c,d],f] and
A17: f in Hom(F.c,G.d);
A18: F.g = id(F.o`11) by CAT_1:71;
A19: G.h = id(G.o`12) by CAT_1:71;
A20: c = o`11 by A16,MCART_1:85;
A21: d = o`12 by A16,MCART_1:85;
A22: cod(o`2) = cod f by A16
.= G.d by A17,CAT_1:1
.= G.o`12 by A21;
dom(o`2) = F.c by A16,A17,CAT_1:1
.= F.o`11 by A20;
then
A23: (o`2)(*)(F.g) = o`2 by A18,CAT_1:22
.= (G.h)(*)(o`2) by A19,A22,CAT_1:21;
i in {[[o1,o2], [gg,hh]]
where gg is (Morphism of C), hh is (Morphism of D),
o1 is Element of commaObjs(F,G), o2 is Element of commaObjs(F,G):
dom gg = o1`11 & cod gg = o2`11 & dom hh = o1`12 & cod hh = o2`12 &
(o2`2)(*)(F.gg) = (G.hh)(*)(o1`2)} by A12,A13,A14,A15,A23;
then i in commaMorphs(F,G) by Def2,A1;
then reconsider i as Morphism of FG;
A24: cod i = C9.i .= [[o,o], [g,h]]`12 by A3
.= b by MCART_1:85;
dom i = D9.i .= [[o,o], [g,h]]`11 by A2
.= b by MCART_1:85;
then i in Hom(b,b) by A24;
hence Hom(b,b) <> {};
end;
A25: for a being Element of FG
ex i being Morphism of a,a st
for b being Element of FG holds
(Hom(a,b)<>{} implies for g being Morphism of a,b holds g(*)i = g) &
(Hom(b,a)<>{} implies for f being Morphism of b,a holds i(*)f = f)
proof let a be Element of FG;
reconsider o = a as Element of commaObjs(F,G);
set i = [[o,o], [id o`11,id o`12]];
reconsider g = id o`11 as Morphism of C;
reconsider h = id o`12 as Morphism of D;
A26: dom g = o`11;
A27: cod g = o`11;
A28: dom h = o`12;
A29: cod h = o`12;
o in commaObjs(F,G);
then o in {[[c,d],f] : f in Hom(F.c,G.d)} by A1,Def1;
then consider c,d,f such that
A30: o = [[c,d],f] and
A31: f in Hom(F.c,G.d);
A32: F.g = id(F.o`11) by CAT_1:71;
A33: G.h = id(G.o`12) by CAT_1:71;
A34: c = o`11 by A30,MCART_1:85;
A35: d = o`12 by A30,MCART_1:85;
A36: cod(o`2) = cod f by A30
.= G.d by A31,CAT_1:1
.= G.o`12 by A35;
dom(o`2) = F.c by A30,A31,CAT_1:1
.= F.o`11 by A34;
then
A37: (o`2)(*)(F.g) = o`2 by A32,CAT_1:22
.= (G.h)(*)(o`2) by A33,A36,CAT_1:21;
i in {[[o1,o2], [gg,hh]]
where gg is (Morphism of C), hh is (Morphism of D),
o1 is Element of commaObjs(F,G), o2 is Element of commaObjs(F,G):
dom gg = o1`11 & cod gg = o2`11 & dom hh = o1`12 & cod hh = o2`12 &
(o2`2)(*)(F.gg) = (G.hh)(*)(o1`2)} by A26,A27,A28,A29,A37;
then
i in commaMorphs(F,G) by Def2,A1;
then reconsider i as Morphism of FG;
A38: cod i = C9.i .= [[o,o], [g,h]]`12 by A3
.= a by MCART_1:85;
dom i = D9.i .= [[o,o], [g,h]]`11 by A2
.= a by MCART_1:85;
then i in Hom(a,a) by A38;
then reconsider i as Morphism of a,a by CAT_1:def 5;
take i;
let b be Element of FG;
thus Hom(a,b)<>{} implies for g being Morphism of a,b holds g(*)i = g
proof assume
A39: Hom(a,b)<>{};
let g be Morphism of a,b;
reconsider gg = g as Element of commaMorphs(F,G);
reconsider ii = i as Element of commaMorphs(F,G);
A40: commaMorphs(F,G) =
{[[o1,o2], [g1,h1]] :
dom g1 = o1`11 & cod g1 = o2`11 & dom h1 = o1`12 & cod h1 = o2`12 &
(o2`2)(*)(F.g1) = (G.h1)(*)(o1`2)} by A1,Def2;
gg in commaMorphs(F,G);
then consider g1,h1,o1,o2 such that
A41: gg = [[o1,o2], [g1,h1]] and
A42: dom g1 = o1`11 and
cod g1 = o2`11 and
A43: dom h1 = o1`12 and cod h1 = o2`12 &
(o2`2)(*)(F.g1) = (G.h1)(*)(o1`2) by A40;
A44: dom commaComp(F,G) = { [k1,k2]: k1`11 = k2`12 } by Def4;
A45: ii`21 = [[o,o], [id o`11,id o`12]]`21
.= id o`11 by MCART_1:85;
A46: ii`22 = [[o,o], [id o`11,id o`12]]`22
.= id o`12 by MCART_1:85;
A47: o1 = [[o1,o2], [g1,h1]]`11 by MCART_1:85 .= gg`11 by A41;
A48: o2 = [[o1,o2], [g1,h1]]`12 by MCART_1:85 .= gg`12 by A41;
A49: g1 = [[o1,o2], [g1,h1]]`21 by MCART_1:85 .= gg`21 by A41;
A50: h1 = [[o1,o2], [g1,h1]]`22 by MCART_1:85 .= gg`22 by A41;
A51: dom g = a by A39,CAT_1:5;
A52: dom g = gg`11 by A2
.= [[o1,o2], [g1,h1]]`11 by A41
.= o1 by MCART_1:85;
A53: o1 = a by A39,A52,CAT_1:5 .= [[c,d],f] by A30;
A54: dom gg`21 = dom([[o1,o2], [g1,h1]]`21) by A41
.= dom g1 by MCART_1:85
.= o1`11 by A42
.= [[c,d],f]`11 by A53
.= o`11 by A30;
A55: dom gg`22 = dom([[o1,o2], [g1,h1]]`22) by A41
.= dom h1 by MCART_1:85
.= o1`12 by A43
.= [[c,d],f]`12 by A53
.= o`12 by A30;
A56: ii`11 = [[o,o], [id o`11,id o`12]]`11
.= dom g by A51,MCART_1:85
.= D9.gg
.= gg`11 by A2;
A57: ii`11 = o by MCART_1:85 .= ii`12 by MCART_1:85;
then
gg`11 = ii`12 by A56;
then
A58: [gg,ii] in dom commaComp(F,G) by A44;
hence g(*)i = commaComp(F,G).(g,i) by CAT_1:def 1
.= gg*ii by A58,Def4
.= [[gg`11,gg`12],[gg`21(*)id o`11,gg`22(*)ii`22]]
by A1,A57,Def3,A56,A45
.= [[gg`11,gg`12],[gg`21,gg`22(*)ii`22]] by A54,CAT_1:22
.= [[gg`11,gg`12],[gg`21,gg`22]] by A46,A55,CAT_1:22
.= g by A47,A48,A49,A50,A41;
end;
thus Hom(b,a)<>{} implies for f being Morphism of b,a holds i(*)f = f
proof assume
A59: Hom(b,a)<>{};
let g be Morphism of b,a;
reconsider gg = g as Element of commaMorphs(F,G);
reconsider ii = i as Element of commaMorphs(F,G);
A60: commaMorphs(F,G) =
{[[o1,o2], [g1,h1]] :
dom g1 = o1`11 & cod g1 = o2`11 & dom h1 = o1`12 & cod h1 = o2`12 &
(o2`2)(*)(F.g1) = (G.h1)(*)(o1`2)} by A1,Def2;
gg in commaMorphs(F,G);
then consider g1,h1,o1,o2 such that
A61: gg = [[o1,o2], [g1,h1]] and
dom g1 = o1`11 and
A62: cod g1 = o2`11 and
dom h1 = o1`12 and
A63: cod h1 = o2`12 and
(o2`2)(*)(F.g1) = (G.h1)(*)(o1`2) by A60;
A64: dom commaComp(F,G) = { [k1,k2]: k1`11 = k2`12 } by Def4;
A65: ii`21 = [[o,o], [id o`11,id o`12]]`21
.= id o`11 by MCART_1:85;
A66: ii`22 = [[o,o], [id o`11,id o`12]]`22
.= id o`12 by MCART_1:85;
A67: o1 = [[o1,o2], [g1,h1]]`11 by MCART_1:85 .= gg`11 by A61;
A68: o2 = [[o1,o2], [g1,h1]]`12 by MCART_1:85 .= gg`12 by A61;
A69: g1 = [[o1,o2], [g1,h1]]`21 by MCART_1:85 .= gg`21 by A61;
A70: h1 = [[o1,o2], [g1,h1]]`22 by MCART_1:85 .= gg`22 by A61;
A71: cod g = a by A59,CAT_1:5;
A72: cod g = gg`12 by A3
.= [[o1,o2], [g1,h1]]`12 by A61
.= o2 by MCART_1:85;
A73: o2 = a by A59,A72,CAT_1:5 .= [[c,d],f] by A30;
A74: cod gg`21 = cod([[o1,o2], [g1,h1]]`21) by A61
.= cod g1 by MCART_1:85
.= o2`11 by A62
.= [[c,d],f]`11 by A73
.= o`11 by A30;
A75: cod gg`22 = cod([[o1,o2], [g1,h1]]`22) by A61
.= cod h1 by MCART_1:85
.= o2`12 by A63
.= [[c,d],f]`12 by A73
.= o`12 by A30;
A76: ii`11 = [[o,o], [id o`11,id o`12]]`11
.= cod g by A71,MCART_1:85
.= C9.gg
.= gg`12 by A3;
A77: ii`11 = o by MCART_1:85 .= ii`12 by MCART_1:85;
gg`12 = ii`11 by A76;
then
A78: [ii,gg] in dom commaComp(F,G) by A64;
hence i(*)g = commaComp(F,G).(i,g) by CAT_1:def 1
.= ii*gg by A78,Def4
.= [[gg`11,gg`12],[ii`21(*)gg`21,ii`22(*)gg`22]]
by A1,A77,Def3,A76
.= [[gg`11,gg`12],[gg`21,ii`22(*)gg`22]] by A74,A65,CAT_1:21
.= [[gg`11,gg`12],[gg`21,gg`22]] by A66,A75,CAT_1:21
.= g by A67,A68,A69,A70,A61;
end;
end;
A79: for f,g being Morphism of FG st dom g = cod f holds dom(g(*)f) = dom f
& cod (g(*)f) = cod g
proof
let f,g be Morphism of FG such that
A80: dom g = cod f;
reconsider f1 = f, g1 = g as Element of commaMorphs(F,G);
A81: dom g = g1`11 & cod f = f1`12 by A2,A3;
then [g1,f1] in dom a9 by A4,A80;
then
A82: g(*)f = a9.(g,f) & a9.(g1,f1) = g1*f1 by Def4,CAT_1:def 1;
A83: dom f = f`11 & cod g = g`12 by A2,A3;
A84: dom (g(*)f) = (g(*)f)`11 & cod (g(*)f) = (g(*)f)`12 by A2,A3;
g1*f1 = [[f1`11,g1`12],[g1`21(*)f1`21,g1`22(*)f1`22]] by A1,A80,A81,Def3;
hence thesis by A84,A83,A82,MCART_1:85;
end;
A85: for f,g,h being Morphism of FG st dom h = cod g & dom g = cod f holds
h(*)(g(*)f) = (h(*)g)(*)f
proof
let f,g,h be Morphism of FG;
reconsider f1 = f, g1 = g, h1 = h, gf = g(*)f, hg = h(*)g as Element of
commaMorphs(F,G);
assume that
A86: dom h = cod g and
A87: dom g = cod f;
A88: dom g = g`11 & cod g = g`12 by A2,A3;
dom (h(*)g) = dom g by A79,A86;
then
A89: (h(*)g)(*)f = [[f`11,hg`12],[hg`21(*)f1`21,hg`22(*)f1`22]] by A5,A87;
A90: dom h = h`11 & cod f = f`12 by A2,A3;
cod (g(*)f) = cod g by A79,A87;
then
A91: h(*)(g(*)f) = [[gf`11,h`12],[h1`21(*)gf`21,h1`22(*)gf`22]] by A5,A86;
A92: dom h1`21 = h1`11`11 & cod f1`21 = f1`12`11 by A1,Th2;
A93: dom h1`22 = h1`11`12 & cod f1`22 = f1`12`12 by A1,Th2;
A94: dom g1`22 = g1`11`12 & cod g1`22 = g1`12`12 by A1,Th2;
A95: h(*)g = [[g`11,h`12],[h1`21(*)g1`21,h1`22(*)g1`22]] by A5,A86;
then
A96: (h(*)g)`12 = h`12 & hg`21 = h1`21(*)g1`21 by MCART_1:85;
A97: g(*)f = [[f`11,g`12],[g1`21(*)f1`21,g1`22(*)f1`22]] by A5,A87;
then
A98: (g(*)f)`11 = f`11 & gf`21 = g1`21(*)f1`21 by MCART_1:85;
A99: gf`22 = g1`22(*)f1`22 by A97,MCART_1:85;
A100: hg`22 = h1`22(*)g1`22 by A95,MCART_1:85;
dom g1`21 = g1`11`11 & cod g1`21 = g1`12`11 by A1,Th2;
then (h1`21(*)g1`21)(*)f1`21 = h1`21(*)(g1`21(*)f1`21)
by A86,A87,A88,A92,A90,CAT_1:18;
hence thesis by A86,A87,A88,A90,A94,A93,A91,A89,A96,A98,A100,A99
,CAT_1:18;
end;
for f,g being Morphism of FG holds [g,f] in dom the Comp of FG iff
dom g = cod f
proof
let f,g be Morphism of FG;
reconsider f1 = f, g1 = g as Element of commaMorphs(F,G);
A101: dom g = g1`11 & cod f = f1`12 by A2,A3;
thus [g,f] in dom the Comp of FG implies dom g = cod f
proof
assume [g,f] in dom the Comp of FG;
then consider k1,k2 such that
A102: [g,f] = [k1,k2] and
A103: k1`11 = k2`12 by A4;
g = k1 by A102,XTUPLE_0:1;
hence thesis by A101,A102,A103,XTUPLE_0:1;
end;
thus thesis by A4,A101;
end;
then reconsider FG as
strict Category by A79,A85,A11,A25,CAT_1:def 6,def 7,def 8,def 9,def 10;
take FG;
thus thesis by A2,A3;
end;
uniqueness
proof
let E1,E2 be strict Category such that
A104: the carrier of E1 = commaObjs(F,G) and
A105: the carrier' of E1 = commaMorphs(F,G) and
A106: for k holds (the Source of E1).k = k`11 and
A107: for k holds (the Target of E1).k = k`12 and
A108: the Comp of E1 = commaComp(F,G) and
A109: the carrier of E2 = commaObjs(F,G) & the carrier' of E2 =
commaMorphs(F,G) and
A110: for k holds (the Source of E2).k = k`11 and
A111: for k holds (the Target of E2).k = k`12 and
A112: the Comp of E2 = commaComp(F,G);
now
let x be Element of morph(E1);
thus (the Target of E1).x = x`12 by A105,A107
.= (the Target of E2).x by A105,A111;
end;
then
A113: the Target of E1 = the Target of E2 by A104,A105,A109,FUNCT_2:63;
now
let x be Element of morph(E1);
thus (the Source of E1).x = x`11 by A105,A106
.= (the Source of E2).x by A105,A110;
end;
then the Source of E1 = the Source of E2 by A104,A105,A109,FUNCT_2:63;
hence thesis by A104,A105,A108,A109,A112,A113;
end;
end;
theorem
the carrier of 1Cat(x,y) = {x} & the carrier' of 1Cat(x,y) = {y};
theorem Th4:
for a,b being Object of 1Cat(x,y) holds Hom(a,b) = {y}
proof
let a,b be Object of 1Cat(x,y);
thus Hom(a,b) c= {y};
y is Morphism of 1Cat(x,y) by TARSKI:def 1;
then y in Hom(a,b) by CAT_1:11;
hence thesis by ZFMISC_1:31;
end;
definition
let C, c;
func 1Cat c -> strict Subcategory of C equals
1Cat(c, id c);
coherence
proof
A1: now
let a be Object of 1Cat(c, id c);
id a = id c by TARSKI:def 1;
hence for c1 st a = c1 holds id a = id c1 by TARSKI:def 1;
end;
A2: now
let a,b be Object of 1Cat(c, id c);
A3: a = c & b = c by TARSKI:def 1;
id c in Hom(c,c) & Hom(a,a) = {id c} by Th4,CAT_1:27;
hence for c1,c2 st a = c1 & b = c2 holds Hom(a,b) c= Hom(c1,c2) by A3,
ZFMISC_1:31;
end;
set m = id c;
set s = (m,m).--> m;
A4: dom s = {[m,m]} by FUNCOP_1:13;
A5: dom m = c;
A6: cod m = c;
A7: s.(m,m) = m by FUNCOP_1:71;
A8: now
let x be object;
assume
A9: x in dom the Comp of 1Cat(c,m);
hence (the Comp of 1Cat(c,m)).x = m by A7,A4,TARSKI:def 1
.= m(*)(m qua Morphism of C) by A6,CAT_1:21
.= (the Comp of C).(m,m) by A5,A6,CAT_1:16
.= (the Comp of C).x by A4,A9,TARSKI:def 1;
end;
[m,m] in dom the Comp of C by A5,A6,CAT_1:15;
then dom the Comp of 1Cat(c,m) c= dom the Comp of C by A4,ZFMISC_1:31;
then
obj(1Cat(c, id c)) = {c} & the Comp of 1Cat(c, id c) c= the Comp of C
by A8,GRFUNC_1:2;
hence thesis by A2,A1,CAT_2:def 4;
end;
end;
definition
let C, c;
func c comma C -> strict Category equals
(incl 1Cat c) comma (id C);
coherence;
func C comma c -> strict Category equals
(id C) comma (incl 1Cat c);
coherence;
end;