Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989
Association of Mizar Users
The abstract of the Mizar article:
-
- by
- Czeslaw Bylinski
- Received October 25, 1989
- MML identifier: CAT_1
- [
Mizar article,
MML identifier index
]
environ
vocabulary FUNCT_1, RELAT_1, BOOLE, FUNCOP_1, PARTFUN1, TARSKI, WELLORD1,
CAT_1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1,
FUNCT_2, FUNCOP_1;
constructors FUNCOP_1, WELLORD2, MEMBERED, PARTFUN1, XBOOLE_0;
clusters FUNCT_1, RELSET_1, FUNCOP_1, SUBSET_1, MEMBERED, ZFMISC_1, FUNCT_2,
XBOOLE_0;
requirements SUBSET, BOOLE;
begin :: Auxiliary theorems
reserve a,b,c,o,m for set;
canceled 3;
theorem :: CAT_1:4
for X,Y,Z being set, D being non empty set, f being Function of X,D
st Y c= X & f.:Y c= Z holds f|Y is Function of Y,Z;
definition let A be non empty set,b;
redefine func A --> b -> Function of A,{b};
end;
definition let a,b,c;
func (a,b).-->c -> PartFunc of [:{a},{b}:],{c} equals
:: CAT_1:def 1
{[a,b]} --> c;
end;
canceled 2;
theorem :: CAT_1:7
dom (a,b).-->c = {[a,b]} & dom (a,b).-->c = [:{a},{b}:];
theorem :: CAT_1:8
((a,b).-->c).[a,b] = c;
theorem :: CAT_1:9
for x being Element of {a} for y being Element of {b}
holds ((a,b).-->c).[x,y] = c;
:: Structure of a Category
definition
struct CatStr
(# Objects,Morphisms -> non empty set,
Dom,Cod -> Function of the Morphisms, the Objects,
Comp -> PartFunc of [:the Morphisms, the Morphisms :],the Morphisms,
Id -> Function of the Objects, the Morphisms
#);
end;
reserve C for CatStr;
definition let C;
mode Object of C is Element of the Objects of C;
mode Morphism of C is Element of the Morphisms of C;
end;
reserve a,b,c,d for Object of C;
reserve f,g for Morphism of C;
:: Domain and Codomain of a Morphism
definition let C,f;
func dom(f) -> Object of C equals
:: CAT_1:def 2
(the Dom of C).f;
func cod(f) -> Object of C equals
:: CAT_1:def 3
(the Cod of C).f;
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 4
( the Comp of C ).[g,f];
end;
definition let C,a;
func id (a) -> Morphism of C equals
:: CAT_1:def 5
( the Id of C ).a;
end;
definition let C,a,b;
func Hom(a,b) -> Subset of the Morphisms of C equals
:: CAT_1:def 6
{ f : dom(f)=a & cod(f)=b };
end;
canceled 8;
theorem :: CAT_1:18
f in Hom(a,b) iff dom(f)=a & cod(f)=b;
theorem :: CAT_1:19
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 7
it in Hom(a,b);
end;
canceled;
theorem :: CAT_1:21
for f being set st f in Hom(a,b) holds f is Morphism of a,b;
theorem :: CAT_1:22
for f being Morphism of C holds f is Morphism of dom(f),cod(f);
theorem :: CAT_1:23
for f being Morphism of a,b st Hom(a,b) <> {} holds dom(f) = a & cod(f) = b;
theorem :: CAT_1:24
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:25
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:26
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:27
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 CatStr;
attr C is Category-like means
:: CAT_1:def 8
(for f,g being Element of the Morphisms of C holds
[g,f] in dom(the Comp of C) iff (the Dom of C).g=(the Cod of C).f)
& (for f,g being Element of the Morphisms of C
st (the Dom of C).g=(the Cod of C).f holds
(the Dom of C).((the Comp of C).[g,f]) = (the Dom of C).f &
(the Cod of C).((the Comp of C).[g,f]) = (the Cod of C).g)
& (for f,g,h being Element of the Morphisms of C
st (the Dom of C).h = (the Cod of C).g &
(the Dom of C).g = (the Cod 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 Objects of C holds
(the Dom of C).((the Id of C).b) = b &
(the Cod of C).((the Id of C).b) = b &
(for f being Element of the Morphisms of C st (the Cod of C).f = b
holds (the Comp of C).[(the Id of C).b,f] = f ) &
(for g being Element of the Morphisms of C st (the Dom of C).g = b
holds (the Comp of C).[g,(the Id of C).b] = g ) );
end;
definition
cluster Category-like CatStr;
end;
definition
mode Category is Category-like CatStr;
end;
definition
cluster strict Category;
end;
canceled;
theorem :: CAT_1:29
for C being CatStr
st ( for f,g being Morphism of C
holds [g,f] in dom(the Comp of C) iff dom g = cod f )
& ( for f,g being Morphism of C st dom g = cod f
holds dom(g*f) = dom f & cod (g*f) = cod g )
& ( for f,g,h being Morphism of C st dom h = cod g & dom g = cod f
holds h*(g*f) = (h*g)*f )
& ( for b being Object of C
holds dom id b = b & cod id b = b &
(for f being Morphism of C st cod f = b holds (id b)*f = f) &
(for g being Morphism of C st dom g = b holds g*(id b) = g) )
holds C is Category-like;
definition let o,m;
func 1Cat(o,m) -> strict Category equals
:: CAT_1:def 9
CatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m #);
end;
canceled 2;
theorem :: CAT_1:32
o is Object of 1Cat(o,m);
theorem :: CAT_1:33
m is Morphism of 1Cat(o,m);
theorem :: CAT_1:34
for a being Object of 1Cat(o,m) holds a = o;
theorem :: CAT_1:35
for f being Morphism of 1Cat(o,m) holds f = m;
theorem :: CAT_1:36
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:37
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:38
for a,b being Object of 1Cat(o,m) holds Hom(a,b) <> {};
theorem :: CAT_1:39
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:40
dom(g) = cod(f) iff [g,f] in dom(the Comp of C);
theorem :: CAT_1:41
dom(g) = cod(f) implies g*f = ( the Comp of C ).[g,f];
theorem :: CAT_1:42
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:43
for f,g,h being Morphism of C
st dom(h) = cod(g) & dom(g) = cod(f) holds h*(g*f) = (h*g)*f;
theorem :: CAT_1:44
dom(id b) = b & cod(id b) = b;
theorem :: CAT_1:45
id a = id b implies a = b;
theorem :: CAT_1:46
for f being Morphism of C st cod(f) = b holds (id b)*f = f;
theorem :: CAT_1:47
for g being Morphism of C st dom(g) = b holds g*(id b) = g;
definition let C,g;
attr g is monic means
:: CAT_1:def 10
for f1,f2 st dom f1 = dom f2 & cod f1 = dom g & cod f2 = dom g & g*f1=g*f2
holds f1=f2;
end;
definition let C,f;
attr f is epi means
:: CAT_1:def 11
for g1,g2 st dom g1 = cod f & dom g2 = cod f & cod g1 = cod g2 & g1*f=g2*f
holds g1=g2;
end;
definition let C,f;
attr f is invertible means
:: CAT_1:def 12
ex g st dom g = cod f & cod g = dom f & f*g = id cod f & g*f = id dom f;
end;
reserve f,f1,f2 for Morphism of a,b;
reserve f' for Morphism of b,a;
reserve g for Morphism of b,c;
reserve h,h1,h2 for Morphism of c,d;
canceled 3;
theorem :: CAT_1:51
Hom(a,b)<>{} & Hom(b,c)<>{} implies g*f in Hom(a,c);
theorem :: CAT_1:52
Hom(a,b)<>{} & Hom(b,c)<>{} implies 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;
canceled;
theorem :: CAT_1:54
Hom(a,b)<>{} & Hom(b,c)<>{} & Hom(c,d)<>{} implies (h*g)*f=h*(g*f);
theorem :: CAT_1:55
id a in Hom(a,a);
theorem :: CAT_1:56
Hom(a,a) <> {};
definition let C,a;
redefine func id a -> Morphism of a,a;
end;
theorem :: CAT_1:57
Hom(a,b)<>{} implies (id b)*f=f;
theorem :: CAT_1:58
Hom(b,c)<>{} implies g*(id b)=g;
theorem :: CAT_1:59
(id a)*(id a) = id a;
:: Monics, Epis
theorem :: CAT_1:60
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:61
Hom(b,c)<>{} & Hom(c,d)<>{} & g is monic & h is monic implies h*g is monic
;
theorem :: CAT_1:62
Hom(b,c)<>{} & Hom(c,d)<>{} & h*g is monic implies g is monic;
theorem :: CAT_1:63
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:64
id b is monic;
theorem :: CAT_1:65
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:66
Hom(a,b)<>{} & Hom(b,c)<>{} & f is epi & g is epi implies g*f is epi;
theorem :: CAT_1:67
Hom(a,b)<>{} & Hom(b,c)<>{} & g*f is epi implies g is epi;
theorem :: CAT_1:68
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:69
id b is epi;
theorem :: CAT_1:70
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:71
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 Hom(a,b) <> {} and f is invertible;
func f" -> Morphism of b,a means
:: CAT_1:def 14
f*it = id b & it*f = id a;
end;
canceled;
theorem :: CAT_1:73
Hom(a,b)<>{} & f is invertible implies f is monic & f is epi;
theorem :: CAT_1:74
id a is invertible;
theorem :: CAT_1:75
Hom(a,b) <> {} & Hom(b,c) <> {} & f is invertible & g is invertible
implies g*f is invertible;
theorem :: CAT_1:76
Hom(a,b)<>{} & f is invertible implies f" is invertible;
theorem :: CAT_1:77
Hom(a,b) <> {} & Hom(b,c) <> {} & f is invertible & g is invertible
implies (g*f)" = f"*g";
definition let C,a;
attr a is terminal means
:: CAT_1:def 15
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 16
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 17
Hom(a,b)<>{} & ex f st f is invertible;
end;
canceled 3;
theorem :: CAT_1:81
a,b are_isomorphic iff
Hom(a,b)<>{} & Hom(b,a)<>{} & ex f,f' st f*f' = id b & f'*f = id a;
theorem :: CAT_1:82
a is initial iff
for b ex f being Morphism of a,b st Hom(a,b) = {f};
theorem :: CAT_1:83
a is initial implies for h being Morphism of a,a holds id a = h;
theorem :: CAT_1:84
a is initial & b is initial implies a,b are_isomorphic;
theorem :: CAT_1:85
a is initial & a,b are_isomorphic implies b is initial;
theorem :: CAT_1:86
b is terminal iff
for a ex f being Morphism of a,b st Hom(a,b) = {f};
theorem :: CAT_1:87
a is terminal implies for h being Morphism of a,a holds id a = h;
theorem :: CAT_1:88
a is terminal & b is terminal implies a,b are_isomorphic;
theorem :: CAT_1:89
b is terminal & a,b are_isomorphic implies a is terminal;
theorem :: CAT_1:90
Hom(a,b) <> {} & a is terminal implies f is monic;
theorem :: CAT_1:91
a,a are_isomorphic;
theorem :: CAT_1:92
a,b are_isomorphic implies b,a are_isomorphic;
theorem :: CAT_1:93
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 Morphisms of C,the Morphisms of D
means
:: CAT_1:def 18
( for c being Element of the Objects of C
ex d being Element of the Objects of D
st it.((the Id of C).c) = (the Id of D).d )
& ( for f being Element of the Morphisms of C holds
it.((the Id of C).((the Dom of C).f)) =
(the Id of D).((the Dom of D).(it.f)) &
it.((the Id of C).((the Cod of C).f)) =
(the Id of D).((the Cod of D).(it.f)) )
& ( for f,g being Element of the Morphisms 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] );
end;
canceled 2;
theorem :: CAT_1:96
for T being Function of the Morphisms of C,the Morphisms 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:97
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:98
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:99
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:100
for T being Function of the Morphisms of C,the Morphisms of D
for F being Function of the Objects of C, the Objects 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 Morphisms of C,the Morphisms of D;
assume
for c being Element of the Objects of C
ex d being Element of the Objects of D
st F.((the Id of C).c) = (the Id of D).d;
func Obj(F) -> Function of the Objects of C,the Objects of D means
:: CAT_1:def 19
for c being Element of the Objects of C
for d being Element of the Objects of D
st F.((the Id of C).c) = (the Id of D).d holds it.c = d;
end;
canceled;
theorem :: CAT_1:102
for T being Function of the Morphisms of C,the Morphisms 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:103
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:104
for T being (Functor of C,D),c being Object of C
holds T.(id c) = id((Obj T).c);
theorem :: CAT_1:105
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 20
(Obj T).c;
end;
canceled;
theorem :: CAT_1:107
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:108
for T being (Functor of C, D),c being Object of C
holds T.(id c) = id(T.c);
theorem :: CAT_1:109
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:110
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:111
id the Morphisms of C is Functor of C,C;
theorem :: CAT_1:112
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:113
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 21
id the Morphisms of C;
end;
canceled;
theorem :: CAT_1:115
for f being Morphism of C holds (id C).f = f;
theorem :: CAT_1:116
for c being Object of C holds (Obj id C).c = c;
theorem :: CAT_1:117
Obj id C = id the Objects of C;
theorem :: CAT_1:118
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 22
T is one-to-one & rng T = the Morphisms of D & rng Obj T = the Objects of D
;
synonym T is_an_isomorphism;
attr T is full means
:: CAT_1:def 23
for c,c' being Object of C st Hom(T.c,T.c') <> {}
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
:: CAT_1:def 24
for c,c' being Object of C st Hom(c,c') <> {}
for f1,f2 being Morphism of c,c' holds T.f1 = T.f2 implies f1 = f2;
end;
canceled 3;
theorem :: CAT_1:122
id C is_an_isomorphism;
theorem :: CAT_1:123
for T being Functor of C,D for c,c' being Object of C
for f being set st f in Hom(c,c') holds T.f in Hom(T.c,T.c');
theorem :: CAT_1:124
for T being Functor of C,D for c,c' being Object of C st Hom(c,c') <> {}
for f being Morphism of c,c' holds T.f in Hom(T.c,T.c');
theorem :: CAT_1:125
for T being Functor of C,D for c,c' being Object of C st Hom(c,c') <> {}
for f being Morphism of c,c' holds T.f is Morphism of T.c,T.c';
theorem :: CAT_1:126
for T being Functor of C,D for c,c' being Object of C
st Hom(c,c') <> {} holds Hom(T.c,T.c') <> {};
theorem :: CAT_1:127
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:128
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:129
for T being Functor of C,D for c,c' being Object of C
holds T.:Hom(c,c') c= Hom(T.c,T.c');
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');
end;
canceled;
theorem :: CAT_1:131
for T being Functor of C,D for c,c' being Object of C st Hom(c,c') <> {}
for f being Morphism of c,c' holds hom(T,c,c').f = T.f;
theorem :: CAT_1:132
for T being Functor of C,D holds
T is full iff
for c,c' being Object of C holds rng hom(T,c,c') = Hom(T.c,T.c');
theorem :: CAT_1:133
for T being Functor of C,D holds
T is faithful iff
for c,c' being Object of C holds hom(T,c,c') is one-to-one;
Back to top