begin
:: deftheorem CAT_1:def 1 :
canceled;
:: deftheorem CAT_1:def 2 :
canceled;
:: deftheorem CAT_1:def 3 :
canceled;
:: deftheorem Def4 defines * CAT_1:def 4 :
:: deftheorem defines id CAT_1:def 5 :
:: deftheorem defines Hom CAT_1:def 6 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th18:
theorem
:: deftheorem Def7 defines Morphism CAT_1:def 7 :
theorem
canceled;
theorem
theorem Th22:
theorem Th23:
theorem
theorem Th25:
theorem Th26:
theorem
for
C being non
empty non
void CatStr for
a,
b,
c,
d being
Object of
C for
f being
Morphism of
a,
b st
Hom a,
b,
Hom c,
d are_equipotent &
Hom a,
b = {f} holds
ex
h being
Morphism of
c,
d st
Hom c,
d = {h}
Lm1:
now
let o,
m be
set ;
for C being non empty non void CatStr st C = CatStr(# {o},{m},(m :-> o),(m :-> o),(m,m :-> m),(o :-> m) #) holds
( ( for f, g being Element of the carrier' of C holds
( [g,f] in dom the Comp of C iff the Source of C . g = the Target of C . f ) ) & ( for f, g being Element of the carrier' of C st the Source of C . g = the Target of C . f holds
( the Source of C . (the Comp of C . [g,f]) = the Source of C . f & the Target of C . (the Comp of C . [g,f]) = the Target of C . g ) ) & ( for f, g, h being Element of the carrier' of C st the Source of C . h = the Target of C . g & the Source of C . g = the Target of C . f holds
the Comp of C . [h,(the Comp of C . [g,f])] = the Comp of C . [(the Comp of C . [h,g]),f] ) & ( for b being Element of C holds
( the Source of C . (the Id of C . b) = b & the Target of C . (the Id of C . b) = b & ( for f being Element of the carrier' of C st the Target of C . f = b holds
the Comp of C . (the Id of C . b),f = f ) & ( for g being Element of the carrier' of C holds the Comp of C . g,(the Id of C . b) = g ) ) ) )let C be non
empty non
void CatStr ;
( C = CatStr(# {o},{m},(m :-> o),(m :-> o),(m,m :-> m),(o :-> m) #) implies ( ( for f, g being Element of the carrier' of C holds
( [g,f] in dom the Comp of C iff the Source of C . g = the Target of C . f ) ) & ( for f, g being Element of the carrier' of C st the Source of C . g = the Target of C . f holds
( the Source of C . (the Comp of C . [g,f]) = the Source of C . f & the Target of C . (the Comp of C . [g,f]) = the Target of C . g ) ) & ( for f, g, h being Element of the carrier' of C st the Source of C . h = the Target of C . g & the Source of C . g = the Target of C . f holds
the Comp of C . [h,(the Comp of C . [g,f])] = the Comp of C . [(the Comp of C . [h,g]),f] ) & ( for b being Element of C holds
( the Source of C . (the Id of C . b) = b & the Target of C . (the Id of C . b) = b & ( for f being Element of the carrier' of C st the Target of C . f = b holds
the Comp of C . (the Id of C . b),f = f ) & ( for g being Element of the carrier' of C holds the Comp of C . g,(the Id of C . b) = g ) ) ) ) )assume A1:
C = CatStr(#
{o},
{m},
(m :-> o),
(m :-> o),
(m,m :-> m),
(o :-> m) #)
;
( ( for f, g being Element of the carrier' of C holds
( [g,f] in dom the Comp of C iff the Source of C . g = the Target of C . f ) ) & ( for f, g being Element of the carrier' of C st the Source of C . g = the Target of C . f holds
( the Source of C . (the Comp of C . [g,f]) = the Source of C . f & the Target of C . (the Comp of C . [g,f]) = the Target of C . g ) ) & ( for f, g, h being Element of the carrier' of C st the Source of C . h = the Target of C . g & the Source of C . g = the Target of C . f holds
the Comp of C . [h,(the Comp of C . [g,f])] = the Comp of C . [(the Comp of C . [h,g]),f] ) & ( for b being Element of C holds
( the Source of C . (the Id of C . b) = b & the Target of C . (the Id of C . b) = b & ( for f being Element of the carrier' of C st the Target of C . f = b holds
the Comp of C . (the Id of C . b),f = f ) & ( for g being Element of the carrier' of C holds the Comp of C . g,(the Id of C . b) = g ) ) ) )set CP = the
Comp of
C;
set CD = the
Source of
C;
set CC = the
Target of
C;
set CI = the
Id of
C;
thus
for
f,
g being
Element of the
carrier' of
C holds
(
[g,f] in dom the
Comp of
C iff the
Source of
C . g = the
Target of
C . f )
( ( for f, g being Element of the carrier' of C st the Source of C . g = the Target of C . f holds
( the Source of C . (the Comp of C . [g,f]) = the Source of C . f & the Target of C . (the Comp of C . [g,f]) = the Target of C . g ) ) & ( for f, g, h being Element of the carrier' of C st the Source of C . h = the Target of C . g & the Source of C . g = the Target of C . f holds
the Comp of C . [h,(the Comp of C . [g,f])] = the Comp of C . [(the Comp of C . [h,g]),f] ) & ( for b being Element of C holds
( the Source of C . (the Id of C . b) = b & the Target of C . (the Id of C . b) = b & ( for f being Element of the carrier' of C st the Target of C . f = b holds
the Comp of C . (the Id of C . b),f = f ) & ( for g being Element of the carrier' of C holds the Comp of C . g,(the Id of C . b) = g ) ) ) )
thus
for
f,
g being
Element of the
carrier' of
C st the
Source of
C . g = the
Target of
C . f holds
( the
Source of
C . (the Comp of C . [g,f]) = the
Source of
C . f & the
Target of
C . (the Comp of C . [g,f]) = the
Target of
C . g )
( ( for f, g, h being Element of the carrier' of C st the Source of C . h = the Target of C . g & the Source of C . g = the Target of C . f holds
the Comp of C . [h,(the Comp of C . [g,f])] = the Comp of C . [(the Comp of C . [h,g]),f] ) & ( for b being Element of C holds
( the Source of C . (the Id of C . b) = b & the Target of C . (the Id of C . b) = b & ( for f being Element of the carrier' of C st the Target of C . f = b holds
the Comp of C . (the Id of C . b),f = f ) & ( for g being Element of the carrier' of C holds the Comp of C . g,(the Id of C . b) = g ) ) ) )
proof
let f,
g be
Element of the
carrier' of
C;
( the Source of C . g = the Target of C . f implies ( the Source of C . (the Comp of C . [g,f]) = the Source of C . f & the Target of C . (the Comp of C . [g,f]) = the Target of C . g ) )
the
Comp of
C . g,
f = m
by A1, FUNCOP_1:92;
then reconsider gf = the
Comp of
C . [g,f] as
Element of the
carrier' of
C by A1, TARSKI:def 1;
the
Source of
C . gf = o
by A1, FUNCT_2:65;
hence
( the
Source of
C . g = the
Target of
C . f implies ( the
Source of
C . (the Comp of C . [g,f]) = the
Source of
C . f & the
Target of
C . (the Comp of C . [g,f]) = the
Target of
C . g ) )
by A1, FUNCT_2:65;
verum
end;
thus
for
f,
g,
h being
Element of the
carrier' of
C st the
Source of
C . h = the
Target of
C . g & the
Source of
C . g = the
Target of
C . f holds
the
Comp of
C . [h,(the Comp of C . [g,f])] = the
Comp of
C . [(the Comp of C . [h,g]),f]
for b being Element of C holds
( the Source of C . (the Id of C . b) = b & the Target of C . (the Id of C . b) = b & ( for f being Element of the carrier' of C st the Target of C . f = b holds
the Comp of C . (the Id of C . b),f = f ) & ( for g being Element of the carrier' of C holds the Comp of C . g,(the Id of C . b) = g ) )
proof
let f,
g,
h be
Element of the
carrier' of
C;
( the Source of C . h = the Target of C . g & the Source of C . g = the Target of C . f implies the Comp of C . [h,(the Comp of C . [g,f])] = the Comp of C . [(the Comp of C . [h,g]),f] )
( the
Comp of
C . g,
f = m & the
Comp of
C . h,
g = m )
by A1, FUNCOP_1:92;
then reconsider gf = the
Comp of
C . g,
f,
hg = the
Comp of
C . h,
g as
Element of the
carrier' of
C by A1, TARSKI:def 1;
( the
Comp of
C . h,
gf = m & the
Comp of
C . hg,
f = m )
by A1, FUNCOP_1:92;
hence
( the
Source of
C . h = the
Target of
C . g & the
Source of
C . g = the
Target of
C . f implies the
Comp of
C . [h,(the Comp of C . [g,f])] = the
Comp of
C . [(the Comp of C . [h,g]),f] )
;
verum
end;
let b be
Element of
C;
( the Source of C . (the Id of C . b) = b & the Target of C . (the Id of C . b) = b & ( for f being Element of the carrier' of C st the Target of C . f = b holds
the Comp of C . (the Id of C . b),f = f ) & ( for g being Element of the carrier' of C holds the Comp of C . g,(the Id of C . b) = g ) )
b = o
by A1, TARSKI:def 1;
hence
( the
Source of
C . (the Id of C . b) = b & the
Target of
C . (the Id of C . b) = b )
by A1, FUNCT_2:65;
( ( for f being Element of the carrier' of C st the Target of C . f = b holds
the Comp of C . (the Id of C . b),f = f ) & ( for g being Element of the carrier' of C holds the Comp of C . g,(the Id of C . b) = g ) )thus
for
f being
Element of the
carrier' of
C st the
Target of
C . f = b holds
the
Comp of
C . (the Id of C . b),
f = f
for g being Element of the carrier' of C holds the Comp of C . g,(the Id of C . b) = g
let g be
Element of the
carrier' of
C;
the Comp of C . g,(the Id of C . b) = g
g = m
by A1, TARSKI:def 1;
hence
the
Comp of
C . g,
(the Id of C . b) = g
by A1, FUNCOP_1:92;
verum
end;
definition
let C be
CatStr ;
attr C is
Category-like means :
Def8:
( ( for
f,
g being
Element of the
carrier' of
C holds
(
[g,f] in dom the
Comp of
C iff the
Source of
C . g = the
Target of
C . f ) ) & ( for
f,
g being
Element of the
carrier' of
C st the
Source of
C . g = the
Target of
C . f holds
( the
Source of
C . (the Comp of C . g,f) = the
Source of
C . f & the
Target of
C . (the Comp of C . g,f) = the
Target of
C . g ) ) & ( for
f,
g,
h being
Element of the
carrier' of
C st the
Source of
C . h = the
Target of
C . g & the
Source of
C . g = the
Target of
C . f holds
the
Comp of
C . h,
(the Comp of C . g,f) = the
Comp of
C . (the Comp of C . h,g),
f ) & ( for
b being
Element of
C holds
( the
Source of
C . (the Id of C . b) = b & the
Target of
C . (the Id of C . b) = b & ( for
f being
Element of the
carrier' of
C st the
Target of
C . f = b holds
the
Comp of
C . (the Id of C . b),
f = f ) & ( for
g being
Element of the
carrier' of
C st the
Source of
C . g = b holds
the
Comp of
C . g,
(the Id of C . b) = g ) ) ) );
end;
:: deftheorem Def8 defines Category-like CAT_1:def 8 :
for
C being
CatStr holds
(
C is
Category-like iff ( ( for
f,
g being
Element of the
carrier' of
C holds
(
[g,f] in dom the
Comp of
C iff the
Source of
C . g = the
Target of
C . f ) ) & ( for
f,
g being
Element of the
carrier' of
C st the
Source of
C . g = the
Target of
C . f holds
( the
Source of
C . (the Comp of C . g,f) = the
Source of
C . f & the
Target of
C . (the Comp of C . g,f) = the
Target of
C . g ) ) & ( for
f,
g,
h being
Element of the
carrier' of
C st the
Source of
C . h = the
Target of
C . g & the
Source of
C . g = the
Target of
C . f holds
the
Comp of
C . h,
(the Comp of C . g,f) = the
Comp of
C . (the Comp of C . h,g),
f ) & ( for
b being
Element of
C holds
( the
Source of
C . (the Id of C . b) = b & the
Target of
C . (the Id of C . b) = b & ( for
f being
Element of the
carrier' of
C st the
Target of
C . f = b holds
the
Comp of
C . (the Id of C . b),
f = f ) & ( for
g being
Element of the
carrier' of
C st the
Source of
C . g = b holds
the
Comp of
C . g,
(the Id of C . b) = g ) ) ) ) );
theorem
canceled;
theorem
definition
let o,
m be
set ;
func 1Cat o,
m -> strict Category equals
CatStr(#
{o},
{m},
(m :-> o),
(m :-> o),
(m,m :-> m),
(o :-> m) #);
correctness
coherence
CatStr(# {o},{m},(m :-> o),(m :-> o),(m,m :-> m),(o :-> m) #) is strict Category;
end;
:: deftheorem defines 1Cat CAT_1:def 9 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th36:
theorem
theorem
theorem
theorem
theorem Th41:
theorem Th42:
theorem Th43:
theorem
theorem Th45:
theorem Th46:
theorem Th47:
:: deftheorem defines monic CAT_1:def 10 :
:: deftheorem defines epi CAT_1:def 11 :
:: deftheorem defines invertible CAT_1:def 12 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th51:
theorem
:: deftheorem Def13 defines * CAT_1:def 13 :
theorem
canceled;
theorem Th54:
theorem Th55:
theorem
theorem Th57:
theorem Th58:
theorem Th59:
theorem Th60:
theorem
theorem
theorem
theorem
theorem Th65:
theorem
theorem
theorem
theorem
theorem Th70:
theorem Th71:
:: deftheorem Def14 defines " CAT_1:def 14 :
theorem
canceled;
theorem
theorem
theorem Th75:
theorem
theorem
:: deftheorem Def15 defines terminal CAT_1:def 15 :
:: deftheorem Def16 defines initial CAT_1:def 16 :
:: deftheorem Def17 defines are_isomorphic CAT_1:def 17 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th81:
theorem
theorem Th83:
theorem
theorem
theorem
theorem Th87:
theorem
theorem
theorem
theorem
theorem
theorem
definition
let C,
D be
Category;
mode Functor of
C,
D -> Function of the
carrier' of
C,the
carrier' of
D means :
Def18:
( ( for
c being
Element of
C ex
d being
Element of
D st
it . (the Id of C . c) = the
Id of
D . d ) & ( for
f being
Element of the
carrier' of
C holds
(
it . (the Id of C . (the Source of C . f)) = the
Id of
D . (the Source of D . (it . f)) &
it . (the Id of C . (the Target of C . f)) = the
Id of
D . (the Target of D . (it . f)) ) ) & ( for
f,
g being
Element of the
carrier' of
C st
[g,f] in dom the
Comp of
C holds
it . (the Comp of C . g,f) = the
Comp of
D . (it . g),
(it . f) ) );
existence
ex b1 being Function of the carrier' of C,the carrier' of D st
( ( for c being Element of C ex d being Element of D st b1 . (the Id of C . c) = the Id of D . d ) & ( for f being Element of the carrier' of C holds
( b1 . (the Id of C . (the Source of C . f)) = the Id of D . (the Source of D . (b1 . f)) & b1 . (the Id of C . (the Target of C . f)) = the Id of D . (the Target of D . (b1 . f)) ) ) & ( for f, g being Element of the carrier' of C st [g,f] in dom the Comp of C holds
b1 . (the Comp of C . g,f) = the Comp of D . (b1 . g),(b1 . f) ) )
end;
:: deftheorem Def18 defines Functor CAT_1:def 18 :
theorem
canceled;
theorem
canceled;
theorem Th96:
theorem Th97:
theorem
theorem Th99:
theorem Th100:
:: deftheorem Def19 defines Obj CAT_1:def 19 :
theorem
canceled;
theorem Th102:
theorem Th103:
theorem Th104:
theorem Th105:
:: deftheorem defines . CAT_1:def 20 :
theorem
canceled;
theorem
theorem
theorem
theorem Th110:
theorem Th111:
theorem Th112:
theorem
:: deftheorem defines id CAT_1:def 21 :
theorem
canceled;
theorem
canceled;
theorem Th116:
theorem Th117:
theorem
definition
let C,
D be
Category;
let T be
Functor of
C,
D;
attr T is
isomorphic means
(
T is
one-to-one &
rng T = the
carrier' of
D &
rng (Obj T) = the
carrier of
D );
attr T is
full means :
Def23:
for
c,
c' being
Object of
C st
Hom (T . c),
(T . c') <> {} holds
for
g being
Morphism of
T . c,
T . c' holds
(
Hom c,
c' <> {} & ex
f being
Morphism of
c,
c' st
g = T . f );
attr T is
faithful means :
Def24:
for
c,
c' being
Object of
C st
Hom c,
c' <> {} holds
for
f1,
f2 being
Morphism of
c,
c' st
T . f1 = T . f2 holds
f1 = f2;
end;
:: deftheorem defines isomorphic CAT_1:def 22 :
:: deftheorem Def23 defines full CAT_1:def 23 :
:: deftheorem Def24 defines faithful CAT_1:def 24 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem Th123:
theorem Th124:
theorem Th125:
theorem Th126:
theorem
theorem
theorem Th129:
definition
let C,
D be
Category;
let T be
Functor of
C,
D;
let c,
c' be
Object of
C;
func hom T,
c,
c' -> Function of
(Hom c,c'),
(Hom (T . c),(T . c')) equals
T | (Hom c,c');
correctness
coherence
T | (Hom c,c') is Function of (Hom c,c'),(Hom (T . c),(T . c'));
end;
:: deftheorem defines hom CAT_1:def 25 :
theorem
canceled;
theorem Th131:
theorem
theorem