Journal of Formalized Mathematics
Volume 6, 1994
University of Bialystok
Copyright (c) 1994
Association of Mizar Users
The abstract of the Mizar article:
-
- by
- Grzegorz Bancerek
- Received October 24, 1994
- MML identifier: CAT_5
- [
Mizar article,
MML identifier index
]
environ
vocabulary COMMACAT, MCART_1, CAT_1, RELAT_1, FUNCT_1, PARTFUN1, CAT_2, BOOLE,
GROUP_6, TARSKI, SETFAM_1, GRCAT_1, FRAENKEL, FUNCT_3, CAT_5;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, MCART_1, DOMAIN_1,
RELAT_1, FUNCT_1, FUNCT_2, FUNCT_4, FRAENKEL, PARTFUN1, CAT_1, CAT_2,
COMMACAT;
constructors NATTRA_1, SETFAM_1, DOMAIN_1, COMMACAT, PARTFUN1, XBOOLE_0;
clusters FRAENKEL, CAT_1, CAT_2, FUNCT_1, RELSET_1, SUBSET_1, XBOOLE_0,
ZFMISC_1;
requirements SUBSET, BOOLE;
begin :: Categories with Triple-like Morphisms
definition let D1,D2,D be non empty set;
let x be Element of [:[:D1,D2:],D:];
redefine func x`11 -> Element of D1;
redefine func x`12 -> Element of D2;
end;
definition let D1,D2 be non empty set;
let x be Element of [:D1,D2:];
redefine func x`2 -> Element of D2;
end;
theorem :: CAT_5:1
for C,D being CatStr st the CatStr of C = the CatStr of D holds
C is Category-like implies D is Category-like;
definition let IT be 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;
definition
cluster with_triple-like_morphisms (strict Category);
end;
theorem :: CAT_5:2
for C being with_triple-like_morphisms 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 CatStr;
let f be Morphism of C;
redefine func f`11 -> Object of C;
redefine func f`12 -> Object of C;
end;
scheme CatEx
{ A, B() -> non empty set, P[set, set, set], F(set,set) -> set }:
ex C being with_triple-like_morphisms strict Category st
the Objects 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 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 Objects 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 Objects 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 FunctorEx
{ A,B() -> Category,
O(set) -> Object of B(),
F(set) -> set }:
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 & 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 Objects of it = (the Objects of C1) /\ the Objects of C2 &
the Morphisms of it = (the Morphisms of C1) /\ the Morphisms of C2 &
the Dom of it = (the Dom of C1)|the Morphisms of C2 &
the Cod of it = (the Cod of C1)|the Morphisms of C2 &
the Comp of it =
(the Comp of C1)|([:the Morphisms of C2,the Morphisms of C2:]) &
the Id of it = (the Id of C1)|the Objects of C2;
end;
reserve C for Category, C1,C2 for Subcategory of C;
theorem :: CAT_5:5
the Objects of C1 meets the Objects of C2 implies C1 /\ C2 = C2 /\ C1;
theorem :: CAT_5:6
the Objects of C1 meets the Objects 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 Objects of it = rng Obj F & rng F c= the Morphisms of it &
for E being Subcategory of D st
the Objects of E = rng Obj F & rng F c= the Morphisms 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 Morphisms 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
cluster categorial (non empty set);
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;
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 Objects 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;
definition
cluster Categorial -> with_triple-like_morphisms 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;
definition
cluster Categorial (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 Objects of C1 = the Objects of C2 &
the Morphisms of C1 = the Morphisms of C2
holds the CatStr of C1 = the CatStr of C2;
definition let C be Categorial Category;
cluster -> Categorial Subcategory of C;
end;
theorem :: CAT_5:15
for C,D being Categorial Category st the Morphisms of C c= the Morphisms of D
holds C is Subcategory of D;
definition
let a be set 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 Objects 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 Objects 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 Objects 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;
definition
cluster full (Categorial strict Category);
end;
theorem :: CAT_5:19
for C1,C2 being full (Categorial Category) st
the Objects of C1 = the Objects 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 Objects of C = A;
theorem :: CAT_5:21
for C being Categorial Category, D being full (Categorial Category) st
the Objects of C c= the Objects 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 Morphisms of C equals
:: CAT_5:def 9
(the Cod of C)"{o};
func o Hom -> Subset of the Morphisms of C equals
:: CAT_5:def 10
(the Dom of C)"{o};
end;
definition
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 Objects 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 Objects 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);
Back to top