let C be Category; for a being Object of C
for F being Injections_family of a, {} holds
( a is_a_coproduct_wrt F iff a is initial )
let a be Object of C; for F being Injections_family of a, {} holds
( a is_a_coproduct_wrt F iff a is initial )
let F be Injections_family of a, {} ; ( a is_a_coproduct_wrt F iff a is initial )
thus
( a is_a_coproduct_wrt F implies a is initial )
( a is initial implies a is_a_coproduct_wrt F )proof
assume A1:
a is_a_coproduct_wrt F
;
a is initial
let b be
Object of
C;
CAT_1:def 19 ( not Hom (a,b) = {} & ex b1 being Morphism of a,b st
for b2 being Morphism of a,b holds b1 = b2 )
set F9 = the
Injections_family of
b,
{} ;
consider h being
Morphism of
C such that A2:
h in Hom (
a,
b)
and A3:
for
k being
Morphism of
C st
k in Hom (
a,
b) holds
( ( for
x being
set st
x in {} holds
k (*) (F /. x) = the
Injections_family of
b,
{} /. x ) iff
h = k )
by A1;
thus
Hom (
a,
b)
<> {}
by A2;
ex b1 being Morphism of a,b st
for b2 being Morphism of a,b holds b1 = b2
reconsider f =
h as
Morphism of
a,
b by A2, CAT_1:def 5;
take
f
;
for b1 being Morphism of a,b holds f = b1
let g be
Morphism of
a,
b;
f = g
A4:
for
x being
set st
x in {} holds
g (*) (F /. x) = the
Injections_family of
b,
{} /. x
;
g in Hom (
a,
b)
by A2, CAT_1:def 5;
hence
f = g
by A3, A4;
verum
end;
assume A5:
a is initial
; a is_a_coproduct_wrt F
thus
F is Injections_family of a, {}
; CAT_3:def 17 for d being Object of C
for F9 being Injections_family of d, {} st doms F = doms F9 holds
ex h being Morphism of C st
( h in Hom (a,d) & ( for k being Morphism of C st k in Hom (a,d) holds
( ( for x being set st x in {} holds
k (*) (F /. x) = F9 /. x ) iff h = k ) ) )
let b be Object of C; for F9 being Injections_family of b, {} st doms F = doms F9 holds
ex h being Morphism of C st
( h in Hom (a,b) & ( for k being Morphism of C st k in Hom (a,b) holds
( ( for x being set st x in {} holds
k (*) (F /. x) = F9 /. x ) iff h = k ) ) )
consider h being Morphism of a,b such that
A6:
for g being Morphism of a,b holds h = g
by A5;
let F9 be Injections_family of b, {} ; ( doms F = doms F9 implies ex h being Morphism of C st
( h in Hom (a,b) & ( for k being Morphism of C st k in Hom (a,b) holds
( ( for x being set st x in {} holds
k (*) (F /. x) = F9 /. x ) iff h = k ) ) ) )
assume
doms F = doms F9
; ex h being Morphism of C st
( h in Hom (a,b) & ( for k being Morphism of C st k in Hom (a,b) holds
( ( for x being set st x in {} holds
k (*) (F /. x) = F9 /. x ) iff h = k ) ) )
take
h
; ( h in Hom (a,b) & ( for k being Morphism of C st k in Hom (a,b) holds
( ( for x being set st x in {} holds
k (*) (F /. x) = F9 /. x ) iff h = k ) ) )
Hom (a,b) <> {}
by A5;
hence
h in Hom (a,b)
by CAT_1:def 5; for k being Morphism of C st k in Hom (a,b) holds
( ( for x being set st x in {} holds
k (*) (F /. x) = F9 /. x ) iff h = k )
let k be Morphism of C; ( k in Hom (a,b) implies ( ( for x being set st x in {} holds
k (*) (F /. x) = F9 /. x ) iff h = k ) )
assume
k in Hom (a,b)
; ( ( for x being set st x in {} holds
k (*) (F /. x) = F9 /. x ) iff h = k )
then
k is Morphism of a,b
by CAT_1:def 5;
hence
( ( for x being set st x in {} holds
k (*) (F /. x) = F9 /. x ) iff h = k )
by A6; verum