:: Coproducts in Categories without Uniqueness of { \bf cod } and { \bf
:: dom}
:: by Maciej Goli\'nski and Artur Korni{\l}owicz
::
:: Received December 8, 2013
:: Copyright (c) 2013-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 ALTCAT_1, CAT_1, RELAT_1, ALTCAT_3, CAT_3, FUNCT_1, PBOOLE,
ALTCAT_5, FUNCOP_1, CARD_1, FUNCT_2, XBOOLE_0, SUBSET_1, STRUCT_0,
PARTFUN1, CARD_3, MSUALG_6, MSAFREE, TARSKI, MCART_1, ALTCAT_6;
notations TARSKI, XBOOLE_0, XTUPLE_0, ORDINAL1, SUBSET_1, RELAT_1, FUNCT_1,
RELSET_1, PARTFUN1, FUNCT_2, PBOOLE, CARD_3, FUNCOP_1, STRUCT_0,
ALTCAT_1, ALTCAT_3, ALTCAT_5, MSAFREE;
constructors ALTCAT_3, RELSET_1, ALTCAT_5, MSAFREE;
registrations XBOOLE_0, RELSET_1, FUNCOP_1, STRUCT_0, ALTCAT_1, FUNCT_2,
FUNCT_1, RELAT_1, ALTCAT_5, MSAFREE, XTUPLE_0;
requirements SUBSET, BOOLE;
definitions TARSKI, RELAT_1, FUNCT_1, FUNCOP_1, PBOOLE, FUNCT_2, ALTCAT_3;
equalities TARSKI, ORDINAL1, CARD_3;
expansions PARTFUN1;
theorems FUNCT_2, FUNCOP_1, TARSKI, ALTCAT_1, FUNCT_5, FUNCT_1, ALTCAT_3,
PARTFUN1, MSAFREE, XTUPLE_0, XBOOLE_0, SCMYCIEL, CARD_3, SUBSET_1;
schemes PBOOLE, FUNCT_2, CLASSES1;
begin
reserve
I for set,
E for non empty set;
set C = EnsCat {{}};
Lm1: the carrier of C = {0} by ALTCAT_1:def 14;
Lm2: Funcs({},{}) = {{}} by FUNCT_5:57;
Lm3:
now
let o1,o be Object of C;
A1: o1 = {} & o = {} by Lm1,TARSKI:def 1;
<^o1,o^> = Funcs(o1,o) by ALTCAT_1:def 14;
hence {} is Morphism of o1,o & {} in <^o1,o^> by A1,Lm1,Lm2;
end;
Lm4:
now
let o1, o be Object of C;
let m1 be Morphism of o1,o;
A1: o = {} & o1 = {} by Lm1,TARSKI:def 1;
<^o1,o^> = Funcs(o1,o) by ALTCAT_1:def 14;
hence m1 = {} by A1,Lm2,TARSKI:def 1;
end;
Lm5:
now
let o1,o be Object of C;
o = {} & o1 = {} by Lm1,TARSKI:def 1;
hence o1 = o;
end;
Lm6:
now
let o1,o be Object of C;
let m1,m be Morphism of o1,o;
thus m1 = {} by Lm4
.= m by Lm4;
end;
registration
let I be non empty set;
let A be ManySortedSet of I;
let i be Element of I;
cluster coprod(i,A) -> Relation-like Function-like;
coherence
proof
set f = coprod(i,A);
thus f is Relation-like
proof
let x be object;
assume x in f;
then ex a being set st a in A.i & x = [a,i] by MSAFREE:def 2;
hence thesis;
end;
let x,y1,y2 be object;
assume [x,y1] in f;
then
A1: ex a being set st a in A.i & [x,y1] = [a,i] by MSAFREE:def 2;
assume [x,y2] in f;
then ex b being set st b in A.i & [x,y2] = [b,i] by MSAFREE:def 2;
then y1 = i & y2 = i by A1,XTUPLE_0:1;
hence thesis;
end;
end;
definition
let C be non empty AltCatStr;
let o be Object of C;
let I be set;
let f be ObjectsFamily of I,C;
mode MorphismsFamily of f,o -> ManySortedSet of I means
:Def1:
for i being object st i in I
ex o1 being Object of C st o1 = f.i & it.i is Morphism of o1,o;
existence
proof
defpred P[object,object] means ex o1 being Object of C st o1 = f.$1 &
$2 is Morphism of o1,o;
A1: for i being object st i in I ex j being object st P[i,j]
proof
let i be object;
assume i in I;
then reconsider o1 = f.i as Object of C by FUNCT_2:5;
take the Morphism of o1,o;
thus thesis;
end;
ex f being ManySortedSet of I st
for i being object st i in I holds P[i,f.i] from PBOOLE:sch 3(A1);
hence thesis;
end;
end;
definition
let C be non empty AltCatStr;
let o be Object of C;
let I be non empty set;
let f be ObjectsFamily of I,C;
redefine mode MorphismsFamily of f,o means :: redefines MorphismsFamily (ALTCAT_6, definition)
:Def2:
for i being Element of I holds it.i is Morphism of f.i,o;
compatibility
proof
let F be ManySortedSet of I;
hereby
assume
A1: F is MorphismsFamily of f,o;
let i be Element of I;
ex o1 being Object of C st o1 = f.i & F.i is Morphism of o1,o
by A1,Def1;
hence F.i is Morphism of f.i,o;
end;
assume
A2: for i being Element of I holds F.i is Morphism of f.i,o;
let i be object;
assume i in I;
then reconsider j = i as Element of I;
take f.j;
thus thesis by A2;
end;
end;
definition
let C be non empty AltCatStr;
let o be Object of C;
let I be non empty set;
let f be ObjectsFamily of I,C;
let M be MorphismsFamily of f,o;
let i be Element of I;
redefine func M.i -> Morphism of f.i,o; :: redefines . (FUNCT_1, definition)
coherence by Def2;
end;
registration
let C be functional non empty AltCatStr;
let o be Object of C;
let I be set;
let f be ObjectsFamily of I,C;
cluster -> Function-yielding for MorphismsFamily of f,o;
coherence
proof
let F be MorphismsFamily of f,o;
let i be object;
assume i in dom F;
then ex o1 being Object of C st
o1 = f.i & F.i is Morphism of o1,o by Def1;
hence thesis;
end;
end;
theorem Th1:
for C being non empty AltCatStr, o being Object of C
for f being ObjectsFamily of {},C holds
{} is MorphismsFamily of f,o
proof
let C be non empty AltCatStr, o be Object of C, f be ObjectsFamily of {},C;
reconsider A = {} as {}-defined Relation;
A is total;
then reconsider A = {} as ManySortedSet of {};
A is MorphismsFamily of f,o
proof
let i be object;
thus thesis;
end;
hence thesis;
end;
definition
let C be non empty AltCatStr;
let I be set;
let A be ObjectsFamily of I,C;
let B be Object of C;
let P be MorphismsFamily of A,B;
attr P is feasible means
for i being set st i in I ex o being Object of C st o = A.i & P.i in <^o,B^>;
end;
definition
let C be non empty AltCatStr;
let I be non empty set;
let A be ObjectsFamily of I,C;
let B be Object of C;
let P be MorphismsFamily of A,B;
redefine attr P is feasible means :Def4: :: redefines feasible (ALTCAT_6, definition)
for i being Element of I holds P.i in <^A.i,B^>;
compatibility
proof
thus P is feasible implies
for i being Element of I holds P.i in <^A.i,B^>
proof
assume
A1: P is feasible;
let i be Element of I;
ex o being Object of C st o = A.i & P.i in <^o,B^> by A1;
hence thesis;
end;
assume
A2: for i being Element of I holds P.i in <^A.i,B^>;
let i be set;
assume i in I;
then reconsider i as Element of I;
reconsider A as ObjectsFamily of I,C;
take A.i;
thus thesis by A2;
end;
end;
definition
let C be category;
let I be set;
let A be ObjectsFamily of I,C;
let B be Object of C; :: coproduct Object
let P be MorphismsFamily of A,B; :: coproductfamily
attr P is coprojection-morphisms means
for X being Object of C, F being MorphismsFamily of A,X
st F is feasible
ex f being Morphism of B,X st f in <^B,X^> &
::existence
(for i being set st i in I
ex si being Object of C, Pi being Morphism of si,B st
si = A.i & Pi = P.i & F.i = f * Pi) &
::uniqueness
for f1 being Morphism of B,X st for i being set st i in I
ex si being Object of C, Pi being Morphism of si,B st
si = A.i & Pi = P.i & F.i = f1 * Pi
holds f = f1;
end;
definition
let C be category;
let I be non empty set;
let A be ObjectsFamily of I,C;
let B be Object of C;
let P be MorphismsFamily of A,B;
redefine attr P is coprojection-morphisms means :: redefines coprojection-morphisms (ALTCAT_6, definition)
for X being Object of C, F being MorphismsFamily of A,X st F is feasible
ex f being Morphism of B,X st f in <^B,X^> &
::existence
(for i being Element of I holds F.i = f * P.i) &
::uniqueness
for f1 being Morphism of B,X st
for i being Element of I holds F.i = f1 * P.i
holds f = f1;
correctness
proof
thus P is coprojection-morphisms implies
for Y being Object of C, F being MorphismsFamily of A,Y st F is feasible
ex f being Morphism of B,Y st f in <^B,Y^> &
(for i being Element of I holds F.i = f * P.i) &
for f1 being Morphism of B,Y st
for i being Element of I holds F.i = f1 * P.i
holds f = f1
proof
assume
A1: P is coprojection-morphisms;
let Y be Object of C, F be MorphismsFamily of A,Y;
assume
A2: F is feasible;
consider f being Morphism of B,Y such that
A3: f in <^B,Y^> and
A4: for i being set st i in I
ex si being Object of C, Pi being Morphism of si,B st
si = A.i & Pi = P.i & F.i = f * Pi and
A5: for f1 being Morphism of B,Y st for i being set st i in I
ex si being Object of C, Pi being Morphism of si,B st
si = A.i & Pi = P.i & F.i = f1 * Pi
holds f = f1 by A2,A1;
take f;
thus f in <^B,Y^> by A3;
hereby
let i be Element of I;
ex si being Object of C, Pi being Morphism of si,B st
si = A.i & Pi = P.i & F.i = f * Pi by A4;
hence F.i = f * P.i;
end;
let f1 be Morphism of B,Y such that
A6: for i being Element of I holds F.i = f1 * P.i;
for i being set st i in I
ex si being Object of C, Pi being Morphism of si,B st
si = A.i & Pi = P.i & F.i = f1 * Pi
proof
let i be set;
assume i in I;
then reconsider i as Element of I;
reconsider si = A.i as Object of C;
reconsider Pi = P.i as Morphism of si,B;
take si, Pi;
thus thesis by A6;
end;
hence thesis by A5;
end;
assume
A7: for Y being Object of C, F being MorphismsFamily of A,Y st F is feasible
ex f being Morphism of B,Y st f in <^B,Y^> &
(for i being Element of I holds F.i = f * P.i) &
for f1 being Morphism of B,Y st
for i being Element of I holds F.i = f1 * P.i
holds f = f1;
let Y be Object of C, F be MorphismsFamily of A,Y;
assume F is feasible;
then consider f be Morphism of B,Y such that
A8: f in <^B,Y^> and
A9: for i being Element of I holds F.i = f * P.i and
A10: for f1 being Morphism of B,Y st
for i being Element of I holds F.i = f1 * P.i
holds f = f1 by A7;
take f;
thus f in <^B,Y^> by A8;
thus for i being set st i in I
ex si being Object of C, Pi being Morphism of si,B st
si = A.i & Pi = P.i & F.i = f * Pi
proof
let i be set;
assume i in I;
then reconsider j = i as Element of I;
take A.j, P.j;
thus thesis by A9;
end;
let f1 be Morphism of B,Y such that
A11: for i being set st i in I
ex si being Object of C, Pi being Morphism of si,B st
si = A.i & Pi = P.i & F.i = f1 * Pi;
now
let i be Element of I;
ex si being Object of C, Pi being Morphism of si,B st
si = A.i & Pi = P.i & F.i = f1 * Pi by A11;
hence F.i = f1 * P.i;
end;
hence thesis by A10;
end;
end;
registration
let C be category, A be ObjectsFamily of {},C;
let B be Object of C;
cluster -> feasible for MorphismsFamily of A,B;
coherence;
end;
theorem Th2:
for C being category, A being ObjectsFamily of {},C
for B being Object of C st B is initial holds
ex P being MorphismsFamily of A,B st P is empty coprojection-morphisms
proof
let C be category;
let A be ObjectsFamily of {},C;
let B be Object of C;
assume
A1: B is initial;
reconsider P = {} as MorphismsFamily of A,B by Th1;
take P;
thus P is empty;
let X be Object of C, F be MorphismsFamily of A,X;
assume F is feasible;
consider f being Morphism of B,X such that
A2: f in <^B,X^> &
for M1 being Morphism of B,X st M1 in <^B,X^> holds f = M1
by A1,ALTCAT_3:25;
take f;
thus thesis by A2;
end;
theorem Th3:
for A being ObjectsFamily of I,EnsCat {{}}, o being Object of EnsCat {{}}
holds I --> {} is MorphismsFamily of A,o
proof
let A be ObjectsFamily of I,C;
let o be Object of C;
let i be object such that
A1: i in I;
reconsider I as non empty set by A1;
reconsider j = i as Element of I by A1;
reconsider A1 = A as ObjectsFamily of I,C;
reconsider o1 = A1.j as Object of C;
take o1;
thus o1 = A.i;
thus thesis by Lm3;
end;
theorem Th4:
for A being ObjectsFamily of I,EnsCat {{}},
o being Object of EnsCat {{}},
P being MorphismsFamily of A,o st P = I --> {} holds
P is feasible coprojection-morphisms
proof
let A be ObjectsFamily of I,EnsCat {{}};
let o be Object of EnsCat {{}};
let P be MorphismsFamily of A,o;
assume
A1: P = I --> {};
thus P is feasible
proof
let i be set;
assume
A2: i in I;
then reconsider I as non empty set;
reconsider i as Element of I by A2;
reconsider A as ObjectsFamily of I,C;
P.i = {} by A1;
then P.i in <^A.i,o^> by Lm3;
hence thesis;
end;
let Y be Object of C, F being MorphismsFamily of A,Y;
assume F is feasible;
reconsider f = {} as Morphism of o,Y by Lm3;
take f;
thus f in <^o,Y^> by Lm3;
thus for i being set st i in I
ex si being Object of C, Pi being Morphism of si,o st
si = A.i & Pi = P.i & F.i = f * Pi
proof
let i be set;
assume
A3: i in I;
then reconsider I as non empty set;
reconsider j = i as Element of I by A3;
reconsider M = {} as Morphism of o,o by Lm3;
reconsider A1 = A as ObjectsFamily of I,C;
reconsider F1 = F as MorphismsFamily of A1,Y;
take o, M;
A1.j = {} by Lm1,TARSKI:def 1;
hence o = A.i by Lm5;
thus M = P.i by A1;
F1.j is Morphism of o,Y & f*M is Morphism of o,Y by Lm5;
hence thesis by Lm6;
end;
thus thesis by Lm4;
end;
definition
let C be category;
attr C is with_coproducts means
:Def7:
for I being set, A being ObjectsFamily of I,C
ex B being Object of C, P being MorphismsFamily of A,B st
P is feasible coprojection-morphisms;
end;
registration
cluster EnsCat {{}} -> with_coproducts;
coherence
proof
let I be set, A be ObjectsFamily of I,C;
reconsider o = {} as Object of C by Lm1,TARSKI:def 1;
reconsider P = I --> {} as MorphismsFamily of A,o by Th3;
take o,P;
thus thesis by Th4;
end;
end;
registration
cluster with_products with_coproducts strict for category;
existence
proof
take EnsCat {{}};
thus thesis;
end;
end;
definition
let C be category;
let I be set, A be ObjectsFamily of I,C;
let B be Object of C;
attr B is A-CatCoproduct-like means
ex P being MorphismsFamily of A,B st P is feasible coprojection-morphisms;
end;
registration
let C be with_coproducts category;
let I be set, A be ObjectsFamily of I,C;
cluster A-CatCoproduct-like for Object of C;
existence
proof
consider B being Object of C, P being MorphismsFamily of A,B such that
A1: P is feasible coprojection-morphisms by Def7;
take B,P;
thus thesis by A1;
end;
end;
registration
let C be category;
let A be ObjectsFamily of {},C;
cluster A-CatCoproduct-like -> initial for Object of C;
coherence
proof
let B be Object of C such that
A1: B is A-CatCoproduct-like;
for X being Object of C
ex M being Morphism of B,X st M in <^B,X^> &
for M1 being Morphism of B,X st M1 in <^B,X^> holds M = M1
proof
let X be Object of C;
consider P being MorphismsFamily of A,B such that
A2: P is feasible coprojection-morphisms by A1;
set F = the MorphismsFamily of A,X;
consider f being Morphism of B,X such that
A3: f in <^B,X^> and
for i being set st i in {}
ex si being Object of C, Pi being Morphism of si,B st
si = A.i & Pi = P.i & F.i = f * Pi and
A4: for f1 being Morphism of B,X st for i being set st i in {}
ex si being Object of C, Pi being Morphism of si,B st
si = A.i & Pi = P.i & F.i = f1*Pi
holds f = f1 by A2;
take f;
thus f in <^B,X^> by A3;
let M be Morphism of B,X;
for i being set st i in {}
ex si being Object of C, Pi being Morphism of si,B st
si = A.i & Pi = P.i & F.i = M*Pi;
hence thesis by A4;
end;
hence thesis by ALTCAT_3:25;
end;
end;
theorem
for C being category, A being ObjectsFamily of {},C
for B being Object of C st B is initial holds
B is A-CatCoproduct-like
proof
let C be category;
let A be ObjectsFamily of {},C;
let B be Object of C;
assume B is initial;
then ex P being MorphismsFamily of A,B st
P is empty coprojection-morphisms by Th2;
hence thesis;
end;
theorem
for C being category, A being ObjectsFamily of I,C,
C1,C2 being Object of C
st C1 is A-CatCoproduct-like & C2 is A-CatCoproduct-like
holds C1,C2 are_iso
proof
let C be category;
let A be ObjectsFamily of I,C;
let C1,C2 be Object of C;
assume that
A1: C1 is A-CatCoproduct-like and
A2: C2 is A-CatCoproduct-like;
per cases;
suppose I is empty;
hence thesis by A1,A2,ALTCAT_3:26;
end;
suppose I is non empty;
then reconsider I as non empty set;
reconsider A as ObjectsFamily of I,C;
consider P1 being MorphismsFamily of A,C1 such that
A3: P1 is feasible and
A4: P1 is coprojection-morphisms by A1;
consider P2 being MorphismsFamily of A,C2 such that
A5: P2 is feasible and
A6: P2 is coprojection-morphisms by A2;
consider f1 being Morphism of C1,C2 such that
A7: f1 in <^C1,C2^> and
A8: for i being Element of I holds P2.i = f1*P1.i and
for fa being Morphism of C1,C2 st
for i being Element of I holds P2.i = fa*P1.i
holds f1 = fa by A4,A5;
consider g1 being Morphism of C1,C1 such that
g1 in <^C1,C1^> and
for i being Element of I holds P1.i =g1* P1.i and
A9: for fa being Morphism of C1,C1 st
for i being Element of I holds P1.i = fa*P1.i
holds g1 = fa by A3,A4;
consider f2 being Morphism of C2,C1 such that
A10: f2 in <^C2,C1^> and
A11: for i being Element of I holds P1.i =f2* P2.i and
for fa being Morphism of C2,C1 st
for i being Element of I holds P1.i =fa* P2.i
holds f2 = fa by A3,A6;
consider g2 being Morphism of C2,C2 such that
g2 in <^C2,C2^> and
for i being Element of I holds P2.i =g2* P2.i and
A12: for fa being Morphism of C2,C2 st
for i being Element of I holds P2.i = fa*P2.i
holds fa = g2 by A5,A6;
thus <^C1,C2^> <> {} & <^C2,C1^> <> {} by A7,A10;
take f1;
A13: f1 is retraction
proof
take f2;
now
let i be Element of I;
P2.i in <^A.i,C2^> by A5;
hence P2.i =idm C2 * P2.i by ALTCAT_1:20;
end;
then
A14: g2 = idm C2 by A12;
now
let i be Element of I;
P2.i in <^A.i,C2^> by A5;
hence (f1 * f2)*P2.i = f1 * (f2 *P2.i) by A7,A10,ALTCAT_1:21
.= f1 * P1.i by A11
.= P2.i by A8;
end;
hence f1*f2 = idm C2 by A14,A12;
end;
f1 is coretraction
proof
take f2;
now
let i be Element of I;
P1.i in <^A.i,C1^> by A3;
hence P1.i = idm C1 *P1.i by ALTCAT_1:20;
end;
then
A15: g1 = idm C1 by A9;
now
let i be Element of I;
P1.i in <^A.i,C1^> by A3;
hence (f2 * f1) *P1.i = f2 * (f1 *P1.i) by A7,A10,ALTCAT_1:21
.= f2 * P2.i by A8
.= P1.i by A11;
end;
hence f2 * f1 = idm C1 by A15,A9;
end;
hence thesis by A7,A10,A13,ALTCAT_3:6;
end;
end;
reserve A for ObjectsFamily of I,EnsCat E;
definition
let I,E,A;
assume
A1: Union coprod A in E;
func EnsCatCoproductObj A -> Object of EnsCat E equals :Def9:
Union coprod A;
coherence by A1,ALTCAT_1:def 14;
end;
definition
let I,E,A;
func Coprod(A) -> ManySortedSet of I means
:Def10:
for i being object st i in I
ex F being Function of A.i,Union coprod A st
it.i = F & for x being object st x in A.i holds F.x = [x,i];
existence
proof
defpred P[object,object] means
ex F being Function of A.$1,Union coprod A st
$2 = F & for x being object st x in A.$1 holds F.x = [x,$1];
A1: for i being object st i in I ex j being object st P[i,j]
proof
let i be object such that
A2: i in I;
defpred R[object,object] means $2 = [$1,i];
A3: for x being object st x in A.i
ex y being object st y in Union coprod A & R[x,y]
proof
let x be object such that
A4: x in A.i;
take y = [x,i];
set Z = coprod(i,A);
A5: y in Z by A2,A4,MSAFREE:def 2;
A6: dom coprod A = I by PARTFUN1:def 2;
(coprod A).i = Z by A2,MSAFREE:def 3;
then Z in rng coprod A by A2,A6,FUNCT_1:3;
hence y in Union coprod A by A5,TARSKI:def 4;
thus R[x,y];
end;
ex F being Function of A.i,Union coprod A st
for x being object st x in A.i holds R[x,F.x] from FUNCT_2:sch 1(A3);
hence thesis;
end;
ex f being ManySortedSet of I st
for i being object st i in I holds P[i,f.i] from PBOOLE:sch 3(A1);
hence thesis;
end;
uniqueness
proof
let X,Y be ManySortedSet of I such that
A7: for i being object st i in I
ex F being Function of A.i,Union coprod A st
X.i = F & for x being object st x in A.i holds F.x = [x,i] and
A8: for i being object st i in I
ex F being Function of A.i,Union coprod A st
Y.i = F & for x being object st x in A.i holds F.x = [x,i];
let i be object such that
A9: i in I;
consider F being Function of A.i,Union coprod A such that
A10: X.i = F and
A11: for x being object st x in A.i holds F.x = [x,i] by A7,A9;
consider G being Function of A.i,Union coprod A such that
A12: Y.i = G and
A13: for x being object st x in A.i holds G.x = [x,i] by A8,A9;
per cases;
suppose A.i is empty;
then G = {} & F = {};
hence thesis by A10,A12;
end;
suppose
A14: A.i is non empty;
F = G
proof
let x be Element of A.i;
thus F.x = [x,i] by A11,A14
.= G.x by A13,A14;
end;
hence thesis by A10,A12;
end;
end;
end;
registration
let I,E,A;
cluster Coprod(A) -> Function-yielding;
coherence
proof
let i be object;
assume i in dom Coprod(A);
then ex F being Function of A.i,Union coprod A st Coprod(A).i = F &
for x being object st x in A.i holds F.x = [x,i] by Def10;
hence thesis;
end;
end;
definition
let I,E,A;
assume
A1: Union coprod A in E;
func EnsCatCoproduct A -> MorphismsFamily of A,EnsCatCoproductObj A equals
:Def11:
Coprod A;
coherence
proof
set P = Coprod A;
set B = EnsCatCoproductObj A;
A2: B = Union coprod A by A1,Def9;
let i be object such that
A3: i in I;
consider F being Function of A.i,Union coprod A such that
A4: P.i = F and
for x being object st x in A.i holds F.x = [x,i] by A3,Def10;
reconsider J = I as non empty set by A3;
reconsider j = i as Element of J by A3;
reconsider A1 = A as ObjectsFamily of J,EnsCat E;
A5: <^A1.j,B^> = Funcs(A1.j,B) by ALTCAT_1:def 14;
take o1 = A1.j;
thus o1 = A.i;
per cases;
suppose B <> {};
hence thesis by A2,A4,A5,FUNCT_2:8;
end;
suppose
A6: B = {};
then
A7: P.i = {} by A4,A2;
dom coprod A = I by PARTFUN1:def 2;
then
A8: (coprod A).i in rng coprod A by A3,FUNCT_1:3;
rng coprod A = {} or rng coprod A = {{}} by A2,A6,SCMYCIEL:18;
then (coprod A).i = {} by A8,TARSKI:def 1;
then A.i = {} by A3,MSAFREE:2;
hence thesis by A5,A7,A6,TARSKI:def 1,FUNCT_2:127;
end;
end;
end;
theorem Th7:
Union coprod A = {} implies Coprod A is empty-yielding
proof
assume
A1: Union coprod A = {};
let i be object;
assume i in I;
then ex F being Function of A.i,Union coprod A st (Coprod A).i = F &
for x being object st x in A.i holds F.x = [x,i] by Def10;
hence thesis by A1;
end;
theorem Th8:
Union coprod A = {} implies A is empty-yielding
proof
assume
A1: Union coprod A = {};
let i be object;
assume i in I;
then consider F being Function of A.i,Union coprod A such that
(Coprod A).i = F and
A2: for x being object st x in A.i holds F.x = [x,i] by Def10;
assume A.i is non empty;
then consider x being object such that
A3: x in A.i by XBOOLE_0:7;
F.x = [x,i] by A2,A3;
hence thesis by A1;
end;
theorem
Union coprod A in E & Union coprod A = {} implies
EnsCatCoproduct A = I --> {}
proof
assume that
A1: Union coprod A in E and
A2: Union coprod A = {};
let i be object;
assume
i in I;
A4: Coprod A is empty-yielding by A2,Th7;
thus (EnsCatCoproduct A).i = (Coprod A).i by A1,Def11
.= {} by A4
.= (I --> {}).i;
end;
theorem Th10:
Union coprod A in E implies
EnsCatCoproduct A is feasible coprojection-morphisms
proof
set B = EnsCatCoproductObj A;
set P = EnsCatCoproduct A;
assume
A1: Union coprod A in E; then
A2: B = Union coprod A by Def9;
A3: P = Coprod A by A1,Def11;
per cases;
suppose
A4: Union coprod A <> {};
then
A5: B <> {} by A1,Def9;
thus
A6: P is feasible
proof
let i be set;
assume
A7: i in I;
then reconsider I as non empty set;
reconsider i as Element of I by A7;
reconsider A as ObjectsFamily of I,EnsCat E;
reconsider P as MorphismsFamily of A,B;
take A.i;
A8: <^A.i,B^> = Funcs(A.i,B) by ALTCAT_1:def 14;
Funcs(A.i,B) <> {} by A5;
then P.i in <^A.i,B^> by A8;
hence thesis;
end;
let X be Object of EnsCat E, F be MorphismsFamily of A,X;
assume
A9: F is feasible;
A10: <^B,X^> = Funcs(B,X) by ALTCAT_1:def 14;
defpred P[object,object] means
$1`2 in I & $1`1 in A.$1`2 & $2 = F.$1`2.$1`1 &
for j being object st j in I & $1 = [$1`1,j] holds F.j.$1`1 = $2;
A11: for b being object st b in B ex u being object st P[b,u]
proof
let b be object;
assume b in B;
then consider Z being set such that
A12: b in Z and
A13: Z in rng coprod A by A2,TARSKI:def 4;
consider i being object such that
A14: i in dom coprod A and
A15: (coprod A).i = Z by A13,FUNCT_1:def 3;
(coprod A).i = coprod(i,A) by A14,MSAFREE:def 3;
then consider x being set such that
A16: x in A.i and
A17: b = [x,i] by A12,A14,A15,MSAFREE:def 2;
take F.i.x;
thus b`2 in I & b`1 in A.b`2 & F.b`2.b`1 = F.i.x by A14,A16,A17;
let j be object such that j in I and
A18: b = [b`1,j];
thus thesis by A17,A18,XTUPLE_0:1;
end;
consider ff being Function such that
A19: dom ff = B and
A20: for x being object st x in B holds P[x,ff.x] from CLASSES1:sch 1(A11);
A21: rng ff c= X
proof
let y be object;
assume y in rng ff;
then consider x being object such that
A22: x in dom ff and
A23: ff.x = y by FUNCT_1:def 3;
set i = x`2;
A24: i in I by A19,A20,A22;
A25: x`1 in A.i by A19,A20,A22;
A26: ff.x = F.i.x`1 by A19,A20,A22;
consider o1 being Object of EnsCat E such that
A27: o1 = A.i and
F.i is Morphism of o1,X by A24,Def1;
A28: <^o1,X^> = Funcs(o1,X) by ALTCAT_1:def 14;
then
A29: X <> {} by A24,A25,A27,A9,Def4;
F.i is Function of o1,X by A9,A24,A27,A28,Def4,FUNCT_2:66;
hence thesis by A23,A25,A26,A27,A29,FUNCT_2:5;
end;
then reconsider ff as Morphism of B,X by A10,A19,FUNCT_2:def 2;
take ff;
thus
A30: ff in <^B,X^> by A10,A21,A19,FUNCT_2:def 2;
thus for i being set st i in I
ex si being Object of EnsCat E, Pi being Morphism of si,B st
si = A.i & Pi = P.i & F.i = ff * Pi
proof
let i be set;
assume
A31: i in I;
then reconsider I as non empty set;
reconsider j = i as Element of I by A31;
reconsider A1 = A as ObjectsFamily of I,EnsCat E;
reconsider P1 = P as MorphismsFamily of A1,B;
reconsider F1 = F as MorphismsFamily of A1,X;
take A1.j,P1.j;
thus A1.j = A.i & P1.j = P.i;
reconsider p = P1.j as Function;
A32: <^A1.j,B^> = Funcs(A1.j,B) by ALTCAT_1:def 14;
A33: <^A1.j,B^> <> {} by A6,Def4;
A34: <^A1.j,X^> = Funcs(A1.j,X) by ALTCAT_1:def 14;
<^A1.j,X^> <> {} by A9,Def4; then
A35: ff * P1.j = ff * p by A30,A33,ALTCAT_1:16;
A36: F1.j in Funcs(A1.j,X) by A34,A9,Def4;
then
A37: dom(F1.j) = A1.j by FUNCT_2:92;
A38: dom(ff*P1.j) = A1.j by A34,A36,FUNCT_2:92;
A39: dom(P1.j) = A1.j by A32,A33,FUNCT_2:92;
now
let x be object;
assume
A40: x in dom(F1.j);
p is Function of A1.j,B by A32,A6,Def4,FUNCT_2:66;
then
A41: p.x in B by A5,A37,A40,FUNCT_2:5;
set x1 = (p.x)`1;
ex C being Function of A.j,Union coprod A st
P.i = C & for x being object st x in A.i holds C.x = [x,i]
by A3,Def10;
then
A42: p.x = [x,j] by A37,A40;
then ff.(p.x) = F.j.x1 by A41,A20;
hence (ff*p).x = F1.j.x by A42,A37,A40,A39,FUNCT_1:13;
end;
hence F.i = ff * P1.j by A35,A38,A36,FUNCT_1:2,FUNCT_2:92;
end;
let f1 be Morphism of B,X such that
A43: for i being set st i in I
ex si being Object of EnsCat E, Pi being Morphism of si,B st
si = A.i & Pi = P.i & F.i = f1 * Pi;
per cases;
suppose X = {};
then f1 = {} & ff = {} by A5,A10,SUBSET_1:def 1;
hence ff = f1;
end;
suppose
A44: X <> {};
f1 is Function of B,X by A10,A30,FUNCT_2:66;
then
A45: dom f1 = B by A44,FUNCT_2:def 1;
now
let x be object;
assume
A46: x in dom ff;
set a = x`1;
set i = x`2;
A47: i in I by A19,A20,A46;
then consider C being Function of A.i,Union coprod A such that
A48: P.i = C and
A49: for x being object st x in A.i holds C.x = [x,i] by A3,Def10;
consider si being Object of EnsCat E, Pi being Morphism of si,B
such that si = A.i and
A50: Pi = P.i and
A51: F.i = f1 * Pi by A43,A47;
A52: a in A.i by A19,A20,A46;
then
A53: a in dom Pi by A48,A50,A4,FUNCT_2:def 1;
A54: <^si,B^> = Funcs(si,B) by ALTCAT_1:def 14;
<^si,X^> = Funcs(si,X) by ALTCAT_1:def 14;
then
A55: f1 * Pi = f1 qua Function * Pi by A2,A4,A44,A54,A10,ALTCAT_1:16;
A56: ex y,z being object st x = [y,z] by A2,A19,A46,CARD_3:21;
C.a = [a,i] by A49,A52;
hence f1.x = F.i.a by A48,A50,A56,A51,A53,A55,FUNCT_1:13
.= ff.x by A19,A20,A46;
end;
hence thesis by A19,A45,FUNCT_1:2;
end;
end;
suppose
A57: Union coprod A = {};
thus P is feasible
proof
let i be set such that
A58: i in I;
reconsider I as non empty set by A58;
reconsider i as Element of I by A58;
reconsider A as ObjectsFamily of I,EnsCat E;
take A.i;
A59: Coprod A is empty-yielding by A57,Th7;
A is empty-yielding by A57,Th8;
then
A60: A.i = {};
A61: <^A.i,B^> = {{}} by A2,A57,A60,Lm2,ALTCAT_1:def 14;
P.i = {} by A3,A59;
hence thesis by A61,TARSKI:def 1;
end;
let X be Object of EnsCat E, F be MorphismsFamily of A,X;
assume F is feasible;
A62: <^B,X^> = Funcs(B,X) by ALTCAT_1:def 14
.= {{}} by A2,A57,FUNCT_5:57;
then reconsider f = {} as Morphism of B,X by TARSKI:def 1;
take f;
thus f in <^B,X^> by A62;
thus for i being set st i in I
ex si being Object of EnsCat E, Pi being Morphism of si,B st
si = A.i & Pi = P.i & F.i = f * Pi
proof
let i be set such that
A63: i in I;
reconsider J = I as non empty set by A63;
reconsider j = i as Element of J by A63;
reconsider A1 = A as ObjectsFamily of J,EnsCat E;
reconsider P1 = P as MorphismsFamily of A1,B;
reconsider si = A1.j as Object of EnsCat E;
reconsider Pi = P1.j as Morphism of si,B;
reconsider F1 = F as MorphismsFamily of A1,X;
reconsider F2 = F1.j as Morphism of si,X;
take si, Pi;
thus si = A.i & Pi = P.i;
A64: A is empty-yielding by A57,Th8;
then
A65: si = {};
then
A66: <^si,B^> = {{}} by A2,A57,Lm2,ALTCAT_1:def 14;
A67: <^si,X^> <> {} by A62,A64,A2,A57;
A68: Funcs(si,X) = {{}} by A65,FUNCT_5:57;
A69: <^si,X^> = Funcs(si,X) by ALTCAT_1:def 14;
thus F.i = F2
.= {} by A68,A69,TARSKI:def 1
.= f qua Function * Pi
.= f * Pi by A62,A66,A67,ALTCAT_1:16;
end;
thus thesis by A62,TARSKI:def 1;
end;
end;
theorem
Union coprod A in E implies EnsCatCoproductObj A is A-CatCoproduct-like
proof
assume
A1: Union coprod A in E;
take EnsCatCoproduct A;
thus thesis by A1,Th10;
end;
theorem
(for I,A holds Union coprod A in E) implies EnsCat E is with_coproducts
proof
assume
A1: for I,A holds Union coprod A in E;
let I,A;
take EnsCatCoproductObj A, EnsCatCoproduct A;
Union coprod A in E by A1;
hence thesis by Th10;
end;