Copyright (c) 1992 Association of Mizar Users
environ
vocabulary CAT_1, FUNCT_1, FINSEQ_4, RELAT_1, FUNCOP_1, FUNCT_4, BOOLE,
FUNCT_6, OPPCAT_1, WELLORD1, CAT_3;
notation TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCOP_1, FUNCT_4,
FUNCT_2, FINSEQ_4, CAT_1, OPPCAT_1;
constructors OPPCAT_1, FINSEQ_4, MEMBERED, XBOOLE_0;
clusters RELSET_1, MEMBERED, ZFMISC_1, XBOOLE_0;
requirements SUBSET, BOOLE;
definitions CAT_1;
theorems TARSKI, FUNCT_2, FUNCOP_1, FUNCT_4, CAT_1, OPPCAT_1, FINSEQ_4,
RELSET_1, PARTFUN1;
schemes FUNCT_2, COMPTS_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;
definition let I,A; let F be Function of I,A; let x be set;
assume
A1: x in I;
redefine func F/.x equals
:Def1: F.x;
compatibility
proof let a be Element of A;
x in dom F by A1,FUNCT_2:def 1;
hence a = F/.x iff a = F.x by FINSEQ_4:def 4;
end;
end;
scheme LambdaIdx{I()->set,A()->non empty set,F(set)->Element of A()}:
ex F being Function of I(),A() st for x st x in I() holds F/.x = F(x)
proof
deffunc f(set) = F($1);
A1: for x st x in I() holds f(x) in A();
consider IT being Function of I(),A() such that
A2: for x st x in I() holds IT.x = f(x) from Lambda1(A1);
take IT;
let x; assume
A3: x in I();
hence F(x) = IT.x by A2 .= IT/.x by A3,Def1;
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; assume
A2: x in I;
hence F1.x = F1/.x by Def1 .= F2/.x by A1,A2 .= F2.x by A2,Def1;
end;
hence thesis by FUNCT_2:18;
end;
scheme FuncIdx_correctness{I()->set,A()->non empty set,F(set)->Element of A()}:
(ex F being Function of I(),A() st for x st x in I() holds F/.x = F(x)) &
(for F1,F2 being Function of I(),A() st
(for x st x in I() holds F1/.x = F(x)) &
(for x st x in I() holds F2/.x = F(x))
holds F1 = F2)
proof
deffunc f(set) = F($1);
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,I; let a be Element of A;
redefine func I --> a -> Function of I,A;
coherence by FUNCOP_1:58;
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:13 .= (I --> a)/.x by A1,Def1;
end;
canceled 4;
theorem Th7:
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);
h.x1 = y1 & h.x2 = y2 & x1 in {x1,x2} & x2 in {x1,x2} by A1,FUNCT_4:66,
TARSKI:def 2;
hence thesis by Def1;
end;
begin :: Indexed families of morphisms
definition let C,I; let F be Function of I,the Morphisms of C;
canceled;
func doms F -> Function of I, the Objects of C means
:Def3: for x st x in I holds it/.x = dom(F/.x);
correctness
proof
set A = the Objects of C;
deffunc F(set) = dom(F/.$1);
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 FuncIdx_correctness;
end;
func cods F -> Function of I, the Objects of C means
:Def4: for x st x in I holds it/.x = cod(F/.x);
correctness
proof
set A = the Objects of C;
deffunc F(set) = cod(F/.$1);
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 FuncIdx_correctness;
end;
end;
theorem Th8:
doms(I-->f) = I-->(dom f)
proof set F = I-->f, F' = I-->(dom f);
now let x; assume
A1: x in I;
then F/.x = f & F'/.x = dom f by Th2;
hence (doms F)/.x = F'/.x by A1,Def3;
end;
hence thesis by Th1;
end;
theorem Th9:
cods(I-->f) = I-->(cod f)
proof set F = I-->f, F' = I-->(cod f);
now let x; assume
A1: x in I;
then F/.x = f & F'/.x = cod f by Th2;
hence (cods F)/.x = F'/.x by A1,Def4;
end;
hence thesis by Th1;
end;
theorem Th10:
doms((x1,x2)-->(p1,p2)) = (x1,x2)-->(dom p1,dom p2)
proof
set F = (x1,x2)-->(p1,p2), f = {x1} --> p1, g = {x2} --> p2,
F' = (x1,x2)-->(dom p1,dom p2), f' = {x1}-->(dom p1), g' = {x2}-->(dom p2);
A1: dom f = {x1} & dom f' = {x1} & dom g = {x2} & dom g' = {x2}
by FUNCOP_1:19;
A2: F = f +* g & F' = f' +* g' by FUNCT_4:def 4;
now let x; assume
A3: x in {x1,x2};
then A4: x in dom F by FUNCT_4:65;
now per cases by A2,A4,FUNCT_4:13;
case
A5: x in dom f & not x in dom g;
then F.x = f.x & F'.x = f'.x by A1,A2,FUNCT_4:12;
then F.x = p1 & F'.x = dom p1 by A1,A5,FUNCOP_1:13;
hence F/.x = p1 & F'/.x = dom p1 by A3,Def1;
case
A6: x in dom g;
then F.x = g.x & F'.x = g'.x by A1,A2,FUNCT_4:14;
then F.x = p2 & F'.x = dom p2 by A1,A6,FUNCOP_1:13;
hence F/.x = p2 & F'/.x = dom p2 by A3,Def1;
end;
hence (doms F)/.x = F'/.x by A3,Def3;
end;
hence thesis by Th1;
end;
theorem Th11:
cods((x1,x2)-->(p1,p2)) = (x1,x2)-->(cod p1,cod p2)
proof
set F = (x1,x2)-->(p1,p2), f = {x1} --> p1, g = {x2} --> p2,
F' = (x1,x2)-->(cod p1,cod p2), f' = {x1}-->(cod p1), g' = {x2}-->(cod p2);
A1: dom f = {x1} & dom f' = {x1} & dom g = {x2} & dom g' = {x2}
by FUNCOP_1:19;
A2: F = f +* g & F' = f' +* g' by FUNCT_4:def 4;
now let x; assume
A3: x in {x1,x2};
then A4: x in dom F by FUNCT_4:65;
now per cases by A2,A4,FUNCT_4:13;
case
A5: x in dom f & not x in dom g;
then F.x = f.x & F'.x = f'.x by A1,A2,FUNCT_4:12;
then F.x = p1 & F'.x = cod p1 by A1,A5,FUNCOP_1:13;
hence F/.x = p1 & F'/.x = cod p1 by A3,Def1;
case
A6: x in dom g;
then F.x = g.x & F'.x = g'.x by A1,A2,FUNCT_4:14;
then F.x = p2 & F'.x = cod p2 by A1,A6,FUNCOP_1:13;
hence F/.x = p2 & F'/.x = cod p2 by A3,Def1;
end;
hence (cods F)/.x = F'/.x by A3,Def4;
end;
hence thesis by Th1;
end;
definition let C,I; let F be Function of I,the Morphisms of C;
func F opp -> Function of I,the Morphisms of C opp means
:Def5: for x st x in I holds it/.x = (F/.x) opp;
correctness
proof
set A = the Morphisms of C opp;
deffunc F(set) = (F/.$1) 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 FuncIdx_correctness;
end;
end;
theorem
(I --> f) opp = I --> f opp
proof set F = I --> f, F' = I --> f opp;
now let x; assume
A1: x in I;
then F/.x = f & F'/.x = f opp by Th2;
hence F opp/.x = F'/.x by A1,Def5;
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), F' = (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 & F'/.x = p1 opp or F/.x = p2 & F'/.x = p2 opp by A1,Th7;
hence F opp/.x = F'/.x by A2,Def5;
end;
hence thesis by Th1;
end;
theorem
for F being Function of I,the Morphisms of C holds F opp opp = F
proof let F be Function of I,the Morphisms of C;
now
C opp = CatStr (#the Objects of C, the Morphisms of C,
the Cod of C, the Dom of C,
~(the Comp of C), the Id of C#) &
C opp opp = CatStr (#the Objects of C opp, the Morphisms of C opp,
the Cod of C opp, the Dom of C opp,
~(the Comp of C opp), the Id of C opp#) by OPPCAT_1:def 1;
hence the Morphisms of C = the Morphisms of C opp opp;
let x; assume
A1: x in I;
hence (F opp opp)/.x = ((F opp)/.x) opp by Def5
.= (F/.x) opp opp by A1,Def5
.= F/.x by OPPCAT_1:6;
end;
hence thesis by Th1;
end;
definition let C,I; let F be Function of I,the Morphisms of C opp;
func opp F -> Function of I,the Morphisms of C means
:Def6: for x st x in I holds it/.x = opp (F/.x);
correctness
proof
set A = the Morphisms of C;
deffunc F(set) = opp (F/.$1);
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 FuncIdx_correctness;
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, F' = I --> (opp f);
now let x; assume
A1: x in I;
then F/.x = f & F'/.x = opp f by Th2;
hence opp F/.x = F'/.x by A1,Def6;
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), F' = (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 & F'/.x = opp p1 or F/.x = p2 & F'/.x = opp p2 by A1,Th7;
hence opp F/.x = F'/.x by A2,Def6;
end;
hence thesis by Th1;
end;
theorem
for F being Function of I,the Morphisms of C holds opp(F opp) = F
proof let F be Function of I,the Morphisms of C;
now let x; assume
A1: x in I;
hence opp(F opp)/.x = opp((F opp)/.x) by Def6
.= opp((F/.x) opp) by A1,Def5
.= F/.x by OPPCAT_1:7;
end;
hence thesis by Th1;
end;
definition let C,I; let F be Function of I,the Morphisms of C, f;
func F*f -> Function of I,the Morphisms of C means
:Def7: for x st x in I holds it/.x = (F/.x)*f;
correctness
proof
set A = the Morphisms of C;
deffunc F(set) = (F/.$1)*f;
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 FuncIdx_correctness;
end;
func f*F -> Function of I,the Morphisms of C means
:Def8: for x st x in I holds it/.x = f*(F/.x);
correctness
proof
set A = the Morphisms of C;
deffunc F(set) = f*(F/.$1);
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 FuncIdx_correctness;
end;
end;
theorem Th18:
x1 <> x2 implies ((x1,x2)-->(p1,p2))*f = (x1,x2)-->(p1*f,p2*f)
proof
assume
A1: x1 <> x2;
set F = (x1,x2)-->(p1,p2), F' = (x1,x2)-->(p1*f,p2*f);
now let x; assume
A2: x in {x1,x2};
then x = x1 or x = x2 by TARSKI:def 2;
then F/.x = p1 & F'/.x = p1*f or F/.x = p2 & F'/.x = p2*f by A1,Th7;
hence (F*f)/.x = F'/.x by A2,Def7;
end;
hence thesis by Th1;
end;
theorem Th19:
x1 <> x2 implies f*((x1,x2)-->(p1,p2)) = (x1,x2)-->(f*p1,f*p2)
proof
assume
A1: x1 <> x2;
set F = (x1,x2)-->(p1,p2), F' = (x1,x2)-->(f*p1,f*p2);
now let x; assume
A2: x in {x1,x2};
then x = x1 or x = x2 by TARSKI:def 2;
then F/.x = p1 & F'/.x = f*p1 or F/.x = p2 & F'/.x = f*p2 by A1,Th7;
hence (f*F)/.x = F'/.x by A2,Def8;
end;
hence thesis by Th1;
end;
theorem Th20:
for F being Function of I,the Morphisms of C st doms F = I-->cod f
holds doms(F*f) = I-->dom f & cods(F*f) = cods F
proof let F be Function of I,the Morphisms 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,Def3 .= cod f by A2,Th2;
thus (doms(F*f))/.x = dom((F*f)/.x) by A2,Def3
.= dom((F/.x)*f) by A2,Def7
.= dom f by A3,CAT_1:42
.= (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,Def3 .= cod f by A4,Th2;
thus (cods F)/.x = cod(F/.x) by A4,Def4
.= cod((F/.x)*f) by A5,CAT_1:42
.= cod((F*f)/.x) by A4,Def7
.= (cods(F*f))/.x by A4,Def4;
end;
hence cods(F*f) = cods F by Th1;
end;
theorem Th21:
for F being Function of I,the Morphisms of C st cods F = I-->dom f
holds doms(f*F) = doms F & cods(f*F) = I-->cod f
proof let F be Function of I,the Morphisms 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,Def4 .= dom f by A2,Th2;
thus (doms F)/.x = dom(F/.x) by A2,Def3
.= dom(f*(F/.x)) by A3,CAT_1:42
.= dom((f*F)/.x) by A2,Def8
.= (doms(f*F))/.x by A2,Def3;
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,Def4 .= dom f by A4,Th2;
thus (cods(f*F))/.x = cod((f*F)/.x) by A4,Def4
.= cod(f*(F/.x)) by A4,Def8
.= cod f by A5,CAT_1:42
.= (I--> cod f)/.x by A4,Th2;
end;
hence cods(f*F) = I-->cod f by Th1;
end;
definition let C,I; let F,G be Function of I,the Morphisms of C;
func F"*"G -> Function of I,the Morphisms of C means
:Def9: for x st x in I holds it/.x = (F/.x)*(G/.x);
correctness
proof
set A = the Morphisms of C;
deffunc F(set) = (F/.$1)*(G/.$1);
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 FuncIdx_correctness;
end;
end;
theorem Th22:
for F,G being Function of I,the Morphisms of C st doms F = cods G
holds doms(F"*"G) = doms G & cods(F"*"G) = cods F
proof let F,G be Function of I,the Morphisms 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,Def4 .= dom(F/.x) by A2,Def3;
thus (doms(F"*"G))/.x = dom((F"*"G)/.x) by A2,Def3
.= dom((F/.x)*(G/.x)) by A2,Def9
.= dom(G/.x) by A3,CAT_1:42
.= (doms G)/.x by A2,Def3;
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,Def4 .= dom(F/.x) by A4,Def3;
thus (cods(F"*"G))/.x = cod((F"*"G)/.x) by A4,Def4
.= cod((F/.x)*(G/.x)) by A4,Def9
.= cod(F/.x) by A5,CAT_1:42
.= (cods F)/.x by A4,Def4;
end;
hence cods(F"*"G) = cods F by Th1;
end;
theorem
x1 <> x2 implies
((x1,x2)-->(p1,p2))"*"((x1,x2)-->(q1,q2)) = (x1,x2)-->(p1*q1,p2*q2)
proof
assume
A1: x1 <> x2;
set F1 = (x1,x2)-->(p1,p2), F2 = (x1,x2)-->(q1,q2),
G = (x1,x2)-->(p1*q1,p2*q2);
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,Th7;
hence (F1"*"F2)/.x = G/.x by A2,Def9;
end;
hence thesis by Th1;
end;
theorem
for F being Function of I,the Morphisms of C holds F*f = F"*"(I-->f)
proof let F be Function of I,the Morphisms of C;
now let x; assume
A1: x in I;
hence (F*f)/.x = (F/.x)*f by Def7
.= (F/.x)*((I-->f)/.x) by A1,Th2
.= (F"*"(I-->f))/.x by A1,Def9;
end;
hence thesis by Th1;
end;
theorem
for F being Function of I,the Morphisms of C holds f*F = (I-->f)"*"F
proof let F be Function of I,the Morphisms of C;
now let x; assume
A1: x in I;
hence (f*F)/.x = f*(F/.x) by Def8
.= ((I-->f)/.x)*(F/.x) by A1,Th2
.= ((I-->f)"*"F)/.x by A1,Def9;
end;
hence thesis by Th1;
end;
begin :: Retractions and Coretractions
definition let C;
let IT be Morphism of C;
attr IT is retraction means
:Def10: ex g st cod g = dom IT & IT*g = id(cod IT);
attr IT is coretraction means
:Def11: ex g st dom g = cod IT & g*IT = id(dom IT);
end;
theorem Th26:
f is retraction implies f is epi
proof given g such that
A1: cod g = dom f and
A2: f*g = id(cod f);
let p1,p2 such that
A3: dom p1 = cod f and
A4: dom p2 = cod f and cod p1 = cod p2 and
A5: p1*f = p2*f;
thus p1 = p1*(f*g) by A2,A3,CAT_1:47
.= (p2*f)*g by A1,A3,A5,CAT_1:43
.= p2*(f*g) by A1,A4,CAT_1:43
.= p2 by A2,A4,CAT_1:47;
end;
theorem
f is coretraction implies f is monic
proof given g such that
A1: dom g = cod f and
A2: g*f = id(dom f);
let p1,p2 such that dom p1 = dom p2 and
A3: cod p1 = dom f and
A4: cod p2 = dom f and
A5: f*p1 = f*p2;
thus p1 = g*f*p1 by A2,A3,CAT_1:46
.= g*(f*p2) by A1,A3,A5,CAT_1:43
.= g*f*p2 by A1,A4,CAT_1:43
.= p2 by A2,A4,CAT_1:46;
end;
theorem
f is retraction & g is retraction & dom g = cod f
implies g*f is retraction
proof given i such that
A1: cod i = dom f and
A2: f*i = id(cod f);
given j such that
A3: cod j = dom g and
A4: g*j = id(cod g);
assume
A5: dom g = cod f;
take i*j;
A6: dom i = dom(f*i) by A1,CAT_1:42 .= cod f by A2,CAT_1:44;
then A7: cod(i*j) = dom f by A1,A3,A5,CAT_1:42;
hence cod(i*j) = dom(g*f) by A5,CAT_1:42;
thus g*f*(i*j) = g*(f*(i*j)) by A5,A7,CAT_1:43
.= g*(f*i*j) by A1,A3,A5,A6,CAT_1:43
.= id(cod g) by A2,A3,A4,A5,CAT_1:46
.= id(cod(g*f)) by A5,CAT_1:42;
end;
theorem
f is coretraction & g is coretraction & dom g = cod f
implies g*f is coretraction
proof given i such that
A1: dom i = cod f and
A2: i*f = id(dom f);
given j such that
A3: dom j = cod g and
A4: j*g = id(dom g);
assume
A5: dom g = cod f;
take i*j;
A6: cod j = cod(j*g) by A3,CAT_1:42 .= dom g by A4,CAT_1:44;
A7: cod g = cod(g*f) by A5,CAT_1:42;
hence dom(i*j) = cod(g*f) by A1,A3,A5,A6,CAT_1:42;
thus i*j*(g*f) = i*(j*(g*f)) by A1,A3,A5,A6,A7,CAT_1:43
.= i*(j*g*f) by A3,A5,CAT_1:43
.= id(dom f) by A2,A4,A5,CAT_1:46
.= id(dom(g*f)) by A5,CAT_1:42;
end;
theorem
dom g = cod f & g*f is retraction implies g is retraction
proof assume
A1: dom g = cod f;
given i such that
A2: cod i = dom(g*f) and
A3: (g*f)*i = id(cod(g*f));
take f*i;
A4: dom f = dom(g*f) by A1,CAT_1:42;
hence cod(f*i) = dom g by A1,A2,CAT_1:42;
thus g*(f*i) = id(cod(g*f)) by A1,A2,A3,A4,CAT_1:43
.= id(cod g) by A1,CAT_1:42;
end;
theorem
dom g = cod f & g*f is coretraction implies f is coretraction
proof assume
A1: dom g = cod f;
given i such that
A2: dom i = cod(g*f) and
A3: i*(g*f) = id(dom(g*f));
take i*g;
A4: cod g = cod(g*f) by A1,CAT_1:42;
hence dom(i*g) = cod f by A1,A2,CAT_1:42;
thus (i*g)*f = id(dom(g*f)) by A1,A2,A3,A4,CAT_1:43
.= id(dom f) by A1,CAT_1:42;
end;
theorem
f is retraction & f is monic implies f is invertible
proof given i such that
A1: cod i = dom f and
A2: f*i = id(cod f);
assume
A3: f is monic;
take i;
thus
A4: dom i = dom(f*i) by A1,CAT_1:42 .= cod f by A2,CAT_1:44;
thus cod i = dom f by A1;
thus f*i = id cod f by A2;
now
thus dom(i*f) = dom f by A4,CAT_1:42 .= dom(id(dom f)) by CAT_1:44;
thus cod(i*f) = dom f by A1,A4,CAT_1:42;
thus cod(id(dom f)) = dom f by CAT_1:44;
thus f*(i*f) = id(cod f)*f by A1,A2,A4,CAT_1:43
.= f by CAT_1:46
.= f * id(dom f) by CAT_1:47;
end;
hence i*f = id(dom f) by A3,CAT_1:def 10;
end;
theorem Th33:
f is coretraction & f is epi implies f is invertible
proof given i such that
A1: dom i = cod f and
A2: i*f = id(dom f);
assume
A3: f is epi;
take i;
thus dom i = cod f by A1;
thus
A4: cod i = cod(i*f) by A1,CAT_1:42 .= dom f by A2,CAT_1:44;
now
thus dom(f*i) = cod f by A1,A4,CAT_1:42;
thus dom(id(cod f)) = cod f by CAT_1:44;
thus cod(f*i) = cod f by A4,CAT_1:42 .= cod(id(cod f)) by CAT_1:44;
thus f*i*f = f * id(dom f) by A1,A2,A4,CAT_1:43
.= f by CAT_1:47
.= id(cod f)*f by CAT_1:46;
end;
hence f*i = id cod f by A3,CAT_1:def 11;
thus i*f = id(dom f) by A2;
end;
theorem
f is invertible iff f is retraction & f is coretraction
proof
thus f is invertible implies f is retraction & f is coretraction
proof
assume ex g st dom g = cod f & cod g = dom f &
f*g = id cod f & g*f = id dom f;
hence thesis by Def10,Def11;
end;
assume f is retraction;
then f is epi by Th26;
hence thesis by Th33;
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;
given i such that
A1: cod i = dom f and
A2: f*i = id(cod f);
take T.i;
thus cod(T.i) = T.(dom f) by A1,CAT_1:109 .= dom(T.f) by CAT_1:109;
thus (T.f)*(T.i) = T.(id(cod f)) by A1,A2,CAT_1:99
.= id(cod(T.f)) by CAT_1:98;
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;
given i such that
A1: dom i = cod f and
A2: i*f = id(dom f);
take T.i;
thus dom(T.i) = T.(cod f) by A1,CAT_1:109 .= cod(T.f) by CAT_1:109;
thus (T.i)*(T.f) = T.(id(dom f)) by A1,A2,CAT_1:99
.= id(dom(T.f)) by CAT_1:98;
end;
theorem
f is retraction iff f opp is coretraction
proof
thus f is retraction implies f opp is coretraction
proof given i such that
A1: cod i = dom f and
A2: f*i = id(cod f);
take i opp;
thus dom(i opp) = dom f by A1,OPPCAT_1:9 .= cod(f opp) by OPPCAT_1:9;
thus (i opp)*(f opp) = (id(cod f)) opp by A1,A2,OPPCAT_1:17
.= id((cod f)opp) by OPPCAT_1:21
.= id(dom(f opp)) by OPPCAT_1:11;
end;
given i being Morphism of C opp such that
A3: dom i = cod(f opp) and
A4: i*(f opp) = id(dom(f opp));
take opp i;
thus
A5: cod(opp i) = cod(f opp) by A3,OPPCAT_1:10 .= dom f by OPPCAT_1:9;
thus f*(opp i) = (f*(opp i)) opp by OPPCAT_1:def 4
.= ((opp i)opp)*(f opp) by A5,OPPCAT_1:17
.= id(dom(f opp)) by A4,OPPCAT_1:8
.= id((cod f)opp) by OPPCAT_1:11
.= (id(cod f))opp by OPPCAT_1:21
.= id(cod f) by OPPCAT_1:def 4;
end;
theorem
f is coretraction iff f opp is retraction
proof
thus f is coretraction implies f opp is retraction
proof given i such that
A1: dom i = cod f and
A2: i*f = id(dom f);
take i opp;
thus cod(i opp) = cod f by A1,OPPCAT_1:9 .= dom(f opp) by OPPCAT_1:9;
thus (f opp)*(i opp) = (id(dom f))opp by A1,A2,OPPCAT_1:17
.= id((dom f)opp) by OPPCAT_1:21
.= id(cod(f opp)) by OPPCAT_1:11;
end;
given i being Morphism of C opp such that
A3: cod i = dom(f opp) and
A4: (f opp)*i = id(cod(f opp));
take opp i;
thus
A5: dom(opp i) = dom(f opp) by A3,OPPCAT_1:10 .= cod f by OPPCAT_1:9;
thus (opp i)*f = ((opp i)*f) opp by OPPCAT_1:def 4
.= (f opp)*((opp i)opp) by A5,OPPCAT_1:17
.= id(cod(f opp)) by A4,OPPCAT_1:8
.= id((dom f)opp) by OPPCAT_1:11
.= (id(dom f))opp by OPPCAT_1:21
.= id(dom f) by OPPCAT_1:def 4;
end;
begin :: Morphisms determined by a terminal Object
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,CAT_1:def 15;
thus f1 = f by A2 .= f2 by A2;
end;
end;
theorem Th39:
b is terminal implies dom(term(a,b)) = a & cod(term(a,b)) = b
proof assume b is terminal;
then Hom(a,b) <> {} by CAT_1:def 15;
hence thesis by CAT_1:23;
end;
theorem Th40:
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,CAT_1:def 15;
f is Morphism of a,b by A2,CAT_1:22;
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) <> {} by CAT_1:def 15;
then dom f = a & cod f = b by CAT_1:23;
hence thesis by A1,Th40;
end;
begin :: Morphisms 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,CAT_1:def 16;
thus f1 = f by A2 .= f2 by A2;
end;
end;
theorem Th42:
a is initial implies dom(init(a,b)) = a & cod(init(a,b)) = b
proof assume a is initial;
then Hom(a,b) <> {} by CAT_1:def 16;
hence dom(init(a,b)) = a & cod(init(a,b)) = b by CAT_1:23;
end;
theorem Th43:
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,CAT_1:def 16;
f is Morphism of a,b by A2,CAT_1:22;
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) <> {} by CAT_1:def 16;
then dom f = a & cod f = b by CAT_1:23;
hence thesis by A1,Th43;
end;
begin :: Products
definition let C,a,I;
mode Projections_family of a,I -> Function of I,the Morphisms of C means
:Def14: doms it = I --> a;
existence
proof take F = I-->id a;
doms F = I --> (dom id a) by Th8;
hence thesis by CAT_1:44;
end;
end;
theorem Th45:
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 Def14;
hence dom(F/.x) = (I --> a)/.x by A1,Def3 .= a by A1,Th2;
end;
theorem Th46:
for F being Function of {},the Morphisms of C
holds F is Projections_family of a,{}
proof let F be Function of {},the Morphisms of C;
thus {} --> a = {} by FUNCT_4:3 .= doms F by PARTFUN1:57;
end;
theorem Th47:
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 Def3
.= a by A1,A2,Th2
.= ({y} --> a)/.x by A2,Th2;
end;
hence doms F = {y} --> a by Th1;
end;
theorem Th48:
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 Th10 .= {x1,x2} --> a by A1,FUNCT_4:68;
hence thesis by Def14;
end;
canceled;
theorem Th50:
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 Def14;
hence doms(F*f) = I --> dom f by Th20;
end;
theorem
for F being Function of I,the Morphisms of C,
G being Projections_family of a,I st doms F = cods G
holds F"*"G is Projections_family of a,I
proof let F be Function of I,the Morphisms of C;
let G be Projections_family of a,I;
assume doms F = cods G;
then doms(F"*"G) = doms G by Th22;
hence doms(F"*"G) = I --> a by Def14;
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 Def3
.= (I --> cod f)/.x by Def14
.= cod f by A1,Th2;
thus ((f opp)*(F opp))/.x = (f opp)*((F opp)/.x) by A1,Def8
.= (f opp)*((F/.x)opp) by A1,Def5
.= ((F/.x)*f)opp by A2,OPPCAT_1:17
.= ((F*f)/.x)opp by A1,Def7
.= ((F*f) opp)/.x by A1,Def5;
end;
hence thesis by Th1;
end;
definition let C,a,I; let F be Function of I,the Morphisms of C;
pred a is_a_product_wrt F means
:Def15: F is Projections_family of a,I &
for b for F' being Projections_family of b,I st cods F = cods F'
ex h st h in Hom(b,a) &
for k st k in Hom(b,a) holds
(for x st x in I holds (F/.x)*k = F'/.x) iff h = k;
end;
theorem Th53:
for F being Projections_family of c,I, F' being Projections_family of d,I
st c is_a_product_wrt F & d is_a_product_wrt F' & cods F = cods F'
holds c,d are_isomorphic
proof
let F be Projections_family of c,I, F' be Projections_family of d,I such that
A1: c is_a_product_wrt F and
A2: d is_a_product_wrt F' and
A3: cods F = cods F';
consider f such that
A4: f in Hom(d,c) and
A5: for k st k in Hom(d,c) holds
(for x st x in I holds (F/.x)*k = F'/.x ) iff f = k by A1,A3,Def15;
consider g such that
A6: g in Hom(c,d) and
A7: for k st k in Hom(c,d) holds
(for x st x in I holds (F'/.x)*k = F/.x ) iff g = k by A2,A3,Def15;
thus Hom(c,d) <> {} by A6;
reconsider g as Morphism of c,d by A6,CAT_1:def 7;
take g,f;
A8: dom f = d & cod g = d & cod f = c & dom g = c by A4,A6,CAT_1:18;
hence dom f = cod g & cod f = dom g;
cods F' = cods F';
then consider gf being Morphism of C such that gf in Hom(d,d) and
A9: for k st k in Hom(d,d) holds
(for x st x in I holds (F'/.x)*k = F'/.x ) iff gf = k by A2,Def15;
A10:
now set k = id d;
thus k in Hom(d,d) by CAT_1:55;
let x;
assume x in I;
then dom(F'/.x) = d by Th45;
hence (F'/.x)*k = F'/.x by CAT_1:47;
end;
now dom(g*f) = d & cod(g*f) = d by A8,CAT_1:42;
hence g*f in Hom(d,d) by CAT_1:18;
let x; assume
A11: x in I;
then dom(F'/.x) = d by Th45;
hence (F'/.x)*(g*f) = (F'/.x)*g*f by A8,CAT_1:43
.= (F/.x)*f by A6,A7,A11
.= F'/.x by A4,A5,A11;
end;
hence g*f = gf by A9 .= id cod g by A8,A9,A10;
A12:
now set k = id c;
thus k in Hom(c,c) by CAT_1:55;
let x;
assume x in I;
then dom(F/.x) = c by Th45;
hence (F/.x)*k = F/.x by CAT_1:47;
end;
cods F = cods F;
then consider fg being Morphism of C such that fg in Hom(c,c) and
A13: 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,Def15;
now dom(f*g) = c & cod(f*g) = c by A8,CAT_1:42;
hence f*g in Hom(c,c) by CAT_1:18;
let x; assume
A14: x in I;
then dom(F/.x) = c by Th45;
hence (F/.x)*(f*g) = (F/.x)*f*g by A8,CAT_1:43
.= (F'/.x)*g by A4,A5,A14
.= F/.x by A6,A7,A14;
end;
hence f*g = fg by A13 .= id dom g by A8,A12,A13;
end;
theorem Th54:
for F being Projections_family of c,I
st c is_a_product_wrt F &
for x1,x2 st x1 in I & x2 in I holds Hom(cod(F/.x1),cod(F/.x2)) <> {}
for x st x in I holds F/.x is retraction
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;
set d = cod(F/.x);
defpred P[set,set] means
($1 = x implies $2 = id d) &
($1 <> x implies $2 in Hom(d,cod(F/.$1)));
A4: for y st y in I holds ex z st z in the Morphisms of C & P[y,z]
proof let y; assume y in I;
then A5: Hom(d,cod(F/.y)) <> {} by A2,A3;
consider z being Element of Hom(d,cod(F/.y));
A6: z is Morphism of d,cod(F/.y) by A5,CAT_1:21;
per cases;
suppose
A7: y = x;
take z = id d;
thus z in the Morphisms of C;
thus (y = x implies z = id d) & (y <> x implies z in Hom(d,cod(F/.y)))
by A7;
suppose
A8: y <> x;
take z;
thus z in the Morphisms of C by A6;
thus (y = x implies z = id d) & (y <> x implies z in Hom(d,cod(F/.y)))
by A5,A8;
end;
consider F' being Function such that
A9: dom F' = I & rng F' c= the Morphisms of C and
A10: for y st y in I holds P[y,F'.y] from NonUniqBoundFuncEx(A4);
reconsider F' as Function of I,the Morphisms of C by A9,FUNCT_2:def 1,
RELSET_1:11;
now
now let y; assume
A11: y in I;
then F'.y = F'/.y & F'.x = F'/.x by A3,Def1;
then (y = x implies F'/.y = id d) &
(y <> x implies F'/.y in Hom(d,cod(F/.y))) by A10,A11;
then dom(F'/.y) = d by CAT_1:18,44;
hence (doms F')/.y = d by A11,Def3 .= (I-->d)/.y by A11,Th2;
end;
hence doms F' = I --> d by Th1;
hence F' is Projections_family of d,I by Def14;
now let y; assume
A12: y in I;
then F'.y = F'/.y & F'.x = F'/.x by A3,Def1;
then (y = x implies F'/.y = id d) &
(y <> x implies F'/.y in Hom(d,cod(F/.y))) by A10,A12;
then cod(F'/.y) = cod(F/.y) by CAT_1:18,44;
hence (cods F')/.y = cod(F/.y) by A12,Def4 .= (cods F)/.y by A12,Def4;
end;
hence cods F = cods F' by Th1;
end;
then consider i such that
A13: i in Hom(d,c) and
A14: for k st k in Hom(d,c) holds
(for y st y in I holds (F/.y)*k = F'/.y) iff i = k by A1,Def15;
take i;
thus cod i = c by A13,CAT_1:18 .= dom(F/.x) by A3,Th45;
thus (F/.x)*i = F'/.x by A3,A13,A14 .= F'.x by A3,Def1 .= id d by A3,A10;
end;
theorem Th55:
for F being Function of {},the Morphisms of C holds
a is_a_product_wrt F iff a is terminal
proof let F be Function of {},the Morphisms of C;
thus a is_a_product_wrt F implies a is terminal
proof assume
A1: a is_a_product_wrt F;
let b;
consider F' being Projections_family of b,{};
cods F = {} & cods F' = {} by PARTFUN1:57;
then 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 = F'/.x ) iff h = k by A1,Def15;
thus
Hom(b,a)<>{} by A2;
reconsider f = h as Morphism of b,a by A2,CAT_1:def 7;
take f;
let g be Morphism of b,a;
g in Hom(b,a) & for x st x in {} holds (F/.x)*g = F'/.x
by A2,CAT_1:def 7;
hence f=g by A3;
end;
assume
A4: a is terminal;
thus F is Projections_family of a,{} by Th46;
let b;
let F' be Projections_family of b,{} such that cods F = cods F';
consider h being Morphism of b,a such that
A5: for g being Morphism of b,a holds h = g by A4,CAT_1:def 15;
take h;
Hom(b,a)<>{} by A4,CAT_1:def 15;
hence h in Hom(b,a) by CAT_1:def 7;
let k;
assume k in Hom(b,a);
then k is Morphism of b,a by CAT_1:def 7;
hence (for x st x in {} holds (F/.x)*k = F'/.x ) iff h = k by A5;
end;
theorem Th56:
for F being Projections_family of a,I
st a is_a_product_wrt F & dom f = b & cod f = a & f is invertible
holds b is_a_product_wrt F*f
proof let F be Projections_family of a,I such that
A1: a is_a_product_wrt F and
A2: dom f = b & cod f = a and
A3: f is invertible;
thus F*f is Projections_family of b,I by A2,Th50;
let c;
let F' be Projections_family of c,I such that
A4: cods(F*f) = cods F';
doms F = I-->cod f by A2,Def14;
then cods F = cods F' by A4,Th20;
then consider h such that
A5: h in Hom(c,a) and
A6: for k st k in Hom(c,a) holds
(for x st x in I holds (F/.x)*k = F'/.x) iff h = k by A1,Def15;
consider g such that
A7: dom g = cod f & cod g = dom f and
A8: f*g = id cod f and
A9: g*f = id dom f by A3,CAT_1:def 12;
take gh = g*h;
A10: cod h = a & dom h = c by A5,CAT_1:18;
then dom(g*h) = c & cod(g*h) = b by A2,A7,CAT_1:42;
hence gh in Hom(c,b) by CAT_1:18;
let k; assume k in Hom(c,b);
then A11: dom k = c & cod k = b by CAT_1:18;
thus (for x st x in I holds ((F*f)/.x)*k = F'/.x) implies gh = k
proof assume
A12: for x st x in I holds ((F*f)/.x)*k = F'/.x;
now dom(f*k) = c & cod(f*k) = a by A2,A11,CAT_1:42;
hence f*k in Hom(c,a) by CAT_1:18;
let x; assume
A13: x in I;
then dom(F/.x) = a by Th45;
hence (F/.x)*(f*k) = (F/.x)*f*k by A2,A11,CAT_1:43
.= ((F*f)/.x)*k by A13,Def7
.= F'/.x by A12,A13;
end;
then g*(f*k) = g*h by A6;
hence gh = (id b)*k by A2,A7,A9,A11,CAT_1:43 .= k by A11,CAT_1:46;
end;
assume
A14: gh = k;
let x; assume
A15: x in I;
then A16: dom(F/.x) = a by Th45;
thus ((F*f)/.x)*k = ((F/.x)*f)*k by A15,Def7
.= (F/.x)*(f*(g*h)) by A2,A11,A14,A16,CAT_1:43
.= (F/.x)*((id cod f)*h) by A2,A7,A8,A10,CAT_1:43
.= (F/.x)*h by A2,A10,CAT_1:46
.= F'/.x by A5,A6,A15;
end;
theorem
a is_a_product_wrt {y} --> id a
proof set F = {y} --> id a;
dom(id a) = a by CAT_1:44;
hence F is Projections_family of a,{y} by Th47;
let b; let F' be Projections_family of b,{y} such that
A1: cods F = cods F';
take h = F'/.y;
A2: y in {y} by TARSKI:def 1;
now
thus dom h = b by A2,Th45;
thus cod h = (cods F)/.y by A1,A2,Def4
.= cod(F/.y) by A2,Def4
.= cod(id a) by A2,Th2
.= a by CAT_1:44;
end;
hence h in Hom(b,a) by CAT_1:18;
let k; assume k in Hom(b,a);
then A3: cod k = a by CAT_1:18;
thus (for x st x in {y} holds (F/.x)*k = F'/.x) implies h = k
proof assume
A4: for x st x in {y} holds (F/.x)*k = F'/.x;
thus k = (id a)*k by A3,CAT_1:46
.= (F/.y)*k by A2,Th2
.= h by A2,A4;
end;
assume
A5: h = k;
let x; assume
A6: x in {y};
hence F'/.x = k by A5,TARSKI:def 1
.= (id a)*k by A3,CAT_1:46
.= (F/.x)*k by A6,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,Th55;
let b;
deffunc f(set) = term(b,cod(F/.$1));
consider F' being Function of I, the Morphisms of C such that
A3: for x st x in I holds F'/.x = f(x) from LambdaIdx;
now let x; assume
A4: x in I;
then A5: cod(F/.x) is terminal by A2;
thus (doms F')/.x = dom(F'/.x) by A4,Def3
.= dom(term(b,cod(F/.x))) by A3,A4
.= b by A5,Th39
.= (I-->b)/.x by A4,Th2;
end;
then doms F' = I --> b by Th1;
then reconsider F' as Projections_family of b,I by Def14;
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,Def4
.= cod(term(b,cod(F/.x))) by A7,Th39
.= cod(F'/.x) by A3,A6
.= (cods F')/.x by A6,Def4;
end;
then cods F = cods F' by Th1;
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 = F'/.x) iff h = k by A1,Def15;
thus
Hom(b,a)<>{} by A8;
reconsider h as Morphism of b,a by A8,CAT_1:def 7;
take h; let g be Morphism of b,a;
now
thus g in Hom(b,a) by A8,CAT_1:def 7;
let x;
set c = cod(F/.x);
assume
A10: x in I;
then c is terminal by A2;
then consider f being Morphism of b,c such that
A11: for f' being Morphism of b,c holds f = f' by CAT_1:def 15;
dom g = b & cod g = a & dom(F/.x) = a by A8,A10,Th45,CAT_1:23;
then dom((F/.x)*g) = b & cod((F/.x)*g) = c by CAT_1:42;
then (F/.x)*g in Hom(b,c) by CAT_1:18;
then A12: (F/.x)*g is Morphism of b,c by CAT_1:def 7;
F'/.x = term(b,c) by A3,A10;
hence F'/.x = f by A11 .= (F/.x)*g by A11,A12;
end;
hence h = g by A9;
end;
hence thesis by CAT_1:def 15;
end;
definition let C,c,p1,p2;
pred c is_a_product_wrt p1,p2 means
:Def16: 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 Th59:
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 by Def16;
hence F is Projections_family of c,I by Th48;
let b; let F' be Projections_family of b,I such that
A3: cods F = cods F';
set f = F'/.x1, g = F'/.x2;
A4: x1 in I & x2 in I by TARSKI:def 2;
then (cods F)/.x1 = cod(F/.x1) & (cods F)/.x2 = cod(F/.x2) by Def4;
then cod f = cod(F/.x1) & cod g = cod(F/.x2) by A3,A4,Def4;
then cod f = cod p1 & cod g = cod p2 & dom f = b & dom g = b
by A1,A4,Th7,Th45;
then f in Hom(b,cod p1) & g in Hom(b,cod p2) by CAT_1:18;
then consider h such that
A5: h in Hom(b,c) and
A6: for k st k in Hom(b,c) holds p1*k = f & p2*k = g iff h = k by A2,Def16;
take h;
thus h in Hom(b,c) by A5;
let k such that
A7: k in Hom(b,c);
thus (for x st x in I holds (F/.x)*k = F'/.x ) implies h = k
proof assume for x st x in I holds (F/.x)*k = F'/.x;
then (F/.x1)*k = f & (F/.x2)*k = g by A4;
then p1*k = f & p2*k = g by A1,Th7;
hence h = k by A6,A7;
end;
assume
A8: h = k;
let x such that
A9: x in I;
p1*k = f & p2*k = g by A6,A7,A8;
then (F/.x1)*k = f & (F/.x2)*k = g & (x = x1 or x = x2)
by A1,A9,Th7,TARSKI:def 2;
hence thesis;
end;
assume
A10: c is_a_product_wrt F;
then x1 in I & x2 in
I & F is Projections_family of c,I by Def15,TARSKI:def 2;
then dom(F/.x1) = c & dom(F/.x2) = c by Th45;
hence dom p1 = c & dom p2 = c by A1,Th7;
let d,f,g such that
A11: f in Hom(d,cod p1) and
A12: g in Hom(d,cod p2);
dom f = d & dom g = d by A11,A12,CAT_1:18;
then reconsider F' = (x1,x2) --> (f,g) as Projections_family of d,I by Th48;
cods F = (x1,x2)-->(cod p1,cod p2) by Th11
.= (x1,x2)-->(cod f,cod p2) by A11,CAT_1:18
.= (x1,x2)-->(cod f,cod g) by A12,CAT_1:18
.= cods F' by Th11;
then consider h such that
A13: h in Hom(d,c) and
A14: for k st k in Hom(d,c) holds
(for x st x in I holds (F/.x)*k = F'/.x ) iff h = k by A10,Def15;
take h;
thus h in Hom(d,c) by A13;
let k such that
A15: k in Hom(d,c);
thus p1*k = f & p2*k = g implies h = k
proof assume
A16: 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 & F'/.x = f or F/.x = p2 & F'/.x = g by A1,Th7;
hence (F/.x)*k = F'/.x by A16;
end;
hence h = k by A14,A15;
end;
assume h = k;
then x1 in I & x2 in I & for x st x in I holds (F/.x)*k = F'/.x
by A14,A15,TARSKI:def 2;
then (F/.x1)*k = F'/.x1 & (F/.x2)*k = F'/.x2;
then (F/.x1)*k = f & (F/.x2)*k = g by A1,Th7;
hence p1*k = f & p2*k = g by A1,Th7;
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
A1: Hom(c,a) <> {} & 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 & 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;
let d such that
A3: Hom(d,a)<>{} & Hom(d,b)<>{};
consider f being Morphism of d,a, g being Morphism of d,b;
A4: cod p1 = a & cod p2 = b by A1,CAT_1:23;
then f in Hom(d,cod p1) & g in Hom(d,cod p2) by A3,CAT_1:def 7;
then A5: 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 A2;
hence
Hom(d,c) <> {};
let f be Morphism of d,a, g be Morphism of d,b;
f in Hom(d,cod p1) & g in Hom(d,cod p2) by A3,A4,CAT_1:def 7;
then consider h such that
A6: h in Hom(d,c) and
A7: for k st k in Hom(d,c) holds p1*k = f & p2*k = g iff h = k by A2;
reconsider h as Morphism of d,c by A6,CAT_1:def 7;
take h; let k be Morphism of d,c;
p1*k = p1*(k qua Morphism of C) & p2*k = p2*(k qua Morphism of C) &
k in Hom(d,c) by A1,A5,CAT_1:def 7,def 13;
hence thesis by A7;
end;
assume
A8: 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,CAT_1:23;
let d,f,g such that
A9: f in Hom(d,cod p1) and
A10: g in Hom(d,cod p2);
A11: cod p1 = a & cod p2 = b by A1,CAT_1:23;
then f is Morphism of d,a & g is Morphism of d,b &
Hom(d,a) <> {} & Hom(d,b) <> {} by A9,A10,CAT_1:def 7;
then consider h being Morphism of d,c such that
A12: for k being Morphism of d,c holds p1*k = f & p2*k = g iff h = k by A8;
reconsider h' = h as Morphism of C;
take h';
A13: Hom(d,c) <> {} by A8,A9,A10,A11;
hence h' in Hom(d,c) by CAT_1:def 7;
let k;
assume k in Hom(d,c);
then reconsider k' = k as Morphism of d,c by CAT_1:def 7;
p1*k = p1*k' & p2*k = p2*k' by A1,A13,CAT_1:def 13;
hence thesis by A12;
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,1}, F = (0,1)-->(p1,p2), F' = (0,1)-->(q1,q2);
now dom p1 = c & dom p2 = c & dom q1 = d & dom q2 = d by A1,A2,Def16;
hence F is Projections_family of c,I & F' is Projections_family of d,I
by Th48;
thus c is_a_product_wrt F & d is_a_product_wrt F' by A1,A2,Th59;
thus cods F = (0,1)-->(cod q1,cod q2) by A3,Th11 .= cods F' by Th11;
end;
hence thesis by Th53;
end;
theorem
c is_a_product_wrt p1,p2 & Hom(cod p1,cod p2) <> {} & Hom(cod p2,cod p1)
<>
{}
implies p1 is retraction & p2 is retraction
proof assume that
A1: c is_a_product_wrt p1,p2 and
A2: Hom(cod p1,cod p2) <> {} & Hom(cod p2,cod p1) <> {};
set I = {0,1}, F = (0,1)-->(p1,p2);
A3: F/.0 = p1 & F/.1 = p2 by Th7;
now dom p1 = c & dom p2 = c by A1,Def16;
hence F is Projections_family of c,I by Th48;
thus c is_a_product_wrt F by A1,Th59;
let x1,x2; assume x1 in I & x2 in I;
then (x1 = 0 or x1 = 1) & (x2 = 0 or x2 = 1) by TARSKI:def 2;
hence Hom(cod(F/.x1),cod(F/.x2)) <> {} by A2,A3,CAT_1:56;
end;
then 0 in I & 1 in I & for x st x in I holds F/.x is retraction
by Th54,TARSKI:def 2;
hence thesis by A3;
end;
theorem Th63:
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 and
A2: 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 and
A4: h in Hom(c,c) and
A5: p1*h = p1 & p2*h = p2;
p1 in Hom(c,cod p1) & p2 in Hom(c,cod p2) by A1,A2,CAT_1:18;
then consider i such that i in Hom(c,c) and
A6: for k st k in Hom(c,c) holds p1*k = p1 & p2*k = p2 iff i = k by A3;
id c in Hom(c,c) & p1*(id c) = p1 & p2*(id c) = p2 by A1,A2,CAT_1:47,55;
hence id c = i by A6 .= h by A4,A5,A6;
end;
theorem
c is_a_product_wrt p1,p2 & dom f = d & cod f = c & f is invertible
implies d is_a_product_wrt p1*f,p2*f
proof
assume that
A1: c is_a_product_wrt p1,p2 and
A2: dom f = d & cod f = c & f is invertible;
dom p1 = c & dom p2 = c by A1,Def16;
then c is_a_product_wrt (0,1)-->(p1,p2) &
(0,1)-->(p1,p2) is Projections_family of c,{0,1} by A1,Th48,Th59;
then d is_a_product_wrt ((0,1)-->(p1,p2))*f by A2,Th56;
then d is_a_product_wrt (0,1)-->(p1*f,p2*f) by Th18;
hence d is_a_product_wrt p1*f,p2*f by Th59;
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;
A3: dom p1 = c & dom p2 = c by A1,Def16;
hence Hom(c,a)<>{} by CAT_1:19;
reconsider p = p1 as Morphism of c,a by A3,CAT_1:22;
take p;
set f = id(a),g = term(a,b);
dom g = a & cod g = b by A2,Th39;
then f in Hom(a,a) & g in Hom(a,b) by CAT_1:18,55;
then consider h such that
A4: h in Hom(a,c) and
A5: for k st k in Hom(a,c) holds p1*k = f & p2*k = g iff h = k by A1,Def16;
take h;
thus dom h = cod p & cod h = dom p by A3,A4,CAT_1:18;
thus
A6: p*h = id cod p by A4,A5;
now
A7: dom h = a & cod h = c by A4,CAT_1:18;
then A8: dom(h*p) = c & cod(h*p) = c by A3,CAT_1:42;
hence h*p in Hom(c,c) by CAT_1:18;
thus p1*(h*p) = (id cod p)*p by A3,A6,A7,CAT_1:43 .= p by CAT_1:46;
dom(p2*(h*p)) = c & cod(p2*(h*p)) = b by A3,A8,CAT_1:42;
hence p2*(h*p) = term(c,b) by A2,Th40 .= p2 by A2,A3,Th40;
end;
hence id dom p = h*p by A1,A3,Th63;
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;
A3: dom p1 = c & dom p2 = c by A1,Def16;
hence Hom(c,b)<>{} by CAT_1:19;
reconsider p = p2 as Morphism of c,b by A3,CAT_1:22;
take p;
set f = id(b),g = term(b,a);
dom g = b & cod g = a by A2,Th39;
then f in Hom(b,b) & g in Hom(b,a) by CAT_1:18,55;
then consider h such that
A4: h in Hom(b,c) and
A5: for k st k in Hom(b,c) holds p1*k = g & p2*k = f iff h = k by A1,Def16;
take h;
thus dom h = cod p & cod h = dom p by A3,A4,CAT_1:18;
thus
A6: p*h = id cod p by A4,A5;
now
A7: dom h = b & cod h = c by A4,CAT_1:18;
then A8: dom(h*p) = c & cod(h*p) = c by A3,CAT_1:42;
hence h*p in Hom(c,c) by CAT_1:18;
dom(p1*(h*p)) = c & cod(p1*(h*p)) = a by A3,A8,CAT_1:42;
hence p1*(h*p) = term(c,a) by A2,Th40 .= p1 by A2,A3,Th40;
thus p2*(h*p) = (id cod p)*p by A3,A6,A7,CAT_1:43 .= p by CAT_1:46;
end;
hence id dom p = h*p by A1,A3,Th63;
end;
begin :: Coproducts
definition let C,c,I;
mode Injections_family of c,I -> Function of I,the Morphisms of C means
:Def17: cods it = I --> c;
existence
proof take F = I-->id c;
cods F = I --> (cod id c) by Th9;
hence thesis by CAT_1:44;
end;
end;
theorem Th67:
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 Def17;
hence cod(F/.x) = (I --> c)/.x by A1,Def4 .= c by A1,Th2;
end;
theorem
for F being Function of {},the Morphisms of C
holds F is Injections_family of a,{}
proof let F be Function of {},the Morphisms of C;
thus {} --> a = {} by FUNCT_4:3 .= cods F by PARTFUN1:57;
end;
theorem Th69:
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 Def4
.= a by A1,A2,Th2
.= ({y} --> a)/.x by A2,Th2;
end;
hence cods F = {y} --> a by Th1;
end;
theorem Th70:
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 Th11 .= {x1,x2} --> c by A1,FUNCT_4:68;
hence thesis by Def17;
end;
canceled;
theorem Th72:
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 Def17;
hence cods(f*F) = I --> cod f by Th21;
end;
theorem
for F being Injections_family of b,I,
G being Function of I,the Morphisms of C st doms F = cods G
holds F"*"G is Injections_family of b,I
proof let F be Injections_family of b,I;
let G be Function of I,the Morphisms of C;
assume doms F = cods G;
then cods(F"*"G) = cods F by Th22;
hence cods(F"*"G) = I --> b by Def17;
end;
theorem Th74:
for F be Function of I,the Morphisms of C holds
F is Projections_family of c,I iff F opp is Injections_family of c opp,I
proof let F be Function of I,the Morphisms 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; assume
A2: x in I;
hence (cods(F opp))/.x = cod((F opp)/.x) by Def4
.= cod((F/.x) opp) by A2,Def5
.= dom(F/.x) opp by OPPCAT_1:11
.= ((I --> c)/.x) opp by A1,A2,Def3
.= c opp by A2,Th2
.= (I --> (c opp))/.x by A2,Th2;
end;
hence cods(F opp) = I --> (c opp) by Th1;
end;
assume
A3: cods(F opp) = I --> (c opp);
now let x; assume
A4: x in I;
hence (doms F)/.x = dom(F/.x) by Def3
.= cod((F/.x) opp) by OPPCAT_1:9
.= cod((F opp)/.x) by A4,Def5
.= (I --> (c opp))/.x by A3,A4,Def4
.= c opp by A4,Th2
.= c by OPPCAT_1:def 2
.= (I --> c)/.x by A4,Th2;
end;
hence doms F = I --> c by Th1;
end;
theorem Th75:
for F be Function of I,the Morphisms of C opp, c being Object of C opp holds
F is Injections_family of c,I iff opp F is Projections_family of opp c,I
proof let F be Function of I,the Morphisms 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; assume
A2: x in I;
hence (doms opp F)/.x = dom(opp F/.x) by Def3
.= dom(opp(F/.x)) by A2,Def6
.= opp(cod(F/.x)) by OPPCAT_1:12
.= opp((I-->c)/.x) by A1,A2,Def4
.= opp c by A2,Th2
.= (I --> (opp c))/.x by A2,Th2;
end;
hence doms opp F = I --> (opp c) by Th1;
end;
assume
A3: doms opp F = I --> (opp c);
now let x; assume
A4: x in I;
hence (cods F)/.x = cod(F/.x) by Def4
.= dom(opp(F/.x)) by OPPCAT_1:10
.= dom(opp F/.x) by A4,Def6
.= (I -->(opp c))/.x by A3,A4,Def3
.= opp c by A4,Th2
.= c opp by OPPCAT_1:def 3
.= c by OPPCAT_1:def 2
.= (I --> c)/.x by A4,Th2;
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 Def4
.= (I --> dom f)/.x by Def17
.= dom f by A1,Th2;
thus ((F opp)*(f opp))/.x = ((F opp)/.x)*(f opp) by A1,Def7
.= ((F/.x)opp)*(f opp) by A1,Def5
.= (f*(F/.x))opp by A2,OPPCAT_1:17
.= ((f*F)/.x)opp by A1,Def8
.= ((f*F) opp)/.x by A1,Def5;
end;
hence thesis by Th1;
end;
definition let C,c,I; let F be Function of I,the Morphisms of C;
pred c is_a_coproduct_wrt F means
:Def18: F is Injections_family of c,I &
for d for F' being Injections_family of d,I st doms F = doms F'
ex h st h in Hom(c,d) &
for k st k in Hom(c,d) holds
(for x st x in I holds k*(F/.x) = F'/.x) iff h = k;
end;
theorem
for F being Function of I,the Morphisms of C holds
c is_a_product_wrt F iff c opp is_a_coproduct_wrt F opp
proof let F be Function of I,the Morphisms 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 by Def15;
hence F opp is Injections_family of c opp,I by Th74;
let d be Object of C opp, F' be Injections_family of d,I such that
A2: doms(F opp) = doms F';
reconsider oppF' = opp F' as Projections_family of opp d,I by Th75;
now let x; assume
A3: x in I;
hence (cods F)/.x = cod(F/.x) by Def4
.= dom((F/.x)opp) by OPPCAT_1:9
.= dom(F opp/.x) by A3,Def5
.= (doms F')/.x by A2,A3,Def3
.= dom(F'/.x) by A3,Def3
.= cod(opp(F'/.x)) by OPPCAT_1:10
.= cod(oppF'/.x) by A3,Def6
.= (cods oppF')/.x by A3,Def4;
end;
then cods F = cods oppF' by Th1;
then consider h such that
A4: h in Hom(opp d,c) and
A5: for k st k in Hom(opp d,c) holds
(for x st x in I holds (F/.x)*k = oppF'/.x ) iff h = k by A1,Def15;
take h opp;
h opp in Hom(c opp,(opp d) opp) by A4,OPPCAT_1:13;
hence h opp in Hom(c opp,d) by OPPCAT_1:5;
let k be Morphism of C opp; assume
A6: k in Hom(c opp,d);
then opp k in Hom(opp d,opp(c opp)) by OPPCAT_1:14;
then A7: opp k in Hom(opp d,c) by OPPCAT_1:4;
thus (for x st x in I holds k*(F opp/.x) = F'/.x ) implies h opp = k
proof assume
A8: for x st x in I holds k*(F opp/.x) = F'/.x;
now let x such that
A9: x in I;
F is Projections_family of c,I by A1,Def15;
then dom(F/.x) = c by A9,Th45;
then cod((F/.x)opp) = c opp by OPPCAT_1:11;
then cod(F opp/.x) = c opp by A9,Def5;
then A10: dom k = cod(F opp/.x) by A6,CAT_1:18;
opp(k*(F opp/.x)) = opp(F'/.x) by A8,A9;
hence oppF'/.x = opp(k*(F opp/.x)) by A9,Def6
.= (opp(F opp/.x))*(opp k) by A10,OPPCAT_1:19
.= (opp((F/.x)opp))*(opp k) by A9,Def5
.= (F/.x)*(opp k) by OPPCAT_1:7;
end;
then h = opp k by A5,A7;
hence h opp = k by OPPCAT_1:8;
end;
assume
A11: h opp = k;
let x such that
A12: x in I;
F is Projections_family of c,I by A1,Def15;
then dom(F/.x) = c by A12,Th45;
then A13: cod opp k = dom(F/.x) by A7,CAT_1:18;
h = opp k by A11,OPPCAT_1:7;
then (F/.x)*(opp k) = oppF'/.x by A5,A7,A12;
then ((opp k) opp)*((F/.x)opp) = (oppF'/.x)opp by A13,OPPCAT_1:17;
then k*((F/.x)opp) = (oppF'/.x)opp by OPPCAT_1:8;
hence k*(F opp/.x) = (oppF'/.x)opp by A12,Def5
.= (opp(F'/.x))opp by A12,Def6
.= F'/.x by OPPCAT_1:8;
end;
assume
A14: c opp is_a_coproduct_wrt F opp;
then F opp is Injections_family of c opp,I by Def18;
hence F is Projections_family of c,I by Th74;
let d; let F' be Projections_family of d,I such that
A15: cods F = cods F';
reconsider F'opp = F' opp as Injections_family of d opp,I by Th74;
now let x; assume
A16: x in I;
hence (doms(F opp))/.x = dom((F opp)/.x) by Def3
.= dom((F/.x) opp) by A16,Def5
.= cod(F/.x) by OPPCAT_1:9
.= (cods F')/.x by A15,A16,Def4
.= cod(F'/.x) by A16,Def4
.= dom((F'/.x)opp) by OPPCAT_1:9
.= dom((F' opp)/.x) by A16,Def5
.= (doms(F' opp))/.x by A16,Def3;
end;
then doms(F opp) = doms(F'opp) by Th1;
then consider h being Morphism of C opp such that
A17: h in Hom(c opp,d opp) and
A18: 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) = F'opp/.x) iff h = k by A14,Def18;
take opp h;
opp h in Hom(opp(d opp),opp(c opp)) by A17,OPPCAT_1:14;
then opp h in Hom(d,opp(c opp)) by OPPCAT_1:4;
hence opp h in Hom(d,c) by OPPCAT_1:4;
let k; assume
A19: k in Hom(d,c);
then A20: k opp in Hom(c opp,d opp) by OPPCAT_1:13;
thus (for x st x in I holds (F/.x)*k = F'/.x) implies opp h = k
proof assume
A21: for x st x in I holds (F/.x)*k = F'/.x;
now let x such that
A22: x in I;
F opp is Injections_family of c opp,I by A14,Def18;
then cod(F opp/.x) = c opp by A22,Th67;
then cod((F/.x)opp) = c opp by A22,Def5;
then dom(F/.x) = c opp by OPPCAT_1:9;
then dom(F/.x) = c by OPPCAT_1:def 2;
then A23: cod k = dom(F/.x) by A19,CAT_1:18;
(F/.x)*k = F'/.x by A21,A22;
then (k opp)*((F/.x)opp) = (F'/.x) opp by A23,OPPCAT_1:17;
hence F'opp/.x = (k opp)*((F/.x)opp) by A22,Def5
.= (k opp)*(F opp/.x) by A22,Def5;
end;
then h = k opp by A18,A20;
hence opp h = k by OPPCAT_1:7;
end;
assume
A24: opp h = k;
let x such that
A25: x in I;
F opp is Injections_family of c opp,I by A14,Def18;
then cod(F opp/.x) = c opp by A25,Th67;
then cod((F/.x)opp) = c opp by A25,Def5;
then dom(F/.x) = c opp by OPPCAT_1:9;
then dom(F/.x) = c by OPPCAT_1:def 2;
then A26: cod k = dom(F/.x) by A19,CAT_1:18;
h = k opp by A24,OPPCAT_1:8;
then (k opp)*(F opp/.x) = F'opp/.x by A18,A20,A25;
then (k opp)*(F opp/.x) = (F'/.x)opp by A25,Def5;
hence F'/.x = (k opp)*(F opp/.x) by OPPCAT_1:def 4
.= (k opp)*((F/.x)opp) by A25,Def5
.= ((F/.x)*k) opp by A26,OPPCAT_1:17
.= (F/.x)*k by OPPCAT_1:def 4;
end;
theorem Th78:
for F being Injections_family of c,I, F' being Injections_family of d,I
st c is_a_coproduct_wrt F & d is_a_coproduct_wrt F' & doms F = doms F'
holds c,d are_isomorphic
proof
let F be Injections_family of c,I, F' be Injections_family of d,I such that
A1: c is_a_coproduct_wrt F and
A2: d is_a_coproduct_wrt F' and
A3: doms F = doms F';
consider f such that
A4: f in Hom(c,d) and
A5: for k st k in Hom(c,d) holds
(for x st x in I holds k*(F/.x) = F'/.x ) iff f = k by A1,A3,Def18;
consider g such that
A6: g in Hom(d,c) and
A7: for k st k in Hom(d,c) holds
(for x st x in I holds k*(F'/.x) = F/.x ) iff g = k by A2,A3,Def18;
thus Hom(c,d) <> {} by A4;
reconsider f as Morphism of c,d by A4,CAT_1:def 7;
take f,g;
A8: cod f = d & dom g = d & dom f = c & cod g = c by A4,A6,CAT_1:18;
hence dom g = cod f & cod g = dom f;
doms F' = doms F';
then consider fg being Morphism of C such that fg in Hom(d,d) and
A9: for k st k in Hom(d,d) holds
(for x st x in I holds k*(F'/.x) = F'/.x) iff fg = k by A2,Def18;
A10:
now set k = id d;
thus k in Hom(d,d) by CAT_1:55;
let x;
assume x in I;
then cod(F'/.x) = d by Th67;
hence k*(F'/.x) = F'/.x by CAT_1:46;
end;
now cod(f*g) = d & dom(f*g) = d by A8,CAT_1:42;
hence f*g in Hom(d,d) by CAT_1:18;
let x; assume
A11: x in I;
then cod(F'/.x) = d by Th67;
hence f*g*(F'/.x) = f*(g*(F'/.x)) by A8,CAT_1:43
.= f*(F/.x) by A6,A7,A11
.= F'/.x by A4,A5,A11;
end;
hence f*g = fg by A9 .= id cod f by A8,A9,A10;
A12:
now set k = id c;
thus k in Hom(c,c) by CAT_1:55;
let x;
assume x in I;
then cod(F/.x) = c by Th67;
hence k*(F/.x) = F/.x by CAT_1:46;
end;
doms F = doms F;
then consider gf being Morphism of C such that gf in Hom(c,c) and
A13: 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,Def18;
now cod(g*f) = c & dom(g*f) = c by A8,CAT_1:42;
hence g*f in Hom(c,c) by CAT_1:18;
let x; assume
A14: x in I;
then cod(F/.x) = c by Th67;
hence g*f*(F/.x) = g*(f*(F/.x)) by A8,CAT_1:43
.= g*(F'/.x) by A4,A5,A14
.= F/.x by A6,A7,A14;
end;
hence g*f = gf by A13 .= id dom f by A8,A12,A13;
end;
theorem Th79:
for F being Injections_family of c,I
st c is_a_coproduct_wrt F &
for x1,x2 st x1 in I & x2 in I holds Hom(dom(F/.x1),dom(F/.x2)) <> {}
for x st x in I holds F/.x is coretraction
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;
set d = dom(F/.x);
defpred P[set,set] means
($1 = x implies $2 = id d) &
($1 <> x implies $2 in Hom(dom(F/.$1),d));
A4: for y st y in I holds ex z st z in the Morphisms of C & P[y,z]
proof let y; assume y in I;
then A5: Hom(dom(F/.y),d) <> {} by A2,A3;
consider z being Element of Hom(dom(F/.y),d);
A6: z is Morphism of dom(F/.y),d by A5,CAT_1:21;
per cases;
suppose
A7: y = x;
take z = id d;
thus z in the Morphisms of C;
thus (y = x implies z = id d) & (y <> x implies z in Hom(dom(F/.y),d))
by A7;
suppose
A8: y <> x;
take z;
thus z in the Morphisms of C by A6;
thus (y = x implies z = id d) & (y <> x implies z in Hom(dom(F/.y),d))
by A5,A8;
end;
consider F' being Function such that
A9: dom F' = I & rng F' c= the Morphisms of C and
A10: for y st y in I holds P[y,F'.y] from NonUniqBoundFuncEx(A4);
reconsider F' as Function of I,the Morphisms of C by A9,FUNCT_2:def 1,
RELSET_1:11;
now
now let y; assume
A11: y in I;
then F'.y = F'/.y & F'.x = F'/.x by A3,Def1;
then (y = x implies F'/.y = id d) &
(y <> x implies F'/.y in Hom(dom(F/.y),d)) by A10,A11;
then cod(F'/.y) = d by CAT_1:18,44;
hence (cods F')/.y = d by A11,Def4 .= (I-->d)/.y by A11,Th2;
end;
hence cods F' = I --> d by Th1;
hence F' is Injections_family of d,I by Def17;
now let y; assume
A12: y in I;
then F'.y = F'/.y & F'.x = F'/.x by A3,Def1;
then (y = x implies F'/.y = id d) &
(y <> x implies F'/.y in Hom(dom(F/.y),d)) by A10,A12;
then dom(F'/.y) = dom(F/.y) by CAT_1:18,44;
hence (doms F')/.y = dom(F/.y) by A12,Def3 .= (doms F)/.y by A12,Def3;
end;
hence doms F = doms F' by Th1;
end;
then consider i such that
A13: i in Hom(c,d) and
A14: for k st k in Hom(c,d) holds
(for y st y in I holds k*(F/.y) = F'/.y) iff i = k by A1,Def18;
take i;
thus dom i = c by A13,CAT_1:18 .= cod(F/.x) by A3,Th67;
thus i*(F/.x) = F'/.x by A3,A13,A14 .= F'.x by A3,Def1 .= id d by A3,A10;
end;
theorem Th80:
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 Injections_family of a,I such that
A1: a is_a_coproduct_wrt F and
A2: dom f = a & cod f = b and
A3: f is invertible;
thus f*F is Injections_family of b,I by A2,Th72;
let c;
let F' be Injections_family of c,I such that
A4: doms(f*F) = doms F';
cods F = I-->dom f by A2,Def17;
then doms F = doms F' by A4,Th21;
then consider h such that
A5: h in Hom(a,c) and
A6: for k st k in Hom(a,c) holds
(for x st x in I holds k*(F/.x) = F'/.x) iff h = k by A1,Def18;
consider g such that
A7: dom g = cod f & cod g = dom f and
A8: f*g = id cod f and
A9: g*f = id dom f by A3,CAT_1:def 12;
take hg = h*g;
A10: dom h = a & cod h = c by A5,CAT_1:18;
then cod(h*g) = c & dom(h*g) = b by A2,A7,CAT_1:42;
hence hg in Hom(b,c) by CAT_1:18;
let k; assume k in Hom(b,c);
then A11: cod k = c & dom k = b by CAT_1:18;
thus (for x st x in I holds k*((f*F)/.x) = F'/.x) implies hg = k
proof assume
A12: for x st x in I holds k*((f*F)/.x) = F'/.x;
now cod(k*f) = c & dom(k*f) = a by A2,A11,CAT_1:42;
hence k*f in Hom(a,c) by CAT_1:18;
let x; assume
A13: x in I;
then cod(F/.x) = a by Th67;
hence k*f*(F/.x) = k*(f*(F/.x)) by A2,A11,CAT_1:43
.= k*((f*F)/.x) by A13,Def8
.= F'/.x by A12,A13;
end;
then k*f*g = h*g by A6;
hence hg = k*(id b) by A2,A7,A8,A11,CAT_1:43 .= k by A11,CAT_1:47;
end;
assume
A14: hg = k;
let x; assume
A15: x in I;
then A16: cod(F/.x) = a by Th67;
then A17: cod(f*(F/.x)) = b by A2,CAT_1:42;
thus k*((f*F)/.x) = k*(f*(F/.x)) by A15,Def8
.= h*(g*(f*(F/.x))) by A2,A7,A10,A14,A17,CAT_1:43
.= h*((id dom f)*(F/.x)) by A2,A7,A9,A16,CAT_1:43
.= h*(F/.x) by A2,A16,CAT_1:46
.= F'/.x by A5,A6,A15;
end;
theorem Th81:
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;
consider F' being Injections_family of b,{};
doms F = {} & doms F' = {} by PARTFUN1:57;
then 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) = F'/.x ) iff h = k by A1,Def18;
thus
Hom(a,b)<>{} by A2;
reconsider f = h as Morphism of a,b by A2,CAT_1:def 7;
take f;
let g be Morphism of a,b;
g in Hom(a,b) & for x st x in {} holds g*(F/.x) = F'/.x
by A2,CAT_1:def 7;
hence f=g by A3;
end;
assume
A4: a is initial;
thus F is Injections_family of a,{};
let b;
let F' be Injections_family of b,{} such that doms F = doms F';
consider h being Morphism of a,b such that
A5: for g being Morphism of a,b holds h = g by A4,CAT_1:def 16;
take h;
Hom(a,b)<>{} by A4,CAT_1:def 16;
hence h in Hom(a,b) by CAT_1:def 7;
let k;
assume k in Hom(a,b);
then k is Morphism of a,b by CAT_1:def 7;
hence (for x st x in {} holds k*(F/.x) = F'/.x ) iff h = k by A5;
end;
theorem
a is_a_coproduct_wrt {y} --> id a
proof set F = {y} --> id a;
cod(id a) = a by CAT_1:44;
hence F is Injections_family of a,{y} by Th69;
let b; let F' be Injections_family of b,{y} such that
A1: doms F = doms F';
take h = F'/.y;
A2: y in {y} by TARSKI:def 1;
now
thus cod h = b by A2,Th67;
thus dom h = (doms F)/.y by A1,A2,Def3
.= dom(F/.y) by A2,Def3
.= dom(id a) by A2,Th2
.= a by CAT_1:44;
end;
hence h in Hom(a,b) by CAT_1:18;
let k; assume k in Hom(a,b);
then A3: dom k = a by CAT_1:18;
thus (for x st x in {y} holds k*(F/.x) = F'/.x) implies h = k
proof assume
A4: for x st x in {y} holds k*(F/.x) = F'/.x;
thus k = k*(id a) by A3,CAT_1:47
.= k*(F/.y) by A2,Th2
.= h by A2,A4;
end;
assume
A5: h = k;
let x; assume
A6: x in {y};
hence F'/.x = k by A5,TARSKI:def 1
.= k*(id a) by A3,CAT_1:47
.= k*(F/.x) by A6,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,Th81;
let b;
deffunc f(set) = init(dom(F/.$1),b);
consider F' being Function of I, the Morphisms of C such that
A3: for x st x in I holds F'/.x = f(x) from LambdaIdx;
now let x; assume
A4: x in I;
then A5: dom(F/.x) is initial by A2;
thus (cods F')/.x = cod(F'/.x) by A4,Def4
.= cod(init(dom(F/.x),b)) by A3,A4
.= b by A5,Th42
.= (I-->b)/.x by A4,Th2;
end;
then cods F' = I --> b by Th1;
then reconsider F' as Injections_family of b,I by Def17;
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,Def3
.= dom(init(dom(F/.x),b)) by A7,Th42
.= dom(F'/.x) by A3,A6
.= (doms F')/.x by A6,Def3;
end;
then doms F = doms F' by Th1;
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) = F'/.x) iff h = k by A1,Def18;
thus
Hom(a,b)<>{} by A8;
reconsider h as Morphism of a,b by A8,CAT_1:def 7;
take h; let g be Morphism of a,b;
now
thus g in Hom(a,b) by A8,CAT_1:def 7;
let x;
set c = dom(F/.x);
assume
A10: x in I;
then c is initial by A2;
then consider f being Morphism of c,b such that
A11: for f' being Morphism of c,b holds f = f' by CAT_1:def 16;
cod g = b & dom g = a & cod(F/.x) = a by A8,A10,Th67,CAT_1:23;
then cod(g*(F/.x)) = b & dom(g*(F/.x)) = c by CAT_1:42;
then g*(F/.x) in Hom(c,b) by CAT_1:18;
then A12: g*(F/.x) is Morphism of c,b by CAT_1:def 7;
F'/.x = init(c,b) by A3,A10;
hence F'/.x = f by A11 .= g*(F/.x) by A11,A12;
end;
hence h = g by A9;
end;
hence thesis by CAT_1:def 16;
end;
definition let C,c,i1,i2;
pred c is_a_coproduct_wrt i1,i2 means
:Def19:
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;
dom p1 = c opp & dom p2 = c opp by A1,OPPCAT_1:def 2;
hence
A3: cod i1 = c opp & cod i2 = c opp by OPPCAT_1:9;
let d be Object of C opp, f,g be Morphism of C opp;
assume f in Hom(dom i1,d) & g in Hom(dom i2,d);
then opp f in Hom(opp d, opp(dom i1)) & opp g in Hom(opp d,opp(dom i2))
by OPPCAT_1:14;
then opp f in Hom(opp d, cod opp i1) & opp g in Hom(opp d,cod opp i2)
by OPPCAT_1:12;
then opp f in Hom(opp d, cod p1) & opp g in Hom(opp d,cod p2)
by OPPCAT_1:7;
then consider h such that
A4: h in Hom(opp d,c) and
A5: for k st k in Hom(opp d,c)
holds p1*k = opp f & p2*k = opp g iff h = k by A2;
take h opp;
h opp in Hom(c opp,(opp d) opp) by A4,OPPCAT_1:13;
hence h opp in Hom(c opp,d) by OPPCAT_1:5;
let k be Morphism of C opp;
assume
A6: k in Hom(c opp,d);
then opp k in Hom(opp d,opp(c opp)) by OPPCAT_1:14;
then opp k in Hom(opp d,c) by OPPCAT_1:4;
then p1*(opp k) = opp f & p2*(opp k) = opp g iff h = opp k by A5;
then p1*(opp k) = f opp & p2*(opp k) = g opp iff h = k opp
by OPPCAT_1:def 5;
then p1*(opp k) = f & p2*(opp k) = g iff h = k by OPPCAT_1:def 4;
then ((opp i1)*(opp k) = f & (opp i2)*(opp k) = g iff h opp = k)
& dom k = c opp by A6,CAT_1:18,OPPCAT_1:7,def 4;
then opp(k*i1) = f & opp(k*i2) = g iff h opp = k by A3,OPPCAT_1:19;
then (k*i1)opp = f & (k*i2)opp = g iff h opp = k by OPPCAT_1:def 5;
hence k*i1 = f & k*i2 = g iff h opp = k by OPPCAT_1:def 4;
end;
assume that
A7: cod i1 = c opp & cod i2 = c opp and
A8: 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;
dom p1 = c opp & dom p2 = c opp by A7,OPPCAT_1:9;
hence
A9: dom p1 = c & dom p2 = c by OPPCAT_1:def 2;
let d,f,g;
assume f in Hom(d,cod p1) & g in Hom(d,cod p2);
then f opp in Hom((cod p1) opp,d opp) & g opp in Hom((cod p2)opp,d opp)
by OPPCAT_1:13;
then f opp in Hom(dom (p1 opp),d opp) & g opp in Hom(dom (p2 opp),d opp)
by OPPCAT_1:11;
then consider h being Morphism of C opp such that
A10: h in Hom(c opp,d opp) and
A11: 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 A8;
take opp h;
h = (opp h) opp by OPPCAT_1:8;
hence opp h in Hom(d,c) by A10,OPPCAT_1:13;
let k;
assume
A12: k in Hom(d,c);
then k opp in Hom(c opp,d opp) by OPPCAT_1:13;
then (k opp)*i1 = f opp & (k opp)*i2 = g opp iff h = k opp by A11;
then ((k opp)*i1 = f & (k opp)*i2 = g iff h opp = k opp) & cod k = c
by A12,CAT_1:18,OPPCAT_1:def 4;
then (p1*k) opp = f & (p2*k) opp = g iff h opp = k
by A9,OPPCAT_1:17,def 4;
hence thesis by OPPCAT_1:def 4,def 5;
end;
theorem Th85:
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 by Def19;
hence F is Injections_family of c,I by Th70;
let b; let F' be Injections_family of b,I such that
A3: doms F = doms F';
set f = F'/.x1, g = F'/.x2;
A4: x1 in I & x2 in I by TARSKI:def 2;
then (doms F)/.x1 = dom(F/.x1) & (doms F)/.x2 = dom(F/.x2) by Def3;
then dom f = dom(F/.x1) & dom g = dom(F/.x2) by A3,A4,Def3;
then dom f = dom i1 & dom g = dom i2 & cod f = b & cod g = b
by A1,A4,Th7,Th67;
then f in Hom(dom i1,b) & g in Hom(dom i2,b) by CAT_1:18;
then consider h such that
A5: h in Hom(c,b) and
A6: for k st k in Hom(c,b) holds k*i1 = f & k*i2 = g iff h = k by A2,Def19;
take h;
thus h in Hom(c,b) by A5;
let k such that
A7: k in Hom(c,b);
thus (for x st x in I holds k*(F/.x) = F'/.x ) implies h = k
proof assume for x st x in I holds k*(F/.x) = F'/.x;
then k*(F/.x1) = f & k*(F/.x2) = g by A4;
then k*i1 = f & k*i2 = g by A1,Th7;
hence h = k by A6,A7;
end;
assume
A8: h = k;
let x such that
A9: x in I;
k*i1 = f & k*i2 = g by A6,A7,A8;
then k*(F/.x1) = f & k*(F/.x2) = g & (x = x1 or x = x2)
by A1,A9,Th7,TARSKI:def 2;
hence thesis;
end;
assume
A10: c is_a_coproduct_wrt F;
then x1 in I & x2 in I & F is Injections_family of c,I by Def18,TARSKI:def 2
;
then cod(F/.x1) = c & cod(F/.x2) = c by Th67;
hence cod i1 = c & cod i2 = c by A1,Th7;
let d,f,g such that
A11: f in Hom(dom i1,d) and
A12: g in Hom(dom i2,d);
cod f = d & cod g = d by A11,A12,CAT_1:18;
then reconsider F' = (x1,x2) --> (f,g) as Injections_family of d,I by Th70;
doms F = (x1,x2)-->(dom i1,dom i2) by Th10
.= (x1,x2)-->(dom f,dom i2) by A11,CAT_1:18
.= (x1,x2)-->(dom f,dom g) by A12,CAT_1:18
.= doms F' by Th10;
then consider h such that
A13: h in Hom(c,d) and
A14: for k st k in Hom(c,d) holds
(for x st x in I holds k*(F/.x) = F'/.x ) iff h = k by A10,Def18;
take h;
thus h in Hom(c,d) by A13;
let k such that
A15: k in Hom(c,d);
thus k*i1 = f & k*i2 = g implies h = k
proof assume
A16: 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 & F'/.x = f or F/.x = i2 & F'/.x = g by A1,Th7;
hence k*(F/.x) = F'/.x by A16;
end;
hence h = k by A14,A15;
end;
assume h = k;
then x1 in I & x2 in I & for x st x in I holds k*(F/.x) = F'/.x
by A14,A15,TARSKI:def 2;
then k*(F/.x1) = F'/.x1 & k*(F/.x2) = F'/.x2;
then k*(F/.x1) = f & k*(F/.x2) = g by A1,Th7;
hence k*i1 = f & k*i2 = g by A1,Th7;
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,1}, F = (0,1)-->(i1,i2), F' = (0,1)-->(j1,j2);
now cod i1 = c & cod i2 = c & cod j1 = d & cod j2 = d by A1,A2,Def19;
hence F is Injections_family of c,I & F' is Injections_family of d,I
by Th70;
thus c is_a_coproduct_wrt F & d is_a_coproduct_wrt F' by A1,A2,Th85;
thus doms F = (0,1)-->(dom j1,dom j2) by A3,Th10 .= doms F' by Th10;
end;
hence thesis by Th78;
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
A1: Hom(a,c) <> {} & 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 & 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;
let d such that
A3: Hom(a,d)<>{} & Hom(b,d)<>{};
consider f being Morphism of a,d, g being Morphism of b,d;
A4: dom i1 = a & dom i2 = b by A1,CAT_1:23;
then f in Hom(dom i1,d) & g in Hom(dom i2,d) by A3,CAT_1:def 7;
then A5: 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 A2;
hence
Hom(c,d) <> {};
let f be Morphism of a,d, g be Morphism of b,d;
f in Hom(dom i1,d) & g in Hom(dom i2,d) by A3,A4,CAT_1:def 7;
then consider h such that
A6: h in Hom(c,d) and
A7: for k st k in Hom(c,d) holds k*i1 = f & k*i2 = g iff h = k by A2;
reconsider h as Morphism of c,d by A6,CAT_1:def 7;
take h;
let k be Morphism of c,d;
k*i1 = k*(i1 qua Morphism of C) & k*i2 = k*(i2 qua Morphism of C) &
k in Hom(c,d) by A1,A5,CAT_1:def 7,def 13;
hence thesis by A7;
end;
assume
A8: 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,CAT_1:23;
let d,f,g such that
A9: f in Hom(dom i1,d) and
A10: g in Hom(dom i2,d);
A11: dom i1 = a & dom i2 = b by A1,CAT_1:23;
then f is Morphism of a,d & g is Morphism of b,d &
Hom(a,d) <> {} & Hom(b,d) <> {} by A9,A10,CAT_1:def 7;
then consider h being Morphism of c,d such that
A12: for k being Morphism of c,d holds k*i1 = f & k*i2 = g iff h = k by A8;
reconsider h' = h as Morphism of C;
take h';
A13: Hom(c,d) <> {} by A8,A9,A10,A11;
hence h' in Hom(c,d) by CAT_1:def 7;
let k;
assume k in Hom(c,d);
then reconsider k' = k as Morphism of c,d by CAT_1:def 7;
k*i1 = k'*i1 & k*i2 = k'*i2 by A1,A13,CAT_1:def 13;
hence thesis by A12;
end;
theorem
c is_a_coproduct_wrt i1,i2 &
Hom(dom i1,dom i2) <> {} & Hom(dom i2,dom i1) <> {}
implies i1 is coretraction & i2 is coretraction
proof assume that
A1: c is_a_coproduct_wrt i1,i2 and
A2: Hom(dom i1,dom i2) <> {} & Hom(dom i2,dom i1) <> {};
set I = {0,1}, F = (0,1)-->(i1,i2);
A3: F/.0 = i1 & F/.1 = i2 by Th7;
now cod i1 = c & cod i2 = c by A1,Def19;
hence F is Injections_family of c,I by Th70;
thus c is_a_coproduct_wrt F by A1,Th85;
let x1,x2; assume x1 in I & x2 in I;
then (x1 = 0 or x1 = 1) & (x2 = 0 or x2 = 1) by TARSKI:def 2;
hence Hom(dom(F/.x1),dom(F/.x2)) <> {} by A2,A3,CAT_1:56;
end;
then 0 in I & 1 in I & for x st x in I holds F/.x is coretraction
by Th79,TARSKI:def 2;
hence thesis by A3;
end;
theorem Th89:
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 and
A2: 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 and
A4: h in Hom(c,c) and
A5: h*i1 = i1 & h*i2 = i2;
i1 in Hom(dom i1,c) & i2 in Hom(dom i2,c) by A1,A2,CAT_1:18;
then consider i such that i in Hom(c,c) and
A6: for k st k in Hom(c,c) holds k*i1 = i1 & k*i2 = i2 iff i = k by A3;
id c in Hom(c,c) & (id c)*i1 = i1 & (id c)*i2 = i2 by A1,A2,CAT_1:46,55;
hence id c = i by A6 .= h by A4,A5,A6;
end;
theorem
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
assume that
A1: c is_a_coproduct_wrt i1,i2 and
A2: dom f = c & cod f = d & f is invertible;
cod i1 = c & cod i2 = c by A1,Def19;
then c is_a_coproduct_wrt (0,1)-->(i1,i2) &
(0,1)-->(i1,i2) is Injections_family of c,{0,1} by A1,Th70,Th85;
then d is_a_coproduct_wrt f*((0,1)-->(i1,i2)) by A2,Th80;
then d is_a_coproduct_wrt (0,1)-->(f*i1,f*i2) by Th19;
hence d is_a_coproduct_wrt f*i1,f*i2 by Th85;
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;
A3: cod i1 = c & cod i2 = c by A1,Def19;
hence Hom(a,c)<>{} by CAT_1:19;
reconsider i = i1 as Morphism of a,c by A3,CAT_1:22;
take i;
set f = id(a),g = init(b,a);
cod g = a & dom g = b by A2,Th42;
then f in Hom(a,a) & g in Hom(b,a) by CAT_1:18,55;
then consider h such that
A4: h in Hom(c,a) and
A5: for k st k in Hom(c,a) holds k*i1 = f & k*i2 = g iff h = k by A1,Def19;
take h;
thus dom h = cod i & cod h = dom i by A3,A4,CAT_1:18;
now
A6: cod h = a & dom h = c by A4,CAT_1:18;
then A7: cod(i*h) = c & dom(i*h) = c by A3,CAT_1:42;
hence i*h in Hom(c,c) by CAT_1:18;
thus i*h*i1 = i*(h*i1) by A3,A6,CAT_1:43
.= i*(id dom i) by A4,A5
.= i by CAT_1:47;
cod(i*h*i2) = c & dom(i*h*i2) = b by A3,A7,CAT_1:42;
hence i*h*i2 = init(b,c) by A2,Th43 .= i2 by A2,A3,Th43;
end;
hence i*h = id cod i by A1,A3,Th89;
thus id dom i = h*i by A4,A5;
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;
A3: cod i1 = c & cod i2 = c by A1,Def19;
hence Hom(b,c)<>{} by CAT_1:19;
reconsider i = i2 as Morphism of b,c by A3,CAT_1:22;
take i;
set f = id(b),g = init(a,b);
cod g = b & dom g = a by A2,Th42;
then f in Hom(b,b) & g in Hom(a,b) by CAT_1:18,55;
then consider h such that
A4: h in Hom(c,b) and
A5: for k st k in Hom(c,b) holds k*i1 = g & k*i2 = f iff h = k by A1,Def19;
take h;
thus dom h = cod i & cod h = dom i by A3,A4,CAT_1:18;
now
A6: cod h = b & dom h = c by A4,CAT_1:18;
then A7: cod(i*h) = c & dom(i*h) = c by A3,CAT_1:42;
hence i*h in Hom(c,c) by CAT_1:18;
cod(i*h*i1) = c & dom(i*h*i1) = a by A3,A7,CAT_1:42;
hence i*h*i1 = init(a,c) by A2,Th43 .= i1 by A2,A3,Th43;
thus i*h*i2 = i*(h*i2) by A3,A6,CAT_1:43
.= i*(id dom i) by A4,A5
.= i by CAT_1:47;
end;
hence i*h = id cod i by A1,A3,Th89;
thus id dom i = h*i by A4,A5;
end;