environ
vocabularies HIDDEN, 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 HIDDEN, 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;
definitions TARSKI, CAT_1;
theorems TARSKI, ZFMISC_1, MCART_1, DOMAIN_1, FUNCT_1, FUNCT_2, FUNCT_3, FUNCT_4, FUNCT_5, PARTFUN1, FUNCOP_1, CAT_1, GRFUNC_1, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, XTUPLE_0;
schemes XBOOLE_0, BINOP_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, REALSET1, CAT_1, STRUCT_0, RELAT_1, XTUPLE_0;
constructors HIDDEN, PARTFUN1, BINOP_1, FUNCT_3, FUNCT_4, FUNCT_5, REALSET1, CAT_1, FUNCOP_1, RELSET_1;
requirements HIDDEN, SUBSET, BOOLE;
equalities CAT_1, REALSET1, FUNCOP_1, BINOP_1, GRAPH_1;
expansions CAT_1;
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 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;