let C be Category; ( C is with_finite_coproduct iff ( ex a being Object of C st a is initial & ( for a, b being Object of C ex c being Object of C ex i1, i2 being Morphism of C st
( dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c & c is_a_coproduct_wrt i1,i2 ) ) ) )
thus
( C is with_finite_coproduct implies ( ex a being Object of C st a is initial & ( for a, b being Object of C ex c being Object of C ex i1, i2 being Morphism of C st
( dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c & c is_a_coproduct_wrt i1,i2 ) ) ) )
( ex a being Object of C st a is initial & ( for a, b being Object of C ex c being Object of C ex i1, i2 being Morphism of C st
( dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c & c is_a_coproduct_wrt i1,i2 ) ) implies C is with_finite_coproduct )proof
reconsider F =
{} as
Function of
{}, the
carrier of
C by RELSET_1:12;
A1:
0 in {0,1}
by TARSKI:def 2;
assume A2:
for
I being
finite set for
F being
Function of
I, the
carrier of
C ex
a being
Object of
C ex
F9 being
Injections_family of
a,
I st
(
doms F9 = F &
a is_a_coproduct_wrt F9 )
;
CAT_4:def 20 ( ex a being Object of C st a is initial & ( for a, b being Object of C ex c being Object of C ex i1, i2 being Morphism of C st
( dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c & c is_a_coproduct_wrt i1,i2 ) ) )
then consider a being
Object of
C,
F9 being
Injections_family of
a,
{} such that
doms F9 = F
and A3:
a is_a_coproduct_wrt F9
;
thus
ex
a being
Object of
C st
a is
initial
by A3, CAT_3:75;
for a, b being Object of C ex c being Object of C ex i1, i2 being Morphism of C st
( dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c & c is_a_coproduct_wrt i1,i2 )
let a,
b be
Object of
C;
ex c being Object of C ex i1, i2 being Morphism of C st
( dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c & c is_a_coproduct_wrt i1,i2 )
set F = (
0,1)
--> (
a,
b);
consider c being
Object of
C,
F9 being
Injections_family of
c,
{0,1} such that A4:
doms F9 = (
0,1)
--> (
a,
b)
and A5:
c is_a_coproduct_wrt F9
by A2;
take
c
;
ex i1, i2 being Morphism of C st
( dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c & c is_a_coproduct_wrt i1,i2 )
take i1 =
F9 /. 0;
ex i2 being Morphism of C st
( dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c & c is_a_coproduct_wrt i1,i2 )
take i2 =
F9 /. 1;
( dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c & c is_a_coproduct_wrt i1,i2 )
A6:
1
in {0,1}
by TARSKI:def 2;
then A7:
i2 = F9 . 1
by FUNCT_2:def 13;
(
((0,1) --> (a,b)) /. 0 = a &
((0,1) --> (a,b)) /. 1
= b )
by CAT_3:3;
hence
(
dom i1 = a &
dom i2 = b )
by A4, A1, A6, CAT_3:def 1;
( cod i1 = c & cod i2 = c & c is_a_coproduct_wrt i1,i2 )
thus
(
cod i1 = c &
cod i2 = c )
by A1, A6, CAT_3:62;
c is_a_coproduct_wrt i1,i2
(
dom F9 = {0,1} &
i1 = F9 . 0 )
by A1, FUNCT_2:def 1, FUNCT_2:def 13;
then
F9 = (
0,1)
--> (
i1,
i2)
by A7, FUNCT_4:66;
hence
c is_a_coproduct_wrt i1,
i2
by A5, CAT_3:79;
verum
end;
given a being Object of C such that A8:
a is initial
; ( ex a, b being Object of C st
for c being Object of C
for i1, i2 being Morphism of C holds
( not dom i1 = a or not dom i2 = b or not cod i1 = c or not cod i2 = c or not c is_a_coproduct_wrt i1,i2 ) or C is with_finite_coproduct )
defpred S1[ Nat] means for I being finite set
for F being Function of I, the carrier of C st card I = $1 holds
ex a being Object of C ex F9 being Injections_family of a,I st
( doms F9 = F & a is_a_coproduct_wrt F9 );
assume A9:
for a, b being Object of C ex c being Object of C ex i1, i2 being Morphism of C st
( dom i1 = a & dom i2 = b & cod i1 = c & cod i2 = c & c is_a_coproduct_wrt i1,i2 )
; C is with_finite_coproduct
A10:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A11:
S1[
n]
;
S1[n + 1]
let I be
finite set ;
for F being Function of I, the carrier of C st card I = n + 1 holds
ex a being Object of C ex F9 being Injections_family of a,I st
( doms F9 = F & a is_a_coproduct_wrt F9 )let F be
Function of
I, the
carrier of
C;
( card I = n + 1 implies ex a being Object of C ex F9 being Injections_family of a,I st
( doms F9 = F & a is_a_coproduct_wrt F9 ) )
assume A12:
card I = n + 1
;
ex a being Object of C ex F9 being Injections_family of a,I st
( doms F9 = F & a is_a_coproduct_wrt F9 )
set x = the
Element of
I;
reconsider Ix =
I \ { the Element of I} as
finite set ;
reconsider sx =
{ the Element of I} as
finite set ;
reconsider G =
F | (I \ { the Element of I}) as
Function of
(I \ { the Element of I}), the
carrier of
C by FUNCT_2:32;
card Ix =
(card I) - (card sx)
by A12, CARD_1:27, CARD_2:44, ZFMISC_1:31
.=
(card I) - 1
by CARD_1:30
.=
n
by A12, XCMPLX_1:26
;
then consider a being
Object of
C,
G9 being
Injections_family of
a,
I \ { the Element of I} such that A13:
doms G9 = G
and A14:
a is_a_coproduct_wrt G9
by A11;
set b =
F /. the
Element of
I;
consider c being
Object of
C,
i1,
i2 being
Morphism of
C such that A15:
dom i1 = a
and A16:
dom i2 = F /. the
Element of
I
and A17:
cod i1 = c
and A18:
cod i2 = c
and A19:
c is_a_coproduct_wrt i1,
i2
by A9;
set F9 =
(i1 * G9) +* ( the Element of I .--> i2);
A20:
dom ({ the Element of I} --> i2) = { the Element of I}
by FUNCT_2:def 1;
rng ((i1 * G9) +* ( the Element of I .--> i2)) c= (rng (i1 * G9)) \/ (rng ( the Element of I .--> i2))
by FUNCT_4:17;
then A21:
rng ((i1 * G9) +* ( the Element of I .--> i2)) c= the
carrier' of
C
by XBOOLE_1:1;
dom (i1 * G9) = I \ { the Element of I}
by FUNCT_2:def 1;
then A22:
(dom (i1 * G9)) \/ (dom ( the Element of I .--> i2)) =
I \/ { the Element of I}
by A20, XBOOLE_1:39
.=
I
by A12, CARD_1:27, ZFMISC_1:40
;
then
dom ((i1 * G9) +* ( the Element of I .--> i2)) = I
by FUNCT_4:def 1;
then reconsider F9 =
(i1 * G9) +* ( the Element of I .--> i2) as
Function of
I, the
carrier' of
C by A21, FUNCT_2:def 1, RELSET_1:4;
A23:
cods G9 = (I \ { the Element of I}) --> a
by CAT_3:def 16;
now for y being object st y in I holds
(cods F9) . y = (I --> c) . ylet y be
object ;
( y in I implies (cods F9) . y = (I --> c) . y )assume A24:
y in I
;
(cods F9) . y = (I --> c) . ynow (I --> c) . y = (cods F9) /. yper cases
( y = the Element of I or y <> the Element of I )
;
suppose A26:
y <> the
Element of
I
;
(cods F9) /. y = (I --> c) . ythen A27:
not
y in { the Element of I}
by TARSKI:def 1;
A28:
y in I \ { the Element of I}
by A24, A26, ZFMISC_1:56;
F9 /. y =
F9 . y
by A24, FUNCT_2:def 13
.=
(i1 * G9) . y
by A20, A22, A24, A27, FUNCT_4:def 1
.=
(i1 * G9) /. y
by A28, FUNCT_2:def 13
;
hence (cods F9) /. y =
cod ((i1 * G9) /. y)
by A24, CAT_3:def 2
.=
(cods (i1 * G9)) /. y
by A28, CAT_3:def 2
.=
((I \ { the Element of I}) --> c) /. y
by A15, A17, A23, CAT_3:17
.=
c
by A24, A26, CAT_3:2, ZFMISC_1:56
.=
(I --> c) . y
by A24, FUNCOP_1:7
;
verum end; end; end; hence
(cods F9) . y = (I --> c) . y
by A24, FUNCT_2:def 13;
verum end;
then reconsider F9 =
F9 as
Injections_family of
c,
I by CAT_3:def 16, FUNCT_2:12;
take
c
;
ex F9 being Injections_family of c,I st
( doms F9 = F & c is_a_coproduct_wrt F9 )
take
F9
;
( doms F9 = F & c is_a_coproduct_wrt F9 )
A29:
now for y being set st y in I holds
(doms F9) /. y = F /. ylet y be
set ;
( y in I implies (doms F9) /. y = F /. y )assume A30:
y in I
;
(doms F9) /. y = F /. ynow (doms F9) /. y = F /. yper cases
( y = the Element of I or y <> the Element of I )
;
suppose A33:
y <> the
Element of
I
;
(doms F9) /. y = F /. ythen A34:
not
y in { the Element of I}
by TARSKI:def 1;
A35:
y in I \ { the Element of I}
by A30, A33, ZFMISC_1:56;
F9 /. y =
F9 . y
by A30, FUNCT_2:def 13
.=
(i1 * G9) . y
by A20, A22, A30, A34, FUNCT_4:def 1
.=
(i1 * G9) /. y
by A35, FUNCT_2:def 13
;
hence (doms F9) /. y =
dom ((i1 * G9) /. y)
by A30, CAT_3:def 1
.=
(doms (i1 * G9)) /. y
by A35, CAT_3:def 1
.=
G /. y
by A13, A15, A23, CAT_3:17
.=
G . y
by A35, FUNCT_2:def 13
.=
F . y
by A30, A33, FUNCT_1:49, ZFMISC_1:56
.=
F /. y
by A30, FUNCT_2:def 13
;
verum end; end; end; hence
(doms F9) /. y = F /. y
;
verum end;
hence
doms F9 = F
by CAT_3:1;
c is_a_coproduct_wrt F9
thus
F9 is
Injections_family of
c,
I
;
CAT_3:def 17 for b1 being Element of the carrier of C
for b2 being Injections_family of b1,I holds
( not doms F9 = doms b2 or ex b3 being Element of the carrier' of C st
( b3 in Hom (c,b1) & ( for b4 being Element of the carrier' of C holds
( not b4 in Hom (c,b1) or ( ( ex b5 being set st
( b5 in I & not b4 (*) (F9 /. b5) = b2 /. b5 ) or b3 = b4 ) & ( not b3 = b4 or for b5 being set holds
( not b5 in I or b4 (*) (F9 /. b5) = b2 /. b5 ) ) ) ) ) ) )
let d be
Object of
C;
for b1 being Injections_family of d,I holds
( not doms F9 = doms b1 or ex b2 being Element of the carrier' of C st
( b2 in Hom (c,d) & ( for b3 being Element of the carrier' of C holds
( not b3 in Hom (c,d) or ( ( ex b4 being set st
( b4 in I & not b3 (*) (F9 /. b4) = b1 /. b4 ) or b2 = b3 ) & ( not b2 = b3 or for b4 being set holds
( not b4 in I or b3 (*) (F9 /. b4) = b1 /. b4 ) ) ) ) ) ) )let F99 be
Injections_family of
d,
I;
( not doms F9 = doms F99 or ex b1 being Element of the carrier' of C st
( b1 in Hom (c,d) & ( for b2 being Element of the carrier' of C holds
( not b2 in Hom (c,d) or ( ( ex b3 being set st
( b3 in I & not b2 (*) (F9 /. b3) = F99 /. b3 ) or b1 = b2 ) & ( not b1 = b2 or for b3 being set holds
( not b3 in I or b2 (*) (F9 /. b3) = F99 /. b3 ) ) ) ) ) ) )
assume A36:
doms F9 = doms F99
;
ex b1 being Element of the carrier' of C st
( b1 in Hom (c,d) & ( for b2 being Element of the carrier' of C holds
( not b2 in Hom (c,d) or ( ( ex b3 being set st
( b3 in I & not b2 (*) (F9 /. b3) = F99 /. b3 ) or b1 = b2 ) & ( not b1 = b2 or for b3 being set holds
( not b3 in I or b2 (*) (F9 /. b3) = F99 /. b3 ) ) ) ) ) )
reconsider G99 =
F99 | (I \ { the Element of I}) as
Function of
(I \ { the Element of I}), the
carrier' of
C by FUNCT_2:32;
then reconsider G99 =
G99 as
Injections_family of
d,
I \ { the Element of I} by CAT_3:1, CAT_3:def 16;
now for y being set st y in I \ { the Element of I} holds
(doms G9) /. y = (doms G99) /. ylet y be
set ;
( y in I \ { the Element of I} implies (doms G9) /. y = (doms G99) /. y )assume A38:
y in I \ { the Element of I}
;
(doms G9) /. y = (doms G99) /. ythen A39:
G /. y =
G . y
by FUNCT_2:def 13
.=
F . y
by A38, FUNCT_1:49
.=
F /. y
by A38, FUNCT_2:def 13
;
F99 /. y =
F99 . y
by A38, FUNCT_2:def 13
.=
G99 . y
by A38, FUNCT_1:49
.=
G99 /. y
by A38, FUNCT_2:def 13
;
hence (doms G9) /. y =
dom (G99 /. y)
by A13, A29, A36, A38, A39, CAT_3:1, CAT_3:def 1
.=
(doms G99) /. y
by A38, CAT_3:def 1
;
verum end;
then consider h9 being
Morphism of
C such that A40:
h9 in Hom (
a,
d)
and A41:
for
k being
Morphism of
C st
k in Hom (
a,
d) holds
( ( for
y being
set st
y in I \ { the Element of I} holds
k (*) (G9 /. y) = G99 /. y ) iff
h9 = k )
by A14, CAT_3:1;
A42:
the
Element of
I in { the Element of I}
by TARSKI:def 1;
set g =
F99 /. the
Element of
I;
A43:
cod (F99 /. the Element of I) = d
by A12, CARD_1:27, CAT_3:62;
A44:
F9 /. the
Element of
I =
F9 . the
Element of
I
by A12, CARD_1:27, FUNCT_2:def 13
.=
( the Element of I .--> i2) . the
Element of
I
by A20, A42, FUNCT_4:13
.=
i2
by A42, FUNCOP_1:7
;
then dom i2 =
(doms F9) /. the
Element of
I
by A12, CARD_1:27, CAT_3:def 1
.=
dom (F99 /. the Element of I)
by A12, A36, CARD_1:27, CAT_3:def 1
;
then
F99 /. the
Element of
I in Hom (
(dom i2),
d)
by A43;
then consider h being
Morphism of
C such that A45:
h in Hom (
c,
d)
and A46:
for
k being
Morphism of
C st
k in Hom (
c,
d) holds
( (
k (*) i1 = h9 &
k (*) i2 = F99 /. the
Element of
I ) iff
h = k )
by A15, A19, A40;
take
h
;
( h in Hom (c,d) & ( for b1 being Element of the carrier' of C holds
( not b1 in Hom (c,d) or ( ( ex b2 being set st
( b2 in I & not b1 (*) (F9 /. b2) = F99 /. b2 ) or h = b1 ) & ( not h = b1 or for b2 being set holds
( not b2 in I or b1 (*) (F9 /. b2) = F99 /. b2 ) ) ) ) ) )
thus
h in Hom (
c,
d)
by A45;
for b1 being Element of the carrier' of C holds
( not b1 in Hom (c,d) or ( ( ex b2 being set st
( b2 in I & not b1 (*) (F9 /. b2) = F99 /. b2 ) or h = b1 ) & ( not h = b1 or for b2 being set holds
( not b2 in I or b1 (*) (F9 /. b2) = F99 /. b2 ) ) ) )
let k be
Morphism of
C;
( not k in Hom (c,d) or ( ( ex b1 being set st
( b1 in I & not k (*) (F9 /. b1) = F99 /. b1 ) or h = k ) & ( not h = k or for b1 being set holds
( not b1 in I or k (*) (F9 /. b1) = F99 /. b1 ) ) ) )
assume A47:
k in Hom (
c,
d)
;
( ( ex b1 being set st
( b1 in I & not k (*) (F9 /. b1) = F99 /. b1 ) or h = k ) & ( not h = k or for b1 being set holds
( not b1 in I or k (*) (F9 /. b1) = F99 /. b1 ) ) )
thus
( ( for
y being
set st
y in I holds
k (*) (F9 /. y) = F99 /. y ) implies
h = k )
( not h = k or for b1 being set holds
( not b1 in I or k (*) (F9 /. b1) = F99 /. b1 ) )proof
A48:
dom k = c
by A47, CAT_1:1;
then A49:
dom (k (*) i1) = a
by A15, A17, CAT_1:17;
assume A50:
for
y being
set st
y in I holds
k (*) (F9 /. y) = F99 /. y
;
h = k
A51:
for
y being
set st
y in I \ { the Element of I} holds
(k (*) i1) (*) (G9 /. y) = G99 /. y
proof
let y be
set ;
( y in I \ { the Element of I} implies (k (*) i1) (*) (G9 /. y) = G99 /. y )
assume A52:
y in I \ { the Element of I}
;
(k (*) i1) (*) (G9 /. y) = G99 /. y
then A53:
not
y in { the Element of I}
by XBOOLE_0:def 5;
A54:
F9 /. y =
F9 . y
by A52, FUNCT_2:def 13
.=
(i1 * G9) . y
by A20, A22, A52, A53, FUNCT_4:def 1
.=
(i1 * G9) /. y
by A52, FUNCT_2:def 13
;
cod (G9 /. y) = a
by A52, CAT_3:62;
hence (k (*) i1) (*) (G9 /. y) =
k (*) (i1 (*) (G9 /. y))
by A15, A17, A48, CAT_1:18
.=
k (*) ((i1 * G9) /. y)
by A52, CAT_3:def 6
.=
F99 /. y
by A50, A52, A54
.=
F99 . y
by A52, FUNCT_2:def 13
.=
G99 . y
by A52, FUNCT_1:49
.=
G99 /. y
by A52, FUNCT_2:def 13
;
verum
end;
cod k = d
by A47, CAT_1:1;
then
cod (k (*) i1) = d
by A17, A48, CAT_1:17;
then
k (*) i1 in Hom (
a,
d)
by A49;
then A55:
k (*) i1 = h9
by A41, A51;
k (*) i2 = F99 /. the
Element of
I
by A12, A44, A50, CARD_1:27;
hence
h = k
by A46, A47, A55;
verum
end;
assume A56:
h = k
;
for b1 being set holds
( not b1 in I or k (*) (F9 /. b1) = F99 /. b1 )
let y be
set ;
( not y in I or k (*) (F9 /. y) = F99 /. y )
assume A57:
y in I
;
k (*) (F9 /. y) = F99 /. y
now k (*) (F9 /. y) = F99 /. yper cases
( y = the Element of I or y <> the Element of I )
;
suppose A60:
y <> the
Element of
I
;
k (*) (F9 /. y) = F99 /. ythen A61:
not
y in { the Element of I}
by TARSKI:def 1;
A62:
dom k = c
by A47, CAT_1:1;
A63:
y in I \ { the Element of I}
by A57, A60, ZFMISC_1:56;
A64:
cod (G9 /. y) = a
by A57, A60, CAT_3:62, ZFMISC_1:56;
F9 /. y =
F9 . y
by A57, FUNCT_2:def 13
.=
(i1 * G9) . y
by A20, A22, A57, A61, FUNCT_4:def 1
.=
(i1 * G9) /. y
by A63, FUNCT_2:def 13
.=
i1 (*) (G9 /. y)
by A63, CAT_3:def 6
;
hence k (*) (F9 /. y) =
(k (*) i1) (*) (G9 /. y)
by A15, A17, A62, A64, CAT_1:18
.=
h9 (*) (G9 /. y)
by A46, A47, A56
.=
G99 /. y
by A40, A41, A63
.=
G99 . y
by A63, FUNCT_2:def 13
.=
F99 . y
by A57, A60, FUNCT_1:49, ZFMISC_1:56
.=
F99 /. y
by A57, FUNCT_2:def 13
;
verum end; end; end;
hence
k (*) (F9 /. y) = F99 /. y
;
verum
end;
let I be finite set ; CAT_4:def 20 for F being Function of I, the carrier of C ex a being Object of C ex F9 being Injections_family of a,I st
( doms F9 = F & a is_a_coproduct_wrt F9 )
let F be Function of I, the carrier of C; ex a being Object of C ex F9 being Injections_family of a,I st
( doms F9 = F & a is_a_coproduct_wrt F9 )
A65:
card I = card I
;
A66:
S1[ 0 ]
proof
let I be
finite set ;
for F being Function of I, the carrier of C st card I = 0 holds
ex a being Object of C ex F9 being Injections_family of a,I st
( doms F9 = F & a is_a_coproduct_wrt F9 )let F be
Function of
I, the
carrier of
C;
( card I = 0 implies ex a being Object of C ex F9 being Injections_family of a,I st
( doms F9 = F & a is_a_coproduct_wrt F9 ) )
assume
card I = 0
;
ex a being Object of C ex F9 being Injections_family of a,I st
( doms F9 = F & a is_a_coproduct_wrt F9 )
then A67:
I = {}
;
{} is
Function of
{}, the
carrier' of
C
by RELSET_1:12;
then reconsider F9 =
{} as
Injections_family of
a,
I by A67, CAT_3:63;
take
a
;
ex F9 being Injections_family of a,I st
( doms F9 = F & a is_a_coproduct_wrt F9 )
take
F9
;
( doms F9 = F & a is_a_coproduct_wrt F9 )
for
x being
set st
x in I holds
(doms F9) /. x = F /. x
;
hence
doms F9 = F
by CAT_3:1;
a is_a_coproduct_wrt F9
thus
a is_a_coproduct_wrt F9
by A8, A67, CAT_3:75;
verum
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A66, A10);
hence
ex a being Object of C ex F9 being Injections_family of a,I st
( doms F9 = F & a is_a_coproduct_wrt F9 )
by A65; verum