:: Products and Coproducts in Categories
:: by Czes{\l}aw Byli\'nski
::
:: Received May 11, 1992
:: Copyright (c) 1992-2021 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 XBOOLE_0, CAT_1, SUBSET_1, FUNCT_1, PARTFUN1, FUNCOP_1, STRUCT_0,
FUNCT_6, RELAT_1, GRAPH_1, FUNCT_4, ARYTM_0, FVSUM_1, ALGSTR_0, WELLORD1,
TARSKI, CARD_1, CAT_3, MONOID_0;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCOP_1,
FUNCT_4, ORDINAL1, NUMBERS, FUNCT_2, STRUCT_0, GRAPH_1, CAT_1, OPPCAT_1;
constructors PARTFUN1, OPPCAT_1, FUNCOP_1, RELSET_1, NUMBERS, FUNCT_4;
registrations XBOOLE_0, RELSET_1, STRUCT_0, CAT_1, OPPCAT_1;
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;
scheme :: CAT_3:sch 1
LambdaIdx{I()->set,A()->non empty set,F(object)->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 :: CAT_3:sch 2
FuncIdxcorrectness{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,x;
let a be Element of A;
redefine func x .--> a -> Function of {x},A;
end;
theorem :: CAT_3:2
for a being Element of A st x in I holds (I --> a)/.x = a;
theorem :: CAT_3:3
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 carrier' of C;
func doms F -> Function of I, the carrier of C means
:: CAT_3:def 1
for x st x in I holds it/.x = dom(F/.x);
func cods F -> Function of I, the carrier of C means
:: CAT_3:def 2
for x st x in I holds it/.x = cod(F/.x);
end;
theorem :: CAT_3:4
doms(I-->f) = I-->(dom f);
theorem :: CAT_3:5
cods(I-->f) = I-->(cod f);
theorem :: CAT_3:6
doms((x1,x2)-->(p1,p2)) = (x1,x2)-->(dom p1,dom p2);
theorem :: CAT_3:7
cods((x1,x2)-->(p1,p2)) = (x1,x2)-->(cod p1,cod p2);
definition
let C,I;
let F be Function of I,the carrier' of C;
func F opp -> Function of I,the carrier' of C opp means
:: CAT_3:def 3
for x st x in I holds it/.x = (F/.x) opp;
end;
theorem :: CAT_3:8
(I --> f) opp = I --> f opp;
theorem :: CAT_3:9
x1 <> x2 implies ((x1,x2)-->(p1,p2)) opp = (x1,x2)-->(p1 opp,p2 opp);
theorem :: CAT_3:10
for F being Function of I,the carrier' of C holds F opp opp = F;
definition
let C,I;
let F be Function of I,the carrier' of C opp;
func opp F -> Function of I,the carrier' of C means
:: CAT_3:def 4
for x st x in I holds it/.x = opp (F/.x);
end;
theorem :: CAT_3:11
for f being Morphism of C opp holds opp(I --> f) = I --> (opp f);
theorem :: CAT_3:12
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:13
for F being Function of I,the carrier' of C holds opp(F opp) = F;
definition
let C,I;
let F be Function of I,the carrier' of C, f;
func F*f -> Function of I,the carrier' of C means
:: CAT_3:def 5
for x st x in I holds it/.x = (F/.x)(*)f;
func f*F -> Function of I,the carrier' of C means
:: CAT_3:def 6
for x st x in I holds it/.x = f(*)(F/.x);
end;
theorem :: CAT_3:14
x1 <> x2 implies ((x1,x2)-->(p1,p2))*f = (x1,x2)-->(p1(*)f,p2(*)f);
theorem :: CAT_3:15
x1 <> x2 implies f*((x1,x2)-->(p1,p2)) = (x1,x2)-->(f(*)p1,f(*)p2);
theorem :: CAT_3:16
for F being Function of I,the carrier' of C st doms F = I-->cod
f holds doms(F*f) = I-->dom f & cods(F*f) = cods F;
theorem :: CAT_3:17
for F being Function of I,the carrier' 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 carrier' of C;
func F"*"G -> Function of I,the carrier' of C means
:: CAT_3:def 7
for x st x in I holds it/.x = (F/.x)(*)(G/.x);
end;
theorem :: CAT_3:18
for F,G being Function of I,the carrier' of C st doms F = cods G
holds doms(F"*"G) = doms G & cods(F"*"G) = cods F;
theorem :: CAT_3:19
x1 <> x2 implies ((x1,x2)-->(p1,p2))"*"((x1,x2)-->(q1,q2)) = (x1,x2)
-->(p1(*)q1,p2(*)q2);
theorem :: CAT_3:20
for F being Function of I,the carrier' of C holds F*f = F"*"(I-->f);
theorem :: CAT_3:21
for F being Function of I,the carrier' of C holds f*F = (I-->f)"*"F;
begin :: Retractions and Coretractions
reserve f for Morphism of a,b,
g for Morphism of b,a;
definition
let C,a,b;
let IT be Morphism of a,b;
attr IT is retraction means
:: CAT_3:def 8
Hom(a,b) <> {} & Hom(b,a) <> {} &
ex g st IT*g = id b;
attr IT is coretraction means
:: CAT_3:def 9
Hom(a,b) <> {} & Hom(b,a) <> {} &
ex g st g*IT = id a;
end;
theorem :: CAT_3:22
f is retraction implies f is epi;
theorem :: CAT_3:23
f is coretraction implies f is monic;
reserve g for Morphism of b,c;
theorem :: CAT_3:24
f is retraction & g is retraction implies g*f is retraction;
theorem :: CAT_3:25
f is coretraction & g is coretraction implies g*f is coretraction;
theorem :: CAT_3:26
Hom(a,b) <> {} & Hom(b,a) <> {} &
g*f is retraction implies g is retraction;
theorem :: CAT_3:27
Hom(b,c) <> {} & Hom(c,b) <> {} &
g*f is coretraction implies f is coretraction;
theorem :: CAT_3:28
f is retraction & f is monic implies f is invertible;
theorem :: CAT_3:29
f is coretraction & f is epi implies f is invertible;
theorem :: CAT_3:30
f is invertible iff f is retraction & f is coretraction;
definition let C,a,b such that
Hom(a,b) <> {};
let D; let T be Functor of C,D, f be Morphism of a,b;
func T/.f -> Morphism of T.a, T.b equals
:: CAT_3:def 10
T.f;
end;
theorem :: CAT_3:31
for T being Functor of C,D st f is retraction holds T/.f is retraction;
theorem :: CAT_3:32
for T being Functor of C,D st f is coretraction holds T/.f is coretraction;
theorem :: CAT_3:33
f is retraction iff f opp is coretraction;
theorem :: CAT_3:34
f is coretraction iff f opp is retraction;
begin :: carrier' determined by a terminal Object
reserve f,g for Morphism of C;
definition
let C,a,b;
assume
b is terminal;
func term(a,b) -> Morphism of a,b means
:: CAT_3:def 11
not contradiction;
end;
theorem :: CAT_3:35
b is terminal implies dom(term(a,b)) = a & cod(term(a,b)) = b;
theorem :: CAT_3:36
b is terminal & dom f = a & cod f = b implies term(a,b) = f;
theorem :: CAT_3:37
for f being Morphism of a,b st b is terminal holds term(a,b) = f;
begin :: carrier' 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 12
not contradiction;
end;
theorem :: CAT_3:38
a is initial implies dom(init(a,b)) = a & cod(init(a,b)) = b;
theorem :: CAT_3:39
a is initial & dom f = a & cod f = b implies init(a,b) = f;
theorem :: CAT_3:40
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 carrier' of C means
:: CAT_3:def 13
doms it = I --> a;
end;
theorem :: CAT_3:41
for F being Projections_family of a,I st x in I holds dom(F/.x) = a;
theorem :: CAT_3:42
for F being Function of {},the carrier' of C holds F is
Projections_family of a,{};
theorem :: CAT_3:43
dom f = a implies y .--> f is Projections_family of a,{y};
theorem :: CAT_3:44
dom p1 = a & dom p2 = a implies (x1,x2)-->(p1,p2) is
Projections_family of a,{x1,x2};
theorem :: CAT_3:45
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:46
for F being Function of I,the carrier' 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:47
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 carrier' of C;
pred a is_a_product_wrt F means
:: CAT_3:def 14
F is Projections_family of a,I &
for b for F9 being Projections_family of b,I
st cods F = cods F9
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 = F9/.x) iff h = k;
end;
theorem :: CAT_3:48
for F being Projections_family of c,I, F9 being
Projections_family of d,I st c is_a_product_wrt F & d is_a_product_wrt F9 &
cods F = cods F9 holds c,d are_isomorphic;
theorem :: CAT_3:49
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
for d being Object of C st d = cod(F/.x) & Hom(c,d) <> {}
for f being Morphism of c,d st f = F/.x
holds f is retraction;
theorem :: CAT_3:50
for F being Function of {},the carrier' of C holds a
is_a_product_wrt F iff a is terminal;
theorem :: CAT_3:51
for F being Projections_family of a,I st a is_a_product_wrt F
for f being Morphism of b,a st
dom f = b & cod f = a &
f is invertible holds b is_a_product_wrt F*f;
theorem :: CAT_3:52
a is_a_product_wrt y .--> id a;
theorem :: CAT_3:53
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 15
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:54
x1 <> x2 implies (c is_a_product_wrt p1,p2 iff c
is_a_product_wrt (x1,x2)-->(p1,p2));
theorem :: CAT_3:55
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:56
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:57
for p1 being Morphism of c,a, p2 being Morphism of c,b st
Hom(c,a) <> {} & Hom(c,b) <> {} &
c is_a_product_wrt p1,p2 &
Hom(a,b) <> {} & Hom(b,a) <> {}
holds p1 is retraction & p2 is retraction;
theorem :: CAT_3:58
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:59
for f being Morphism of d,c
st c is_a_product_wrt p1,p2 & dom f = d & cod f = c & f is invertible
holds d is_a_product_wrt p1(*)f,p2(*)f;
theorem :: CAT_3:60
c is_a_product_wrt p1,p2 & cod p2 is terminal implies c,cod p1 are_isomorphic
;
theorem :: CAT_3:61
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 carrier' of C means
:: CAT_3:def 16
cods it = I --> c;
end;
theorem :: CAT_3:62
for F being Injections_family of c,I st x in I holds cod(F/.x) = c;
theorem :: CAT_3:63
for F being Function of {},the carrier' of C holds F is
Injections_family of a,{};
theorem :: CAT_3:64
cod f = a implies y .--> f is Injections_family of a,{y};
theorem :: CAT_3:65
cod p1 = c & cod p2 = c implies (x1,x2)-->(p1,p2) is
Injections_family of c,{x1,x2};
theorem :: CAT_3:66
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:67
for F being Injections_family of b,I, G being Function of I,the
carrier' of C st doms F = cods G holds F"*"G is Injections_family of b,I;
theorem :: CAT_3:68
for F be Function of I,the carrier' of C holds F is
Projections_family of c,I iff F opp is Injections_family of c opp,I;
theorem :: CAT_3:69
for F be Function of I,the carrier' 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:70
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 carrier' of C;
pred c is_a_coproduct_wrt F means
:: CAT_3:def 17
F is Injections_family of c,I &
for d for F9 being Injections_family of d,I st doms F = doms F9 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) = F9/.x
) iff h = k;
end;
theorem :: CAT_3:71
for F being Function of I,the carrier' of C holds c is_a_product_wrt F
iff c opp is_a_coproduct_wrt F opp;
theorem :: CAT_3:72
for F being Injections_family of c,I, F9 being Injections_family
of d,I st c is_a_coproduct_wrt F & d is_a_coproduct_wrt F9 & doms F = doms F9
holds c,d are_isomorphic;
theorem :: CAT_3:73
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
for d being Object of C st d = dom(F/.x) & Hom(d,c) <> {}
for f being Morphism of d,c st f = F/.x
holds f is coretraction;
theorem :: CAT_3:74
for f being Morphism of a,b
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:75
for F being Injections_family of a,{} holds a is_a_coproduct_wrt
F iff a is initial;
theorem :: CAT_3:76
a is_a_coproduct_wrt y .--> id a;
theorem :: CAT_3:77
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 18
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:78
c is_a_product_wrt p1,p2 iff c opp is_a_coproduct_wrt p1 opp, p2 opp;
theorem :: CAT_3:79
x1 <> x2 implies (c is_a_coproduct_wrt i1,i2 iff c
is_a_coproduct_wrt (x1,x2)-->(i1,i2));
theorem :: CAT_3:80
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:81
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:82
for i1 being Morphism of a,c, i2 being Morphism of b,c
st Hom(a,c) <> {} & Hom(b,c) <> {}
holds
c is_a_coproduct_wrt i1,i2 & Hom(a,b) <> {} & Hom(b,a) <> {}
implies i1 is coretraction & i2 is coretraction;
theorem :: CAT_3:83
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:84
for f being Morphism of c,d holds
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:85
c is_a_coproduct_wrt i1,i2 & dom i2 is initial implies dom i1,c
are_isomorphic;
theorem :: CAT_3:86
c is_a_coproduct_wrt i1,i2 & dom i1 is initial implies dom i2,c
are_isomorphic;