Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

### Subcategories and Products of Categories

by
Czeslaw Bylinski

MML identifier: CAT_2
[ Mizar article, MML identifier index ]

```environ

vocabulary FRAENKEL, FUNCT_1, FUNCT_5, FUNCT_2, RELAT_1, BOOLE, CAT_1,
FUNCOP_1, FUNCT_3, TARSKI, PARTFUN1, FUNCT_4, MCART_1, CAT_2;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, RELAT_1, FUNCT_1,
FUNCT_2, PARTFUN1, FUNCT_3, FUNCT_4, FUNCT_5, FRAENKEL, CAT_1;
constructors DOMAIN_1, FUNCT_3, FUNCT_4, FUNCT_5, FRAENKEL, CAT_1, MEMBERED,
PARTFUN1, XBOOLE_0;
clusters FUNCT_1, RELSET_1, SUBSET_1, MEMBERED, ZFMISC_1, XBOOLE_0;
requirements SUBSET, BOOLE;

begin

reserve X for set;
reserve C,D,E for non empty set;
reserve c for Element of C, d for Element of D;

:: Auxiliary theorems

definition let D,X,E; let F be FUNCTION_DOMAIN of X,E;
let f be Function of D,F; let d be Element of D;
redefine func f.d -> Element of F;
end;

reserve f for Function of [:C,D:],E;

theorem :: CAT_2:1
curry f is Function of C,Funcs(D,E);

theorem :: CAT_2:2
curry' f is Function of D,Funcs(C,E);

definition let C,D,E,f;
redefine func curry f -> Function of C,Funcs(D,E);
func curry' f -> Function of D,Funcs(C,E);
end;

theorem :: CAT_2:3
f.[c,d] = ((curry f).c).d;

theorem :: CAT_2:4
f.[c,d] = ((curry' f).d).c;

reserve B,C,D,C',D' 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 Morphisms of B) --> (id c);
end;

canceled;

theorem :: CAT_2:6
for c being Object of C, f being Morphism of B holds (B --> c).f = id c;

theorem :: CAT_2:7
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;

definition 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 Objects of it c= the Objects of C &
(for a,b being Object of it, a',b' being Object of C
st a = a' & b = b' holds Hom(a,b) c= Hom(a',b')) &
the Comp of it <= the Comp of C &
(for a being Object of it, a' being Object of C st a = a'
holds id a = id a');
end;

definition let C;
cluster strict Subcategory of C;
end;

reserve E for Subcategory of C;

canceled 4;

theorem :: CAT_2:12
for e being Object of E holds e is Object of C;

theorem :: CAT_2:13
the Morphisms of E c= the Morphisms of C;

theorem :: CAT_2:14
for f being Morphism of E holds f is Morphism of C;

theorem :: CAT_2:15
for f being (Morphism of E), f' being Morphism of C st f = f'
holds dom f = dom f' & cod f = cod f';

theorem :: CAT_2:16
for a,b being Object of E, a',b' being Object of C,f being Morphism of a,b
st a = a' & b = b' & Hom(a,b)<>{} holds f is Morphism of a',b';

theorem :: CAT_2:17
for f,g being (Morphism of E), f',g' being Morphism of C
st f = f' & g = g' & dom g = cod f holds g*f = g'*f';

theorem :: CAT_2:18
C is Subcategory of C;

theorem :: CAT_2:19
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;

canceled;

theorem :: CAT_2:21
for f being Morphism of E holds (incl E).f = f;

theorem :: CAT_2:22
for a being Object of E holds (Obj incl E).a = a;

theorem :: CAT_2:23
for a being Object of E holds (incl E).a = a;

theorem :: CAT_2:24
incl E is faithful;

theorem :: CAT_2:25
incl E is full iff
for a,b being Object of E, a',b' being Object of C
st a = a' & b = b' holds Hom(a,b) = Hom(a',b');

definition let C be CatStr, D;
pred C is_full_subcategory_of D means
:: CAT_2:def 6
C is Subcategory of D &
for a,b being Object of C, a',b' being Object of D
st a = a' & b = b' holds Hom(a,b) = Hom(a',b');
end;

canceled;

theorem :: CAT_2:27
E is_full_subcategory_of C iff incl(E) is full;

theorem :: CAT_2:28
for O being non empty Subset of the Objects 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 Morphisms of C;

theorem :: CAT_2:29
for O being non empty Subset of the Objects 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 Dom of C)|M is Function of M,O &
(the Cod of C)|M is Function of M,O &
(the Comp of C)|[:M,M:] is PartFunc of [:M,M:],M &
(the Id of C)|O is Function of O,M;

theorem :: CAT_2:30
for O being non empty Subset of the Objects 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 Dom of C)|M & c = (the Cod of C)|M
& p = (the Comp of C)|[:M,M:] & i = (the Id of C)|O
holds CatStr(#O,M,d,c,p,i#) is_full_subcategory_of C;

theorem :: CAT_2:31
for O being non empty Subset of the Objects 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 CatStr(#O,M,d,c,p,i#) 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 Dom of C)|M & c = (the Cod of C)|M
& p = (the Comp of C)|[:M,M:] & i = (the Id of C)|O;

:: Product of Categories

definition let X1,X2,Y1,Y2 be non empty set;
let f1 be Function of X1,Y1; let f2 be Function of X2,Y2;
redefine func [:f1,f2:] -> Function of [:X1,X2:],[:Y1,Y2:];
end;

definition let A,B be non empty set;
let f be PartFunc of [:A,A:],A; let g be PartFunc of [:B,B:],B;
redefine func |:f,g:| -> PartFunc of [:[:A,B:],[:A,B:]:],[:A,B:];
end;

definition let C,D;
func [:C,D:] -> Category equals
:: CAT_2:def 7
CatStr (# [:the Objects of C,the Objects of D:],
[:the Morphisms of C,the Morphisms of D:],
[:the Dom of C,the Dom of D:],
[:the Cod of C,the Cod of D:],
|:the Comp of C, the Comp of D:|,
[:the Id of C,the Id of D:]
#);
end;

definition let C,D;
cluster [:C,D:] -> strict;
end;

canceled;

theorem :: CAT_2:33
the Objects of [:C,D:] = [:the Objects of C,the Objects of D:] &
the Morphisms of [:C,D:] = [:the Morphisms of C,the Morphisms of D:] &
the Dom of [:C,D:] = [:the Dom of C,the Dom of D:] &
the Cod of [:C,D:] = [:the Cod of C,the Cod of D:] &
the Comp of [:C,D:] = |:the Comp of C, the Comp of D:| &
the Id of [:C,D:] = [:the Id of C,the Id of D:];

theorem :: CAT_2:34
for c being Object of C, d being Object of D
holds [c,d] is Object of [:C,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;

theorem :: CAT_2:35
for cd being Object of [:C,D:]
ex c being Object of C, d being Object of D st cd = [c,d];

theorem :: CAT_2:36
for f being Morphism of C for g being Morphism of D
holds [f,g] is Morphism of [: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;

theorem :: CAT_2:37
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:38
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:39
for f,f' being Morphism of C for g,g' being Morphism of D
st dom f' = cod f & dom g' = cod g holds [f',g']*[f,g] = [f'*f,g'*g];

theorem :: CAT_2:40
for f,f' being Morphism of C for g,g' being Morphism of D
st dom [f',g'] = cod [f,g] holds [f',g']*[f,g] = [f'*f,g'*g];

theorem :: CAT_2:41
for c being Object of C, d being Object of D
holds id [c,d] = [id c,id d];

theorem :: CAT_2:42
for c,c' being Object of C, d,d' being Object of D
holds Hom([c,d],[c',d']) = [:Hom(c,c'),Hom(d,d'):];

theorem :: CAT_2:43
for c,c' being Object of C, f being Morphism of c,c',
d,d' being Object of D, g being Morphism of d,d'
st Hom(c,c') <> {} & Hom(d,d') <> {}
holds [f,g] is Morphism of [c,d],[c',d'];

:: Bifunctors

theorem :: CAT_2:44
for S being Functor of [:C,C':],D, c being Object of C
holds (curry S).(id c) is Functor of C',D;

theorem :: CAT_2:45
for S being Functor of [:C,C':],D, c' being Object of C'
holds (curry' S).(id c') is Functor of C,D;

:: Partial Functors

definition let C,C',D; let S be Functor of [:C,C':],D, c be Object of C;
func S?-c -> Functor of C',D equals
:: CAT_2:def 8
(curry S).(id c);
end;

canceled;

theorem :: CAT_2:47
for S being Functor of [:C,C':],D, c being Object of C,
f being Morphism of C' holds (S?-c).f = S.[id c,f];

theorem :: CAT_2:48
for S being Functor of [:C,C':],D,
c being Object of C, c' being Object of C'
holds (Obj S?-c).c' = (Obj S).[c,c'];

definition let C,C',D; let S be Functor of [:C,C':],D, c' be Object of C';
func S-?c' -> Functor of C,D equals
:: CAT_2:def 9
(curry' S).(id c');
end;

canceled;

theorem :: CAT_2:50
for S being Functor of [:C,C':],D, c' being Object of C',
f being Morphism of C holds (S-?c').f = S.[f,id c'];

theorem :: CAT_2:51
for S being Functor of [:C,C':],D,
c being Object of C, c' being Object of C'
holds (Obj S-?c').c = (Obj S).[c,c'];

theorem :: CAT_2:52
for L being Function of the Objects of C,Funct(B,D),
M being Function of the Objects 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:53
for L being Function of the Objects of C,Funct(B,D),
M being Function of the Objects 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);

theorem :: CAT_2:54
pr1(the Morphisms of C,the Morphisms of D) is Functor of [:C,D:],C;

theorem :: CAT_2:55
pr2(the Morphisms of C,the Morphisms of D) is Functor of [:C,D:],D;

definition let C,D;
func pr1(C,D) -> Functor of [:C,D:],C equals
:: CAT_2:def 10
pr1(the Morphisms of C,the Morphisms of D);
func pr2(C,D) -> Functor of [:C,D:],D equals
:: CAT_2:def 11
pr2(the Morphisms of C,the Morphisms of D);
end;

canceled 2;

theorem :: CAT_2:58
for f being (Morphism of C),g being Morphism of D
holds pr1(C,D).[f,g] = f;

theorem :: CAT_2:59
for c being Object of C, d being Object of D
holds (Obj pr1(C,D)).[c,d] = c;

theorem :: CAT_2:60
for f being (Morphism of C),g being Morphism of D
holds pr2(C,D).[f,g] = g;

theorem :: CAT_2:61
for c being Object of C, d being Object of D
holds (Obj pr2(C,D)).[c,d] = d;

theorem :: CAT_2:62
for T being Functor of C,D, T' being Functor of C,D'
holds <:T,T':> is Functor of C,[:D,D':];

definition let C,D,D';
let T be Functor of C,D, T' be Functor of C,D';
redefine func <:T,T':> -> Functor of C,[:D,D':];
end;

theorem :: CAT_2:63
for T being Functor of C,D, T' being Functor of C,D', c being Object of C
holds (Obj <:T,T':>).c = [(Obj T).c,(Obj T').c];

theorem :: CAT_2:64
for T being Functor of C,D, T' being Functor of C',D'
holds [:T,T':] = <:T*pr1(C,C'),T'*pr2(C,C'):>;

theorem :: CAT_2:65
for T being Functor of C,D, T' being Functor of C',D'
holds [:T,T':] is Functor of [:C,C':],[:D,D':];

definition let C,C',D,D';
let T be Functor of C,D, T' be Functor of C',D';
redefine func [:T,T':] -> Functor of [:C,C':],[:D,D':];
end;

theorem :: CAT_2:66
for T being Functor of C,D, T' being Functor of C',D',
c being Object of C, c' being Object of C'
holds (Obj [:T,T':]).[c,c'] = [(Obj T).c,(Obj T').c'];
```