:: Categorial Categories and Slice Categories
:: by Grzegorz Bancerek
::
:: Received October 24, 1994
:: Copyright (c) 1994-2021 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;
begin :: Categories with Triple-like Morphisms
theorem :: CAT_5:1
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;
definition
let IT be non void non empty CatStr;
attr IT is with_triple-like_morphisms means
:: CAT_5:def 1
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;
end;
theorem :: CAT_5:2
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];
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;
redefine func f`12 -> Object of C;
end;
scheme :: CAT_5:sch 1
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
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
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
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);
scheme :: CAT_5:sch 2
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);
scheme :: CAT_5:sch 3
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
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
for a being Object of A() holds F(id a) = id O(a) and
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;
theorem :: CAT_5:3
for C1 being Category, C2 being Subcategory of C1 st C1 is Subcategory of C2
holds the CatStr of C1 = the CatStr of C2;
theorem :: CAT_5:4
for C being Category, D being Subcategory of C, E being Subcategory of D
holds E is Subcategory of C;
definition
let C1,C2 be Category;
given C being Category such that
C1 is Subcategory of C and
C2 is Subcategory of C;
given o1 being Object of C1 such that
o1 is Object of C2;
func C1 /\ C2 -> strict Category means
:: CAT_5:def 2
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;
end;
reserve C for Category,
C1,C2 for Subcategory of C;
theorem :: CAT_5:5
the carrier of C1 meets the carrier of C2 implies C1 /\ C2 = C2 /\ C1;
theorem :: CAT_5:6
the carrier of C1 meets the carrier of C2 implies
C1 /\ C2 is Subcategory of C1 & C1 /\ C2 is Subcategory of C2;
definition
let C,D be Category;
let F be Functor of C,D;
func Image F -> strict Subcategory of D means
:: CAT_5:def 3
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;
end;
theorem :: CAT_5:7
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;
theorem :: CAT_5:8
for C,D being Category, F being Functor of C,D holds
F is Functor of C, Image F;
theorem :: CAT_5:9
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;
begin :: Categorial Categories
definition
let IT be set;
attr IT is categorial means
:: CAT_5:def 4
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
:: CAT_5:def 5
for x being Element of X holds x is Category;
end;
registration
cluster categorial for non empty set;
end;
definition
let X be non empty categorial set;
redefine mode Element of X -> Category;
end;
definition
let C be Category;
attr C is Categorial means
:: CAT_5:def 6
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;
end;
theorem :: CAT_5:10
for C,D being Category st the CatStr of C = the CatStr of D holds
C is Categorial implies D is Categorial;
theorem :: CAT_5:11
for C being Category holds 1Cat(C, [[C,C], id C]) is Categorial;
registration
cluster Categorial for strict Category;
end;
theorem :: CAT_5:12
for C being Categorial Category, a being Object of C holds a is Category;
theorem :: CAT_5:13
for C being Categorial Category, f being Morphism of C holds
dom f = f`11 & cod f = f`12;
definition
let C be Categorial Category;
let m be Morphism of C;
redefine func m`11 -> Category;
redefine func m`12 -> Category;
end;
theorem :: CAT_5:14
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;
registration
let C be Categorial Category;
cluster -> Categorial for Subcategory of C;
end;
theorem :: CAT_5:15
for C,D being Categorial Category st the carrier' of C c= the carrier' of D
holds C is Subcategory of D;
definition
let a be object such that
a is Category;
func cat a -> Category equals
:: CAT_5:def 7
a;
end;
theorem :: CAT_5:16
for C being Categorial Category, c being Object of C holds cat c = c;
definition
let C be Categorial Category;
let m be Morphism of C;
redefine func m`2 -> Functor of cat dom m, cat cod m;
end;
theorem :: CAT_5:17
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;
theorem :: CAT_5:18
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;
definition
let IT be Categorial Category;
attr IT is full means
:: CAT_5:def 8
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;
end;
theorem :: CAT_5:19
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;
theorem :: CAT_5:20
for A being categorial non empty set
ex C being full Categorial strict Category st the carrier of C = A;
theorem :: CAT_5:21
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;
theorem :: CAT_5:22
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;
begin :: Slice category
definition
let C be Category;
let o be Object of C;
func Hom o -> Subset of the carrier' of C equals
:: CAT_5:def 9
(the Target of C)"{o};
func o Hom -> Subset of the carrier' of C equals
:: CAT_5:def 10
(the Source of C)"{o};
end;
registration
let C be Category;
let o be Object of C;
cluster Hom o -> non empty;
cluster o Hom -> non empty;
end;
theorem :: CAT_5:23
for C being Category, a being Object of C, f being Morphism of C holds
f in Hom a iff cod f = a;
theorem :: CAT_5:24
for C being Category, a being Object of C, f being Morphism of C holds
f in a Hom iff dom f = a;
theorem :: CAT_5:25
for C being Category, a,b being Object of C holds
Hom(a,b) = (a Hom) /\ (Hom b);
theorem :: CAT_5:26
for C being Category, f being Morphism of C holds
f in (dom f) Hom & f in Hom (cod f);
theorem :: CAT_5:27
for C being Category, f being (Morphism of C), g being Element of Hom dom f
holds f(*)g in Hom cod f;
theorem :: CAT_5:28
for C being Category, f being (Morphism of C),
g being Element of (cod f) Hom holds g(*)f in (dom f) Hom;
definition
let C be Category, o be Object of C;
func C-SliceCat(o) -> strict with_triple-like_morphisms Category means
:: CAT_5:def 11
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];
func o-SliceCat(C) -> strict with_triple-like_morphisms Category means
:: CAT_5:def 12
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];
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;
redefine func m`11 -> Element of Hom o;
redefine func m`12 -> Element of Hom o;
end;
theorem :: CAT_5:29
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;
theorem :: CAT_5:30
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];
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;
redefine func m`11 -> Element of o Hom;
redefine func m`12 -> Element of o Hom;
end;
theorem :: CAT_5:31
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;
theorem :: CAT_5:32
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];
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
:: CAT_5:def 13
for m being Morphism of C-SliceCat dom f holds
it.m = [[f(*)m`11, f(*)m`12], m`2];
func SliceContraFunctor f ->
Functor of (cod f)-SliceCat C, (dom f)-SliceCat C means
:: CAT_5:def 14
for m being Morphism of (cod f)-SliceCat C holds
it.m = [[m`11(*)f, m`12(*)f], m`2];
end;
theorem :: CAT_5:33
for C being Category, f,g being Morphism of C st dom g = cod f holds
SliceFunctor (g(*)f) = (SliceFunctor g)*(SliceFunctor f);
theorem :: CAT_5:34
for C being Category, f,g being Morphism of C st dom g = cod f holds
SliceContraFunctor (g(*)f) = (SliceContraFunctor f)*(SliceContraFunctor g);