:: Products and Coproducts in Categories
:: by Czes{\l}aw Byli\'nski
::
:: Received May 11, 1992
:: Copyright (c) 1992-2026 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;
definitions CAT_1;
equalities CAT_1, FUNCOP_1, OPPCAT_1, ORDINAL1;
expansions CAT_1;
theorems TARSKI, FUNCT_2, FUNCOP_1, FUNCT_4, CAT_1, OPPCAT_1, RELSET_1;
schemes FUNCT_2, FUNCT_1;
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
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) proof
A1: for x being object st x in I() holds F(x) in A();
consider IT being Function of I(),A() such that
A2: for x being object st x in I() holds IT.x = F(x) from FUNCT_2:sch 2(A1);
take IT;
let x;
assume
A3: x in I();
hence F(x) = IT.x by A2
.= IT/.x by A3,FUNCT_2:def 13;
end;
theorem Th1:
for F1,F2 being Function of I,A st for x st x in I holds F1/.x =
F2/.x holds F1 = F2
proof
let F1,F2 be Function of I,A such that
A1: for x st x in I holds F1/.x = F2/.x;
now
let x be object;
assume
A2: x in I;
hence F1.x = F1/.x by FUNCT_2:def 13
.= F2/.x by A1,A2
.= F2.x by A2,FUNCT_2:def 13;
end;
hence thesis by FUNCT_2:12;
end;
scheme
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 proof
thus ex F being Function of I(),A() st for x st x in I() holds F/.x = F(x)
from LambdaIdx;
let F1,F2 be Function of I(),A() such that
A1: for x st x in I() holds F1/.x = F(x) and
A2: for x st x in I() holds F2/.x = F(x);
now
let x;
assume
A3: x in I();
hence F1/.x = F(x) by A1
.= F2/.x by A2,A3;
end;
hence thesis by Th1;
end;
definition
let A,x;
let a be Element of A;
redefine func x .--> a -> Function of {x},A; :: redefines .--> (FUNCOP_1, definition)
coherence by FUNCOP_1:46;
end;
theorem Th2:
for a being Element of A st x in I holds (I --> a)/.x = a
proof
let a be Element of A;
assume
A1: x in I;
hence a = (I --> a).x by FUNCOP_1:7
.= (I --> a)/.x by A1,FUNCT_2:def 13;
end;
theorem Th3:
x1 <> x2 implies for y1,y2 being Element of A holds ((x1,x2) -->
(y1,y2))/.x1 = y1 & ((x1,x2) --> (y1,y2))/.x2 = y2
proof
assume
A1: x1 <> x2;
let y1,y2 be Element of A;
set h = (x1,x2) --> (y1,y2);
A2: h.x2 = y2 & x1 in {x1,x2} by FUNCT_4:63,TARSKI:def 2;
A3: x2 in {x1,x2} by TARSKI:def 2;
h.x1 = y1 by A1,FUNCT_4:63;
hence thesis by A2,A3,FUNCT_2:def 13;
end;
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
:Def1:
for x st x in I holds it/.x = dom(F/.x);
correctness
proof
deffunc F(set) = dom(F/.$1);
set A = the carrier of C;
thus (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 from FuncIdxcorrectness;
end;
func cods F -> Function of I, the carrier of C means
:Def2:
for x st x in I holds it/.x = cod(F/.x);
correctness
proof
deffunc F(set) = cod(F/.$1);
set A = the carrier of C;
thus (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 from FuncIdxcorrectness;
end;
end;
theorem Th4:
doms(I-->f) = I-->(dom f)
proof
set F = I-->f, F9 = I-->(dom f);
now
let x;
assume
A1: x in I;
then F/.x = f & F9/.x = dom f by Th2;
hence (doms F)/.x = F9/.x by A1,Def1;
end;
hence thesis by Th1;
end;
theorem Th5:
cods(I-->f) = I-->(cod f)
proof
set F = I-->f, F9 = I-->(cod f);
now
let x;
assume
A1: x in I;
then F/.x = f & F9/.x = cod f by Th2;
hence (cods F)/.x = F9/.x by A1,Def2;
end;
hence thesis by Th1;
end;
theorem Th6:
doms((x1,x2)-->(p1,p2)) = (x1,x2)-->(dom p1,dom p2)
proof
set F = (x1,x2)-->(p1,p2), f = x1 .--> p1, g = x2 .--> p2, F9 = (x1,x2)-->(
dom p1,dom p2), f9 = x1.-->(dom p1), g9 = x2.-->(dom p2);
A1: dom g = {x2} by FUNCOP_1:13;
A2: dom g9 = {x2} & F9 = f9 +* g9 by FUNCOP_1:13,FUNCT_4:def 4;
A3: F = f +* g by FUNCT_4:def 4;
A4: dom f = {x1} by FUNCOP_1:13;
now
let x;
assume
A5: x in {x1,x2};
then
A6: x in dom F by FUNCT_4:62;
now
per cases by A3,A6,FUNCT_4:12;
case
A7: x in dom f & not x in dom g;
then F.x = f.x by A3,FUNCT_4:11;
then
A8: F.x = p1 by A4,A7,FUNCOP_1:7;
F9.x = f9.x by A1,A2,A7,FUNCT_4:11;
then F9.x = dom p1 by A4,A7,FUNCOP_1:7;
hence F/.x = p1 & F9/.x = dom p1 by A5,A8,FUNCT_2:def 13;
end;
case
A9: x in dom g;
then F.x = g.x by A3,FUNCT_4:13;
then
A10: F.x = p2 by A1,A9,FUNCOP_1:7;
F9.x = g9.x by A1,A2,A9,FUNCT_4:13;
then F9.x = dom p2 by A1,A9,FUNCOP_1:7;
hence F/.x = p2 & F9/.x = dom p2 by A5,A10,FUNCT_2:def 13;
end;
end;
hence (doms F)/.x = F9/.x by A5,Def1;
end;
hence thesis by Th1;
end;
theorem Th7:
cods((x1,x2)-->(p1,p2)) = (x1,x2)-->(cod p1,cod p2)
proof
set F = (x1,x2)-->(p1,p2), f = x1 .--> p1, g = x2 .--> p2, F9 = (x1,x2)-->(
cod p1,cod p2), f9 = x1.-->(cod p1), g9 = x2.-->(cod p2);
A1: dom g = {x2} by FUNCOP_1:13;
A2: dom g9 = {x2} & F9 = f9 +* g9 by FUNCOP_1:13,FUNCT_4:def 4;
A3: F = f +* g by FUNCT_4:def 4;
A4: dom f = {x1} by FUNCOP_1:13;
now
let x;
assume
A5: x in {x1,x2};
then
A6: x in dom F by FUNCT_4:62;
now
per cases by A3,A6,FUNCT_4:12;
case
A7: x in dom f & not x in dom g;
then F.x = f.x by A3,FUNCT_4:11;
then
A8: F.x = p1 by A4,A7,FUNCOP_1:7;
F9.x = f9.x by A1,A2,A7,FUNCT_4:11;
then F9.x = cod p1 by A4,A7,FUNCOP_1:7;
hence F/.x = p1 & F9/.x = cod p1 by A5,A8,FUNCT_2:def 13;
end;
case
A9: x in dom g;
then F.x = g.x by A3,FUNCT_4:13;
then
A10: F.x = p2 by A1,A9,FUNCOP_1:7;
F9.x = g9.x by A1,A2,A9,FUNCT_4:13;
then F9.x = cod p2 by A1,A9,FUNCOP_1:7;
hence F/.x = p2 & F9/.x = cod p2 by A5,A10,FUNCT_2:def 13;
end;
end;
hence (cods F)/.x = F9/.x by A5,Def2;
end;
hence thesis by Th1;
end;
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
:Def3:
for x st x in I holds it/.x = (F/.x) opp;
correctness
proof
deffunc F(set) = (F/.$1) opp;
set A = the carrier' of C opp;
thus (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 from FuncIdxcorrectness;
end;
end;
theorem
(I --> f) opp = I --> f opp
proof
set F = I --> f, F9 = I --> f opp;
now
let x;
assume
A1: x in I;
then F/.x = f & F9/.x = f opp by Th2;
hence F opp/.x = F9/.x by A1,Def3;
end;
hence thesis by Th1;
end;
theorem
x1 <> x2 implies ((x1,x2)-->(p1,p2)) opp = (x1,x2)-->(p1 opp,p2 opp)
proof
set F = (x1,x2)-->(p1,p2), F9 = (x1,x2)-->(p1 opp,p2 opp);
assume
A1: x1 <> x2;
now
let x;
assume
A2: x in {x1,x2};
then x = x1 or x = x2 by TARSKI:def 2;
then F/.x = p1 & F9/.x = p1 opp or F/.x = p2 & F9/.x = p2 opp by A1,Th3;
hence F opp/.x = F9/.x by A2,Def3;
end;
hence thesis by Th1;
end;
theorem
for F being Function of I,the carrier' of C holds F opp opp = F
proof
let F be Function of I,the carrier' of C;
now
thus the carrier' of C = the carrier' of C opp opp;
let x;
assume
A1: x in I;
hence (F opp opp)/.x = ((F opp)/.x) opp by Def3
.= (F/.x) opp opp by A1,Def3
.= F/.x;
end;
hence thesis by Th1;
end;
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
:Def4:
for x st x in I holds it/.x = opp (F/.x);
correctness
proof
deffunc F(set) = opp (F/.$1);
set A = the carrier' of C;
thus (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 from FuncIdxcorrectness;
end;
end;
theorem
for f being Morphism of C opp holds opp(I --> f) = I --> (opp f)
proof
let f be Morphism of C opp;
set F = I --> f, F9 = I --> (opp f);
now
let x;
assume
A1: x in I;
then F/.x = f & F9/.x = opp f by Th2;
hence opp F/.x = F9/.x by A1,Def4;
end;
hence thesis by Th1;
end;
theorem
x1 <> x2 implies for p1,p2 being Morphism of C opp holds opp ((x1,x2)
-->(p1,p2)) = (x1,x2)-->(opp p1,opp p2)
proof
assume
A1: x1 <> x2;
let p1,p2 be Morphism of C opp;
set F = (x1,x2)-->(p1,p2), F9 = (x1,x2)-->(opp p1,opp p2);
now
let x;
assume
A2: x in {x1,x2};
then x = x1 or x = x2 by TARSKI:def 2;
then F/.x = p1 & F9/.x = opp p1 or F/.x = p2 & F9/.x = opp p2 by A1,Th3;
hence opp F/.x = F9/.x by A2,Def4;
end;
hence thesis by Th1;
end;
theorem
for F being Function of I,the carrier' of C holds opp(F opp) = F
proof
let F be Function of I,the carrier' of C;
now
let x;
assume
A1: x in I;
hence opp(F opp)/.x = opp((F opp)/.x) by Def4
.= opp((F/.x) opp) by A1,Def3
.= F/.x;
end;
hence thesis by Th1;
end;
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
:Def5:
for x st x in I holds it/.x = (F/.x)(*)f;
correctness
proof
deffunc F(set) = (F/.$1)(*)f;
set A = the carrier' of C;
thus (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 from FuncIdxcorrectness;
end;
func f*F -> Function of I,the carrier' of C means
:Def6:
for x st x in I holds it/.x = f(*)(F/.x);
correctness
proof
deffunc F(set) = f(*)(F/.$1);
set A = the carrier' of C;
thus (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 from FuncIdxcorrectness;
end;
end;
theorem Th14:
x1 <> x2 implies ((x1,x2)-->(p1,p2))*f = (x1,x2)-->(p1(*)f,p2(*)f)
proof
set F = (x1,x2)-->(p1,p2), F9 = (x1,x2)-->(p1(*)f,p2(*)f);
assume
A1: x1 <> x2;
now
let x;
assume
A2: x in {x1,x2};
then x = x1 or x = x2 by TARSKI:def 2;
then F/.x = p1 & F9/.x = p1(*)f or F/.x = p2 & F9/.x = p2(*)f by A1,Th3;
hence (F*f)/.x = F9/.x by A2,Def5;
end;
hence thesis by Th1;
end;
theorem Th15:
x1 <> x2 implies f*((x1,x2)-->(p1,p2)) = (x1,x2)-->(f(*)p1,f(*)p2)
proof
set F = (x1,x2)-->(p1,p2), F9 = (x1,x2)-->(f(*)p1,f(*)p2);
assume
A1: x1 <> x2;
now
let x;
assume
A2: x in {x1,x2};
then x = x1 or x = x2 by TARSKI:def 2;
then F/.x = p1 & F9/.x = f(*)p1 or F/.x = p2 & F9/.x = f(*)p2 by A1,Th3;
hence (f*F)/.x = F9/.x by A2,Def6;
end;
hence thesis by Th1;
end;
theorem Th16:
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
proof
let F be Function of I,the carrier' of C such that
A1: doms F = I-->cod f;
now
let x;
assume
A2: x in I;
then
A3: dom(F/.x) = (I-->cod f)/.x by A1,Def1
.= cod f by A2,Th2;
thus (doms(F*f))/.x = dom((F*f)/.x) by A2,Def1
.= dom((F/.x)(*)f) by A2,Def5
.= dom f by A3,CAT_1:17
.= (I--> dom f)/.x by A2,Th2;
end;
hence doms(F*f) = I --> dom f by Th1;
now
let x;
assume
A4: x in I;
then
A5: dom(F/.x) = (I-->cod f)/.x by A1,Def1
.= cod f by A4,Th2;
thus (cods F)/.x = cod(F/.x) by A4,Def2
.= cod((F/.x)(*)f) by A5,CAT_1:17
.= cod((F*f)/.x) by A4,Def5
.= (cods(F*f))/.x by A4,Def2;
end;
hence thesis by Th1;
end;
theorem Th17:
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
proof
let F be Function of I,the carrier' of C such that
A1: cods F = I-->dom f;
now
let x;
assume
A2: x in I;
then
A3: cod(F/.x) = (I-->dom f)/.x by A1,Def2
.= dom f by A2,Th2;
thus (doms F)/.x = dom(F/.x) by A2,Def1
.= dom(f(*)(F/.x)) by A3,CAT_1:17
.= dom((f*F)/.x) by A2,Def6
.= (doms(f*F))/.x by A2,Def1;
end;
hence doms(f*F) = doms F by Th1;
now
let x;
assume
A4: x in I;
then
A5: cod(F/.x) = (I-->dom f)/.x by A1,Def2
.= dom f by A4,Th2;
thus (cods(f*F))/.x = cod((f*F)/.x) by A4,Def2
.= cod(f(*)(F/.x)) by A4,Def6
.= cod f by A5,CAT_1:17
.= (I--> cod f)/.x by A4,Th2;
end;
hence thesis by Th1;
end;
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
:Def7:
for x st x in I holds it/.x = (F/.x)(*)(G/.x);
correctness
proof
deffunc F(set) = (F/.$1)(*)(G/.$1);
set A = the carrier' of C;
thus (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 from FuncIdxcorrectness;
end;
end;
theorem Th18:
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
proof
let F,G be Function of I,the carrier' of C such that
A1: doms F = cods G;
now
let x;
assume
A2: x in I;
then
A3: cod(G/.x) = (doms F)/.x by A1,Def2
.= dom(F/.x) by A2,Def1;
thus (doms(F"*"G))/.x = dom((F"*"G)/.x) by A2,Def1
.= dom((F/.x)(*)(G/.x)) by A2,Def7
.= dom(G/.x) by A3,CAT_1:17
.= (doms G)/.x by A2,Def1;
end;
hence doms(F"*"G) = doms G by Th1;
now
let x;
assume
A4: x in I;
then
A5: cod(G/.x) = (doms F)/.x by A1,Def2
.= dom(F/.x) by A4,Def1;
thus (cods(F"*"G))/.x = cod((F"*"G)/.x) by A4,Def2
.= cod((F/.x)(*)(G/.x)) by A4,Def7
.= cod(F/.x) by A5,CAT_1:17
.= (cods F)/.x by A4,Def2;
end;
hence thesis by Th1;
end;
theorem
x1 <> x2 implies ((x1,x2)-->(p1,p2))"*"((x1,x2)-->(q1,q2)) = (x1,x2)
-->(p1(*)q1,p2(*)q2)
proof
set F1 = (x1,x2)-->(p1,p2),
F2 = (x1,x2)-->(q1,q2), G = (x1,x2)-->(p1(*)q1,p2(*)
q2);
assume
A1: x1 <> x2;
now
let x;
assume
A2: x in {x1,x2};
then x = x1 or x = x2 by TARSKI:def 2;
then
F1/.x = p1 & F2/.x = q1 & G/.x = p1(*)q1 or F1/.x = p2 & F2/.x = q2 & G
/.x = p2(*)q2 by A1,Th3;
hence (F1"*"F2)/.x = G/.x by A2,Def7;
end;
hence thesis by Th1;
end;
theorem
for F being Function of I,the carrier' of C holds F*f = F"*"(I-->f)
proof
let F be Function of I,the carrier' of C;
now
let x;
assume
A1: x in I;
hence (F*f)/.x = (F/.x)(*)f by Def5
.= (F/.x)(*)((I-->f)/.x) by A1,Th2
.= (F"*"(I-->f))/.x by A1,Def7;
end;
hence thesis by Th1;
end;
theorem
for F being Function of I,the carrier' of C holds f*F = (I-->f)"*"F
proof
let F be Function of I,the carrier' of C;
now
let x;
assume
A1: x in I;
hence (f*F)/.x = f(*)(F/.x) by Def6
.= ((I-->f)/.x)(*)(F/.x) by A1,Th2
.= ((I-->f)"*"F)/.x by A1,Def7;
end;
hence thesis by Th1;
end;
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
Hom(a,b) <> {} & Hom(b,a) <> {} &
ex g st IT*g = id b;
attr IT is coretraction means
Hom(a,b) <> {} & Hom(b,a) <> {} &
ex g st g*IT = id a;
end;
theorem Th22:
f is retraction implies f is epi
proof assume
A1: Hom(a,b) <> {} & Hom(b,a) <> {};
given g such that
A2: f*g = id b;
thus Hom(a,b) <> {} by A1;
let c be Object of C such that
A3: Hom(b,c) <> {};
let p1,p2 be Morphism of b,c;
assume
A4: p1*f = p2*f;
thus p1 = p1*(f*g) by A3,A2,CAT_1:29
.= (p2*f)*g by A3,A1,A4,CAT_1:25
.= p2*(f*g) by A3,A1,CAT_1:25
.= p2 by A3,A2,CAT_1:29;
end;
theorem
f is coretraction implies f is monic
proof assume
A1: Hom(a,b) <> {} & Hom(b,a) <> {};
given g such that
A2: g*f = id a;
thus Hom(a,b) <> {} by A1;
let c be Object of C such that
A3: Hom(c,a) <> {};
let p1,p2 be Morphism of c,a;
assume
A4: f*p1 = f*p2;
thus p1 = g*f*p1 by A3,A2,CAT_1:28
.= g*(f*p2) by A3,A1,A4,CAT_1:25
.= g*f*p2 by A3,A1,CAT_1:25
.= p2 by A3,A2,CAT_1:28;
end;
reserve g for Morphism of b,c;
theorem
f is retraction & g is retraction implies g*f is retraction
proof
assume
A1: Hom(a,b) <> {} & Hom(b,a) <> {};
given i being Morphism of b,a such that
A2: f*i = id b;
assume
A3: Hom(b,c) <> {} & Hom(c,b) <> {};
given j being Morphism of c,b such that
A4: g*j = id c;
thus
A5: Hom(a,c) <> {} & Hom(c,a) <> {} by A1,A3,CAT_1:24;
take i*j;
thus g*f*(i*j) = g*(f*(i*j)) by A1,A3,A5,CAT_1:25
.= g*(f*i*j) by A1,A3,CAT_1:25
.= id c by A2,A3,A4,CAT_1:28;
end;
theorem
f is coretraction & g is coretraction implies g*f is coretraction
proof
assume
A1: Hom(a,b) <> {} & Hom(b,a) <> {};
given i being Morphism of b,a such that
A2: i*f = id a;
assume
A3: Hom(b,c) <> {} & Hom(c,b) <> {};
given j being Morphism of c,b such that
A4: j*g = id b;
thus
A5: Hom(a,c) <> {} & Hom(c,a) <> {} by A1,A3,CAT_1:24;
take i*j;
thus i*j*(g*f) = i*(j*(g*f)) by A1,A3,A5,CAT_1:25
.= i*(j*g*f) by A1,A3,CAT_1:25
.= id a by A1,A2,A4,CAT_1:28;
end;
theorem
Hom(a,b) <> {} & Hom(b,a) <> {} &
g*f is retraction implies g is retraction
proof assume
A1: Hom(a,b) <> {} & Hom(b,a) <> {};
assume
A2: Hom(a,c) <> {} & Hom(c,a) <> {};
given i being Morphism of c,a such that
A3: (g*f)*i = id c;
thus
A4: Hom(b,c) <> {} & Hom(c,b) <> {} by A2,A1,CAT_1:24;
take f*i;
thus g*(f*i) = id c by A2,A3,A4,A1,CAT_1:25;
end;
theorem
Hom(b,c) <> {} & Hom(c,b) <> {} &
g*f is coretraction implies f is coretraction
proof assume
A1: Hom(b,c) <> {} & Hom(c,b) <> {};
assume
A2: Hom(a,c) <> {} & Hom(c,a) <> {};
given i being Morphism of c,a such that
A3: i*(g*f) = id a;
thus
A4: Hom(a,b) <> {} & Hom(b,a) <> {} by A1,A2,CAT_1:24;
take i*g;
thus (i*g)*f = id a by A4,A1,A2,A3,CAT_1:25;
end;
theorem
f is retraction & f is monic implies f is invertible
proof assume
A1: Hom(a,b) <> {} & Hom(b,a) <> {};
given i being Morphism of b,a such that
A2: f*i = id b;
assume
A3: f is monic;
thus Hom(a,b) <> {} & Hom(b,a) <> {} by A1;
take i;
thus f*i = id b by A2;
A4: f*(i*f) = (id b)*f by A1,A2,CAT_1:25
.= f by A1,CAT_1:28
.= f*id a by A1,CAT_1:29;
Hom(a,a) <> {};
hence i*f = id a by A3,A4;
end;
theorem Th29:
f is coretraction & f is epi implies f is invertible
proof
assume
A1: Hom(a,b) <> {} & Hom(b,a) <> {};
given i being Morphism of b,a such that
A2: i*f = id a;
assume
A3: f is epi;
thus Hom(a,b) <> {} & Hom(b,a) <> {} by A1;
take i;
A4: f*i*f = f*id a by A1,A2,CAT_1:25
.= f by A1,CAT_1:29
.= (id b)*f by A1,CAT_1:28;
Hom(b,b) <> {};
hence f*i = id b by A3,A4;
thus i*f = id a by A2;
end;
theorem
f is invertible iff f is retraction & f is coretraction
by Th22,Th29;
definition let C,a,b such that
A1: 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
:Def10: T.f;
coherence
proof
f in Hom(a,b) by A1,CAT_1:def 5;
then T.f in Hom(T.a,T.b) by CAT_1:81;
hence thesis by CAT_1:def 5;
end;
end;
Lm1:
for T being Functor of C,D, a,b,c being Object of C
st Hom(a,b) <> {} & Hom(b,c) <> {}
for f being Morphism of a,b, g being Morphism of b,c
holds T/.(g*f) = (T/.g)*(T/.f)
proof
let T be Functor of C,D, a,b,c being Object of C such that
A1: Hom(a,b) <> {} & Hom(b,c) <> {};
let f be Morphism of a,b, g being Morphism of b,c;
A2: cod f = b by A1,CAT_1:5 .= dom g by A1,CAT_1:5;
reconsider gg = g, ff= f as Morphism of C;
A3: Hom(a,c) <> {} by A1,CAT_1:24;
A4: T/.g = T.gg by Def10,A1;
A5: T/.f = T.ff by Def10,A1;
A6: Hom(T.a,T.b) <> {} & Hom(T.b,T.c) <> {} by A1,CAT_1:84;
g*f = gg(*)ff by A1,CAT_1:def 13;
hence T/.(g*f) = T.(gg(*)ff) by Def10,A3
.= (T.gg)(*)(T.ff) by A2,CAT_1:64
.= (T/.g)*(T/.f) by A6,A4,A5,CAT_1:def 13;
end;
Lm2:
for T being Functor of C,D, c being Object of C
holds T/.id c = id(T.c)
proof let T be Functor of C,D, c being Object of C;
Hom(c,c) <> {} ;
hence T/.id c = T.id c by Def10
.= id(T.c) by CAT_1:71;
end;
theorem
for T being Functor of C,D st f is retraction holds T/.f is retraction
proof
let T be Functor of C,D;
assume
A1: Hom(a,b) <> {} & Hom(b,a) <> {};
given i being Morphism of b,a such that
A2: f*i = id b;
thus Hom(T.a,T.b) <> {} & Hom(T.b,T.a) <> {} by A1,CAT_1:84;
take T/.i;
thus (T/.f)*(T/.i) = T/.id b by A1,A2,Lm1
.= id(T.b) by Lm2;
end;
theorem
for T being Functor of C,D st f is coretraction holds T/.f is coretraction
proof
let T be Functor of C,D;
assume
A1: Hom(a,b) <> {} & Hom(b,a) <> {};
given i being Morphism of b,a such that
A2: i*f = id a;
thus Hom(T.a,T.b) <> {} & Hom(T.b,T.a) <> {} by A1,CAT_1:84;
take T/.i;
thus (T/.i)*(T/.f) = T/.(id a) by A1,A2,Lm1
.= id(T.a) by Lm2;
end;
theorem
f is retraction iff f opp is coretraction
proof
thus f is retraction implies f opp is coretraction
proof
assume
A1: Hom(a,b) <> {} & Hom(b,a) <> {};
given i being Morphism of b,a such that
A2: f*i = id b;
thus Hom(b opp,a opp) <> {} & Hom(a opp,b opp) <> {} by A1,OPPCAT_1:5;
take i opp;
thus (i opp)*(f opp) = id b by A1,A2,OPPCAT_1:70
.= id (b opp) by OPPCAT_1:71;
end;
assume
A3: Hom(b opp,a opp) <> {} & Hom(a opp,b opp) <> {};
given i being Morphism of a opp, b opp such that
A4: i*(f opp) = id(b opp);
thus
A5: Hom(a,b) <> {} & Hom(b,a) <> {} by A3,OPPCAT_1:5;
take opp i;
A6: (opp i) opp = opp i by A5,OPPCAT_1:def 6
.= i by A3,OPPCAT_1:def 7;
thus f*(opp i) = id(b opp) by A4,A6,A5,OPPCAT_1:70
.= id b by OPPCAT_1:71;
end;
theorem
f is coretraction iff f opp is retraction
proof
thus f is coretraction implies f opp is retraction
proof
assume
A1: Hom(a,b) <> {} & Hom(b,a) <> {};
given i being Morphism of b,a such that
A2: i*f = id a;
thus Hom(b opp,a opp) <> {} & Hom(a opp,b opp) <> {} by A1,OPPCAT_1:5;
take i opp;
thus (f opp)*(i opp) = id a by A1,A2,OPPCAT_1:70
.= id(a opp) by OPPCAT_1:71;
end;
assume
A3: Hom(b opp,a opp) <> {} & Hom(a opp,b opp) <> {};
given i being Morphism of a opp, b opp such that
A4: (f opp)*i = id(a opp);
thus
A5: Hom(a,b) <> {} & Hom(b,a) <> {} by A3,OPPCAT_1:5;
take opp i;
(opp i) opp = opp i by A5,OPPCAT_1:def 6
.= i by A3,OPPCAT_1:def 7;
hence (opp i)*f = (f opp)*i by A5,OPPCAT_1:70
.= id(a opp) by A4
.= id a by OPPCAT_1:71;
end;
begin :: carrier' determined by a terminal Object
reserve f,g for Morphism of C;
definition
let C,a,b;
assume
A1: b is terminal;
func term(a,b) -> Morphism of a,b means
not contradiction;
existence;
uniqueness
proof
let f1,f2 be Morphism of a,b;
consider f being Morphism of a,b such that
A2: for g being Morphism of a,b holds f = g by A1;
thus f1 = f by A2
.= f2 by A2;
end;
end;
theorem Th35:
b is terminal implies dom(term(a,b)) = a & cod(term(a,b)) = b
proof
assume b is terminal;
then Hom(a,b) <> {};
hence thesis by CAT_1:5;
end;
theorem Th36:
b is terminal & dom f = a & cod f = b implies term(a,b) = f
proof
assume that
A1: b is terminal and
A2: dom f = a & cod f = b;
consider h being Morphism of a,b such that
A3: for g being Morphism of a,b holds h = g by A1;
f is Morphism of a,b by A2,CAT_1:4;
hence f = h by A3
.= term(a,b) by A3;
end;
theorem
for f being Morphism of a,b st b is terminal holds term(a,b) = f
proof
let f be Morphism of a,b;
assume
A1: b is terminal;
then Hom(a,b) <> {};
then dom f = a & cod f = b by CAT_1:5;
hence thesis by A1,Th36;
end;
begin :: carrier' determined by an iniatial object
definition
let C,a,b;
assume
A1: a is initial;
func init(a,b) -> Morphism of a,b means
not contradiction;
existence;
uniqueness
proof
let f1,f2 be Morphism of a,b;
consider f being Morphism of a,b such that
A2: for g being Morphism of a,b holds f = g by A1;
thus f1 = f by A2
.= f2 by A2;
end;
end;
theorem Th38:
a is initial implies dom(init(a,b)) = a & cod(init(a,b)) = b
proof
assume a is initial;
then Hom(a,b) <> {};
hence thesis by CAT_1:5;
end;
theorem Th39:
a is initial & dom f = a & cod f = b implies init(a,b) = f
proof
assume that
A1: a is initial and
A2: dom f = a & cod f = b;
consider h being Morphism of a,b such that
A3: for g being Morphism of a,b holds h = g by A1;
f is Morphism of a,b by A2,CAT_1:4;
hence f = h by A3
.= init(a,b) by A3;
end;
theorem
for f being Morphism of a,b st a is initial holds init(a,b) = f
proof
let f be Morphism of a,b;
assume
A1: a is initial;
then Hom(a,b) <> {};
then dom f = a & cod f = b by CAT_1:5;
hence thesis by A1,Th39;
end;
begin :: Products
definition
let C,a,I;
mode Projections_family of a,I -> Function of I,the carrier' of C means
:Def13: doms it = I --> a;
existence
proof
take F = I-->id a;
doms F = I --> (dom id a) by Th4;
hence thesis;
end;
end;
theorem Th41:
for F being Projections_family of a,I st x in I holds dom(F/.x) = a
proof
let F be Projections_family of a,I such that
A1: x in I;
(doms F)/.x = (I --> a)/.x by Def13;
hence dom(F/.x) = (I --> a)/.x by A1,Def1
.= a by A1,Th2;
end;
theorem Th42:
for F being Function of {},the carrier' of C holds F is
Projections_family of a,{}
proof
let F be Function of {},the carrier' of C;
thus {} --> a = doms F;
end;
theorem Th43:
dom f = a implies y .--> f is Projections_family of a,{y}
proof
set F = y .--> f;
assume
A1: dom f = a;
now
let x;
assume
A2: x in {y};
hence (doms F)/.x = dom(F/.x) by Def1
.= a by A1,A2,Th2
.= (y .--> a)/.x by A2,Th2;
end;
hence doms F = {y} --> a by Th1;
end;
theorem Th44:
dom p1 = a & dom p2 = a implies (x1,x2)-->(p1,p2) is
Projections_family of a,{x1,x2}
proof
assume
A1: dom p1 = a & dom p2 = a;
doms ((x1,x2)-->(p1,p2)) = (x1,x2) --> (dom p1,dom p2) by Th6
.= {x1,x2} --> a by A1,FUNCT_4:65;
hence thesis by Def13;
end;
theorem Th45:
for F being Projections_family of a,I st cod f = a holds F*f is
Projections_family of dom f,I
proof
let F be Projections_family of a,I;
assume cod f = a;
then doms F = I-->cod f by Def13;
hence doms(F*f) = I --> dom f by Th16;
end;
theorem
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
proof
let F be Function of I,the carrier' of C;
let G be Projections_family of a,I;
assume doms F = cods G;
then doms(F"*"G) = doms G by Th18;
hence doms(F"*"G) = I --> a by Def13;
end;
theorem
for F being Projections_family of cod f,I holds (f opp)*(F opp) = (F*f ) opp
proof
let F be Projections_family of cod f, I;
now
let x;
assume
A1: x in I;
then
A2: dom(F/.x) = (doms F)/.x by Def1
.= (I --> cod f)/.x by Def13
.= cod f by A1,Th2;
reconsider ff=f as Morphism of dom f,cod f by CAT_1:4;
reconsider gg=F/.x as Morphism of cod f,cod(F/.x) by A2,CAT_1:4;
A3: Hom(dom f,cod f)<>{} & Hom(dom(F/.x),cod(F/.x))<>{} by CAT_1:2;
then
A4: ff opp = f opp by OPPCAT_1:def 6;
A5: gg opp = (F/.x)opp by A3,A2,OPPCAT_1:def 6;
thus ((f opp)*(F opp))/.x = (f opp)(*)((F opp)/.x) by A1,Def6
.= (f opp)(*)((F/.x)opp) by A1,Def3
.= (gg(*)ff)opp by A2,A4,A5,A3,OPPCAT_1:16
.= ((F*f)/.x)opp by A1,Def5
.= ((F*f) opp)/.x by A1,Def3;
end;
hence thesis by Th1;
end;
definition
let C,a,I;
let F be Function of I,the carrier' of C;
pred a is_a_product_wrt F means
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 Th48:
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
proof
let F be Projections_family of c,I, F9 be Projections_family of d,I such
that
A1: c is_a_product_wrt F and
A2: d is_a_product_wrt F9 and
A3: cods F = cods F9;
consider gf being Morphism of C such that
gf in Hom(d,d) and
A4: for k st k in Hom(d,d) holds (for x st x in I holds (F9/.x)(*)k = F9
/.x ) iff gf = k by A2;
consider f such that
A5: f in Hom(d,c) and
A6: for k st k in Hom(d,c) holds (for x st x in I holds (F/.x)(*)k = F9/.x
) iff f = k by A1,A3;
reconsider f as Morphism of d,c by A5,CAT_1:def 5;
consider fg being Morphism of C such that
fg in Hom(c,c) and
A7: for k st k in Hom(c,c) holds (for x st x in I holds (F/.x)(*)k = F/.x
) iff fg = k by A1;
consider g such that
A8: g in Hom(c,d) and
A9: for k st k in Hom(c,d) holds (for x st x in I holds (F9/.x)(*)k = F/.x
) iff g = k by A2,A3;
reconsider g as Morphism of c,d by A8,CAT_1:def 5;
A10: cod g = d by A8,CAT_1:1;
A11: now
set k = id c;
thus k in Hom(c,c) by CAT_1:27;
let x;
assume x in I;
then dom(F/.x) = c by Th41;
hence (F/.x)(*)k = F/.x by CAT_1:22;
end;
A12: now
set k = id d;
thus k in Hom(d,d) by CAT_1:27;
let x;
assume x in I;
then dom(F9/.x) = d by Th41;
hence (F9/.x)(*)k = F9/.x by CAT_1:22;
end;
take g;
thus
Hom(c,d) <> {} & Hom(d,c) <> {} by A5,A8;
take f;
A13: dom g = c by A8,CAT_1:1;
A14: cod f = c by A5,CAT_1:1;
A15: dom f = d by A5,CAT_1:1;
A16: now
dom(g(*)f) = d & cod(g(*)f) = d by A15,A10,A14,A13,CAT_1:17;
hence g(*)f in Hom(d,d);
let x;
assume
A17: x in I;
then dom(F9/.x) = d by Th41;
hence (F9/.x)(*)(g(*)f) = (F9/.x)(*)g(*)f by A10,A14,A13,CAT_1:18
.= (F/.x)(*)f by A8,A9,A17
.= F9/.x by A5,A6,A17;
end;
thus g*f = g(*)f by A5,A8,CAT_1:def 13
.= gf by A4,A16
.= id d by A4,A12;
A18: now
dom(f(*)g) = c & cod(f(*)g) = c by A15,A10,A14,A13,CAT_1:17;
hence f(*)g in Hom(c,c);
let x;
assume
A19: x in I;
then dom(F/.x) = c by Th41;
hence (F/.x)(*)(f(*)g) = (F/.x)(*)f(*)g by A15,A10,A14,CAT_1:18
.= (F9/.x)(*)g by A5,A6,A19
.= F/.x by A8,A9,A19;
end;
thus f*g = f(*)g by A5,A8,CAT_1:def 13
.= fg by A7,A18
.= id c by A11,A7;
end;
theorem Th49:
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
proof
let F be Projections_family of c,I such that
A1: c is_a_product_wrt F and
A2: for x1,x2 st x1 in I & x2 in I holds Hom(cod(F/.x1),cod(F/.x2)) <> {};
let x such that
A3: x in I;
let d be Object of C such that
A4: d = cod(F/.x) and
A5: Hom(c,d) <> {};
let f be Morphism of c,d such that
A6: f = F/.x;
defpred P[object,object] means
($1 = x implies $2 = id d) & ($1 <> x implies $2 in
Hom(d,cod(F/.$1)));
A7: for y being object st y in I holds
ex z being object st z in the carrier' of C & P[y,z]
proof
let y be object;
set z = the Element of Hom(d,cod(F/.y));
assume y in I;
then
A8: Hom(d,cod(F/.y)) <> {} by A2,A3,A4;
then
A9: z in Hom(d,cod(F/.y));
per cases;
suppose
A10: y = x;
take z = id d;
thus z in the carrier' of C;
thus thesis by A10;
end;
suppose
A11: y <> x;
take z;
thus z in the carrier' of C by A9;
thus thesis by A8,A11;
end;
end;
consider F9 being Function such that
A12: dom F9 = I & rng F9 c= the carrier' of C and
A13: for y being object st y in I holds P[y,F9.y] from FUNCT_1:sch 6(A7);
reconsider F9 as Function of I,the carrier' of C by A12,FUNCT_2:def 1
,RELSET_1:4;
now
let y;
assume
A14: y in I;
then
A15: F9.y = F9/.y by FUNCT_2:def 13;
then
A16: y <> x implies F9/.y in Hom(d,cod(F/.y)) by A13,A14;
y = x implies F9/.y = id d by A13,A14,A15;
then dom(F9/.y) = d by A16,CAT_1:1;
hence (doms F9)/.y = d by A14,Def1
.= (I-->d)/.y by A14,Th2;
end;
then
A17: F9 is Projections_family of d,I by Def13,Th1;
now
let y;
assume
A18: y in I;
then
A19: F9.y = F9/.y by FUNCT_2:def 13;
then
A20: y <> x implies F9/.y in Hom(d,cod(F/.y)) by A13,A18;
y = x implies F9/.y = id d by A13,A18,A19;
then cod(F9/.y) = cod(F/.y) by A20,A4,CAT_1:1;
hence (cods F9)/.y = cod(F/.y) by A18,Def2
.= (cods F)/.y by A18,Def2;
end;
then consider i such that
A21: i in Hom(d,c) and
A22: for k st k in Hom(d,c) holds (for y st y in I holds (F/.y)(*)k = F9/.
y) iff i = k by A1,A17,Th1;
reconsider i as Morphism of d,c by A21,CAT_1:def 5;
thus
Hom(c,d) <> {} & Hom(d,c) <> {} by A21,A5;
take i;
thus f*i = f(*)i by A21,A5,CAT_1:def 13
.= F9/.x by A3,A21,A22,A6
.= F9.x by A3,FUNCT_2:def 13
.= id d by A3,A13;
end;
theorem Th50:
for F being Function of {},the carrier' of C holds a
is_a_product_wrt F iff a is terminal
proof
let F be Function of {},the carrier' of C;
thus a is_a_product_wrt F implies a is terminal
proof
assume
A1: a is_a_product_wrt F;
let b;
set F9 = the Projections_family of b,{};
consider h such that
A2: h in Hom(b,a) and
A3: for k st k in Hom(b,a) holds (for x st x in {} holds (F/.x)(*)k = F9
/.x ) iff h = k by A1;
thus Hom(b,a)<>{} by A2;
reconsider f = h as Morphism of b,a by A2,CAT_1:def 5;
take f;
let g be Morphism of b,a;
A4: for x st x in {} holds (F/.x)(*)g = F9/.x;
g in Hom(b,a) by A2,CAT_1:def 5;
hence thesis by A3,A4;
end;
assume
A5: a is terminal;
thus F is Projections_family of a,{} by Th42;
let b;
consider h being Morphism of b,a such that
A6: for g being Morphism of b,a holds h = g by A5;
let F9 be Projections_family of b,{} such that
cods F = cods F9;
take h;
Hom(b,a)<>{} by A5;
hence h in Hom(b,a) by CAT_1:def 5;
let k;
assume k in Hom(b,a);
then k is Morphism of b,a by CAT_1:def 5;
hence thesis by A6;
end;
theorem Th51:
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
proof
let F be Projections_family of a,I such that
A1: a is_a_product_wrt F;
let f be Morphism of b,a such that
A2: dom f = b and
A3: cod f = a and
A4: f is invertible;
thus F*f is Projections_family of b,I by A2,A3,Th45;
let c;
A5: doms F = I-->cod f by A3,Def13;
let F9 be Projections_family of c,I;
assume cods(F*f) = cods F9;
then cods F = cods F9 by A5,Th16;
then consider h such that
A6: h in Hom(c,a) and
A7: for k st k in Hom(c,a) holds (for x st x in I holds (F/.x)(*)k = F9/.x
) iff h = k by A1;
A8: cod h = a by A6,CAT_1:1;
consider g being Morphism of a,b such that
A9: f*g = id a and
A10: g*f = id b by A4;
A11: Hom(a,b) <> {} & Hom(b,a) <> {} by A4;
then
A12: dom g = cod f by A3,CAT_1:5;
A13: cod g = dom f by A2,A11,CAT_1:5;
A14: f(*)g = id cod f by A9,A3,A11,CAT_1:def 13;
A15: g(*)f = id dom f by A10,A2,A11,CAT_1:def 13;
dom h = c by A6,CAT_1:1;
then
A16: dom(g(*)h) = c by A3,A12,A8,CAT_1:17;
take gh = g(*)h;
cod(g(*)h) = b by A2,A3,A12,A13,A8,CAT_1:17;
hence gh in Hom(c,b) by A16;
let k;
assume
A17: k in Hom(c,b);
then
A18: cod k = b by CAT_1:1;
A19: dom k = c by A17,CAT_1:1;
thus (for x st x in I holds ((F*f)/.x)(*)k = F9/.x) implies gh = k
proof
assume
A20: for x st x in I holds ((F*f)/.x)(*)k = F9/.x;
now
dom(f(*)k) = c & cod(f(*)k) = a by A2,A3,A19,A18,CAT_1:17;
hence f(*)k in Hom(c,a);
let x;
assume
A21: x in I;
then dom(F/.x) = a by Th41;
hence (F/.x)(*)(f(*)k) = (F/.x)(*)f(*)k by A2,A3,A18,CAT_1:18
.= ((F*f)/.x)(*)k by A21,Def5
.= F9/.x by A20,A21;
end;
then g(*)(f(*)k) = g(*)h by A7;
hence gh = (id b)(*)k by A2,A12,A15,A18,CAT_1:18
.= k by A18,CAT_1:21;
end;
assume
A22: gh = k;
let x;
assume
A23: x in I;
then
A24: dom(F/.x) = a by Th41;
thus ((F*f)/.x)(*)k = ((F/.x)(*)f)(*)k by A23,Def5
.= (F/.x)(*)(f(*)(g(*)h)) by A2,A3,A18,A22,A24,CAT_1:18
.= (F/.x)(*)((id cod f)(*)h) by A3,A12,A13,A14,A8,CAT_1:18
.= (F/.x)(*)h by A3,A8,CAT_1:21
.= F9/.x by A6,A7,A23;
end;
theorem
a is_a_product_wrt y .--> id a
proof
set F = y .--> id a;
dom(id a) = a;
hence F is Projections_family of a,{y} by Th43;
let b;
let F9 be Projections_family of b,{y} such that
A1: cods F = cods F9;
take h = F9/.y;
A2: y in {y} by TARSKI:def 1;
then
A3: dom h = b by Th41;
cod h = (cods F)/.y by A1,A2,Def2
.= cod(F/.y) by A2,Def2
.= cod(id a) by A2,Th2
.= a;
hence h in Hom(b,a) by A3;
let k;
assume k in Hom(b,a);
then
A4: cod k = a by CAT_1:1;
thus (for x st x in {y} holds (F/.x)(*)k = F9/.x) implies h = k
proof
assume
A5: for x st x in {y} holds (F/.x)(*)k = F9/.x;
thus k = (id a)(*)k by A4,CAT_1:21
.= (F/.y)(*)k by A2,Th2
.= h by A2,A5;
end;
assume
A6: h = k;
let x;
assume
A7: x in {y};
hence F9/.x = k by A6,TARSKI:def 1
.= (id a)(*)k by A4,CAT_1:21
.= (F/.x)(*)k by A7,Th2;
end;
theorem
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
proof
let F be Projections_family of a,I such that
A1: a is_a_product_wrt F and
A2: for x st x in I holds cod(F/.x) is terminal;
now
thus I = {} implies a is terminal by A1,Th50;
let b;
deffunc f(set) = term(b,cod(F/.$1));
consider F9 being Function of I, the carrier' of C such that
A3: for x st x in I holds F9/.x = f(x) from LambdaIdx;
now
let x;
assume
A4: x in I;
then
A5: cod(F/.x) is terminal by A2;
thus (doms F9)/.x = dom(F9/.x) by A4,Def1
.= dom(term(b,cod(F/.x))) by A3,A4
.= b by A5,Th35
.= (I-->b)/.x by A4,Th2;
end;
then reconsider F9 as Projections_family of b,I by Def13,Th1;
now
let x;
assume
A6: x in I;
then
A7: cod(F/.x) is terminal by A2;
thus (cods F)/.x = cod(F/.x) by A6,Def2
.= cod(term(b,cod(F/.x))) by A7,Th35
.= cod(F9/.x) by A3,A6
.= (cods F9)/.x by A6,Def2;
end;
then consider h such that
A8: h in Hom(b,a) and
A9: for k st k in Hom(b,a) holds (for x st x in I holds (F/.x)(*)k = F9
/.x) iff h = k by A1,Th1;
thus Hom(b,a)<>{} by A8;
reconsider h as Morphism of b,a by A8,CAT_1:def 5;
take h;
let g be Morphism of b,a;
now
thus g in Hom(b,a) by A8,CAT_1:def 5;
let x;
set c = cod(F/.x);
A10: cod g = a by A8,CAT_1:5;
assume
A11: x in I;
then c is terminal by A2;
then consider f being Morphism of b,c such that
A12: for f9 being Morphism of b,c holds f = f9;
A13: dom(F/.x) = a by A11,Th41;
then
A14: cod((F/.x)(*)g) = c by A10,CAT_1:17;
dom g = b by A8,CAT_1:5;
then dom((F/.x)(*)g) = b by A10,A13,CAT_1:17;
then (F/.x)(*)g in Hom(b,c) by A14;
then
A15: (F/.x)(*)g is Morphism of b,c by CAT_1:def 5;
F9/.x = term(b,c) by A3,A11;
hence F9/.x = f by A12
.= (F/.x)(*)g by A12,A15;
end;
hence h = g by A9;
end;
hence thesis;
end;
definition
let C,c,p1,p2;
pred c is_a_product_wrt p1,p2 means
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 Th54:
x1 <> x2 implies (c is_a_product_wrt p1,p2 iff c
is_a_product_wrt (x1,x2)-->(p1,p2))
proof
set F = (x1,x2)-->(p1,p2), I = {x1,x2};
assume
A1: x1 <> x2;
thus c is_a_product_wrt p1,p2 implies c is_a_product_wrt F
proof
assume
A2: c is_a_product_wrt p1,p2;
then dom p1 = c & dom p2 = c;
hence F is Projections_family of c,I by Th44;
let b;
let F9 be Projections_family of b,I such that
A3: cods F = cods F9;
set f = F9/.x1, g = F9/.x2;
A4: x1 in I by TARSKI:def 2;
then (cods F)/.x1 = cod(F/.x1) by Def2;
then cod f = cod(F/.x1) by A3,A4,Def2;
then
A5: cod f = cod p1 by A1,Th3;
A6: x2 in I by TARSKI:def 2;
then (cods F)/.x2 = cod(F/.x2) by Def2;
then cod g = cod(F/.x2) by A3,A6,Def2;
then
A7: cod g = cod p2 by A1,Th3;
dom g = b by A6,Th41;
then
A8: g in Hom(b,cod p2) by A7;
dom f = b by A4,Th41;
then f in Hom(b,cod p1) by A5;
then consider h such that
A9: h in Hom(b,c) and
A10: for k st k in Hom(b,c) holds p1(*)k = f & p2(*)k = g iff h = k
by A2,A8;
take h;
thus h in Hom(b,c) by A9;
let k such that
A11: k in Hom(b,c);
thus (for x st x in I holds (F/.x)(*)k = F9/.x ) implies h = k
proof
assume
A12: for x st x in I holds (F/.x)(*)k = F9/.x;
then (F/.x2)(*)k = g by A6;
then
A13: p2(*)k = g by A1,Th3;
(F/.x1)(*)k = f by A4,A12;
then p1(*)k = f by A1,Th3;
hence thesis by A10,A11,A13;
end;
assume h = k;
then
A14: p1(*)k = f & p2(*)k = g by A10,A11;
let x;
assume x in I;
then x = x1 or x = x2 by TARSKI:def 2;
hence thesis by A1,A14,Th3;
end;
assume
A15: c is_a_product_wrt F;
then
A16: F is Projections_family of c,I;
x2 in I by TARSKI:def 2;
then
A17: dom(F/.x2) = c by A16,Th41;
x1 in I by TARSKI:def 2;
then dom(F/.x1) = c by A16,Th41;
hence dom p1 = c & dom p2 = c by A1,A17,Th3;
let d,f,g such that
A18: f in Hom(d,cod p1) and
A19: g in Hom(d,cod p2);
dom f = d & dom g = d by A18,A19,CAT_1:1;
then reconsider F9 = (x1,x2) --> (f,g) as Projections_family of d,I by Th44;
cods F = (x1,x2)-->(cod p1,cod p2) by Th7
.= (x1,x2)-->(cod f,cod p2) by A18,CAT_1:1
.= (x1,x2)-->(cod f,cod g) by A19,CAT_1:1
.= cods F9 by Th7;
then consider h such that
A20: h in Hom(d,c) and
A21: for k st k in Hom(d,c) holds (for x st x in I holds (F/.x)(*)k = F9/.
x ) iff h = k by A15;
take h;
thus h in Hom(d,c) by A20;
let k such that
A22: k in Hom(d,c);
thus p1(*)k = f & p2(*)k = g implies h = k
proof
assume
A23: p1(*)k = f & p2(*)k = g;
now
let x;
assume x in I;
then x = x1 or x = x2 by TARSKI:def 2;
then F/.x = p1 & F9/.x = f or F/.x = p2 & F9/.x = g by A1,Th3;
hence (F/.x)(*)k = F9/.x by A23;
end;
hence thesis by A21,A22;
end;
assume
A24: h = k;
x2 in I by TARSKI:def 2;
then (F/.x2)(*)k = F9/.x2 by A21,A22,A24;
then
A25: (F/.x2)(*)k = g by A1,Th3;
x1 in I by TARSKI:def 2;
then (F/.x1)(*)k = F9/.x1 by A21,A22,A24;
then (F/.x1)(*)k = f by A1,Th3;
hence thesis by A1,A25,Th3;
end;
theorem
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
proof
assume that
A1: Hom(c,a) <> {} and
A2: Hom(c,b) <> {};
let p1 be Morphism of c,a, p2 be Morphism of c,b;
thus c is_a_product_wrt p1,p2 implies 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
proof
assume that
dom p1 = c and
dom p2 = c and
A3: 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;
let d such that
A4: Hom(d,a)<>{} and
A5: Hom(d,b)<>{};
set f = the Morphism of d,a,g = the Morphism of d,b;
A6: cod p2 = b by A2,CAT_1:5;
then
A7: g in Hom(d,cod p2) by A5,CAT_1:def 5;
A8: cod p1 = a by A1,CAT_1:5;
then f in Hom(d,cod p1) by A4,CAT_1:def 5;
then
A9: 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 by A3,A7;
hence Hom(d,c) <> {};
let f be Morphism of d,a, g be Morphism of d,b;
A10: g in Hom(d,cod p2) by A5,A6,CAT_1:def 5;
f in Hom(d,cod p1) by A4,A8,CAT_1:def 5;
then consider h such that
A11: h in Hom(d,c) and
A12: for k st k in Hom(d,c) holds p1(*)k = f & p2(*)k = g iff h = k by A3,A10;
reconsider h as Morphism of d,c by A11,CAT_1:def 5;
take h;
let k be Morphism of d,c;
A13: k in Hom(d,c) by A9,CAT_1:def 5;
p1*k = p1(*)(k qua Morphism of C) & p2*k
= p2(*)(k qua Morphism of C) by A1,A2,A9,CAT_1:def 13;
hence thesis by A12,A13;
end;
assume
A14: 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;
thus dom p1 = c & dom p2 = c by A1,A2,CAT_1:5;
let d,f,g such that
A15: f in Hom(d,cod p1) and
A16: g in Hom(d,cod p2);
A17: Hom(d,a) <> {} by A1,A15,CAT_1:5;
A18: cod p1 = a by A1,CAT_1:5;
then
A19: f is Morphism of d,a by A15,CAT_1:def 5;
A20: cod p2 = b by A2,CAT_1:5;
then g is Morphism of d,b by A16,CAT_1:def 5;
then consider h being Morphism of d,c such that
A21: for k being Morphism of d,c holds p1*k = f & p2*k = g iff h = k by A14,A16
,A20,A19,A17;
reconsider h9 = h as Morphism of C;
take h9;
A22: Hom(d,c) <> {} by A14,A15,A16,A18,A20;
hence h9 in Hom(d,c) by CAT_1:def 5;
let k;
assume k in Hom(d,c);
then reconsider k9 = k as Morphism of d,c by CAT_1:def 5;
p1(*)k = p1*k9 & p2(*)k = p2*k9 by A1,A2,A22,CAT_1:def 13;
hence thesis by A21;
end;
theorem
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
proof
assume that
A1: c is_a_product_wrt p1,p2 and
A2: d is_a_product_wrt q1,q2 and
A3: cod p1 = cod q1 & cod p2 = cod q2;
set I = {0,{0}}, F = (0,{0})-->(p1,p2), F9 = (0,{0})-->(q1,q2);
A4: c is_a_product_wrt F & d is_a_product_wrt F9 by A1,A2,Th54;
cods F = (0,{0})-->(cod q1,cod q2) by A3,Th7
.= cods F9 by Th7;
hence thesis by A4,Th48;
end;
theorem
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
proof
let p1 be Morphism of c,a, p2 be Morphism of c,b such that
A1: Hom(c,a) <> {} & Hom(c,b) <> {} and
A2: c is_a_product_wrt p1,p2 and
A3: Hom(a,b) <> {} & Hom(b,a) <> {};
set I = {0,{0}};
dom p1 = c & dom p2 = c by A2;
then reconsider F = (0,{0})-->(p1,p2) as Projections_family of c,I by Th44;
A4: F/.0 = p1 by Th3;
A5: F/.{0} = p2 by Th3;
A6: now
thus F is Projections_family of c,I;
thus c is_a_product_wrt F by A2,Th54;
let x1,x2;
assume that
A7: x1 in I and
A8: x2 in I;
A9: x2 = 0 or x2 = {0} by A8,TARSKI:def 2;
x1 = 0 or x1 = {0} by A7,TARSKI:def 2;
then
A10: cod(F/.x1) = a or cod(F/.x1) = b by A4,A5,A1,CAT_1:5;
cod(F/.x2) = a or cod(F/.x2) = b by A9,A4,A5,A1,CAT_1:5;
hence Hom(cod(F/.x1),cod(F/.x2)) <> {} by A3,A10;
end;
A11: {0} in I by TARSKI:def 2;
A12: 0 in I by TARSKI:def 2;
cod(F/.0) = a & cod(F/.{0}) = b by A4,A5,A1,CAT_1:5;
hence thesis by A4,A6,A11,Th49,A5,A1,A12;
end;
theorem Th58:
c is_a_product_wrt p1,p2 & h in Hom(c,c) & p1(*)h = p1 & p2(*)h = p2
implies h = id c
proof
assume that
A1: dom p1 = c & dom p2 = c and
A2: 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 and
A3: h in Hom(c,c) & p1(*)h = p1 & p2(*)h = p2;
p1 in Hom(c,cod p1) & p2 in Hom(c,cod p2) by A1;
then consider i such that
i in Hom(c,c) and
A4: for k st k in Hom(c,c) holds p1(*)k = p1 & p2(*)k = p2 iff i = k by A2;
A5: id c in Hom(c,c) by CAT_1:27;
p1(*)(id c) = p1 & p2(*)(id c) = p2 by A1,CAT_1:22;
hence id c = i by A4,A5
.= h by A3,A4;
end;
theorem
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
proof
let f be Morphism of d,c such that
A1: c is_a_product_wrt p1,p2 and
A2: dom f = d & cod f = c & f is invertible;
c is_a_product_wrt (0,{0})-->(p1,p2) by A1,Th54;
then d is_a_product_wrt ((0,{0})-->(p1,p2))*f by A2,Th51;
then d is_a_product_wrt (0,{0})-->(p1(*)f,p2(*)f) by Th14;
hence thesis by Th54;
end;
theorem
c is_a_product_wrt p1,p2 & cod p2 is terminal implies c,cod p1 are_isomorphic
proof
set a = cod p1, b = cod p2;
assume that
A1: c is_a_product_wrt p1,p2 and
A2: b is terminal;
set f = id(a),g = term(a,b);
dom g = a & cod g = b by A2,Th35;
then f in Hom(a,a) & g in Hom(a,b) by CAT_1:27;
then consider h such that
A3: h in Hom(a,c) and
A4: for k st k in Hom(a,c) holds p1(*)k = f & p2(*)k = g iff h = k by A1;
A5: dom h = a by A3,CAT_1:1;
reconsider h as Morphism of a,c by A3,CAT_1:def 5;
A6: dom p1 = c by A1;
then reconsider p = p1 as Morphism of c,a by CAT_1:4;
A7: cod h = c by A3,CAT_1:1;
then
A8: cod(h(*)p) = c by A5,CAT_1:17;
A9: dom p2 = c by A1;
then
A10: cod(p2(*)(h(*)p)) = b by A8,CAT_1:17;
A11: dom(h(*)p) = c by A6,A5,CAT_1:17;
then
A12: h(*)p in Hom(c,c) by A8;
dom(p2(*)(h(*)p)) = c by A9,A11,A8,CAT_1:17;
then
A13: p2(*)(h(*)p) = term(c,b) by A2,A10,Th36
.= p2 by A2,A9,Th36;
A14: Hom(c,a)<>{} by A6,CAT_1:2;
take p;
thus Hom(c,a) <> {} & Hom(a,c) <> {} by A3,A6,CAT_1:2;
take h;
thus p*h = p(*)h by A3,A14,CAT_1:def 13
.= id a by A3,A4;
p1(*)(h(*)p) = p1(*)h(*)p by A6,A5,A7,CAT_1:18
.= (id cod p)(*)p by A3,A4
.= p by CAT_1:21;
hence id c = h(*)p by A1,A13,A12,Th58
.= h*p by A3,A14,CAT_1:def 13;
end;
theorem
c is_a_product_wrt p1,p2 & cod p1 is terminal implies c,cod p2 are_isomorphic
proof
set a = cod p1, b = cod p2;
assume that
A1: c is_a_product_wrt p1,p2 and
A2: a is terminal;
set f = id(b),g = term(b,a);
dom g = b & cod g = a by A2,Th35;
then f in Hom(b,b) & g in Hom(b,a) by CAT_1:27;
then consider h such that
A3: h in Hom(b,c) and
A4: for k st k in Hom(b,c) holds p1(*)k = g & p2(*)k = f iff h = k by A1;
A5: dom h = b by A3,CAT_1:1;
A6: dom p2 = c by A1;
then reconsider p = p2 as Morphism of c,b by CAT_1:4;
A7: cod h = c by A3,CAT_1:1;
then
A8: cod(h(*)p) = c by A5,CAT_1:17;
A9: dom p1 = c by A1;
then
A10: cod(p1(*)(h(*)p)) = a by A8,CAT_1:17;
A11: dom(h(*)p) = c by A6,A5,CAT_1:17;
then
A12: h(*)p in Hom(c,c) by A8;
dom(p1(*)(h(*)p)) = c by A9,A11,A8,CAT_1:17;
then
A13: p1(*)(h(*)p) = term(c,a) by A2,A10,Th36
.= p1 by A2,A9,Th36;
A14: Hom(c,b)<>{} by A6,CAT_1:2;
take p;
thus Hom(c,b) <> {} & Hom(b,c) <> {} by A6,A3,CAT_1:2;
reconsider h as Morphism of b,c by A3,CAT_1:def 5;
take h;
thus p*h = p(*)h by A14,A3,CAT_1:def 13
.= id b by A3,A4;
p(*)h = id cod p by A3,A4;
then
A15: p2(*)(h(*)p) = (id cod p)(*)p by A6,A5,A7,CAT_1:18
.= p by CAT_1:21;
thus id c = h(*)p by A1,A13,A12,Th58,A15
.= h*p by A14,A3,CAT_1:def 13;
end;
begin :: Coproducts
definition
let C,c,I;
mode Injections_family of c,I -> Function of I,the carrier' of C means
:
Def16: cods it = I --> c;
existence
proof
take F = I-->id c;
cods F = I --> (cod id c) by Th5;
hence thesis;
end;
end;
theorem Th62:
for F being Injections_family of c,I st x in I holds cod(F/.x) = c
proof
let F be Injections_family of c,I such that
A1: x in I;
(cods F)/.x = (I --> c)/.x by Def16;
hence cod(F/.x) = (I --> c)/.x by A1,Def2
.= c by A1,Th2;
end;
theorem
for F being Function of {},the carrier' of C holds F is
Injections_family of a,{}
proof
let F be Function of {},the carrier' of C;
thus {} --> a = cods F;
end;
theorem Th64:
cod f = a implies y .--> f is Injections_family of a,{y}
proof
set F = y .--> f;
assume
A1: cod f = a;
now
let x;
assume
A2: x in {y};
hence (cods F)/.x = cod(F/.x) by Def2
.= a by A1,A2,Th2
.= (y .--> a)/.x by A2,Th2;
end;
hence cods F = {y} --> a by Th1;
end;
theorem Th65:
cod p1 = c & cod p2 = c implies (x1,x2)-->(p1,p2) is
Injections_family of c,{x1,x2}
proof
assume
A1: cod p1 = c & cod p2 = c;
cods ((x1,x2)-->(p1,p2)) = (x1,x2) --> (cod p1,cod p2) by Th7
.= {x1,x2} --> c by A1,FUNCT_4:65;
hence thesis by Def16;
end;
theorem Th66:
for F being Injections_family of b,I st dom f = b holds f*F is
Injections_family of cod f,I
proof
let F be Injections_family of b,I;
assume dom f = b;
then cods F = I--> dom f by Def16;
hence cods(f*F) = I --> cod f by Th17;
end;
theorem
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
proof
let F be Injections_family of b,I;
let G be Function of I,the carrier' of C;
assume doms F = cods G;
then cods(F"*"G) = cods F by Th18;
hence cods(F"*"G) = I --> b by Def16;
end;
theorem Th68:
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
proof
let F be Function of I,the carrier' of C;
thus F is Projections_family of c,I implies F opp is Injections_family of c
opp,I
proof
assume
A1: doms F = I --> c;
now
let x;
reconsider gg = F/.x as Morphism of dom(F/.x), cod(F/.x) by CAT_1:4;
A2: Hom(dom gg,cod gg) <> {} by CAT_1:2;
then
A3: gg opp = (F/.x)opp by OPPCAT_1:def 6;
assume
A4: x in I;
hence (cods(F opp))/.x = cod((F opp)/.x) by Def2
.= cod((F/.x) opp) by A4,Def3
.= dom(F/.x) opp by A2,A3,OPPCAT_1:12
.= (I --> (c opp))/.x by A1,A4,Def1;
end;
hence cods(F opp) = I --> (c opp) by Th1;
end;
assume
A5: cods(F opp) = I --> (c opp);
now
let x;
reconsider gg = F/.x as Morphism of dom(F/.x), cod(F/.x) by CAT_1:4;
A6: Hom(dom gg,cod gg) <> {} by CAT_1:2;
then
A7: gg opp = (F/.x)opp by OPPCAT_1:def 6;
assume
A8: x in I;
hence (doms F)/.x = dom(F/.x) by Def1
.= cod(gg opp) by A6,OPPCAT_1:10
.= cod((F opp)/.x) by A8,Def3,A7
.= (I --> c)/.x by A8,A5,Def2;
end;
hence doms F = I --> c by Th1;
end;
theorem Th69:
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
proof
let F be Function of I,the carrier' of C opp, c be Object of C opp;
thus F is Injections_family of c,I implies opp F is Projections_family of
opp c,I
proof
assume
A1: cods F = I --> c;
now
let x;
reconsider gg = F/.x as Morphism of dom(F/.x), cod(F/.x) by CAT_1:4;
A2: Hom(dom gg,cod gg) <> {} by CAT_1:2;
assume
A3: x in I;
hence (doms opp F)/.x = dom(opp F/.x) by Def1
.= dom(opp(F/.x)) by A3,Def4
.= opp(cod(F/.x)) by A2,OPPCAT_1:13
.= (I --> (opp c))/.x by A1,A3,Def2;
end;
hence doms opp F = I --> (opp c) by Th1;
end;
assume
A4: doms opp F = I --> (opp c);
now
let x;
reconsider gg = F/.x as Morphism of dom(F/.x), cod(F/.x) by CAT_1:4;
Hom(dom gg,cod gg) <> {} by CAT_1:2;
then
A5: gg opp = (F/.x)opp by OPPCAT_1:def 6;
assume
A6: x in I;
hence (cods F)/.x = cod(F/.x) by Def2
.= dom(opp(F/.x)) by A5,OPPCAT_1:11
.= dom(opp F/.x) by A6,Def4
.= (I --> c)/.x by A4,A6,Def1;
end;
hence cods F = I --> c by Th1;
end;
theorem
for F being Injections_family of dom f,I holds (F opp)*(f opp) = (f*F) opp
proof
let F be Injections_family of dom f, I;
now
let x;
assume
A1: x in I;
then
A2: cod(F/.x) = (cods F)/.x by Def2
.= (I --> dom f)/.x by Def16
.= dom f by A1,Th2;
reconsider ff=f as Morphism of dom f,cod f by CAT_1:4;
reconsider gg=F/.x as Morphism of dom(F/.x),dom f by A2,CAT_1:4;
A3: Hom(dom f,cod f)<>{} & Hom(dom(F/.x),cod(F/.x))<>{} by CAT_1:2;
then
A4: ff opp = f opp by OPPCAT_1:def 6;
A5: gg opp = (F/.x)opp by A3,A2,OPPCAT_1:def 6;
thus ((F opp)*(f opp))/.x = ((F opp)/.x)(*)(f opp) by A1,Def5
.= ((F/.x)opp)(*)(f opp) by A1,Def3
.= (f(*)(F/.x))opp by A2,A4,A5,A3,OPPCAT_1:16
.= ((f*F)/.x)opp by A1,Def6
.= ((f*F) opp)/.x by A1,Def3;
end;
hence thesis by Th1;
end;
definition
let C,c,I;
let F be Function of I,the carrier' of C;
pred c is_a_coproduct_wrt F means
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
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
proof
let F be Function of I,the carrier' of C;
thus c is_a_product_wrt F implies c opp is_a_coproduct_wrt F opp
proof
assume
A1: c is_a_product_wrt F;
then F is Projections_family of c,I;
hence F opp is Injections_family of c opp,I by Th68;
let d be Object of C opp, F9 be Injections_family of d,I such that
A2: doms(F opp) = doms F9;
reconsider oppF9 = opp F9 as Projections_family of opp d,I by Th69;
now
let x;
reconsider gg = F/.x as Morphism of dom(F/.x), cod(F/.x) by CAT_1:4;
A3: Hom(dom gg,cod gg) <> {} by CAT_1:2;
then
A4: gg opp = (F/.x)opp by OPPCAT_1:def 6;
reconsider g9 = F9/.x as Morphism of dom(F9/.x), cod(F9/.x) by CAT_1:4;
Hom(dom g9,cod g9) <> {} by CAT_1:2;
then
A5: g9 opp = (F9/.x)opp by OPPCAT_1:def 6;
assume
A6: x in I;
hence (cods F)/.x = cod(F/.x) by Def2
.= dom(gg opp) by A3,OPPCAT_1:10
.= dom(F opp/.x) by A6,Def3,A4
.= (doms F9)/.x by A2,A6,Def1
.= dom(F9/.x) by A6,Def1
.= cod(opp(F9/.x)) by A5,OPPCAT_1:11
.= cod(oppF9/.x) by A6,Def4
.= (cods oppF9)/.x by A6,Def2;
end;
then consider h such that
A7: h in Hom(opp d,c) and
A8: for k st k in Hom(opp d,c) holds (for x st x in I holds (F/.x)(*)k =
oppF9/.x ) iff h = k by A1,Th1;
take h opp;
h in Hom(c opp,(opp d) opp) by A7,OPPCAT_1:5;
hence h opp in Hom(c opp,d);
let k be Morphism of C opp;
assume
A9: k in Hom(c opp,d);
then
A10: opp k in Hom(opp d,opp(c opp)) by OPPCAT_1:6;
thus (for x st x in I holds k(*)(F opp/.x) = F9/.x ) implies h opp = k
proof
assume
A11: for x st x in I holds k(*)(F opp/.x) = F9/.x;
now
let x such that
A12: x in I;
reconsider gg = F/.x as Morphism of dom(F/.x), cod(F/.x) by CAT_1:4;
A13: Hom(dom gg,cod gg) <> {} by CAT_1:2;
then
A14: gg opp = (F/.x)opp by OPPCAT_1:def 6;
F is Projections_family of c,I by A1;
then dom(F/.x) = c by A12,Th41;
then cod((F/.x)opp) = c opp by A13,A14,OPPCAT_1:12;
then cod(F opp/.x) = c opp by A12,Def3;
then
A15: dom k = cod(F opp/.x) by A9,CAT_1:1;
opp(k(*)(F opp/.x)) = opp(F9/.x) by A11,A12;
hence oppF9/.x = opp(k(*)(F opp/.x)) by A12,Def4
.= (opp(F opp/.x))(*)(opp k) by A15,OPPCAT_1:18
.= (opp((F/.x)opp))(*)(opp k) by A12,Def3
.= (F/.x)(*)(opp k);
end;
hence thesis by A8,A10;
end;
assume
A16: h opp = k;
let x such that
A17: x in I;
F is Projections_family of c,I by A1;
then dom(F/.x) = c by A17,Th41;
then
A18: cod opp k = dom(F/.x) by A10,CAT_1:1;
reconsider ff=opp k as Morphism of dom opp k, cod opp k by CAT_1:4;
reconsider gg=F/.x as Morphism of cod opp k, cod(F/.x) by A18,CAT_1:4;
A19: Hom(dom opp k,cod opp k)<>{} & Hom(dom(F/.x),cod(F/.x))<>{} by CAT_1:2;
then
A20: ff opp = (opp k)opp by OPPCAT_1:def 6;
A21: gg opp = (F/.x)opp by A19,A18,OPPCAT_1:def 6;
(F/.x)(*)(opp k) = oppF9/.x by A8,A10,A17,A16;
then ((opp k) opp)(*)((F/.x)opp) = (oppF9/.x)opp by A18,A20,A21,A19
,OPPCAT_1:16;
hence k(*)(F opp/.x) = (oppF9/.x)opp by A17,Def3
.= (opp(F9/.x))opp by A17,Def4
.= F9/.x;
end;
assume
A22: c opp is_a_coproduct_wrt F opp;
then F opp is Injections_family of c opp,I;
hence F is Projections_family of c,I by Th68;
let d;
let F9 be Projections_family of d,I such that
A23: cods F = cods F9;
A24: now
let x;
reconsider gg = F/.x as Morphism of dom(F/.x), cod(F/.x) by CAT_1:4;
A25: Hom(dom gg,cod gg) <> {} by CAT_1:2;
then
A26: gg opp = (F/.x)opp by OPPCAT_1:def 6;
reconsider g9 = F9/.x as Morphism of dom(F9/.x), cod(F9/.x) by CAT_1:4;
A27: Hom(dom g9,cod g9) <> {} by CAT_1:2;
then
A28: g9 opp = (F9/.x)opp by OPPCAT_1:def 6;
assume
A29: x in I;
hence (doms(F opp))/.x = dom((F opp)/.x) by Def1
.= dom(gg opp) by A29,Def3,A26
.= cod(F/.x) by A25,OPPCAT_1:10
.= (cods F9)/.x by A23,A29,Def2
.= cod(F9/.x) by A29,Def2
.= dom(g9 opp) by A27,OPPCAT_1:10
.= dom((F9 opp)/.x) by A29,Def3,A28
.= (doms(F9 opp))/.x by A29,Def1;
end;
reconsider F9opp = F9 opp as Injections_family of d opp,I by Th68;
consider h being Morphism of C opp such that
A30: h in Hom(c opp,d opp) and
A31: for k being Morphism of C opp st k in Hom(c opp,d opp) holds (for x
st x in I holds k(*)(F opp/.x) = F9opp/.x) iff h = k by A22,A24,Th1;
take opp h;
opp h in Hom(opp(d opp),opp(c opp)) by A30,OPPCAT_1:6;
hence opp h in Hom(d,c);
let k;
assume
A32: k in Hom(d,c);
then
A33: k opp in Hom(c opp,d opp) by OPPCAT_1:5;
thus (for x st x in I holds (F/.x)(*)k = F9/.x) implies opp h = k
proof
assume
A34: for x st x in I holds (F/.x)(*)k = F9/.x;
now
let x such that
A35: x in I;
reconsider gg = F/.x as Morphism of dom(F/.x), cod(F/.x) by CAT_1:4;
A36: Hom(dom gg,cod gg) <> {} by CAT_1:2;
then
A37: gg opp = (F/.x)opp by OPPCAT_1:def 6;
F opp is Injections_family of c opp,I by A22;
then cod(F opp/.x) = c opp by A35,Th62;
then cod(gg opp) = c opp by A35,Def3,A37;
then dom(F/.x) = c by A36,OPPCAT_1:10;
then
A38: cod k = dom(F/.x) by A32,CAT_1:1;
reconsider ff=k as Morphism of dom k,cod k by CAT_1:4;
reconsider gg=F/.x as Morphism of cod k,cod(F/.x) by A38,CAT_1:4;
A39: Hom(dom k,cod k)<>{} & Hom(dom(F/.x),cod(F/.x))<>{} by CAT_1:2;
then
A40: ff opp = k opp by OPPCAT_1:def 6;
A41: gg opp = (F/.x)opp by A39,A38,OPPCAT_1:def 6;
(F/.x)(*)k = F9/.x by A34,A35;
then (k opp)(*)((F/.x)opp) = (F9/.x) opp by A38,A40,A41,A39,OPPCAT_1:16;
hence F9opp/.x = (k opp)(*)((F/.x)opp) by A35,Def3
.= (k opp)(*)(F opp/.x) by A35,Def3;
end;
hence thesis by A31,A33;
end;
assume
A42: opp h = k;
let x such that
A43: x in I;
reconsider gg = F/.x as Morphism of dom(F/.x), cod(F/.x) by CAT_1:4;
A44: Hom(dom gg,cod gg) <> {} by CAT_1:2;
then
A45: gg opp = (F/.x)opp by OPPCAT_1:def 6;
F opp is Injections_family of c opp,I by A22;
then cod(F opp/.x) = c opp by A43,Th62;
then cod(gg opp) = c opp by A43,Def3,A45;
then dom(F/.x) = c by A44,OPPCAT_1:10;
then
A46: cod k = dom(F/.x) by A32,CAT_1:1;
reconsider ff=k as Morphism of dom k,cod k by CAT_1:4;
reconsider gg=F/.x as Morphism of cod k,cod(F/.x) by A46,CAT_1:4;
A47: Hom(dom k,cod k)<>{} & Hom(dom(F/.x),cod(F/.x))<>{} by CAT_1:2;
then
A48: ff opp = k opp by OPPCAT_1:def 6;
A49: gg opp = (F/.x)opp by A47,A46,OPPCAT_1:def 6;
(k opp)(*)(F opp/.x) = F9opp/.x by A31,A33,A43,A42;
then (k opp)(*)(F opp/.x) = (F9/.x)opp by A43,Def3;
hence F9/.x = (k opp)(*)((F/.x)opp) by A43,Def3
.= ((F/.x)(*)k) opp by A46,A48,A49,A47,OPPCAT_1:16
.= (F/.x)(*)k;
end;
theorem Th72:
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
proof
let F be Injections_family of c,I, F9 be Injections_family of d,I such that
A1: c is_a_coproduct_wrt F and
A2: d is_a_coproduct_wrt F9 and
A3: doms F = doms F9;
consider fg being Morphism of C such that
fg in Hom(d,d) and
A4: for k st k in Hom(d,d) holds (for x st x in I holds k(*)(F9/.x) = F9
/.x) iff fg = k by A2;
consider f such that
A5: f in Hom(c,d) and
A6: for k st k in Hom(c,d) holds (for x st x in I holds k(*)(F/.x) = F9/.x
) iff f = k by A1,A3;
reconsider f as Morphism of c,d by A5,CAT_1:def 5;
A7: dom f = c by A5,CAT_1:1;
A8: now
set k = id c;
thus k in Hom(c,c) by CAT_1:27;
let x;
assume x in I;
then cod(F/.x) = c by Th62;
hence k(*)(F/.x) = F/.x by CAT_1:21;
end;
A9: now
set k = id d;
thus k in Hom(d,d) by CAT_1:27;
let x;
assume x in I;
then cod(F9/.x) = d by Th62;
hence k(*)(F9/.x) = F9/.x by CAT_1:21;
end;
consider gf being Morphism of C such that
gf in Hom(c,c) and
A10: for k st k in Hom(c,c) holds (for x st x in I holds k(*)(F/.x) = F/.x
) iff gf = k by A1;
consider g such that
A11: g in Hom(d,c) and
A12: for k st k in Hom(d,c) holds (for x st x in I holds k(*)(F9/.x) = F/.x
) iff g = k by A2,A3;
reconsider g as Morphism of d,c by A11,CAT_1:def 5;
take f;
thus Hom(c,d) <> {} & Hom(d,c) <> {} by A11,A5;
take g;
A13: cod f = d by A5,CAT_1:1;
A14: dom g = d by A11,CAT_1:1;
A15: cod g = c by A11,CAT_1:1;
A16: now
cod(f(*)g) = d & dom(f(*)g) = d by A13,A14,A7,A15,CAT_1:17;
hence f(*)g in Hom(d,d);
let x;
assume
A17: x in I;
then cod(F9/.x) = d by Th62;
hence f(*)g(*)(F9/.x) = f(*)(g(*)(F9/.x)) by A14,A7,A15,CAT_1:18
.= f(*)(F/.x) by A11,A12,A17
.= F9/.x by A5,A6,A17;
end;
thus f*g = f(*)g by A11,A5,CAT_1:def 13
.= fg by A4,A16
.= id d by A4,A9;
A18: now
cod(g(*)f) = c & dom(g(*)f) = c by A13,A14,A7,A15,CAT_1:17;
hence g(*)f in Hom(c,c);
let x;
assume
A19: x in I;
then cod(F/.x) = c by Th62;
hence g(*)f(*)(F/.x) = g(*)(f(*)(F/.x)) by A13,A14,A7,CAT_1:18
.= g(*)(F9/.x) by A5,A6,A19
.= F/.x by A11,A12,A19;
end;
thus g*f = g(*)f by A11,A5,CAT_1:def 13
.= gf by A10,A18
.= id c by A8,A10;
end;
theorem Th73:
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
proof
let F be Injections_family of c,I such that
A1: c is_a_coproduct_wrt F and
A2: for x1,x2 st x1 in I & x2 in I holds Hom(dom(F/.x1),dom(F/.x2)) <> {};
let x such that
A3: x in I;
let d be Object of C such that
A4: d = dom(F/.x) and
A5: Hom(d,c)<> {};
let f be Morphism of d,c such that
A6: f = F/.x;
defpred P[object,object] means
($1 = x implies $2 = id d) & ($1 <> x implies $2 in
Hom(dom(F/.$1),d));
A7: for y being object st y in I
ex z being object st z in the carrier' of C & P[y,z]
proof
let y be object;
set z = the Element of Hom(dom(F/.y),d);
assume y in I;
then
A8: Hom(dom(F/.y),d) <> {} by A2,A3,A4;
then
A9: z in Hom(dom(F/.y),d);
per cases;
suppose
A10: y = x;
take z = id d;
thus z in the carrier' of C;
thus thesis by A10;
end;
suppose
A11: y <> x;
take z;
thus z in the carrier' of C by A9;
thus thesis by A8,A11;
end;
end;
consider F9 being Function such that
A12: dom F9 = I & rng F9 c= the carrier' of C and
A13: for y being object st y in I holds P[y,F9.y] from FUNCT_1:sch 6(A7);
reconsider F9 as Function of I,the carrier' of C by A12,FUNCT_2:def 1
,RELSET_1:4;
now
let y;
assume
A14: y in I;
then
A15: F9.y = F9/.y by FUNCT_2:def 13;
then
A16: y <> x implies F9/.y in Hom(dom(F/.y),d) by A13,A14;
y = x implies F9/.y = id d by A13,A14,A15;
then cod(F9/.y) = d by A16,CAT_1:1;
hence (cods F9)/.y = d by A14,Def2
.= (I-->d)/.y by A14,Th2;
end;
then
A17: F9 is Injections_family of d,I by Def16,Th1;
now
let y;
assume
A18: y in I;
then
A19: F9.y = F9/.y by FUNCT_2:def 13;
then
A20: y <> x implies F9/.y in Hom(dom(F/.y),d) by A13,A18;
y = x implies F9/.y = id d by A13,A18,A19;
then dom(F9/.y) = dom(F/.y) by A20,A4,CAT_1:1;
hence (doms F9)/.y = dom(F/.y) by A18,Def1
.= (doms F)/.y by A18,Def1;
end;
then consider i such that
A21: i in Hom(c,d) and
A22: for k st k in Hom(c,d) holds (for y st y in I holds k(*)(F/.y) = F9/.
y) iff i = k by A1,A17,Th1;
thus Hom(d,c) <> {} & Hom(c,d) <> {} by A21,A5;
reconsider i as Morphism of c,d by A21,CAT_1:def 5;
take i;
thus i*f = i(*)(F/.x) by A6,A21,A5,CAT_1:def 13
.= F9/.x by A3,A21,A22
.= F9.x by A3,FUNCT_2:def 13
.= id d by A3,A13;
end;
theorem Th74:
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
proof let f be Morphism of a,b;
let F be Injections_family of a,I such that
A1: a is_a_coproduct_wrt F and
A2: dom f = a and
A3: cod f = b and
A4: f is invertible;
thus f*F is Injections_family of b,I by A2,A3,Th66;
let c;
A5: cods F = I-->dom f by A2,Def16;
let F9 be Injections_family of c,I;
assume doms(f*F) = doms F9;
then doms F = doms F9 by A5,Th17;
then consider h such that
A6: h in Hom(a,c) and
A7: for k st k in Hom(a,c) holds (for x st x in I holds k(*)(F/.x) = F9/.x
) iff h = k by A1;
A8: dom h = a by A6,CAT_1:1;
consider g being Morphism of b,a such that
A9: f*g = id b and
A10: g*f = id a by A4;
A11: Hom(b,a) <> {} & Hom(a,b) <> {} by A4;
then
A12: dom g = cod f by A3,CAT_1:5;
A13: cod g = dom f by A2,A11,CAT_1:5;
A14: f*g = f(*)g by A11,CAT_1:def 13;
A15: g*f = g(*)f by A11,CAT_1:def 13;
cod h = c by A6,CAT_1:1;
then
A16: cod(h(*)g) = c by A2,A13,A8,CAT_1:17;
take hg = h(*)g;
dom(h(*)g) = b by A2,A3,A12,A13,A8,CAT_1:17;
hence hg in Hom(b,c) by A16;
let k;
assume
A17: k in Hom(b,c);
then
A18: dom k = b by CAT_1:1;
A19: cod k = c by A17,CAT_1:1;
thus (for x st x in I holds k(*)((f*F)/.x) = F9/.x) implies hg = k
proof
assume
A20: for x st x in I holds k(*)((f*F)/.x) = F9/.x;
now
cod(k(*)f) = c & dom(k(*)f) = a by A2,A3,A19,A18,CAT_1:17;
hence k(*)f in Hom(a,c);
let x;
assume
A21: x in I;
then cod(F/.x) = a by Th62;
hence k(*)f(*)(F/.x) = k(*)(f(*)(F/.x)) by A2,A3,A18,CAT_1:18
.= k(*)((f*F)/.x) by A21,Def6
.= F9/.x by A20,A21;
end;
then k(*)f(*)g = h(*)g by A7;
hence hg = k(*)(id b) by A3,A13,A9,A18,A14,CAT_1:18
.= k by A18,CAT_1:22;
end;
assume
A22: hg = k;
let x;
assume
A23: x in I;
then
A24: cod(F/.x) = a by Th62;
then
A25: cod(f(*)(F/.x)) = b by A2,A3,CAT_1:17;
thus k(*)((f*F)/.x) = k(*)(f(*)(F/.x)) by A23,Def6
.= h(*)(g(*)(f(*)(F/.x))) by A2,A3,A12,A13,A8,A22,A25,CAT_1:18
.= h(*)((id dom f)(*)(F/.x)) by A2,A12,A10,A24,A15,CAT_1:18
.= h(*)(F/.x) by A2,A24,CAT_1:21
.= F9/.x by A6,A7,A23;
end;
theorem Th75:
for F being Injections_family of a,{} holds a is_a_coproduct_wrt
F iff a is initial
proof
let F be Injections_family of a,{};
thus a is_a_coproduct_wrt F implies a is initial
proof
assume
A1: a is_a_coproduct_wrt F;
let b;
set F9 = the Injections_family of b,{};
consider h such that
A2: h in Hom(a,b) and
A3: for k st k in Hom(a,b) holds (for x st x in {} holds k(*)(F/.x) = F9
/.x ) iff h = k by A1;
thus Hom(a,b)<>{} by A2;
reconsider f = h as Morphism of a,b by A2,CAT_1:def 5;
take f;
let g be Morphism of a,b;
A4: for x st x in {} holds g(*)(F/.x) = F9/.x;
g in Hom(a,b) by A2,CAT_1:def 5;
hence thesis by A3,A4;
end;
assume
A5: a is initial;
thus F is Injections_family of a,{};
let b;
consider h being Morphism of a,b such that
A6: for g being Morphism of a,b holds h = g by A5;
let F9 be Injections_family of b,{} such that
doms F = doms F9;
take h;
Hom(a,b)<>{} by A5;
hence h in Hom(a,b) by CAT_1:def 5;
let k;
assume k in Hom(a,b);
then k is Morphism of a,b by CAT_1:def 5;
hence thesis by A6;
end;
theorem
a is_a_coproduct_wrt y .--> id a
proof
set F = y .--> id a;
cod(id a) = a;
hence F is Injections_family of a,{y} by Th64;
let b;
let F9 be Injections_family of b,{y} such that
A1: doms F = doms F9;
take h = F9/.y;
A2: y in {y} by TARSKI:def 1;
then
A3: cod h = b by Th62;
dom h = (doms F)/.y by A1,A2,Def1
.= dom(F/.y) by A2,Def1
.= dom(id a) by A2,Th2
.= a;
hence h in Hom(a,b) by A3;
let k;
assume k in Hom(a,b);
then
A4: dom k = a by CAT_1:1;
thus (for x st x in {y} holds k(*)(F/.x) = F9/.x) implies h = k
proof
assume
A5: for x st x in {y} holds k(*)(F/.x) = F9/.x;
thus k = k(*)(id a) by A4,CAT_1:22
.= k(*)(F/.y) by A2,Th2
.= h by A2,A5;
end;
assume
A6: h = k;
let x;
assume
A7: x in {y};
hence F9/.x = k by A6,TARSKI:def 1
.= k(*)(id a) by A4,CAT_1:22
.= k(*)(F/.x) by A7,Th2;
end;
theorem
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
proof
let F be Injections_family of a,I such that
A1: a is_a_coproduct_wrt F and
A2: for x st x in I holds dom(F/.x) is initial;
now
thus I = {} implies a is initial by A1,Th75;
let b;
deffunc f(set) = init(dom(F/.$1),b);
consider F9 being Function of I, the carrier' of C such that
A3: for x st x in I holds F9/.x = f(x) from LambdaIdx;
now
let x;
assume
A4: x in I;
then
A5: dom(F/.x) is initial by A2;
thus (cods F9)/.x = cod(F9/.x) by A4,Def2
.= cod(init(dom(F/.x),b)) by A3,A4
.= b by A5,Th38
.= (I-->b)/.x by A4,Th2;
end;
then reconsider F9 as Injections_family of b,I by Def16,Th1;
now
let x;
assume
A6: x in I;
then
A7: dom(F/.x) is initial by A2;
thus (doms F)/.x = dom(F/.x) by A6,Def1
.= dom(init(dom(F/.x),b)) by A7,Th38
.= dom(F9/.x) by A3,A6
.= (doms F9)/.x by A6,Def1;
end;
then consider h such that
A8: h in Hom(a,b) and
A9: for k st k in Hom(a,b) holds (for x st x in I holds k(*)(F/.x) = F9
/.x) iff h = k by A1,Th1;
thus Hom(a,b)<>{} by A8;
reconsider h as Morphism of a,b by A8,CAT_1:def 5;
take h;
let g be Morphism of a,b;
now
thus g in Hom(a,b) by A8,CAT_1:def 5;
let x;
set c = dom(F/.x);
A10: dom g = a by A8,CAT_1:5;
assume
A11: x in I;
then c is initial by A2;
then consider f being Morphism of c,b such that
A12: for f9 being Morphism of c,b holds f = f9;
A13: cod(F/.x) = a by A11,Th62;
then
A14: dom(g(*)(F/.x)) = c by A10,CAT_1:17;
cod g = b by A8,CAT_1:5;
then cod(g(*)(F/.x)) = b by A10,A13,CAT_1:17;
then g(*)(F/.x) in Hom(c,b) by A14;
then
A15: g(*)(F/.x) is Morphism of c,b by CAT_1:def 5;
F9/.x = init(c,b) by A3,A11;
hence F9/.x = f by A12
.= g(*)(F/.x) by A12,A15;
end;
hence h = g by A9;
end;
hence thesis;
end;
definition
let C,c,i1,i2;
pred c is_a_coproduct_wrt i1,i2 means
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
c is_a_product_wrt p1,p2 iff c opp is_a_coproduct_wrt p1 opp, p2 opp
proof
set i1 = p1 opp,i2 = p2 opp;
thus c is_a_product_wrt p1,p2 implies c opp is_a_coproduct_wrt p1 opp, p2 opp
proof
assume that
A1: dom p1 = c & dom p2 = c and
A2: 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;
reconsider gg = p1 as Morphism of dom p1, cod p1 by CAT_1:4;
A3: Hom(dom gg,cod gg) <> {} by CAT_1:2;
then
A4: gg opp = p1 opp by OPPCAT_1:def 6;
thus
A5: cod i1 = c opp by A1,A3,A4,OPPCAT_1:10;
reconsider gg = p2 as Morphism of dom p2, cod p2 by CAT_1:4;
A6: Hom(dom gg,cod gg) <> {} by CAT_1:2;
then
A7: gg opp = p2 opp by OPPCAT_1:def 6;
thus
A8: cod i2 = c opp by A1,A6,A7,OPPCAT_1:10;
let d be Object of C opp, f,g be Morphism of C opp;
assume that
A9: f in Hom(dom i1,d) and
A10: g in Hom(dom i2,d);
reconsider gg = i2 as Morphism of dom i2, cod i2 by CAT_1:4;
A11: Hom(dom gg,cod gg) <> {} by CAT_1:2;
opp g in Hom(opp d,opp(dom i2)) by A10,OPPCAT_1:6;
then
A12: opp g in Hom(opp d,cod opp i2) by A11,OPPCAT_1:13;
reconsider gg = i1 as Morphism of dom i1, cod i1 by CAT_1:4;
A13: Hom(dom gg,cod gg) <> {} by CAT_1:2;
opp f in Hom(opp d, opp(dom i1)) by A9,OPPCAT_1:6;
then opp f in Hom(opp d, cod opp i1) by A13,OPPCAT_1:13;
then consider h such that
A14: h in Hom(opp d,c) and
A15: for k st k in Hom(opp d,c) holds p1(*)k = opp f & p2(*)k = opp g iff
h = k by A2,A12;
take h opp;
h opp in Hom(c opp,(opp d) opp) by A14,OPPCAT_1:5;
hence h opp in Hom(c opp,d);
let k be Morphism of C opp;
assume
A16: k in Hom(c opp,d);
then opp k in Hom(opp d,opp(c opp)) by OPPCAT_1:6;
then
A17: (opp i1)(*)(opp k) = f & (opp i2)(*)(opp k) = g iff h opp = k by A15;
dom k = c opp by A16,CAT_1:1;
then opp(k(*)i1) = f & opp(k(*)i2) = g iff h opp = k
by A8,A5,A17,OPPCAT_1:18;
hence thesis;
end;
assume that
A18: cod i1 = c opp & cod i2 = c opp and
A19: for d being Object of C opp, f,g being Morphism of C opp st f in
Hom(dom i1,d) & g in Hom(dom i2,d) ex h being Morphism of C opp st h in Hom(c
opp,d) & for k being Morphism of C opp st k in Hom(c opp,d)
holds k(*)i1 = f & k(*)
i2 = g iff h = k;
reconsider gg = p1 as Morphism of dom p1, cod p1 by CAT_1:4;
A20: Hom(dom gg,cod gg) <> {} by CAT_1:2;
then
A21: gg opp = p1 opp by OPPCAT_1:def 6;
A22: dom p1 = c opp by A18,A20,A21,OPPCAT_1:10;
reconsider gg = p2 as Morphism of dom p2, cod p2 by CAT_1:4;
A23: Hom(dom gg,cod gg) <> {} by CAT_1:2;
then
A24: gg opp = p2 opp by OPPCAT_1:def 6;
A25: dom p2 = c opp by A18,A23,A24,OPPCAT_1:10;
hence dom p1 = c & dom p2 = c by A22;
let d,f,g;
assume that
A26: f in Hom(d,cod p1) and
A27: g in Hom(d,cod p2);
g opp in Hom((cod p2)opp,d opp) by A27,OPPCAT_1:5;
then
A28: g opp in Hom(dom (p2 opp),d opp) by A23,A24,OPPCAT_1:12;
f opp in Hom((cod p1) opp,d opp) by A26,OPPCAT_1:5;
then f opp in Hom(dom (p1 opp),d opp) by A20,A21,OPPCAT_1:12;
then consider h being Morphism of C opp such that
A29: h in Hom(c opp,d opp) and
A30: for k being Morphism of C opp st k in Hom(c opp,d opp) holds k(*)i1 =
f opp & k(*)i2 = g opp iff h = k by A19,A28;
take opp h;
thus opp h in Hom(d,c) by A29,OPPCAT_1:5;
let k;
assume
A31: k in Hom(d,c);
then k opp in Hom(c opp,d opp) by OPPCAT_1:5;
then
A32: (k opp)(*)i1 = f opp & (k opp)(*)i2 = g opp iff h = k opp by A30;
A33: cod k = c by A31,CAT_1:1;
reconsider ff=p1 as Morphism of dom p1, cod p1 by CAT_1:4;
reconsider gg=k as Morphism of dom k, dom p1 by A33,A22,CAT_1:4;
A34: Hom(dom k,cod k)<>{} & Hom(dom p1,cod p1)<>{} by CAT_1:2;
then
A35: ff opp = p1 opp by OPPCAT_1:def 6;
A36: gg opp = k opp by A34,A33,A22,OPPCAT_1:def 6;
A37: (p1(*)k) opp = (k opp)(*)(p1 opp) by A22,A34,A33,A35,A36,OPPCAT_1:16;
reconsider ff=p2 as Morphism of dom p2, cod p2 by CAT_1:4;
reconsider gg=k as Morphism of dom k, dom p2 by A33,A25,CAT_1:4;
A38: Hom(dom k,cod k)<>{} & Hom(dom p2,cod p2)<>{} by CAT_1:2;
then
A39: ff opp = p2 opp by OPPCAT_1:def 6;
A40: gg opp = k opp by A38,A33,A25,OPPCAT_1:def 6;
(p2(*)k) opp = (k opp)(*)(p2 opp) by A38,A33,A39,A40,A25,OPPCAT_1:16;
hence thesis by A37,A32;
end;
theorem Th79:
x1 <> x2 implies (c is_a_coproduct_wrt i1,i2 iff c
is_a_coproduct_wrt (x1,x2)-->(i1,i2))
proof
set F = (x1,x2)-->(i1,i2), I = {x1,x2};
assume
A1: x1 <> x2;
thus c is_a_coproduct_wrt i1,i2 implies c is_a_coproduct_wrt F
proof
assume
A2: c is_a_coproduct_wrt i1,i2;
then cod i1 = c & cod i2 = c;
hence F is Injections_family of c,I by Th65;
let b;
let F9 be Injections_family of b,I such that
A3: doms F = doms F9;
set f = F9/.x1, g = F9/.x2;
A4: x1 in I by TARSKI:def 2;
then (doms F)/.x1 = dom(F/.x1) by Def1;
then dom f = dom(F/.x1) by A3,A4,Def1;
then
A5: dom f = dom i1 by A1,Th3;
A6: x2 in I by TARSKI:def 2;
then (doms F)/.x2 = dom(F/.x2) by Def1;
then dom g = dom(F/.x2) by A3,A6,Def1;
then
A7: dom g = dom i2 by A1,Th3;
cod g = b by A6,Th62;
then
A8: g in Hom(dom i2,b) by A7;
cod f = b by A4,Th62;
then f in Hom(dom i1,b) by A5;
then consider h such that
A9: h in Hom(c,b) and
A10: for k st k in Hom(c,b) holds k(*)i1 = f & k(*)i2 = g iff h = k
by A2,A8;
take h;
thus h in Hom(c,b) by A9;
let k such that
A11: k in Hom(c,b);
thus (for x st x in I holds k(*)(F/.x) = F9/.x ) implies h = k
proof
assume
A12: for x st x in I holds k(*)(F/.x) = F9/.x;
then k(*)(F/.x2) = g by A6;
then
A13: k(*)i2 = g by A1,Th3;
k(*)(F/.x1) = f by A4,A12;
then k(*)i1 = f by A1,Th3;
hence thesis by A10,A11,A13;
end;
assume h = k;
then
A14: k(*)i1 = f & k(*)i2 = g by A10,A11;
let x;
assume x in I;
then x = x1 or x = x2 by TARSKI:def 2;
hence thesis by A1,A14,Th3;
end;
assume
A15: c is_a_coproduct_wrt F;
then
A16: F is Injections_family of c,I;
x2 in I by TARSKI:def 2;
then
A17: cod(F/.x2) = c by A16,Th62;
x1 in I by TARSKI:def 2;
then cod(F/.x1) = c by A16,Th62;
hence cod i1 = c & cod i2 = c by A1,A17,Th3;
let d,f,g such that
A18: f in Hom(dom i1,d) and
A19: g in Hom(dom i2,d);
cod f = d & cod g = d by A18,A19,CAT_1:1;
then reconsider F9 = (x1,x2) --> (f,g) as Injections_family of d,I by Th65;
doms F = (x1,x2)-->(dom i1,dom i2) by Th6
.= (x1,x2)-->(dom f,dom i2) by A18,CAT_1:1
.= (x1,x2)-->(dom f,dom g) by A19,CAT_1:1
.= doms F9 by Th6;
then consider h such that
A20: h in Hom(c,d) and
A21: for k st k in Hom(c,d) holds (for x st x in I holds k(*)(F/.x) = F9/.
x ) iff h = k by A15;
take h;
thus h in Hom(c,d) by A20;
let k such that
A22: k in Hom(c,d);
thus k(*)i1 = f & k(*)i2 = g implies h = k
proof
assume
A23: k(*)i1 = f & k(*)i2 = g;
now
let x;
assume x in I;
then x = x1 or x = x2 by TARSKI:def 2;
then F/.x = i1 & F9/.x = f or F/.x = i2 & F9/.x = g by A1,Th3;
hence k(*)(F/.x) = F9/.x by A23;
end;
hence thesis by A21,A22;
end;
assume
A24: h = k;
x2 in I by TARSKI:def 2;
then k(*)(F/.x2) = F9/.x2 by A21,A22,A24;
then
A25: k(*)(F/.x2) = g by A1,Th3;
x1 in I by TARSKI:def 2;
then k(*)(F/.x1) = F9/.x1 by A21,A22,A24;
then k(*)(F/.x1) = f by A1,Th3;
hence thesis by A1,A25,Th3;
end;
theorem
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
proof
assume that
A1: c is_a_coproduct_wrt i1,i2 and
A2: d is_a_coproduct_wrt j1,j2 and
A3: dom i1 = dom j1 & dom i2 = dom j2;
set I = {0,{0}}, F = (0,{0})-->(i1,i2), F9 = (0,{0})-->(j1,j2);
A4: c is_a_coproduct_wrt F & d is_a_coproduct_wrt F9 by A1,A2,Th79;
doms F = (0,{0})-->(dom j1,dom j2) by A3,Th6
.= doms F9 by Th6;
hence thesis by A4,Th72;
end;
theorem
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
proof
assume that
A1: Hom(a,c) <> {} and
A2: Hom(b,c) <> {};
let i1 be Morphism of a,c, i2 be Morphism of b,c;
thus c is_a_coproduct_wrt i1,i2 implies 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
proof
assume that
cod i1 = c and
cod i2 = c and
A3: 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;
let d such that
A4: Hom(a,d)<>{} and
A5: Hom(b,d)<>{};
set f = the Morphism of a,d,g = the Morphism of b,d;
A6: dom i2 = b by A2,CAT_1:5;
then
A7: g in Hom(dom i2,d) by A5,CAT_1:def 5;
A8: dom i1 = a by A1,CAT_1:5;
then f in Hom(dom i1,d) by A4,CAT_1:def 5;
then
A9: 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 by A3,A7;
hence Hom(c,d) <> {};
let f be Morphism of a,d, g be Morphism of b,d;
A10: g in Hom(dom i2,d) by A5,A6,CAT_1:def 5;
f in Hom(dom i1,d) by A4,A8,CAT_1:def 5;
then consider h such that
A11: h in Hom(c,d) and
A12: for k st k in Hom(c,d) holds k(*)i1 = f & k(*)i2 = g iff h = k by A3,A10;
reconsider h as Morphism of c,d by A11,CAT_1:def 5;
take h;
let k be Morphism of c,d;
A13: k in Hom(c,d) by A9,CAT_1:def 5;
k*i1 = k(*)(i1 qua Morphism of C) & k*i2 = k(*)(i2 qua Morphism of C)
by A1,A2,A9,CAT_1:def 13;
hence thesis by A12,A13;
end;
assume
A14: 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;
thus cod i1 = c & cod i2 = c by A1,A2,CAT_1:5;
let d,f,g such that
A15: f in Hom(dom i1,d) and
A16: g in Hom(dom i2,d);
A17: Hom(a,d) <> {} by A1,A15,CAT_1:5;
A18: dom i1 = a by A1,CAT_1:5;
then
A19: f is Morphism of a,d by A15,CAT_1:def 5;
A20: dom i2 = b by A2,CAT_1:5;
then g is Morphism of b,d by A16,CAT_1:def 5;
then consider h being Morphism of c,d such that
A21: for k being Morphism of c,d holds k*i1 = f & k*i2 = g iff h = k by A14,A16
,A20,A19,A17;
reconsider h9 = h as Morphism of C;
take h9;
A22: Hom(c,d) <> {} by A14,A15,A16,A18,A20;
hence h9 in Hom(c,d) by CAT_1:def 5;
let k;
assume k in Hom(c,d);
then reconsider k9 = k as Morphism of c,d by CAT_1:def 5;
k(*)i1 = k9*i1 & k(*)i2 = k9*i2 by A1,A2,A22,CAT_1:def 13;
hence thesis by A21;
end;
theorem
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
proof let i1 be Morphism of a,c, i2 be Morphism of b,c such that
A1: Hom(a,c) <> {} & Hom(b,c) <> {};
assume that
A2: c is_a_coproduct_wrt i1,i2 and
A3: Hom(a,b) <> {} & Hom(b,a) <> {};
set I = {0,{0}};
cod i1 = c & cod i2 = c by A2;
then reconsider F = (0,{0})-->(i1,i2) as Injections_family of c,I
by Th65;
A4: F/.0 = i1 by Th3;
A5: F/.{0} = i2 by Th3;
A6: now
thus F is Injections_family of c,I;
thus c is_a_coproduct_wrt F by A2,Th79;
let x1,x2;
assume that
A7: x1 in I and
A8: x2 in I;
A9: x2 = 0 or x2 = {0} by A8,TARSKI:def 2;
x1 = 0 or x1 = {0} by A7,TARSKI:def 2;
then
A10: dom(F/.x1) = a or dom(F/.x1) = b by A4,A5,A1,CAT_1:5;
dom(F/.x2) = a or dom(F/.x2) = b by A9,A4,A5,A1,CAT_1:5;
hence Hom(dom(F/.x1),dom(F/.x2)) <> {} by A3,A10;
end;
A11: {0} in I by TARSKI:def 2;
A12: 0 in I by TARSKI:def 2;
dom(F/.0) = a & dom(F/.{0}) = b by A4,A5,A1,CAT_1:5;
hence thesis by A4,A6,A11,Th73,A5,A12,A1;
end;
theorem Th83:
c is_a_coproduct_wrt i1,i2 & h in Hom(c,c) & h(*)i1 = i1 & h(*)i2 =
i2 implies h = id c
proof
assume that
A1: cod i1 = c & cod i2 = c and
A2: 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 and
A3: h in Hom(c,c) & h(*)i1 = i1 & h(*)i2 = i2;
i1 in Hom(dom i1,c) & i2 in Hom(dom i2,c) by A1;
then consider i such that
i in Hom(c,c) and
A4: for k st k in Hom(c,c) holds k(*)i1 = i1 & k(*)i2 = i2 iff i = k by A2;
A5: id c in Hom(c,c) by CAT_1:27;
(id c)(*)i1 = i1 & (id c)(*)i2 = i2 by A1,CAT_1:21;
hence id c = i by A4,A5
.= h by A3,A4;
end;
theorem
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
proof let f be Morphism of c,d;
assume that
A1: c is_a_coproduct_wrt i1,i2 and
A2: dom f = c & cod f = d & f is invertible;
c is_a_coproduct_wrt (0,{0})-->(i1,i2) by A1,Th79;
then d is_a_coproduct_wrt f*((0,{0})-->(i1,i2)) by A2,Th74;
then d is_a_coproduct_wrt (0,{0})-->(f(*)i1,f(*)i2) by Th15;
hence thesis by Th79;
end;
theorem
c is_a_coproduct_wrt i1,i2 & dom i2 is initial implies dom i1,c
are_isomorphic
proof
set a = dom i1, b = dom i2;
assume that
A1: c is_a_coproduct_wrt i1,i2 and
A2: b is initial;
set f = id(a),g = init(b,a);
cod g = a & dom g = b by A2,Th38;
then f in Hom(a,a) & g in Hom(b,a) by CAT_1:27;
then consider h such that
A3: h in Hom(c,a) and
A4: for k st k in Hom(c,a) holds k(*)i1 = f & k(*)i2 = g iff h = k by A1;
A5: cod h = a by A3,CAT_1:1;
A6: cod i1 = c by A1;
then reconsider i = i1 as Morphism of a,c by CAT_1:4;
A7: dom h = c by A3,CAT_1:1;
then
A8: dom(i(*)h) = c by A5,CAT_1:17;
A9: cod i2 = c by A1;
then
A10: dom(i(*)h(*)i2) = b by A8,CAT_1:17;
A11: cod(i(*)h) = c by A6,A5,CAT_1:17;
then
A12: i(*)h in Hom(c,c) by A8;
cod(i(*)h(*)i2) = c by A9,A11,A8,CAT_1:17;
then
A13: i(*)h(*)i2 = init(b,c) by A2,A10,Th39
.= i2 by A2,A9,Th39;
A14: Hom(a,c)<>{} by A6,CAT_1:2;
take i;
thus Hom(a,c) <> {} & Hom(c,a) <> {} by A3,A6,CAT_1:2;
reconsider h as Morphism of c,a by A3,CAT_1:def 5;
take h;
A15: i(*)h(*)i1 = i(*)(h(*)i1) by A6,A5,A7,CAT_1:18
.= i(*)(id dom i) by A3,A4
.= i by CAT_1:22;
thus i*h = i(*)h by A3,A14,CAT_1:def 13
.= id c by A1,A13,A12,Th83,A15;
thus id a = h(*)i by A3,A4
.= h*i by A14,A3,CAT_1:def 13;
end;
theorem
c is_a_coproduct_wrt i1,i2 & dom i1 is initial implies dom i2,c
are_isomorphic
proof
set a = dom i1, b = dom i2;
assume that
A1: c is_a_coproduct_wrt i1,i2 and
A2: a is initial;
set f = id(b),g = init(a,b);
cod g = b & dom g = a by A2,Th38;
then f in Hom(b,b) & g in Hom(a,b) by CAT_1:27;
then consider h such that
A3: h in Hom(c,b) and
A4: for k st k in Hom(c,b) holds k(*)i1 = g & k(*)i2 = f iff h = k by A1;
A5: cod h = b by A3,CAT_1:1;
A6: cod i2 = c by A1;
then reconsider i = i2 as Morphism of b,c by CAT_1:4;
A7: dom h = c by A3,CAT_1:1;
then
A8: dom(i(*)h) = c by A5,CAT_1:17;
A9: cod i1 = c by A1;
then
A10: dom(i(*)h(*)i1) = a by A8,CAT_1:17;
A11: cod(i(*)h) = c by A6,A5,CAT_1:17;
then
A12: i(*)h in Hom(c,c) by A8;
cod(i(*)h(*)i1) = c by A9,A11,A8,CAT_1:17;
then
A13: i(*)h(*)i1 = init(a,c) by A2,A10,Th39
.= i1 by A2,A9,Th39;
A14: Hom(b,c)<>{} by A6,CAT_1:2;
take i;
thus Hom(b,c) <> {} & Hom(c,b) <> {} by A6,A3,CAT_1:2;
reconsider h as Morphism of c,b by A3,CAT_1:def 5;
take h;
A15: i(*)h(*)i2 = i(*)(h(*)i2) by A6,A5,A7,CAT_1:18
.= i(*)(id dom i) by A3,A4
.= i by CAT_1:22;
thus i*h = i(*)h by A3,A14,CAT_1:def 13
.= id c by A1,A13,A12,Th83,A15;
thus id b = h(*)i by A3,A4
.= h*i by A3,A14,CAT_1:def 13;
end;