let C be Category; for a, b, c being Object of C st Hom (a,c) <> {} & Hom (b,c) <> {} holds
for i1 being Morphism of a,c
for i2 being Morphism of b,c holds
( c is_a_coproduct_wrt i1,i2 iff for d being Object of C st Hom (a,d) <> {} & Hom (b,d) <> {} holds
( Hom (c,d) <> {} & ( for f being Morphism of a,d
for 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 ) ) ) )
let a, b, c be Object of C; ( Hom (a,c) <> {} & Hom (b,c) <> {} implies for i1 being Morphism of a,c
for i2 being Morphism of b,c holds
( c is_a_coproduct_wrt i1,i2 iff for d being Object of C st Hom (a,d) <> {} & Hom (b,d) <> {} holds
( Hom (c,d) <> {} & ( for f being Morphism of a,d
for 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 ) ) ) ) )
assume that
A1:
Hom (a,c) <> {}
and
A2:
Hom (b,c) <> {}
; for i1 being Morphism of a,c
for i2 being Morphism of b,c holds
( c is_a_coproduct_wrt i1,i2 iff for d being Object of C st Hom (a,d) <> {} & Hom (b,d) <> {} holds
( Hom (c,d) <> {} & ( for f being Morphism of a,d
for 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 ) ) ) )
let i1 be Morphism of a,c; for i2 being Morphism of b,c holds
( c is_a_coproduct_wrt i1,i2 iff for d being Object of C st Hom (a,d) <> {} & Hom (b,d) <> {} holds
( Hom (c,d) <> {} & ( for f being Morphism of a,d
for 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 ) ) ) )
let i2 be Morphism of b,c; ( c is_a_coproduct_wrt i1,i2 iff for d being Object of C st Hom (a,d) <> {} & Hom (b,d) <> {} holds
( Hom (c,d) <> {} & ( for f being Morphism of a,d
for 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
( c is_a_coproduct_wrt i1,i2 implies for d being Object of C st Hom (a,d) <> {} & Hom (b,d) <> {} holds
( Hom (c,d) <> {} & ( for f being Morphism of a,d
for 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 ) ) ) )
( ( for d being Object of C st Hom (a,d) <> {} & Hom (b,d) <> {} holds
( Hom (c,d) <> {} & ( for f being Morphism of a,d
for 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 ) ) ) ) implies c is_a_coproduct_wrt i1,i2 )proof
assume that
cod i1 = c
and
cod i2 = c
and A3:
for
d being
Object of
C for
f,
g being
Morphism of
C st
f in Hom (
(dom i1),
d) &
g in Hom (
(dom i2),
d) holds
ex
h being
Morphism of
C st
(
h in Hom (
c,
d) & ( for
k being
Morphism of
C st
k in Hom (
c,
d) holds
( (
k (*) i1 = f &
k (*) i2 = g ) iff
h = k ) ) )
;
CAT_3:def 18 for d being Object of C st Hom (a,d) <> {} & Hom (b,d) <> {} holds
( Hom (c,d) <> {} & ( for f being Morphism of a,d
for 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 ) ) )
let d be
Object of
C;
( Hom (a,d) <> {} & Hom (b,d) <> {} implies ( Hom (c,d) <> {} & ( for f being Morphism of a,d
for 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 ) ) ) )
assume that A4:
Hom (
a,
d)
<> {}
and A5:
Hom (
b,
d)
<> {}
;
( Hom (c,d) <> {} & ( for f being Morphism of a,d
for 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 ) ) )
set f = the
Morphism of
a,
d;
set g = the
Morphism of
b,
d;
A6:
dom i2 = b
by A2, CAT_1:5;
then A7:
the
Morphism of
b,
d in Hom (
(dom i2),
d)
by A5, CAT_1:def 5;
A8:
dom i1 = a
by A1, CAT_1:5;
then
the
Morphism of
a,
d in Hom (
(dom i1),
d)
by A4, CAT_1:def 5;
then A9:
ex
h being
Morphism of
C st
(
h in Hom (
c,
d) & ( for
k being
Morphism of
C st
k in Hom (
c,
d) holds
( (
k (*) i1 = the
Morphism of
a,
d &
k (*) i2 = the
Morphism of
b,
d ) iff
h = k ) ) )
by A3, A7;
hence
Hom (
c,
d)
<> {}
;
for f being Morphism of a,d
for 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 )
let f be
Morphism of
a,
d;
for 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 )let g be
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 )
A10:
g in Hom (
(dom i2),
d)
by A5, A6, CAT_1:def 5;
f in Hom (
(dom i1),
d)
by A4, A8, CAT_1:def 5;
then consider h being
Morphism of
C such that A11:
h in Hom (
c,
d)
and A12:
for
k being
Morphism of
C st
k in Hom (
c,
d) holds
( (
k (*) i1 = f &
k (*) i2 = g ) iff
h = k )
by A3, A10;
reconsider h =
h as
Morphism of
c,
d by A11, CAT_1:def 5;
take
h
;
for k being Morphism of c,d holds
( ( k * i1 = f & k * i2 = g ) iff h = k )
let k be
Morphism of
c,
d;
( ( k * i1 = f & k * i2 = g ) iff h = k )
A13:
k in Hom (
c,
d)
by A9, CAT_1:def 5;
(
k * i1 = k (*) i1 &
k * i2 = k (*) i2 )
by A1, A2, A9, CAT_1:def 13;
hence
( (
k * i1 = f &
k * i2 = g ) iff
h = k )
by A12, A13;
verum
end;
assume A14:
for d being Object of C st Hom (a,d) <> {} & Hom (b,d) <> {} holds
( Hom (c,d) <> {} & ( for f being Morphism of a,d
for 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 ) ) )
; c is_a_coproduct_wrt i1,i2
thus
( cod i1 = c & cod i2 = c )
by A1, A2, CAT_1:5; CAT_3:def 18 for d being Object of C
for f, g being Morphism of C st f in Hom ((dom i1),d) & g in Hom ((dom i2),d) holds
ex h being Morphism of C st
( h in Hom (c,d) & ( for k being Morphism of C st k in Hom (c,d) holds
( ( k (*) i1 = f & k (*) i2 = g ) iff h = k ) ) )
let d be Object of C; for f, g being Morphism of C st f in Hom ((dom i1),d) & g in Hom ((dom i2),d) holds
ex h being Morphism of C st
( h in Hom (c,d) & ( for k being Morphism of C st k in Hom (c,d) holds
( ( k (*) i1 = f & k (*) i2 = g ) iff h = k ) ) )
let f, g be Morphism of C; ( f in Hom ((dom i1),d) & g in Hom ((dom i2),d) implies ex h being Morphism of C st
( h in Hom (c,d) & ( for k being Morphism of C st k in Hom (c,d) holds
( ( k (*) i1 = f & k (*) i2 = g ) iff h = k ) ) ) )
assume that
A15:
f in Hom ((dom i1),d)
and
A16:
g in Hom ((dom i2),d)
; ex h being Morphism of C st
( h in Hom (c,d) & ( for k being Morphism of C st k in Hom (c,d) holds
( ( k (*) i1 = f & k (*) i2 = g ) iff h = k ) ) )
A17:
Hom (a,d) <> {}
by A1, A15, CAT_1:5;
A18:
dom i1 = a
by A1, CAT_1:5;
then A19:
f is Morphism of a,d
by A15, CAT_1:def 5;
A20:
dom i2 = b
by A2, CAT_1:5;
then
g is Morphism of b,d
by A16, CAT_1:def 5;
then consider h being Morphism of c,d such that
A21:
for k being Morphism of c,d holds
( ( k * i1 = f & k * i2 = g ) iff h = k )
by A14, A16, A20, A19, A17;
reconsider h9 = h as Morphism of C ;
take
h9
; ( h9 in Hom (c,d) & ( for k being Morphism of C st k in Hom (c,d) holds
( ( k (*) i1 = f & k (*) i2 = g ) iff h9 = k ) ) )
A22:
Hom (c,d) <> {}
by A14, A15, A16, A18, A20;
hence
h9 in Hom (c,d)
by CAT_1:def 5; for k being Morphism of C st k in Hom (c,d) holds
( ( k (*) i1 = f & k (*) i2 = g ) iff h9 = k )
let k be Morphism of C; ( k in Hom (c,d) implies ( ( k (*) i1 = f & k (*) i2 = g ) iff h9 = k ) )
assume
k in Hom (c,d)
; ( ( k (*) i1 = f & k (*) i2 = g ) iff h9 = k )
then reconsider k9 = k as Morphism of c,d by CAT_1:def 5;
( k (*) i1 = k9 * i1 & k (*) i2 = k9 * i2 )
by A1, A2, A22, CAT_1:def 13;
hence
( ( k (*) i1 = f & k (*) i2 = g ) iff h9 = k )
by A21; verum