begin
registration
let O,
M be non
empty set ;
let d,
c be
Function of
M,
O;
let p be
PartFunc of
[:M,M:],
M;
coherence
( not CatStr(# O,M,d,c,p #) is void & not CatStr(# O,M,d,c,p #) is empty )
;
end;
Lm1:
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 holds
CatStr(# O,M,d,c,p #) is Category
Lm2:
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 holds
CatStr(# O,M,d,c,p #) is Subcategory of C
theorem
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 holds
CatStr(#
O,
M,
d,
c,
p #) is
full Subcategory of
C
theorem
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 st
CatStr(#
O,
M,
d,
c,
p #) 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 )
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:];
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;
|: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:59;
end;
definition
let C,
D be
Category;
func [:C,D:] -> Category equals
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:| #);
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:| #) 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:| #);
theorem
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:| ) ;
theorem
for
C,
D being
Category for
c,
c9 being
Object of
C for
f being
Morphism of
c,
c9 for
d,
d9 being
Object of
D for
g being
Morphism of
d,
d9 st
Hom (
c,
c9)
<> {} &
Hom (
d,
d9)
<> {} holds
[f,g] is
Morphism of
[c,d],
[c9,d9]
definition
let C,
D,
D9 be
Category;
let T be
Functor of
C,
D;
let T9 be
Functor of
C,
D9;
<:redefine func <:T,T9:> -> Functor of
C,
[:D,D9:];
coherence
<:T,T9:> is Functor of C,[:D,D9:]
end;
definition
let C,
C9,
D,
D9 be
Category;
let T be
Functor of
C,
D;
let T9 be
Functor of
C9,
D9;
[:redefine func [:T,T9:] -> Functor of
[:C,C9:],
[:D,D9:];
coherence
[:T,T9:] is Functor of [:C,C9:],[:D,D9:]
end;