:: Subcategories and Products of Categories
:: by Czes{\l}aw Byli\'nski
::
:: Received May 31, 1990
:: Copyright (c) 1990 Association of Mizar Users
theorem Th1: :: CAT_2:1
theorem Th2: :: CAT_2:2
definition
let C,
D,
E be non
empty set ;
let f be
Function of
[:C,D:],
E;
:: original: curryredefine func curry f -> Function of
C,
Funcs D,
E;
coherence
curry f is Function of C, Funcs D,E
by Th1;
:: original: curry'redefine func curry' f -> Function of
D,
Funcs C,
E;
coherence
curry' f is Function of D, Funcs C,E
by Th2;
end;
theorem Th3: :: CAT_2:3
theorem Th4: :: CAT_2:4
:: deftheorem defines --> CAT_2:def 1 :
theorem :: CAT_2:5
canceled;
theorem :: CAT_2:6
canceled;
theorem :: CAT_2:7
:: deftheorem Def2 defines Funct CAT_2:def 2 :
:: deftheorem Def3 defines FUNCTOR-DOMAIN CAT_2:def 3 :
:: deftheorem Def4 defines Subcategory CAT_2:def 4 :
theorem :: CAT_2:8
canceled;
theorem :: CAT_2:9
canceled;
theorem :: CAT_2:10
canceled;
theorem :: CAT_2:11
canceled;
theorem Th12: :: CAT_2:12
theorem Th13: :: CAT_2:13
theorem Th14: :: CAT_2:14
theorem Th15: :: CAT_2:15
theorem :: CAT_2:16
theorem Th17: :: CAT_2:17
theorem :: CAT_2:18
theorem Th19: :: CAT_2:19
:: deftheorem defines incl CAT_2:def 5 :
theorem :: CAT_2:20
canceled;
theorem :: CAT_2:21
canceled;
theorem Th22: :: CAT_2:22
theorem :: CAT_2:23
theorem :: CAT_2:24
theorem Th25: :: CAT_2:25
:: deftheorem Def6 defines is_full_subcategory_of CAT_2:def 6 :
theorem :: CAT_2:26
canceled;
theorem :: CAT_2:27
theorem Th28: :: CAT_2:28
theorem Th29: :: CAT_2:29
registration
let O,
M be non
empty set ;
let d,
c be
Function of
M,
O;
let p be
PartFunc of
[:M,M:],
M;
let i be
Function of
O,
M;
cluster CatStr(#
O,
M,
d,
c,
p,
i #)
-> non
empty non
void ;
coherence
( not CatStr(# O,M,d,c,p,i #) is void & not CatStr(# O,M,d,c,p,i #) is empty )
;
end;
theorem :: CAT_2:30
for
C being
Category for
O being non
empty Subset of the
carrier of
C for
M being non
empty set for
d,
c being
Function of
M,
O for
p being
PartFunc of
[:M,M:],
M for
i being
Function of
O,
M st
M = union { (Hom a,b) where a, 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 &
i = the
Id of
C | O holds
CatStr(#
O,
M,
d,
c,
p,
i #)
is_full_subcategory_of C
theorem :: CAT_2:31
for
C being
Category for
O being non
empty Subset of the
carrier of
C for
M being non
empty set for
d,
c being
Function of
M,
O for
p being
PartFunc of
[:M,M:],
M for
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, 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 &
i = the
Id of
C | O )
definition
let X1,
X2,
Y1,
Y2 be non
empty set ;
let f1 be
Function of
X1,
Y1;
let f2 be
Function of
X2,
Y2;
:: original: [:redefine func [:f1,f2:] -> Function of
[:X1,X2:],
[:Y1,Y2:];
coherence
[:f1,f2:] is 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;
:: original: |:redefine func |:f,g:| -> PartFunc of
[:[:A,B:],[:A,B:]:],
[:A,B:];
coherence
|:f,g:| is PartFunc of [:[:A,B:],[:A,B:]:],[:A,B:]
by FUNCT_4:62;
end;
definition
let C,
D be
Category;
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:|,
[:the Id of C,the Id of D:] #);
coherence
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:|,[:the Id of C,the Id of D:] #) is Category
end;
:: deftheorem defines [: CAT_2:def 7 :
for
C,
D being
Category holds
[:C,D:] = 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:|,
[:the Id of C,the Id of D:] #);
theorem :: CAT_2:32
canceled;
theorem :: CAT_2:33
for
C,
D being
Category holds
( 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:| & the
Id of
[:C,D:] = [:the Id of C,the Id of D:] ) ;
theorem Th34: :: CAT_2:34
theorem :: CAT_2:35
theorem Th36: :: CAT_2:36
theorem :: CAT_2:37
theorem Th38: :: CAT_2:38
theorem Th39: :: CAT_2:39
theorem Th40: :: CAT_2:40
theorem Th41: :: CAT_2:41
theorem :: CAT_2:42
theorem :: CAT_2:43
for
C,
D being
Category for
c,
c' being
Object of
C for
f being
Morphism of
c,
c' for
d,
d' being
Object of
D for
g being
Morphism of
d,
d' st
Hom c,
c' <> {} &
Hom d,
d' <> {} holds
[f,g] is
Morphism of
[c,d],
[c',d']
theorem Th44: :: CAT_2:44
theorem Th45: :: CAT_2:45
:: deftheorem defines ?- CAT_2:def 8 :
theorem :: CAT_2:46
canceled;
theorem :: CAT_2:47
theorem :: CAT_2:48
:: deftheorem defines -? CAT_2:def 9 :
theorem :: CAT_2:49
canceled;
theorem :: CAT_2:50
theorem :: CAT_2:51
theorem :: CAT_2:52
theorem :: CAT_2:53
theorem Th54: :: CAT_2:54
theorem Th55: :: CAT_2:55
definition
let C,
D be
Category;
func pr1 C,
D -> Functor of
[:C,D:],
C equals :: CAT_2:def 10
pr1 the
carrier' of
C,the
carrier' of
D;
coherence
pr1 the carrier' of C,the carrier' of D is Functor of [:C,D:],C
by Th54;
func pr2 C,
D -> Functor of
[:C,D:],
D equals :: CAT_2:def 11
pr2 the
carrier' of
C,the
carrier' of
D;
coherence
pr2 the carrier' of C,the carrier' of D is Functor of [:C,D:],D
by Th55;
end;
:: deftheorem defines pr1 CAT_2:def 10 :
:: deftheorem defines pr2 CAT_2:def 11 :
theorem :: CAT_2:56
canceled;
theorem :: CAT_2:57
canceled;
theorem :: CAT_2:58
canceled;
theorem :: CAT_2:59
theorem :: CAT_2:60
canceled;
theorem :: CAT_2:61
theorem Th62: :: CAT_2:62
definition
let C,
D,
D' be
Category;
let T be
Functor of
C,
D;
let T' be
Functor of
C,
D';
:: original: <:redefine func <:T,T':> -> Functor of
C,
[:D,D':];
coherence
<:T,T':> is Functor of C,[:D,D':]
by Th62;
end;
theorem :: CAT_2:63
theorem Th64: :: CAT_2:64
theorem Th65: :: CAT_2:65
definition
let C,
C',
D,
D' be
Category;
let T be
Functor of
C,
D;
let T' be
Functor of
C',
D';
:: original: [:redefine func [:T,T':] -> Functor of
[:C,C':],
[:D,D':];
coherence
[:T,T':] is Functor of [:C,C':],[:D,D':]
by Th65;
end;
theorem :: CAT_2:66