:: Introduction to Categories and Functors
:: by Czes{\l}aw Byli\'nski
::
:: Received October 25, 1989
:: Copyright (c) 1990 Association of Mizar Users
:: 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 :: CAT_1:1
canceled;
theorem :: CAT_1:2
canceled;
theorem :: CAT_1:3
canceled;
theorem :: CAT_1:4
canceled;
theorem :: CAT_1:5
canceled;
theorem :: CAT_1:6
canceled;
theorem :: CAT_1:7
canceled;
theorem :: CAT_1:8
canceled;
theorem :: CAT_1:9
canceled;
theorem :: CAT_1:10
canceled;
theorem :: CAT_1:11
canceled;
theorem :: CAT_1:12
canceled;
theorem :: CAT_1:13
canceled;
theorem :: CAT_1:14
canceled;
theorem :: CAT_1:15
canceled;
theorem :: CAT_1:16
canceled;
theorem :: CAT_1:17
canceled;
theorem Th18: :: CAT_1:18
theorem :: CAT_1:19
:: deftheorem Def7 defines Morphism CAT_1:def 7 :
theorem :: CAT_1:20
canceled;
theorem :: CAT_1:21
theorem Th22: :: CAT_1:22
theorem Th23: :: CAT_1:23
theorem :: CAT_1:24
theorem Th25: :: CAT_1:25
theorem Th26: :: CAT_1:26
theorem :: CAT_1:27
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 ;
:: thesis: 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 the carrier 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 ;
:: thesis: ( 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 the carrier 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) #)
;
:: thesis: ( ( 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 the carrier 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 )
:: thesis: ( ( 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 the carrier 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 )
:: thesis: ( ( 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 the carrier 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;
:: thesis: ( 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 . f = o & the
Target of
C . g = o & the
Source of
C . gf = o & the
Target 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 ) )
;
:: thesis: 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]
:: thesis: for b being Element of the carrier 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;
:: thesis: ( 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] )
;
:: thesis: verum
end;
let b be
Element of the
carrier of
C;
:: thesis: ( 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;
:: thesis: ( ( 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
:: thesis: 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;
:: thesis: 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;
:: thesis: verum
end;
definition
let C be
CatStr ;
attr C is
Category-like means :
Def8:
:: CAT_1:def 8
( ( 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 the
carrier 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 the
carrier 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 :: CAT_1:28
canceled;
theorem :: CAT_1:29
definition
let o,
m be
set ;
func 1Cat o,
m -> strict Category equals :: CAT_1:def 9
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 :: CAT_1:30
canceled;
theorem :: CAT_1:31
canceled;
theorem :: CAT_1:32
canceled;
theorem :: CAT_1:33
canceled;
theorem :: CAT_1:34
canceled;
theorem :: CAT_1:35
canceled;
theorem Th36: :: CAT_1:36
theorem :: CAT_1:37
theorem :: CAT_1:38
theorem :: CAT_1:39
theorem :: CAT_1:40
theorem Th41: :: CAT_1:41
theorem Th42: :: CAT_1:42
theorem Th43: :: CAT_1:43
theorem :: CAT_1:44
theorem Th45: :: CAT_1:45
theorem Th46: :: CAT_1:46
theorem Th47: :: CAT_1:47
:: deftheorem defines monic CAT_1:def 10 :
:: deftheorem defines epi CAT_1:def 11 :
:: deftheorem defines invertible CAT_1:def 12 :
theorem :: CAT_1:48
canceled;
theorem :: CAT_1:49
canceled;
theorem :: CAT_1:50
canceled;
theorem Th51: :: CAT_1:51
theorem :: CAT_1:52
:: deftheorem Def13 defines * CAT_1:def 13 :
theorem :: CAT_1:53
canceled;
theorem Th54: :: CAT_1:54
theorem Th55: :: CAT_1:55
theorem :: CAT_1:56
theorem Th57: :: CAT_1:57
theorem Th58: :: CAT_1:58
theorem Th59: :: CAT_1:59
theorem Th60: :: CAT_1:60
theorem :: CAT_1:61
theorem :: CAT_1:62
theorem :: CAT_1:63
theorem :: CAT_1:64
theorem Th65: :: CAT_1:65
theorem :: CAT_1:66
theorem :: CAT_1:67
theorem :: CAT_1:68
theorem :: CAT_1:69
theorem Th70: :: CAT_1:70
theorem Th71: :: CAT_1:71
:: deftheorem Def14 defines " CAT_1:def 14 :
theorem :: CAT_1:72
canceled;
theorem :: CAT_1:73
theorem :: CAT_1:74
theorem Th75: :: CAT_1:75
theorem :: CAT_1:76
theorem :: CAT_1:77
:: 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 :: CAT_1:78
canceled;
theorem :: CAT_1:79
canceled;
theorem :: CAT_1:80
canceled;
theorem Th81: :: CAT_1:81
theorem :: CAT_1:82
theorem Th83: :: CAT_1:83
theorem :: CAT_1:84
theorem :: CAT_1:85
theorem :: CAT_1:86
theorem Th87: :: CAT_1:87
theorem :: CAT_1:88
theorem :: CAT_1:89
theorem :: CAT_1:90
theorem :: CAT_1:91
theorem :: CAT_1:92
theorem :: CAT_1:93
definition
let C,
D be
Category;
mode Functor of
C,
D -> Function of the
carrier' of
C,the
carrier' of
D means :
Def18:
:: CAT_1:def 18
( ( for
c being
Element of the
carrier of
C ex
d being
Element of the
carrier 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 the carrier of C ex d being Element of the carrier 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 :: CAT_1:94
canceled;
theorem :: CAT_1:95
canceled;
theorem Th96: :: CAT_1:96
theorem Th97: :: CAT_1:97
theorem :: CAT_1:98
theorem Th99: :: CAT_1:99
theorem Th100: :: CAT_1:100
:: deftheorem Def19 defines Obj CAT_1:def 19 :
theorem :: CAT_1:101
canceled;
theorem Th102: :: CAT_1:102
theorem Th103: :: CAT_1:103
theorem Th104: :: CAT_1:104
theorem Th105: :: CAT_1:105
:: deftheorem defines . CAT_1:def 20 :
theorem :: CAT_1:106
canceled;
theorem :: CAT_1:107
theorem :: CAT_1:108
theorem :: CAT_1:109
theorem Th110: :: CAT_1:110
theorem Th111: :: CAT_1:111
theorem Th112: :: CAT_1:112
theorem :: CAT_1:113
:: deftheorem defines id CAT_1:def 21 :
theorem :: CAT_1:114
canceled;
theorem :: CAT_1:115
canceled;
theorem Th116: :: CAT_1:116
theorem Th117: :: CAT_1:117
theorem :: CAT_1:118
definition
let C,
D be
Category;
let T be
Functor of
C,
D;
attr T is
isomorphic means :: CAT_1:def 22
(
T is
one-to-one &
rng T = the
carrier' of
D &
rng (Obj T) = the
carrier of
D );
attr T is
full means :
Def23:
:: CAT_1:def 23
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:
:: CAT_1:def 24
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 :: CAT_1:119
canceled;
theorem :: CAT_1:120
canceled;
theorem :: CAT_1:121
canceled;
theorem :: CAT_1:122
theorem Th123: :: CAT_1:123
theorem Th124: :: CAT_1:124
theorem Th125: :: CAT_1:125
theorem Th126: :: CAT_1:126
theorem :: CAT_1:127
theorem :: CAT_1:128
theorem Th129: :: CAT_1:129
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 :: CAT_1:def 25
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 :: CAT_1:130
canceled;
theorem Th131: :: CAT_1:131
theorem :: CAT_1:132
theorem :: CAT_1:133