:: Subcategories and Products of Categories
:: by Czes{\l}aw Byli\'nski
::
:: Received May 31, 1990
:: Copyright (c) 1990-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, FUNCT_2, FUNCT_1, ZFMISC_1, FUNCT_5, RELAT_1,
TARSKI, CAT_1, FUNCOP_1, STRUCT_0, GRAPH_1, FUNCT_3, REALSET1, PARTFUN1,
FUNCT_4, MCART_1, CAT_2, MONOID_0, RELAT_2, BINOP_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, RELAT_1, FUNCT_1,
FUNCT_2, BINOP_1, PARTFUN1, FUNCT_3, FUNCT_4, FUNCT_5, REALSET1,
FUNCOP_1, STRUCT_0, GRAPH_1, CAT_1;
constructors PARTFUN1, BINOP_1, FUNCT_3, FUNCT_4, FUNCT_5, REALSET1, CAT_1,
FUNCOP_1, RELSET_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, REALSET1, CAT_1, STRUCT_0,
RELAT_1, XTUPLE_0;
requirements SUBSET, BOOLE;
begin
::$CT 4
reserve B,C,D,C9,D9 for Category;
:: Auxiliary theorems on Functors
definition
let B,C;
let c be Object of C;
func B --> c -> Functor of B,C equals
:: CAT_2:def 1
(the carrier' of B) --> (id c);
end;
theorem :: CAT_2:5
for c being Object of C, b being Object of B holds (Obj (B --> c)).b = c;
definition
let C,D;
func Funct(C,D) -> set means
:: CAT_2:def 2
for x being set holds x in it iff x is Functor of C,D;
end;
registration
let C,D;
cluster Funct(C,D) -> non empty;
end;
definition
let C,D;
mode FUNCTOR-DOMAIN of C,D -> non empty set means
:: CAT_2:def 3
for x being Element of it holds x is Functor of C,D;
end;
definition
let C,D;
let F be FUNCTOR-DOMAIN of C,D;
redefine mode Element of F -> Functor of C,D;
end;
definition
let A be non empty set;
let C,D;
let F be FUNCTOR-DOMAIN of C,D, T be Function of A,F, x be Element of A;
redefine func T.x -> Element of F;
end;
definition
let C,D;
redefine func Funct(C,D) -> FUNCTOR-DOMAIN of C,D;
end;
:: Subcategory
definition
let C;
mode Subcategory of C -> Category means
:: CAT_2:def 4
the carrier of it c= the carrier of C &
(for a,b being Object of it, a9,b9 being Object of C
st a = a9 & b = b9
holds Hom(a,b) c= Hom(a9,b9)) & the Comp of it c= the Comp of C &
for a being Object of it, a9 being Object of C st a = a9
holds id a = id a9;
end;
registration
let C;
cluster strict for Subcategory of C;
end;
reserve E for Subcategory of C;
theorem :: CAT_2:6
for e being Object of E holds e is Object of C;
theorem :: CAT_2:7
the carrier' of E c= the carrier' of C;
theorem :: CAT_2:8
for f being Morphism of E holds f is Morphism of C;
theorem :: CAT_2:9
for f being (Morphism of E), f9 being Morphism of C st f = f9
holds dom f = dom f9 & cod f = cod f9;
theorem :: CAT_2:10
for a,b being Object of E, a9,b9 being Object of C,f being Morphism of
a, b st a = a9 & b = b9 & Hom(a,b)<>{} holds f is Morphism of a9,b9;
theorem :: CAT_2:11
for f,g being (Morphism of E), f9,g9 being Morphism of C st f =
f9 & g = g9 & dom g = cod f holds g(*)f = g9(*)f9;
theorem :: CAT_2:12
C is Subcategory of C;
theorem :: CAT_2:13
id E is Functor of E,C;
definition
let C,E;
func incl(E) -> Functor of E,C equals
:: CAT_2:def 5
id E;
end;
theorem :: CAT_2:14
for a being Object of E holds (Obj incl E).a = a;
theorem :: CAT_2:15
for a being Object of E holds (incl E).a = a;
theorem :: CAT_2:16
incl E is faithful;
theorem :: CAT_2:17
incl E is full iff for a,b being Object of E, a9,b9 being Object
of C st a = a9 & b = b9 holds Hom(a,b) = Hom(a9,b9);
definition let D;
let C be Subcategory of D;
attr C is full means
:: CAT_2:def 6
for c1,c2 being Object of C, d1,d2 being Object of D
st c1 = d1 & c2 = d2
holds Hom(c1,c2) = Hom(d1,d2);
end;
registration let D;
cluster full for Subcategory of D;
end;
theorem :: CAT_2:18
E is full iff incl(E) is full;
theorem :: CAT_2:19
for O being non empty Subset of the carrier of C holds union{Hom
(a,b) where a is Object of C,b is Object of C: a in O & b in O} is non empty
Subset of the carrier' of C;
theorem :: CAT_2:20
for O being non empty Subset of the carrier of C, M being non
empty set st M = union{Hom(a,b) where a is Object of C,b is Object of C: a in O
& b in O} holds (the Source of C)|M is Function of M,O & (the Target of C)|M is
Function of M,O & (the Comp of C)||M is PartFunc of [:M,M:],M;
registration
let O, M be non empty set, d,c being Function of M,O, p being PartFunc of [:
M,M:],M;
cluster CatStr(#O,M,d,c,p#) -> non void non empty;
end;
theorem :: CAT_2:21
for O being non empty Subset of the carrier of C, M being non empty
set, d,c being Function of M,O, p being PartFunc of [:M,M:],M, i being Function
of O,M st M = union{Hom(a,b) where a is Object of C,b is Object of C: a in O &
b in O} & d = (the Source of C)|M & c = (the Target of C)|M & p = (the Comp of
C)||M
holds CatStr(#O,M,d,c,p#) is full Subcategory of C;
theorem :: CAT_2:22
for O being non empty Subset of the carrier of C, M being non empty
set , d,c being Function of M,O, p being PartFunc of [:M,M:],M
st CatStr(#O,M,d,c,p#) is full Subcategory of C
holds M =
union{Hom(a,b) where a is Object of C,b is Object of C: a in O & b in O} & d =
(the Source of C)|M & c = (the Target of C)|M & p = (the Comp of C)||M;
:: Product of Categories
definition
let C,D;
func [:C,D:] -> Category equals
:: CAT_2:def 7
CatStr (# [:the carrier of C,the carrier of D:],
[:the carrier' of C,the carrier' of D:],
[:the Source of C,the Source of D:],
[:the Target of C,the Target of D:],
|:the Comp of C, the Comp of D:| #);
end;
theorem :: CAT_2:23
the carrier of [:C,D:] = [:the carrier of C,the carrier of D:] & the
carrier' of [:C,D:] = [:the carrier' of C,the carrier' of D:] & the Source of
[:C,D:] = [:the Source of C,the Source of D:] & the Target of [:C,D:] = [:the
Target of C,the Target of D:] & the Comp of [:C,D:] = |:the Comp of C, the Comp
of D:|;
definition
let C,D;
let c be Object of C;
let d be Object of D;
redefine func [c,d] -> Object of [:C,D:];
end;
::$CT
theorem :: CAT_2:25
for cd being Object of [:C,D:] ex c being Object of C, d being Object
of D st cd = [c,d];
definition
let C,D;
let f be Morphism of C;
let g be Morphism of D;
redefine func [f,g] -> Morphism of [:C,D:];
end;
::$CT
theorem :: CAT_2:27
for fg being Morphism of [:C,D:] ex f being (Morphism of C), g being
Morphism of D st fg = [f,g];
theorem :: CAT_2:28
for f being Morphism of C for g being Morphism of D
holds dom [f,g] = [dom f,dom g] & cod [f,g] = [cod f,cod g];
theorem :: CAT_2:29
for f,f9 being Morphism of C for g,g9 being Morphism of D st dom
f9 = cod f & dom g9 = cod g holds [f9,g9](*)[f,g] = [f9(*)f,g9(*)g];
theorem :: CAT_2:30
for f,f9 being Morphism of C for g,g9 being Morphism of D st dom
[f9,g9] = cod [f,g] holds [f9,g9](*)[f,g] = [f9(*)f,g9(*)g];
theorem :: CAT_2:31
for c being Object of C, d being Object of D holds id [c,d] = [id c,id d];
theorem :: CAT_2:32
for c,c9 being Object of C, d,d9 being Object of D
holds Hom([c,d],[c9,d9]) = [:Hom(c,c9),Hom(d,d9):];
theorem :: CAT_2:33
for c,c9 being Object of C, f being Morphism of c,c9, d,d9 being
Object of D, g being Morphism of d,d9 st Hom(c,c9) <> {} & Hom(d,d9) <> {}
holds [f,g] is Morphism of [c,d],[c9,d9];
:: Bifunctors
definition
let C,C9,D;
let S being Functor of [:C,C9:],D;
let m be Morphism of C;
let m9 be Morphism of C9;
redefine func S.(m,m9) -> Morphism of D;
end;
theorem :: CAT_2:34
for S being Functor of [:C,C9:],D, c being Object of C holds (
curry S).(id c) is Functor of C9,D;
theorem :: CAT_2:35
for S being Functor of [:C,C9:],D, c9 being Object of C9 holds (
curry' S).(id c9) is Functor of C,D;
:: Partial Functors
definition
let C,C9,D;
let S be Functor of [:C,C9:],D, c be Object of C;
func S?-c -> Functor of C9,D equals
:: CAT_2:def 8
(curry S).(id c);
end;
theorem :: CAT_2:36
for S being Functor of [:C,C9:],D, c being Object of C, f being
Morphism of C9 holds (S?-c).f = S.(id c,f);
theorem :: CAT_2:37
for S being Functor of [:C,C9:],D, c being Object of C, c9 being
Object of C9 holds (Obj S?-c).c9 = (Obj S).(c,c9);
definition
let C,C9,D;
let S be Functor of [:C,C9:],D, c9 be Object of C9;
func S-?c9 -> Functor of C,D equals
:: CAT_2:def 9
(curry' S).(id c9);
end;
theorem :: CAT_2:38
for S being Functor of [:C,C9:],D, c9 being Object of C9, f being
Morphism of C holds (S-?c9).f = S.(f,id c9);
theorem :: CAT_2:39
for S being Functor of [:C,C9:],D, c being Object of C, c9 being
Object of C9 holds (Obj S-?c9).c = (Obj S).(c,c9);
theorem :: CAT_2:40
for L being Function of the carrier of C,Funct(B,D), M being Function
of the carrier of B,Funct(C,D) st ( for c being Object of C,b being Object of B
holds (M.b).(id c) = (L.c).(id b) ) & ( for f being Morphism of B for g being
Morphism of C
holds ((M.(cod f)).g)(*)((L.(dom g)).f) = ((L.(cod g)).f)(*)((M.(dom
f)).g) ) ex S being Functor of [:B,C:],D st for f being Morphism of B for g
being Morphism of C holds S.(f,g) = ((L.(cod g)).f)(*)((M.(dom f)).g);
theorem :: CAT_2:41
for L being Function of the carrier of C,Funct(B,D),
M being Function of the carrier of B,Funct(C,D)
st ex S being Functor of [:B,C:],D st
for c being Object of C,b being Object of B
holds S-?c = L.c & S?-b = M.b
for f being Morphism of B for g being Morphism of C
holds ((M.(cod f)).g)(*)((L.(dom g)).f) =
((L.(cod g)).f)(*)((M.(dom f)).g);
definition
let C,D;
func pr1(C,D) -> Functor of [:C,D:],C equals
:: CAT_2:def 10
pr1(the carrier' of C,the carrier' of D);
func pr2(C,D) -> Functor of [:C,D:],D equals
:: CAT_2:def 11
pr2(the carrier' of C,the carrier' of D);
end;
::$CT 2
theorem :: CAT_2:44
for c being Object of C, d being Object of D holds (Obj pr1(C,D)).(c,d ) = c;
theorem :: CAT_2:45
for c being Object of C, d being Object of D holds (Obj pr2(C,D)).(c,d ) = d;
definition
let C,D,D9;
let T be Functor of C,D, T9 be Functor of C,D9;
redefine func <:T,T9:> -> Functor of C,[:D,D9:];
end;
::$CT
theorem :: CAT_2:47
for T being Functor of C,D, T9 being Functor of C,D9, c being Object
of C holds (Obj <:T,T9:>).c = [(Obj T).c,(Obj T9).c];
theorem :: CAT_2:48
for T being Functor of C,D, T9 being Functor of C9,D9 holds [:T,
T9:] = <:T*pr1(C,C9),T9*pr2(C,C9):>;
definition
let C,C9,D,D9;
let T be Functor of C,D, T9 be Functor of C9,D9;
redefine func [:T,T9:] -> Functor of [:C,C9:],[:D,D9:];
end;
::$CT
theorem :: CAT_2:50
for T being Functor of C,D, T9 being Functor of C9,D9, c being Object
of C, c9 being Object of C9 holds (Obj [:T,T9:]).(c,c9) = [(Obj T).c,(Obj T9).
c9];