Journal of Formalized Mathematics
Volume 4, 1992
University of Bialystok
Copyright (c) 1992 Association of Mizar Users

### Cartesian Categories

by
Czeslaw Bylinski

MML identifier: CAT_4
[ Mizar article, MML identifier index ]

```environ

vocabulary FUNCT_1, CAT_1, WELLORD1, BOOLE, FINSET_1, CAT_3, RELAT_1,
FUNCOP_1, FINSEQ_4, CARD_1, ARYTM_1, FUNCT_4, FUNCT_6, PARTFUN1, FUNCT_3,
ALGSTR_1, DIRAF, EQREL_1, CAT_4;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSET_1, DOMAIN_1, RELAT_1,
FUNCT_1, PARTFUN1, FUNCT_2, ALGSTR_1, REAL_1, NAT_1, CARD_1, FUNCT_4,
CAT_1, CAT_3;
constructors DOMAIN_1, ALGSTR_1, REAL_1, NAT_1, CAT_3, FINSEQ_4, PARTFUN1,
XREAL_0, XBOOLE_0;
clusters SUBSET_1, FINSET_1, RELSET_1, RELAT_1, FUNCT_1, NAT_1, ZFMISC_1,
XBOOLE_0;
requirements NUMERALS, SUBSET, BOOLE;

begin

reserve o,m,r for set;

definition let o,m,r;
func (o,m) :-> r -> Function of [:{o},{m}:],{r} means
:: CAT_4:def 1
end;

definition let C be Category, a,b be Object of C;
redefine pred a,b are_isomorphic means
:: CAT_4:def 2
Hom(a,b)<>{} & Hom(b,a)<>{} &
ex f being Morphism of a,b, f' being Morphism of b,a
st f*f' = id b & f'*f = id a;
end;

begin :: Cartesian Categories

definition let C be Category;
attr C is with_finite_product means
:: CAT_4:def 3
for I being finite set, F being Function of I,the Objects of C
ex a being Object of C, F' being Projections_family of a,I
st cods F' = F & a is_a_product_wrt F';
synonym C has_finite_product;
end;

theorem :: CAT_4:1
for C being Category holds
C has_finite_product iff
(ex a being Object of C st a is terminal) &
for a,b being Object of C
ex c being Object of C, p1,p2 being Morphism of C
st dom p1 = c & dom p2 = c & cod p1 = a & cod p2 = b &
c is_a_product_wrt p1,p2;

definition
struct (CatStr)ProdCatStr
(# 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,
TerminalObj -> Element of the Objects,
CatProd -> Function of [:the Objects,the Objects:],the Objects,
Proj1,Proj2 -> Function of [:the Objects,the Objects:],the Morphisms
#);
end;

definition let C be ProdCatStr;
func [1]C -> Object of C equals
:: CAT_4:def 4
the TerminalObj of C;
let a,b be Object of C;
func a[x]b -> Object of C equals
:: CAT_4:def 5
(the CatProd of C).[a,b];
func pr1(a,b) -> Morphism of C equals
:: CAT_4:def 6
(the Proj1 of C).[a,b];
func pr2(a,b) -> Morphism of C equals
:: CAT_4:def 7
(the Proj2 of C).[a,b];
end;

definition let o,m;
func c1Cat(o,m) -> strict ProdCatStr equals
:: CAT_4:def 8
ProdCatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m,
Extract(o),(o,o):->o,(o,o):->m,(o,o):->m #);
end;

theorem :: CAT_4:2
the CatStr of c1Cat(o,m) = 1Cat(o,m);

definition
cluster strict Category-like ProdCatStr;
end;

definition let o,m be set;
cluster c1Cat(o,m) -> Category-like;
end;

theorem :: CAT_4:3
for a being Object of c1Cat(o,m) holds a = o;

theorem :: CAT_4:4
for a,b being Object of c1Cat(o,m) holds a = b;

theorem :: CAT_4:5
for f being Morphism of c1Cat(o,m) holds f = m;

theorem :: CAT_4:6
for f,g being Morphism of c1Cat(o,m) holds f = g;

theorem :: CAT_4:7
for a,b being Object of c1Cat(o,m), f being Morphism of c1Cat(o,m)
holds f in Hom(a,b);

theorem :: CAT_4:8
for a,b being Object of c1Cat(o,m), f being Morphism of c1Cat(o,m)
holds f is Morphism of a,b;

theorem :: CAT_4:9
for a,b being Object of c1Cat(o,m) holds Hom(a,b) <> {};

theorem :: CAT_4:10
for a being Object of c1Cat(o,m) holds a is terminal;

theorem :: CAT_4:11
for c being Object of c1Cat(o,m), p1,p2 being Morphism of c1Cat(o,m)
holds c is_a_product_wrt p1,p2;

definition let IT be Category-like ProdCatStr;
attr IT is Cartesian means
:: CAT_4:def 9

the TerminalObj of IT is terminal &
for a,b being Object of IT holds
cod((the Proj1 of IT).[a,b]) = a & cod((the Proj2 of IT).[a,b]) = b &
(the CatProd of IT).[a,b]
is_a_product_wrt (the Proj1 of IT).[a,b],(the Proj2 of IT).[a,b];
end;

theorem :: CAT_4:12
for o,m being set holds c1Cat(o,m) is Cartesian;

definition
cluster strict Cartesian (Category-like ProdCatStr);
end;

definition
mode Cartesian_category is Cartesian (Category-like ProdCatStr);
end;

reserve C for Cartesian_category;
reserve a,b,c,d,e,s for Object of C;

theorem :: CAT_4:13
[1]C is terminal;

theorem :: CAT_4:14
for f1,f2 being Morphism of a,[1]C holds f1 = f2;

theorem :: CAT_4:15
Hom(a,[1]C) <> {};

definition let C,a;
func term(a) -> Morphism of a,[1]C means
:: CAT_4:def 10
end;

theorem :: CAT_4:16
term a = term(a,[1]C);

theorem :: CAT_4:17
dom(term a) = a & cod(term a) = [1]C;

theorem :: CAT_4:18
Hom(a,[1]C) = {term a};

theorem :: CAT_4:19
dom pr1(a,b) = a[x]b & cod pr1(a,b) = a;

theorem :: CAT_4:20
dom pr2(a,b) = a[x]b & cod pr2(a,b) = b;

definition let C,a,b;
redefine func pr1(a,b) -> Morphism of a[x]b,a;
func pr2(a,b) -> Morphism of a[x]b,b;
end;

theorem :: CAT_4:21
Hom(a[x]b,a) <> {} & Hom(a[x]b,b) <> {};

theorem :: CAT_4:22
a[x]b is_a_product_wrt pr1(a,b),pr2(a,b);

theorem :: CAT_4:23
C has_finite_product;

theorem :: CAT_4:24
Hom(a,b) <> {} & Hom(b,a) <> {}
implies pr1(a,b) is retraction & pr2(a,b) is retraction;

definition let C,a,b,c;
let f be Morphism of c,a, g be Morphism of c,b;
assume  Hom(c,a) <> {} & Hom(c,b) <> {};
func <:f,g:> -> Morphism of c,a[x]b means
:: CAT_4:def 11
pr1(a,b)*it = f & pr2(a,b)*it = g;
end;

theorem :: CAT_4:25
Hom(c,a) <> {} & Hom(c,b) <> {} implies Hom(c,a[x]b) <> {};

theorem :: CAT_4:26
<:pr1(a,b),pr2(a,b):> = id(a[x]b);

theorem :: CAT_4:27
for f being Morphism of c,a, g being Morphism of c,b, h being Morphism of d,c
st Hom(c,a)<>{} & Hom(c,b)<>{} & Hom(d,c)<>{}
holds <:f*h,g*h:> = <:f,g:>*h;

theorem :: CAT_4:28
for f,k being Morphism of c,a, g,h being Morphism of c,b
st Hom(c,a) <> {} & Hom(c,b) <> {} & <:f,g:> = <:k,h:>
holds f = k & g = h;

theorem :: CAT_4:29
for f being Morphism of c,a, g being Morphism of c,b
st Hom(c,a) <> {} & Hom(c,b) <> {} & (f is monic or g is monic)
holds <:f,g:> is monic;

theorem :: CAT_4:30
Hom(a,a[x][1]C) <> {} & Hom(a,[1]C[x]a) <> {};

definition let C,a;
func lambda(a) -> Morphism of [1]C[x]a,a equals
:: CAT_4:def 12
pr2([1]C,a);
func lambda'(a) -> Morphism of a,[1]C[x]a equals
:: CAT_4:def 13
<:term a,id a:>;
func rho(a) -> Morphism of a[x][1]C,a equals
:: CAT_4:def 14
pr1(a,[1]C);
func rho'(a) -> Morphism of a,a[x][1]C equals
:: CAT_4:def 15
<:id a,term a:>;
end;

theorem :: CAT_4:31
lambda(a)*lambda'(a) = id a & lambda'(a)*lambda(a) = id([1]C[x]a) &
rho(a)*rho'(a) = id a & rho'(a)*rho(a) = id(a[x][1]C);

theorem :: CAT_4:32
a, a[x][1]C are_isomorphic & a,[1]C[x]a are_isomorphic;

definition let C,a,b;
func Switch(a,b) -> Morphism of a[x]b,b[x]a equals
:: CAT_4:def 16
<:pr2(a,b),pr1(a,b):>;
end;

theorem :: CAT_4:33
Hom(a[x]b,b[x]a)<>{};

theorem :: CAT_4:34
Switch(a,b)*Switch(b,a) = id(b[x]a);

theorem :: CAT_4:35
a[x]b,b[x]a are_isomorphic;

definition let C,a;
func Delta a -> Morphism of a,a[x]a equals
:: CAT_4:def 17
<:id a,id a:>;
end;

theorem :: CAT_4:36
Hom(a,a[x]a) <> {};

theorem :: CAT_4:37
for f being Morphism of a,b st Hom(a,b) <> {}
holds <:f,f:> = Delta(b)*f;

definition let C,a,b,c;
func Alpha(a,b,c) -> Morphism of (a[x]b)[x]c,a[x](b[x]c) equals
:: CAT_4:def 18
<:pr1(a,b)*pr1(a[x]b,c),<:pr2(a,b)*pr1(a[x]b,c),pr2(a[x]b,c):>:>;
func Alpha'(a,b,c) -> Morphism of a[x](b[x]c),(a[x]b)[x]c equals
:: CAT_4:def 19
<:<:pr1(a,b[x]c),pr1(b,c)*pr2(a,b[x]c):>,pr2(b,c)*pr2(a,b[x]c):>;
end;

theorem :: CAT_4:38
Hom((a[x]b)[x]c,a[x](b[x]c)) <> {} & Hom(a[x](b[x]c),(a[x]b)[x]c) <> {};

theorem :: CAT_4:39
Alpha(a,b,c)*Alpha'(a,b,c) = id(a[x](b[x]c)) &
Alpha'(a,b,c)*Alpha(a,b,c) = id((a[x]b)[x]c);

theorem :: CAT_4:40
(a[x]b)[x]c,a[x](b[x]c) are_isomorphic;

definition let C,a,b,c,d;
let f be Morphism of a,b, g be Morphism of c,d;
func f[x]g -> Morphism of a[x]c,b[x]d equals
:: CAT_4:def 20
<:f*pr1(a,c),g*pr2(a,c):>;
end;

theorem :: CAT_4:41
Hom(a,c) <> {} & Hom(b,d) <> {} implies Hom(a[x]b,c[x]d) <> {};

theorem :: CAT_4:42
(id a)[x](id b) = id(a[x]b);

theorem :: CAT_4:43
for f being Morphism of a,b, h being Morphism of c,d,
g being Morphism of e,a, k being Morphism of e,c
st Hom(a,b) <> {} & Hom(c,d) <> {} & Hom(e,a) <> {} & Hom(e,c) <> {}
holds (f[x]h)*<:g,k:> = <:f*g,h*k:>;

theorem :: CAT_4:44
for f being Morphism of c,a, g being Morphism of c,b
st Hom(c,a) <> {} & Hom(c,b) <> {} holds <:f,g:> = (f[x]g)*Delta(c);

theorem :: CAT_4:45
for f being Morphism of a,b, h being Morphism of c,d,
g being Morphism of e,a, k being Morphism of s,c
st Hom(a,b) <> {} & Hom(c,d) <> {} & Hom(e,a) <> {} & Hom(s,c) <> {}
holds (f[x]h)*(g[x]k) = (f*g)[x](h*k);

begin :: Categories with Finite Coproducts

definition let C be Category;
attr C is with_finite_coproduct means
:: CAT_4:def 21
for I being finite set, F being Function of I,the Objects of C
ex a being Object of C, F' being Injections_family of a,I
st doms F' = F & a is_a_coproduct_wrt F';
synonym C has_finite_coproduct;
end;

theorem :: CAT_4:46
for C being Category holds
C has_finite_coproduct iff
(ex a being Object of C st a is initial) &
for a,b being Object of C
ex c being Object of C, i1,i2 being Morphism of C
st dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c &
c is_a_coproduct_wrt i1,i2;

definition
struct (CatStr)CoprodCatStr
(# 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,
Initial -> Element of the Objects,
Coproduct -> Function of [:the Objects,the Objects:],the Objects,
Incl1,Incl2 -> Function of [:the Objects,the Objects:],the Morphisms
#);
end;

definition let C be CoprodCatStr;
func [0]C -> Object of C equals
:: CAT_4:def 22
the Initial of C;
let a,b be Object of C;
func a+b -> Object of C equals
:: CAT_4:def 23
(the Coproduct of C).[a,b];
func in1(a,b) -> Morphism of C equals
:: CAT_4:def 24
(the Incl1 of C).[a,b];
func in2(a,b) -> Morphism of C equals
:: CAT_4:def 25
(the Incl2 of C).[a,b];
end;

definition let o,m;
func c1Cat*(o,m) -> strict CoprodCatStr equals
:: CAT_4:def 26
CoprodCatStr(# {o},{m},{m}-->o,{m}-->o,(m,m).-->m,{o}-->m,
Extract(o),(o,o):->o,(o,o):->m,(o,o):->m #);
end;

theorem :: CAT_4:47
the CatStr of c1Cat*(o,m) = 1Cat(o,m);

definition
cluster strict Category-like CoprodCatStr;
end;

definition let o,m be set;
cluster c1Cat*(o,m) -> Category-like;
end;

theorem :: CAT_4:48
for a being Object of c1Cat*(o,m) holds a = o;

theorem :: CAT_4:49
for a,b being Object of c1Cat*(o,m) holds a = b;

theorem :: CAT_4:50
for f being Morphism of c1Cat*(o,m) holds f = m;

theorem :: CAT_4:51
for f,g being Morphism of c1Cat*(o,m) holds f = g;

theorem :: CAT_4:52
for a,b being Object of c1Cat*(o,m), f being Morphism of c1Cat*(o,m)
holds f in Hom(a,b);

theorem :: CAT_4:53
for a,b being Object of c1Cat*(o,m), f being Morphism of c1Cat*(o,m)
holds f is Morphism of a,b;

theorem :: CAT_4:54
for a,b being Object of c1Cat*(o,m) holds Hom(a,b) <> {};

theorem :: CAT_4:55
for a being Object of c1Cat*(o,m) holds a is initial;

theorem :: CAT_4:56
for c being Object of c1Cat*(o,m),
i1,i2 being Morphism of c1Cat*(o,m) holds c is_a_coproduct_wrt i1,i2;

definition let IT be Category-like CoprodCatStr;
attr IT is Cocartesian means
:: CAT_4:def 27

the Initial of IT is initial &
for a,b being Object of IT holds
dom((the Incl1 of IT).[a,b]) = a & dom((the Incl2 of IT).[a,b]) = b &
(the Coproduct of IT).[a,b]
is_a_coproduct_wrt (the Incl1 of IT).[a,b],(the Incl2 of IT).[a,b];
end;

theorem :: CAT_4:57
for o,m being set holds c1Cat*(o,m) is Cocartesian;

definition
cluster strict Cocartesian (Category-like CoprodCatStr);
end;

definition
mode Cocartesian_category is Cocartesian (Category-like CoprodCatStr);
end;

reserve C for Cocartesian_category;
reserve a,b,c,d,e,s for Object of C;

theorem :: CAT_4:58
[0]C is initial;

theorem :: CAT_4:59
for f1,f2 being Morphism of [0]C,a holds f1 = f2;

definition let C,a;
func init a -> Morphism of [0]C, a means
:: CAT_4:def 28
end;

theorem :: CAT_4:60
Hom([0]C,a) <> {};

theorem :: CAT_4:61
init a = init([0]C,a);

theorem :: CAT_4:62
dom(init a) = [0]C & cod(init a) = a;

theorem :: CAT_4:63
Hom([0]C,a) = {init a};

theorem :: CAT_4:64
dom in1(a,b) = a & cod in1(a,b) = a+b;

theorem :: CAT_4:65
dom in2(a,b) = b & cod in2(a,b) = a+b;

theorem :: CAT_4:66
Hom(a,a+b) <> {} & Hom(b,a+b) <> {};

theorem :: CAT_4:67
a+b is_a_coproduct_wrt in1(a,b),in2(a,b);

theorem :: CAT_4:68
C has_finite_coproduct;

theorem :: CAT_4:69
Hom(a,b) <> {} & Hom(b,a) <> {}
implies in1(a,b) is coretraction & in2(a,b) is coretraction;

definition let C,a,b; redefine
func in1(a,b) -> Morphism of a,a+b;
func in2(a,b) -> Morphism of b,a+b;
end;

definition let C,a,b,c;
let f be Morphism of a,c, g be Morphism of b,c;
assume  Hom(a,c) <> {} & Hom(b,c) <> {};
func [\$f,g\$] -> Morphism of a+b,c means
:: CAT_4:def 29
it*in1(a,b) = f & it*in2(a,b) = g;
end;

theorem :: CAT_4:70
Hom(a,c) <> {} & Hom(b,c) <> {} implies Hom(a+b,c) <> {};

theorem :: CAT_4:71
[\$in1(a,b),in2(a,b)\$] = id(a+b);

theorem :: CAT_4:72
for f being Morphism of a,c, g being Morphism of b,c, h being Morphism of c,d
st Hom(a,c)<>{} & Hom(b,c)<>{} & Hom(c,d)<>{}
holds [\$h*f,h*g\$] = h*[\$f,g\$];

theorem :: CAT_4:73
for f,k being Morphism of a,c, g,h being Morphism of b,c
st Hom(a,c) <> {} & Hom(b,c) <> {} & [\$f,g\$] = [\$k,h\$]
holds f = k & g = h;

theorem :: CAT_4:74
for f being Morphism of a,c, g being Morphism of b,c
st Hom(a,c) <> {} & Hom(b,c) <> {} & (f is epi or g is epi)
holds [\$f,g\$] is epi;

theorem :: CAT_4:75
a, a+[0]C are_isomorphic & a,[0]C+a are_isomorphic;

theorem :: CAT_4:76
a+b,b+a are_isomorphic;

theorem :: CAT_4:77
(a+b)+c,a+(b+c) are_isomorphic;

definition let C,a;
func nabla a -> Morphism of a+a,a equals
:: CAT_4:def 30
[\$id a,id a\$];
end;

definition let C,a,b,c,d;
let f be Morphism of a,c, g be Morphism of b,d;
func f+g -> Morphism of a+b,c+d equals
:: CAT_4:def 31
[\$in1(c,d)*f,in2(c,d)*g\$];
end;

theorem :: CAT_4:78
Hom(a,c) <> {} & Hom(b,d) <> {} implies Hom(a+b,c+d) <> {};

theorem :: CAT_4:79
(id a)+(id b) = id(a+b);

theorem :: CAT_4:80
for f being Morphism of a,c, h being Morphism of b,d,
g being Morphism of c,e, k being Morphism of d,e
st Hom(a,c) <> {} & Hom(b,d) <> {} & Hom(c,e) <> {} & Hom(d,e) <> {}
holds [\$g,k\$]*(f+h) = [\$g*f,k*h\$];

theorem :: CAT_4:81
for f being Morphism of a,c, g being Morphism of b,c
st Hom(a,c) <> {} & Hom(b,c) <> {} holds nabla(c)*(f+g) = [\$f,g\$];

theorem :: CAT_4:82
for f being Morphism of a,c, h being Morphism of b,d,
g being Morphism of c,e, k being Morphism of d,s
st Hom(a,c) <> {} & Hom(b,d) <> {} & Hom(c,e) <> {} & Hom(d,s) <> {}
holds (g+k)*(f+h) = (g*f)+(k*h);
```