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

### Products and Coproducts in Categories

by
Czeslaw Bylinski

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

```environ

vocabulary CAT_1, FUNCT_1, FINSEQ_4, RELAT_1, FUNCOP_1, FUNCT_4, BOOLE,
FUNCT_6, OPPCAT_1, WELLORD1, CAT_3;
notation TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCOP_1, FUNCT_4,
FUNCT_2, FINSEQ_4, CAT_1, OPPCAT_1;
constructors OPPCAT_1, FINSEQ_4, MEMBERED, XBOOLE_0;
clusters RELSET_1, MEMBERED, ZFMISC_1, XBOOLE_0;
requirements SUBSET, BOOLE;

begin :: Indexed families

reserve I for set, x,x1,x2,y,z for set, A for non empty set;
reserve C,D for Category;
reserve a,b,c,d for Object of C;
reserve f,g,h,i,j,k,p1,p2,q1,q2,i1,i2,j1,j2 for Morphism of C;

definition let I,A; let F be Function of I,A; let x be set;
assume
x in I;
redefine func F/.x equals
:: CAT_3:def 1
F.x;
end;

scheme LambdaIdx{I()->set,A()->non empty set,F(set)->Element of A()}:
ex F being Function of I(),A() st for x st x in I() holds F/.x = F(x);

theorem :: CAT_3:1
for F1,F2 being Function of I,A st for x st x in I holds F1/.x = F2/.x
holds F1 = F2;

scheme FuncIdx_correctness{I()->set,A()->non empty set,F(set)->Element of A()}:
(ex F being Function of I(),A() st for x st x in I() holds F/.x = F(x)) &
(for F1,F2 being Function of I(),A() st
(for x st x in I() holds F1/.x = F(x)) &
(for x st x in I() holds F2/.x = F(x))
holds F1 = F2);

definition let A,I; let a be Element of A;
redefine func I --> a -> Function of I,A;
end;

theorem :: CAT_3:2
for a being Element of A st x in I holds (I --> a)/.x = a;

canceled 4;

theorem :: CAT_3:7
x1 <> x2 implies for y1,y2 being Element of A
holds ((x1,x2) --> (y1,y2))/.x1 = y1 & ((x1,x2) --> (y1,y2))/.x2 = y2;

begin :: Indexed families of morphisms

definition let C,I; let F be Function of I,the Morphisms of C;
canceled;

func doms F -> Function of I, the Objects of C means
:: CAT_3:def 3
for x st x in I holds it/.x = dom(F/.x);
func cods F -> Function of I, the Objects of C means
:: CAT_3:def 4
for x st x in I holds it/.x = cod(F/.x);
end;

theorem :: CAT_3:8
doms(I-->f) = I-->(dom f);

theorem :: CAT_3:9
cods(I-->f) = I-->(cod f);

theorem :: CAT_3:10
doms((x1,x2)-->(p1,p2)) = (x1,x2)-->(dom p1,dom p2);

theorem :: CAT_3:11
cods((x1,x2)-->(p1,p2)) = (x1,x2)-->(cod p1,cod p2);

definition let C,I; let F be Function of I,the Morphisms of C;
func F opp -> Function of I,the Morphisms of C opp means
:: CAT_3:def 5
for x st x in I holds it/.x = (F/.x) opp;
end;

theorem :: CAT_3:12
(I --> f) opp = I --> f opp;

theorem :: CAT_3:13
x1 <> x2 implies ((x1,x2)-->(p1,p2)) opp = (x1,x2)-->(p1 opp,p2 opp);

theorem :: CAT_3:14
for F being Function of I,the Morphisms of C holds F opp opp = F;

definition let C,I; let F be Function of I,the Morphisms of C opp;
func opp F -> Function of I,the Morphisms of C means
:: CAT_3:def 6
for x st x in I holds it/.x = opp (F/.x);
end;

theorem :: CAT_3:15
for f being Morphism of C opp holds opp(I --> f) = I --> (opp f);

theorem :: CAT_3:16
x1 <> x2 implies for p1,p2 being Morphism of C opp holds
opp ((x1,x2)-->(p1,p2)) = (x1,x2)-->(opp p1,opp p2);

theorem :: CAT_3:17
for F being Function of I,the Morphisms of C holds opp(F opp) = F;

definition let C,I; let F be Function of I,the Morphisms of C, f;
func F*f -> Function of I,the Morphisms of C means
:: CAT_3:def 7
for x st x in I holds it/.x = (F/.x)*f;
func f*F -> Function of I,the Morphisms of C means
:: CAT_3:def 8
for x st x in I holds it/.x = f*(F/.x);
end;

theorem :: CAT_3:18
x1 <> x2 implies ((x1,x2)-->(p1,p2))*f = (x1,x2)-->(p1*f,p2*f);

theorem :: CAT_3:19
x1 <> x2 implies f*((x1,x2)-->(p1,p2)) = (x1,x2)-->(f*p1,f*p2);

theorem :: CAT_3:20
for F being Function of I,the Morphisms of C st doms F = I-->cod f
holds doms(F*f) = I-->dom f & cods(F*f) = cods F;

theorem :: CAT_3:21
for F being Function of I,the Morphisms of C st cods F = I-->dom f
holds doms(f*F) = doms F & cods(f*F) = I-->cod f;

definition let C,I; let F,G be Function of I,the Morphisms of C;
func F"*"G -> Function of I,the Morphisms of C means
:: CAT_3:def 9
for x st x in I holds it/.x = (F/.x)*(G/.x);
end;

theorem :: CAT_3:22
for F,G being Function of I,the Morphisms of C st doms F = cods G
holds doms(F"*"G) = doms G & cods(F"*"G) = cods F;

theorem :: CAT_3:23
x1 <> x2 implies
((x1,x2)-->(p1,p2))"*"((x1,x2)-->(q1,q2)) = (x1,x2)-->(p1*q1,p2*q2);

theorem :: CAT_3:24
for F being Function of I,the Morphisms of C holds F*f = F"*"(I-->f);

theorem :: CAT_3:25
for F being Function of I,the Morphisms of C holds f*F = (I-->f)"*"F;

begin :: Retractions and Coretractions

definition let C;
let IT be Morphism of C;
attr IT is retraction means
:: CAT_3:def 10
ex g st cod g = dom IT & IT*g = id(cod IT);
attr IT is coretraction means
:: CAT_3:def 11
ex g st dom g = cod IT & g*IT = id(dom IT);
end;

theorem :: CAT_3:26
f is retraction implies f is epi;

theorem :: CAT_3:27
f is coretraction implies f is monic;

theorem :: CAT_3:28
f is retraction & g is retraction & dom g = cod f
implies g*f is retraction;

theorem :: CAT_3:29
f is coretraction & g is coretraction & dom g = cod f
implies g*f is coretraction;

theorem :: CAT_3:30
dom g = cod f & g*f is retraction implies g is retraction;

theorem :: CAT_3:31
dom g = cod f & g*f is coretraction implies f is coretraction;

theorem :: CAT_3:32
f is retraction & f is monic implies f is invertible;

theorem :: CAT_3:33
f is coretraction & f is epi implies f is invertible;

theorem :: CAT_3:34
f is invertible iff f is retraction & f is coretraction;

theorem :: CAT_3:35
for T being Functor of C,D st f is retraction holds T.f is retraction;

theorem :: CAT_3:36
for T being Functor of C,D st f is coretraction holds T.f is coretraction;

theorem :: CAT_3:37
f is retraction iff f opp is coretraction;

theorem :: CAT_3:38
f is coretraction iff f opp is retraction;

begin :: Morphisms determined by a terminal Object

definition let C,a,b;
assume
b is terminal;
func term(a,b) -> Morphism of a,b means
:: CAT_3:def 12
end;

theorem :: CAT_3:39
b is terminal implies dom(term(a,b)) = a & cod(term(a,b)) = b;

theorem :: CAT_3:40
b is terminal & dom f = a & cod f = b implies term(a,b) = f;

theorem :: CAT_3:41
for f being Morphism of a,b st b is terminal holds term(a,b) = f;

begin :: Morphisms determined by an iniatial object

definition let C,a,b;
assume
a is initial;
func init(a,b) -> Morphism of a,b means
:: CAT_3:def 13
end;

theorem :: CAT_3:42
a is initial implies dom(init(a,b)) = a & cod(init(a,b)) = b;

theorem :: CAT_3:43
a is initial & dom f = a & cod f = b implies init(a,b) = f;

theorem :: CAT_3:44
for f being Morphism of a,b st a is initial holds init(a,b) = f;

begin :: Products

definition let C,a,I;
mode Projections_family of a,I -> Function of I,the Morphisms of C means
:: CAT_3:def 14
doms it = I --> a;
end;

theorem :: CAT_3:45
for F being Projections_family of a,I st x in I holds dom(F/.x) = a;

theorem :: CAT_3:46
for F being Function of {},the Morphisms of C
holds F is Projections_family of a,{};

theorem :: CAT_3:47
dom f = a implies {y} --> f is Projections_family of a,{y};

theorem :: CAT_3:48
dom p1 = a & dom p2 = a
implies (x1,x2)-->(p1,p2) is Projections_family of a,{x1,x2};

canceled;

theorem :: CAT_3:50
for F being Projections_family of a,I st cod f = a
holds F*f is Projections_family of dom f,I;

theorem :: CAT_3:51
for F being Function of I,the Morphisms of C,
G being Projections_family of a,I st doms F = cods G
holds F"*"G is Projections_family of a,I;

theorem :: CAT_3:52
for F being Projections_family of cod f,I holds (f opp)*(F opp) = (F*f)
opp;

definition let C,a,I; let F be Function of I,the Morphisms of C;
pred a is_a_product_wrt F means
:: CAT_3:def 15
F is Projections_family of a,I &
for b for F' being Projections_family of b,I st cods F = cods F'
ex h st h in Hom(b,a) &
for k st k in Hom(b,a) holds
(for x st x in I holds (F/.x)*k = F'/.x) iff h = k;
end;

theorem :: CAT_3:53
for F being Projections_family of c,I, F' being Projections_family of d,I
st c is_a_product_wrt F & d is_a_product_wrt F' & cods F = cods F'
holds c,d are_isomorphic;

theorem :: CAT_3:54
for F being Projections_family of c,I
st c is_a_product_wrt F &
for x1,x2 st x1 in I & x2 in I holds Hom(cod(F/.x1),cod(F/.x2)) <> {}
for x st x in I holds F/.x is retraction;

theorem :: CAT_3:55
for F being Function of {},the Morphisms of C holds
a is_a_product_wrt F iff a is terminal;

theorem :: CAT_3:56
for F being Projections_family of a,I
st a is_a_product_wrt F & dom f = b & cod f = a & f is invertible
holds b is_a_product_wrt F*f;

theorem :: CAT_3:57
a is_a_product_wrt {y} --> id a;

theorem :: CAT_3:58
for F being Projections_family of a,I
st a is_a_product_wrt F &
for x st x in I holds cod(F/.x) is terminal
holds a is terminal;

definition let C,c,p1,p2;
pred c is_a_product_wrt p1,p2 means
:: CAT_3:def 16
dom p1 = c & dom p2 = c &
for d,f,g st f in Hom(d,cod p1) & g in Hom(d,cod p2)
ex h st h in Hom(d,c) &
for k st k in Hom(d,c) holds p1*k = f & p2*k = g iff h = k;
end;

theorem :: CAT_3:59
x1 <> x2 implies
(c is_a_product_wrt p1,p2 iff c is_a_product_wrt (x1,x2)-->(p1,p2));

theorem :: CAT_3:60
Hom(c,a) <> {} & Hom(c,b) <> {} implies
for p1 being Morphism of c,a, p2 being Morphism of c,b
holds c is_a_product_wrt p1,p2 iff
for d st Hom(d,a)<>{} & Hom(d,b)<>{} holds
Hom(d,c) <> {} &
for f being Morphism of d,a, g being Morphism of d,b
ex h being Morphism of d,c st
for k being Morphism of d,c holds p1*k = f & p2*k = g iff h = k;

theorem :: CAT_3:61
c is_a_product_wrt p1,p2 & d is_a_product_wrt q1,q2 &
cod p1 = cod q1 & cod p2 = cod q2 implies c,d are_isomorphic;

theorem :: CAT_3:62
c is_a_product_wrt p1,p2 & Hom(cod p1,cod p2) <> {} & Hom(cod p2,cod p1)
<>
{}
implies p1 is retraction & p2 is retraction;

theorem :: CAT_3:63
c is_a_product_wrt p1,p2 & h in Hom(c,c) & p1*h = p1 & p2*h = p2
implies h = id c;

theorem :: CAT_3:64
c is_a_product_wrt p1,p2 & dom f = d & cod f = c & f is invertible
implies d is_a_product_wrt p1*f,p2*f;

theorem :: CAT_3:65
c is_a_product_wrt p1,p2 & cod p2 is terminal
implies c,cod p1 are_isomorphic;

theorem :: CAT_3:66
c is_a_product_wrt p1,p2 & cod p1 is terminal
implies c,cod p2 are_isomorphic;

begin :: Coproducts

definition let C,c,I;
mode Injections_family of c,I -> Function of I,the Morphisms of C means
:: CAT_3:def 17
cods it = I --> c;
end;

theorem :: CAT_3:67
for F being Injections_family of c,I st x in I holds cod(F/.x) = c;

theorem :: CAT_3:68
for F being Function of {},the Morphisms of C
holds F is Injections_family of a,{};

theorem :: CAT_3:69
cod f = a implies {y} --> f is Injections_family of a,{y};

theorem :: CAT_3:70
cod p1 = c & cod p2 = c
implies (x1,x2)-->(p1,p2) is Injections_family of c,{x1,x2};

canceled;

theorem :: CAT_3:72
for F being Injections_family of b,I st dom f = b
holds f*F is Injections_family of cod f,I;

theorem :: CAT_3:73
for F being Injections_family of b,I,
G being Function of I,the Morphisms of C st doms F = cods G
holds F"*"G is Injections_family of b,I;

theorem :: CAT_3:74
for F be Function of I,the Morphisms of C holds
F is Projections_family of c,I iff F opp is Injections_family of c opp,I;

theorem :: CAT_3:75
for F be Function of I,the Morphisms of C opp, c being Object of C opp holds
F is Injections_family of c,I iff opp F is Projections_family of opp c,I;

theorem :: CAT_3:76
for F being Injections_family of dom f,I holds (F opp)*(f opp) = (f*F) opp
;

definition let C,c,I; let F be Function of I,the Morphisms of C;
pred c is_a_coproduct_wrt F means
:: CAT_3:def 18
F is Injections_family of c,I &
for d for F' being Injections_family of d,I st doms F = doms F'
ex h st h in Hom(c,d) &
for k st k in Hom(c,d) holds
(for x st x in I holds k*(F/.x) = F'/.x) iff h = k;
end;

theorem :: CAT_3:77
for F being Function of I,the Morphisms of C holds
c is_a_product_wrt F iff c opp is_a_coproduct_wrt F opp;

theorem :: CAT_3:78
for F being Injections_family of c,I, F' being Injections_family of d,I
st c is_a_coproduct_wrt F & d is_a_coproduct_wrt F' & doms F = doms F'
holds c,d are_isomorphic;

theorem :: CAT_3:79
for F being Injections_family of c,I
st c is_a_coproduct_wrt F &
for x1,x2 st x1 in I & x2 in I holds Hom(dom(F/.x1),dom(F/.x2)) <> {}
for x st x in I holds F/.x is coretraction;

theorem :: CAT_3:80
for F being Injections_family of a,I
st a is_a_coproduct_wrt F & dom f = a & cod f = b & f is invertible
holds b is_a_coproduct_wrt f*F;

theorem :: CAT_3:81
for F being Injections_family of a,{} holds
a is_a_coproduct_wrt F iff a is initial;

theorem :: CAT_3:82
a is_a_coproduct_wrt {y} --> id a;

theorem :: CAT_3:83
for F being Injections_family of a,I
st a is_a_coproduct_wrt F &
for x st x in I holds dom(F/.x) is initial
holds a is initial;

definition let C,c,i1,i2;
pred c is_a_coproduct_wrt i1,i2 means
:: CAT_3:def 19

cod i1 = c & cod i2 = c &
for d,f,g st f in Hom(dom i1,d) & g in Hom(dom i2,d)
ex h st h in Hom(c,d) &
for k st k in Hom(c,d) holds k*i1 = f & k*i2 = g iff h = k;
end;

theorem :: CAT_3:84
c is_a_product_wrt p1,p2 iff c opp is_a_coproduct_wrt p1 opp, p2 opp;

theorem :: CAT_3:85
x1 <> x2 implies
(c is_a_coproduct_wrt i1,i2 iff c is_a_coproduct_wrt (x1,x2)-->(i1,i2));

theorem :: CAT_3:86
c is_a_coproduct_wrt i1,i2 & d is_a_coproduct_wrt j1,j2 &
dom i1 = dom j1 & dom i2 = dom j2 implies c,d are_isomorphic;

theorem :: CAT_3:87
Hom(a,c) <> {} & Hom(b,c) <> {} implies
for i1 being Morphism of a,c, i2 being Morphism of b,c
holds c is_a_coproduct_wrt i1,i2 iff
for d st Hom(a,d)<>{} & Hom(b,d)<>{} holds
Hom(c,d) <> {} &
for f being Morphism of a,d, g being Morphism of b,d
ex h being Morphism of c,d st
for k being Morphism of c,d holds k*i1 = f & k*i2 = g iff h = k;

theorem :: CAT_3:88
c is_a_coproduct_wrt i1,i2 &
Hom(dom i1,dom i2) <> {} & Hom(dom i2,dom i1) <> {}
implies i1 is coretraction & i2 is coretraction;

theorem :: CAT_3:89
c is_a_coproduct_wrt i1,i2 & h in Hom(c,c) & h*i1 = i1 & h*i2 = i2
implies h = id c;

theorem :: CAT_3:90
c is_a_coproduct_wrt i1,i2 & dom f = c & cod f = d & f is invertible
implies d is_a_coproduct_wrt f*i1,f*i2;

theorem :: CAT_3:91
c is_a_coproduct_wrt i1,i2 & dom i2 is initial
implies dom i1,c are_isomorphic;

theorem :: CAT_3:92
c is_a_coproduct_wrt i1,i2 & dom i1 is initial
implies dom i2,c are_isomorphic;
```