:: Comma Category
:: by Grzegorz Bancerek and Agata Darmochwa\l
::
:: Received February 20, 1992
:: Copyright (c) 1992-2017 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;
begin
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
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
:: COMMACAT:def 1
{[[c,d],f] : f in Hom(F.c,G.d)};
end;
reserve o,o1,o2 for Element of commaObjs(F,G);
theorem :: COMMACAT:1
(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;
definition
let C,D,E,F,G;
given c1,d1,f1 such that
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
:: COMMACAT:def 2
{[[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)};
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);
redefine func k`12 -> Element of commaObjs(F,G);
end;
theorem :: COMMACAT:2
(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);
definition
let C,D,E,F,G,k1,k2;
given c1,d1,f1 such that
f1 in Hom(F.c1,G.d1);
assume
k1`12 = k2`11;
func k2*k1 -> Element of commaMorphs(F,G) equals
:: COMMACAT:def 3
[[k1`11,k2`12],[k2`21(*)k1`21,k2`22(*)k1`22]];
end;
definition
let C,D,E,F,G;
func commaComp(F,G) -> PartFunc of [:commaMorphs(F,G),commaMorphs(F,G):],
commaMorphs(F,G) means
:: COMMACAT:def 4
dom it = { [k1,k2]: k1`11 = k2`12 } & for k,k9
st [k,k9] in dom it holds it.[k,k9] = k*k9;
end;
definition
let C,D,E,F,G;
given c1,d1,f1 such that
f1 in Hom(F.c1,G.d1);
func F comma G -> strict Category means
:: COMMACAT:def 5
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);
end;
theorem :: COMMACAT:3
the carrier of 1Cat(x,y) = {x} & the carrier' of 1Cat(x,y) = {y};
theorem :: COMMACAT:4
for a,b being Object of 1Cat(x,y) holds Hom(a,b) = {y};
definition
let C, c;
func 1Cat c -> strict Subcategory of C equals
:: COMMACAT:def 6
1Cat(c, id c);
end;
definition
let C, c;
func c comma C -> strict Category equals
:: COMMACAT:def 7
(incl 1Cat c) comma (id C);
func C comma c -> strict Category equals
:: COMMACAT:def 8
(id C) comma (incl 1Cat c);
end;