:: Introduction to Categories and Functors
:: by Czes{\l}aw Byli\'nski
::
:: Received October 25, 1989
:: Copyright (c) 1990-2017 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies GRAPH_1, STRUCT_0, FUNCT_1, PARTFUN1, ZFMISC_1, SUBSET_1,
XBOOLE_0, CARD_1, FUNCOP_1, RELAT_1, TARSKI, ALGSTR_0, WELLORD1, CAT_1,
MONOID_0, RELAT_2, BINOP_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1,
FUNCT_2, ORDINAL1, NUMBERS, BINOP_1, FUNCOP_1, STRUCT_0, GRAPH_1;
constructors PARTFUN1, WELLORD2, BINOP_1, PBOOLE, GRAPH_1, RELSET_1, NUMBERS;
registrations XBOOLE_0, FUNCT_1, RELSET_1, FUNCT_2, STRUCT_0, RELAT_1,
ZFMISC_1;
requirements SUBSET, BOOLE;
begin :: Structure of a Category
definition
struct(MultiGraphStruct) CatStr (# carrier,carrier' -> set,
Source,Target -> Function of the carrier', the carrier,
Comp -> PartFunc of [:the carrier', the carrier' :],the carrier' #);
end;
reserve C for CatStr;
definition
let C;
mode Object of C is Element of C;
mode Morphism of C is Element of the carrier' of C;
end;
reserve f,g for Morphism of C;
:: Domain and codomain of a Morphism
registration
cluster non void non empty for CatStr;
end;
definition
let C,f,g;
assume
[g,f] in dom(the Comp of C);
func g(*)f -> Morphism of C equals
:: CAT_1:def 1
( the Comp of C ).(g,f);
end;
definition
::$CD 2
let C be non void non empty CatStr, a,b be Object of C;
func Hom(a,b) -> Subset of the carrier' of C equals
:: CAT_1:def 4
{f where f is Morphism of C : dom f = a & cod f = b};
end;
reserve C for non void non empty CatStr,
f,g for Morphism of C,
a,b,c,d for Object of C;
theorem :: CAT_1:1
f in Hom(a,b) iff dom(f)=a & cod(f)=b;
theorem :: CAT_1:2
Hom(dom(f),cod(f)) <> {};
definition
let C,a,b;
assume
Hom(a,b)<>{};
mode Morphism of a,b -> Morphism of C means
:: CAT_1:def 5
it in Hom(a,b);
end;
::$CT
theorem :: CAT_1:4
for f being Morphism of C holds f is Morphism of dom(f),cod(f);
theorem :: CAT_1:5
for f being Morphism of a,b st Hom(a,b) <> {} holds dom(f) = a & cod(f) = b;
theorem :: CAT_1:6
for f being Morphism of a,b for h being Morphism of c,d st Hom(a,b) <>
{} & Hom(c,d) <> {} & f = h holds a = c & b = d;
theorem :: CAT_1:7
for f being Morphism of a,b st Hom(a,b) = {f} for g being
Morphism of a,b holds f = g;
theorem :: CAT_1:8
for f being Morphism of a,b st Hom(a,b) <> {} & for g being
Morphism of a,b holds f = g holds Hom(a,b) = {f};
theorem :: CAT_1:9
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};
:: Category
definition
let C be non empty non void CatStr;
attr C is Category-like means
:: CAT_1:def 6
for f,g being Morphism of C
holds [g,f] in dom(the Comp of C) iff dom g = cod f;
attr C is transitive means
:: CAT_1:def 7
for f,g being Morphism of C st dom g = cod f
holds dom(g(*)f) = dom f & cod(g(*)f) = cod g;
attr C is associative means
:: CAT_1:def 8
for f,g,h being Morphism of C
st dom h = cod g & dom g = cod f
holds h(*)(g(*)f) = (h(*)g)(*)f;
attr C is reflexive means
:: CAT_1:def 9
for b being Element of C holds Hom(b,b) <> {};
attr C is with_identities means
:: CAT_1:def 10
for a being Element of C
ex i being Morphism of a,a st
for b being Element of C holds
(Hom(a,b)<>{} implies for g being Morphism of a,b holds g(*)i = g) &
(Hom(b,a)<>{} implies for f being Morphism of b,a holds i(*)f = f);
end;
definition
let o,m be object;
func 1Cat(o,m) -> strict CatStr equals
:: CAT_1:def 11
CatStr(# {o},{m},m:->o,m:->o,(m,m):->m #);
end;
registration let o,m be object;
cluster 1Cat(o,m) -> non empty trivial non void trivial';
end;
registration
cluster non empty trivial -> transitive reflexive
for non empty non void CatStr;
end;
registration
cluster non void trivial' -> associative with_identities
for non empty non void CatStr;
end;
registration let o,m be object;
cluster 1Cat(o,m) -> Category-like;
end;
registration
cluster reflexive transitive associative with_identities Category-like
non void non empty strict for non empty non void CatStr;
end;
definition
mode Category is reflexive transitive associative with_identities
Category-like non void non empty CatStr;
end;
registration let C be reflexive non void non empty CatStr,
a be Object of C;
cluster Hom(a,a) -> non empty;
end;
::$CT
reserve o,m for set;
theorem :: CAT_1:11
for a,b being Object of 1Cat(o,m) for f being Morphism of 1Cat(o,m)
holds f in Hom(a,b);
theorem :: CAT_1:12
for a,b being Object of 1Cat(o,m) for f being Morphism of 1Cat(o,m)
holds f is Morphism of a,b;
theorem :: CAT_1:13
for a,b being Object of 1Cat(o,m) holds Hom(a,b) <> {};
theorem :: CAT_1:14
for a,b,c,d being Object of 1Cat(o,m) for f being Morphism of a,b for
g being Morphism of c,d holds f=g;
reserve B,C,D for Category;
reserve a,b,c,d for Object of C;
reserve f,f1,f2,g,g1,g2 for Morphism of C;
theorem :: CAT_1:15
dom(g) = cod(f) iff [g,f] in dom(the Comp of C);
theorem :: CAT_1:16
dom(g) = cod(f) implies g(*)f = ( the Comp of C ).(g,f);
theorem :: CAT_1:17
for f,g being Morphism of C st dom(g) = cod(f) holds dom(g(*)f) =
dom(f) & cod(g(*)f) = cod(g);
theorem :: CAT_1:18
for f,g,h being Morphism of C st dom(h) = cod(g) & dom(g) = cod(
f) holds h(*)(g(*)f) = (h(*)g)(*)f;
definition
let C be with_identities reflexive non void non empty CatStr,
a be Object of C;
func id a -> Morphism of a,a means
:: CAT_1:def 12
for b being Object of C holds
(Hom(a,b) <> {} implies
for f being Morphism of a,b holds f(*)it = f)
& (Hom(b,a) <> {} implies
for f being Morphism of b,a holds it(*)f = f);
end;
::$CT 2
theorem :: CAT_1:21
for f being Morphism of C st cod(f) = b holds (id b)(*)f = f;
theorem :: CAT_1:22
for g being Morphism of C st dom(g) = b holds g(*)(id b) = g;
reserve f,f1,f2 for Morphism of a,b;
reserve f9 for Morphism of b,a;
reserve g for Morphism of b,c;
reserve h,h1,h2 for Morphism of c,d;
theorem :: CAT_1:23
Hom(a,b)<>{} & Hom(b,c)<>{} implies g(*)f in Hom(a,c);
definition
let C,a,b,c,f,g;
assume
Hom(a,b)<>{} & Hom(b,c)<>{};
func g*f -> Morphism of a,c equals
:: CAT_1:def 13
g(*)f;
end;
theorem :: CAT_1:24
Hom(a,b)<>{} & Hom(b,c)<>{} implies Hom(a,c)<>{};
theorem :: CAT_1:25
Hom(a,b)<>{} & Hom(b,c)<>{} & Hom(c,d)<>{} implies (h*g)*f=h*(g* f);
::$CT
theorem :: CAT_1:27
id a in Hom(a,a);
theorem :: CAT_1:28
Hom(a,b)<>{} implies (id b)*f=f;
theorem :: CAT_1:29
Hom(b,c)<>{} implies g*(id b)=g;
registration let C,a; let f be Morphism of a,a;
reduce f*id a to f;
reduce (id a)*f to f;
end;
theorem :: CAT_1:30
(id a)*(id a) = id a;
:: Monics, Epis
definition
let C be Category, b,c be Object of C, g be Morphism of b,c;
attr g is monic means
:: CAT_1:def 14
Hom(b,c) <> {} &
for a being Object of C st Hom(a,b) <> {}
for f1,f2 being Morphism of a,b
st g*f1=g*f2 holds f1=f2;
end;
definition
let C be Category, a,b be Object of C, f be Morphism of a,b;
attr f is epi means
:: CAT_1:def 15
Hom(a,b) <> {} &
for c being Object of C st Hom(b,c) <> {}
for g1,g2 being Morphism of b,c st g1*f=g2*f holds g1=g2;
end;
definition
let C be Category, a,b be Object of C, f be Morphism of a,b;
attr f is invertible means
:: CAT_1:def 16
Hom(a,b) <> {} & Hom(b,a) <> {} &
ex g being Morphism of b,a st f*g = id b & g*f = id a;
end;
theorem :: CAT_1:31
Hom(b,c) <> {} implies (g is monic iff for a for f1,f2 being
Morphism of a,b st Hom(a,b)<>{} & g*f1=g*f2 holds f1=f2);
theorem :: CAT_1:32
g is monic & h is monic implies h*g is monic;
theorem :: CAT_1:33
Hom(b,c)<>{} & Hom(c,d)<>{} & h*g is monic implies g is monic;
theorem :: CAT_1:34
for h being Morphism of a,b for g being Morphism of b,a st Hom(a,b) <>
{} & Hom(b,a) <> {} & h*g = id b holds g is monic;
theorem :: CAT_1:35
id b is monic;
theorem :: CAT_1:36
Hom(a,b) <> {} implies (f is epi iff for c for g1,g2 being
Morphism of b,c st Hom(b,c)<>{} & g1*f=g2*f holds g1=g2);
theorem :: CAT_1:37
f is epi & g is epi implies g*f is epi;
theorem :: CAT_1:38
Hom(a,b)<>{} & Hom(b,c)<>{} & g*f is epi implies g is epi;
theorem :: CAT_1:39
for h being Morphism of a,b for g being Morphism of b,a st Hom(a,b) <>
{} & Hom(b,a) <> {} & h*g = id b holds h is epi;
theorem :: CAT_1:40
id b is epi;
theorem :: CAT_1:41
Hom(a,b) <> {} implies (f is invertible iff Hom(b,a)<>{} & ex g
being Morphism of b,a st f*g=id b & g*f=id a);
theorem :: CAT_1:42
Hom(a,b) <> {} & Hom(b,a) <> {} implies for g1,g2 being Morphism
of b,a st f*g1=id b & g2*f=id a holds g1=g2;
definition
let C,a,b,f;
assume that
f is invertible;
func f" -> Morphism of b,a means
:: CAT_1:def 17
f*it = id b & it*f = id a;
end;
theorem :: CAT_1:43
f is invertible implies f is monic & f is epi;
theorem :: CAT_1:44
id a is invertible;
theorem :: CAT_1:45
f is invertible & g is invertible implies g*f is invertible;
theorem :: CAT_1:46
f is invertible implies f" is invertible;
theorem :: CAT_1:47
f is invertible & g is invertible
implies (g*f)" = f"*g";
definition
let C,a;
attr a is terminal means
:: CAT_1:def 18
Hom(b,a)<>{} & ex f being Morphism of b,a
st for g being Morphism of b,a holds f=g;
attr a is initial means
:: CAT_1:def 19
Hom(a,b)<>{} & ex f being Morphism of a,b st
for g being Morphism of a,b holds f=g;
let b;
pred a,b are_isomorphic means
:: CAT_1:def 20
ex f st f is invertible;
reflexivity;
symmetry;
end;
theorem :: CAT_1:48
a,b are_isomorphic iff Hom(a,b)<>{} & Hom(b,a)<>{} & ex f,f9 st
f*f9 = id b & f9*f = id a;
theorem :: CAT_1:49
a is initial iff for b ex f being Morphism of a,b st Hom(a,b) = {f};
theorem :: CAT_1:50
a is initial implies for h being Morphism of a,a holds id a = h;
theorem :: CAT_1:51
a is initial & b is initial implies a,b are_isomorphic;
theorem :: CAT_1:52
a is initial & a,b are_isomorphic implies b is initial;
theorem :: CAT_1:53
b is terminal iff for a ex f being Morphism of a,b st Hom(a,b) = {f};
theorem :: CAT_1:54
a is terminal implies for h being Morphism of a,a holds id a = h;
theorem :: CAT_1:55
a is terminal & b is terminal implies a,b are_isomorphic;
theorem :: CAT_1:56
b is terminal & a,b are_isomorphic implies a is terminal;
theorem :: CAT_1:57
Hom(a,b) <> {} & a is terminal implies f is monic;
registration let C,a;
reduce dom id a to a;
reduce cod id a to a;
end;
theorem :: CAT_1:58
dom id a = a & cod id a =a;
theorem :: CAT_1:59
id a = id b implies a = b;
theorem :: CAT_1:60
a,b are_isomorphic & b,c are_isomorphic implies a,c are_isomorphic;
:: Functors (Covariant Functors)
definition
let C,D;
mode Functor of C,D -> Function of the carrier' of C,the carrier' of D means
:: CAT_1:def 21
(for c being Element of C ex d being Element of D st it.id c = id d ) &
(for f being Element of the carrier' of C
holds it.(id dom f) = id dom(it.f) &
it.(id cod f) = id cod(it.f)) &
for f,g being Element of the carrier' of C
st [g,f] in dom(the Comp of C)
holds it.(g(*)f) = (it.g)(*)(it.f);
end;
theorem :: CAT_1:61
for T being Function of the carrier' of C,the carrier' of D st
(for c being Object of C ex d being Object of D st T.(id c) = id d) &
(for f being Morphism of C
holds T.(id dom f) = id dom (T.f) &
T.(id cod f) = id cod (T.f)) &
(for f,g being Morphism of C st dom g = cod f
holds T.(g(*)f) = (T.g)(*)(T.f)) holds T is Functor of C,D;
theorem :: CAT_1:62
for T being Functor of C,D for c being Object of C ex d being
Object of D st T.(id c) = id d;
theorem :: CAT_1:63
for T being Functor of C,D for f being Morphism of C
holds T.(id dom f) = id dom (T.f) & T.(id cod f) = id cod (T.f);
theorem :: CAT_1:64
for T being Functor of C,D for f,g being Morphism of C st dom g
= cod f holds dom(T.g) = cod(T.f) & T.(g(*)f) = (T.g)(*)(T.f);
theorem :: CAT_1:65
for T being Function of the carrier' of C,the carrier' of D for
F being Function of the carrier of C, the carrier of D st ( for c being Object
of C holds T.(id c) = id(F.c) ) & ( for f being Morphism of C holds F.(dom f) =
dom (T.f) & F.(cod f) = cod (T.f) ) & ( for f,g being Morphism of C st dom g =
cod f holds T.(g(*)f) = (T.g)(*)(T.f)) holds T is Functor of C,D;
:: Object Function of a Functor
definition
let C,D;
let F be Function of the carrier' of C,the carrier' of D;
assume
for c being Element of C ex d being Element
of D st F.id c = id d;
func Obj(F) -> Function of the carrier of C,the carrier of D means
:: CAT_1:def 22
for c being Element of C for d being Element of D
st F.id c = id d holds it.c = d;
end;
theorem :: CAT_1:66
for T being Function of the carrier' of C,the carrier' of D st
for c being Object of C ex d being Object of D st T.(id c) = id d for c being
Object of C for d being Object of D st T.(id c) = id d holds (Obj T).c = d;
theorem :: CAT_1:67
for T being Functor of C,D for c being Object of C for d being
Object of D st T.(id c) = id d holds (Obj T).c = d;
theorem :: CAT_1:68
for T being (Functor of C,D),c being Object of C holds T.(id c)
= id((Obj T).c);
theorem :: CAT_1:69
for T being (Functor of C,D), f being Morphism of C holds (Obj
T).(dom f) = dom (T.f) & (Obj T).(cod f) = cod (T.f);
definition
let C,D be Category;
let T be Functor of C,D;
let c be Object of C;
func T.c -> Object of D equals
:: CAT_1:def 23
(Obj T).c;
end;
theorem :: CAT_1:70
for T being Functor of C,D for c being Object of C for d being Object
of D st T.(id c) = id d holds T.c = d;
theorem :: CAT_1:71
for T being (Functor of C, D),c being Object of C holds T.(id c) = id(
T.c);
theorem :: CAT_1:72
for T being (Functor of C, D), f being Morphism of C holds T.(dom f) =
dom (T.f) & T.(cod f) = cod (T.f);
theorem :: CAT_1:73
for T being Functor of B,C for S being Functor of C,D holds S*T
is Functor of B,D;
:: Composition of Functors
definition
let B,C,D;
let T be Functor of B,C;
let S be Functor of C,D;
redefine func S*T -> Functor of B,D;
end;
theorem :: CAT_1:74
id the carrier' of C is Functor of C,C;
theorem :: CAT_1:75
for T being (Functor of B,C),S being (Functor of C,D),b being
Object of B holds (Obj (S*T)).b = (Obj S).((Obj T).b);
theorem :: CAT_1:76
for T being Functor of B,C for S being Functor of C,D for b being
Object of B holds (S*T).b = S.(T.b);
:: Identity Functor
definition
let C;
func id C -> Functor of C,C equals
:: CAT_1:def 24
id the carrier' of C;
end;
theorem :: CAT_1:77
for c being Object of C holds (Obj id C).c = c;
theorem :: CAT_1:78
Obj id C = id the carrier of C;
theorem :: CAT_1:79
for c being Object of C holds (id C).c = c;
definition
let C,D be Category;
let T be Functor of C,D;
attr T is isomorphic means
:: CAT_1:def 25
T is one-to-one & rng T = the carrier' of D & rng Obj T = the carrier of D;
attr T is full means
:: CAT_1:def 26
for c,c9 being Object of C st Hom(T.c,T.c9) <>
{} for g being Morphism of T.c,T.c9 holds Hom(c,c9) <> {} & ex f being Morphism
of c,c9 st g = T.f;
attr T is faithful means
:: CAT_1:def 27
for c,c9 being Object of C st Hom(c,c9) <>
{} for f1,f2 being Morphism of c,c9 holds T.f1 = T.f2 implies f1 = f2;
end;
theorem :: CAT_1:80
id C is isomorphic;
theorem :: CAT_1:81
for T being Functor of C,D for c,c9 being Object of C for f
being set st f in Hom(c,c9) holds T.f in Hom(T.c,T.c9);
theorem :: CAT_1:82
for T being Functor of C,D for c,c9 being Object of C st Hom(c,
c9) <> {} for f being Morphism of c,c9 holds T.f in Hom(T.c,T.c9);
theorem :: CAT_1:83
for T being Functor of C,D for c,c9 being Object of C st Hom(c,
c9) <> {} for f being Morphism of c,c9 holds T.f is Morphism of T.c,T.c9;
theorem :: CAT_1:84
for T being Functor of C,D for c,c9 being Object of C st Hom(c,
c9) <> {} holds Hom(T.c,T.c9) <> {};
theorem :: CAT_1:85
for T being Functor of B,C for S being Functor of C,D st T is full & S
is full holds S*T is full;
theorem :: CAT_1:86
for T being Functor of B,C for S being Functor of C,D st T is faithful
& S is faithful holds S*T is faithful;
theorem :: CAT_1:87
for T being Functor of C,D for c,c9 being Object of C holds T.:
Hom(c,c9) c= Hom(T.c,T.c9);
definition
let C,D be Category;
let T be Functor of C,D;
let c,c9 be Object of C;
func hom(T,c,c9) -> Function of Hom(c,c9) , Hom(T.c,T.c9) equals
:: CAT_1:def 28
T|Hom(c,c9);
end;
theorem :: CAT_1:88
for T being Functor of C,D for c,c9 being Object of C st Hom(c,
c9) <> {} for f being Morphism of c,c9 holds hom(T,c,c9).f = T.f;
theorem :: CAT_1:89
for T being Functor of C,D holds T is full iff for c,c9 being Object
of C holds rng hom(T,c,c9) = Hom(T.c,T.c9);
theorem :: CAT_1:90
for T being Functor of C,D holds T is faithful iff for c,c9 being
Object of C holds hom(T,c,c9) is one-to-one;
theorem :: CAT_1:91
for a,b being Element of C st Hom(a,b)<>{}
ex m being Morphism of a,b st m in Hom(a,b);
theorem :: CAT_1:92
the carrier' of C = union the set of all Hom(a,b);