let I be set ; for C being Category
for c being Object of C
for F being Function of I, the carrier' of C holds
( c is_a_product_wrt F iff c opp is_a_coproduct_wrt F opp )
let C be Category; for c being Object of C
for F being Function of I, the carrier' of C holds
( c is_a_product_wrt F iff c opp is_a_coproduct_wrt F opp )
let c be Object of C; for F being Function of I, the carrier' of C holds
( c is_a_product_wrt F iff c opp is_a_coproduct_wrt F opp )
let F be Function of I, the carrier' of C; ( c is_a_product_wrt F iff c opp is_a_coproduct_wrt F opp )
thus
( c is_a_product_wrt F implies c opp is_a_coproduct_wrt F opp )
( c opp is_a_coproduct_wrt F opp implies c is_a_product_wrt F )proof
assume A1:
c is_a_product_wrt F
;
c opp is_a_coproduct_wrt F opp
then
F is
Projections_family of
c,
I
;
hence
F opp is
Injections_family of
c opp ,
I
by Th68;
CAT_3:def 17 for d being Object of (C opp)
for F9 being Injections_family of d,I st doms (F opp) = doms F9 holds
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
( ( for x being set st x in I holds
k (*) ((F opp) /. x) = F9 /. x ) iff h = k ) ) )
let d be
Object of
(C opp);
for F9 being Injections_family of d,I st doms (F opp) = doms F9 holds
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
( ( for x being set st x in I holds
k (*) ((F opp) /. x) = F9 /. x ) iff h = k ) ) )let F9 be
Injections_family of
d,
I;
( doms (F opp) = doms F9 implies 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
( ( for x being set st x in I holds
k (*) ((F opp) /. x) = F9 /. x ) iff h = k ) ) ) )
assume A2:
doms (F opp) = doms F9
;
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
( ( for x being set st x in I holds
k (*) ((F opp) /. x) = F9 /. x ) iff h = k ) ) )
reconsider oppF9 =
opp F9 as
Projections_family of
opp d,
I by Th69;
now for x being set st x in I holds
(cods F) /. x = (cods oppF9) /. xlet x be
set ;
( x in I implies (cods F) /. x = (cods oppF9) /. x )reconsider gg =
F /. x as
Morphism of
dom (F /. x),
cod (F /. x) by CAT_1:4;
A3:
Hom (
(dom gg),
(cod gg))
<> {}
by CAT_1:2;
then A4:
gg opp = (F /. x) opp
by OPPCAT_1:def 6;
reconsider g9 =
F9 /. x as
Morphism of
dom (F9 /. x),
cod (F9 /. x) by CAT_1:4;
Hom (
(dom g9),
(cod g9))
<> {}
by CAT_1:2;
then A5:
g9 opp = (F9 /. x) opp
by OPPCAT_1:def 6;
assume A6:
x in I
;
(cods F) /. x = (cods oppF9) /. xhence (cods F) /. x =
cod (F /. x)
by Def2
.=
dom (gg opp)
by A3, OPPCAT_1:10
.=
dom ((F opp) /. x)
by A6, Def3, A4
.=
(doms F9) /. x
by A2, A6, Def1
.=
dom (F9 /. x)
by A6, Def1
.=
cod (opp (F9 /. x))
by A5, OPPCAT_1:11
.=
cod (oppF9 /. x)
by A6, Def4
.=
(cods oppF9) /. x
by A6, Def2
;
verum end;
then consider h being
Morphism of
C such that A7:
h in Hom (
(opp d),
c)
and A8:
for
k being
Morphism of
C st
k in Hom (
(opp d),
c) holds
( ( for
x being
set st
x in I holds
(F /. x) (*) k = oppF9 /. x ) iff
h = k )
by A1, Th1;
take
h opp
;
( h opp in Hom ((c opp),d) & ( for k being Morphism of (C opp) st k in Hom ((c opp),d) holds
( ( for x being set st x in I holds
k (*) ((F opp) /. x) = F9 /. x ) iff h opp = k ) ) )
h in Hom (
(c opp),
((opp d) opp))
by A7, OPPCAT_1:5;
hence
h opp in Hom (
(c opp),
d)
;
for k being Morphism of (C opp) st k in Hom ((c opp),d) holds
( ( for x being set st x in I holds
k (*) ((F opp) /. x) = F9 /. x ) iff h opp = k )
let k be
Morphism of
(C opp);
( k in Hom ((c opp),d) implies ( ( for x being set st x in I holds
k (*) ((F opp) /. x) = F9 /. x ) iff h opp = k ) )
assume A9:
k in Hom (
(c opp),
d)
;
( ( for x being set st x in I holds
k (*) ((F opp) /. x) = F9 /. x ) iff h opp = k )
then A10:
opp k in Hom (
(opp d),
(opp (c opp)))
by OPPCAT_1:6;
thus
( ( for
x being
set st
x in I holds
k (*) ((F opp) /. x) = F9 /. x ) implies
h opp = k )
( h opp = k implies for x being set st x in I holds
k (*) ((F opp) /. x) = F9 /. x )proof
assume A11:
for
x being
set st
x in I holds
k (*) ((F opp) /. x) = F9 /. x
;
h opp = k
now for x being set st x in I holds
oppF9 /. x = (F /. x) (*) (opp k)let x be
set ;
( x in I implies oppF9 /. x = (F /. x) (*) (opp k) )assume A12:
x in I
;
oppF9 /. x = (F /. x) (*) (opp k)reconsider gg =
F /. x as
Morphism of
dom (F /. x),
cod (F /. x) by CAT_1:4;
A13:
Hom (
(dom gg),
(cod gg))
<> {}
by CAT_1:2;
then A14:
gg opp = (F /. x) opp
by OPPCAT_1:def 6;
F is
Projections_family of
c,
I
by A1;
then
dom (F /. x) = c
by A12, Th41;
then
cod ((F /. x) opp) = c opp
by A13, A14, OPPCAT_1:12;
then
cod ((F opp) /. x) = c opp
by A12, Def3;
then A15:
dom k = cod ((F opp) /. x)
by A9, CAT_1:1;
opp (k (*) ((F opp) /. x)) = opp (F9 /. x)
by A11, A12;
hence oppF9 /. x =
opp (k (*) ((F opp) /. x))
by A12, Def4
.=
(opp ((F opp) /. x)) (*) (opp k)
by A15, OPPCAT_1:18
.=
(opp ((F /. x) opp)) (*) (opp k)
by A12, Def3
.=
(F /. x) (*) (opp k)
;
verum end;
hence
h opp = k
by A8, A10;
verum
end;
assume A16:
h opp = k
;
for x being set st x in I holds
k (*) ((F opp) /. x) = F9 /. x
let x be
set ;
( x in I implies k (*) ((F opp) /. x) = F9 /. x )
assume A17:
x in I
;
k (*) ((F opp) /. x) = F9 /. x
F is
Projections_family of
c,
I
by A1;
then
dom (F /. x) = c
by A17, Th41;
then A18:
cod (opp k) = dom (F /. x)
by A10, CAT_1:1;
reconsider ff =
opp k as
Morphism of
dom (opp k),
cod (opp k) by CAT_1:4;
reconsider gg =
F /. x as
Morphism of
cod (opp k),
cod (F /. x) by A18, CAT_1:4;
A19:
(
Hom (
(dom (opp k)),
(cod (opp k)))
<> {} &
Hom (
(dom (F /. x)),
(cod (F /. x)))
<> {} )
by CAT_1:2;
then A20:
ff opp = (opp k) opp
by OPPCAT_1:def 6;
A21:
gg opp = (F /. x) opp
by A19, A18, OPPCAT_1:def 6;
(F /. x) (*) (opp k) = oppF9 /. x
by A8, A10, A17, A16;
then
((opp k) opp) (*) ((F /. x) opp) = (oppF9 /. x) opp
by A18, A20, A21, A19, OPPCAT_1:16;
hence k (*) ((F opp) /. x) =
(oppF9 /. x) opp
by A17, Def3
.=
(opp (F9 /. x)) opp
by A17, Def4
.=
F9 /. x
;
verum
end;
assume A22:
c opp is_a_coproduct_wrt F opp
; c is_a_product_wrt F
then
F opp is Injections_family of c opp ,I
;
hence
F is Projections_family of c,I
by Th68; CAT_3:def 14 for b being Object of C
for F9 being Projections_family of b,I st cods F = cods F9 holds
ex h being Morphism of C st
( h in Hom (b,c) & ( for k being Morphism of C st k in Hom (b,c) holds
( ( for x being set st x in I holds
(F /. x) (*) k = F9 /. x ) iff h = k ) ) )
let d be Object of C; for F9 being Projections_family of d,I st cods F = cods F9 holds
ex h being Morphism of C st
( h in Hom (d,c) & ( for k being Morphism of C st k in Hom (d,c) holds
( ( for x being set st x in I holds
(F /. x) (*) k = F9 /. x ) iff h = k ) ) )
let F9 be Projections_family of d,I; ( cods F = cods F9 implies ex h being Morphism of C st
( h in Hom (d,c) & ( for k being Morphism of C st k in Hom (d,c) holds
( ( for x being set st x in I holds
(F /. x) (*) k = F9 /. x ) iff h = k ) ) ) )
assume A23:
cods F = cods F9
; ex h being Morphism of C st
( h in Hom (d,c) & ( for k being Morphism of C st k in Hom (d,c) holds
( ( for x being set st x in I holds
(F /. x) (*) k = F9 /. x ) iff h = k ) ) )
A24:
now for x being set st x in I holds
(doms (F opp)) /. x = (doms (F9 opp)) /. xlet x be
set ;
( x in I implies (doms (F opp)) /. x = (doms (F9 opp)) /. x )reconsider gg =
F /. x as
Morphism of
dom (F /. x),
cod (F /. x) by CAT_1:4;
A25:
Hom (
(dom gg),
(cod gg))
<> {}
by CAT_1:2;
then A26:
gg opp = (F /. x) opp
by OPPCAT_1:def 6;
reconsider g9 =
F9 /. x as
Morphism of
dom (F9 /. x),
cod (F9 /. x) by CAT_1:4;
A27:
Hom (
(dom g9),
(cod g9))
<> {}
by CAT_1:2;
then A28:
g9 opp = (F9 /. x) opp
by OPPCAT_1:def 6;
assume A29:
x in I
;
(doms (F opp)) /. x = (doms (F9 opp)) /. xhence (doms (F opp)) /. x =
dom ((F opp) /. x)
by Def1
.=
dom (gg opp)
by A29, Def3, A26
.=
cod (F /. x)
by A25, OPPCAT_1:10
.=
(cods F9) /. x
by A23, A29, Def2
.=
cod (F9 /. x)
by A29, Def2
.=
dom (g9 opp)
by A27, OPPCAT_1:10
.=
dom ((F9 opp) /. x)
by A29, Def3, A28
.=
(doms (F9 opp)) /. x
by A29, Def1
;
verum end;
reconsider F9opp = F9 opp as Injections_family of d opp ,I by Th68;
consider h being Morphism of (C opp) such that
A30:
h in Hom ((c opp),(d opp))
and
A31:
for k being Morphism of (C opp) st k in Hom ((c opp),(d opp)) holds
( ( for x being set st x in I holds
k (*) ((F opp) /. x) = F9opp /. x ) iff h = k )
by A22, A24, Th1;
take
opp h
; ( opp h in Hom (d,c) & ( for k being Morphism of C st k in Hom (d,c) holds
( ( for x being set st x in I holds
(F /. x) (*) k = F9 /. x ) iff opp h = k ) ) )
opp h in Hom ((opp (d opp)),(opp (c opp)))
by A30, OPPCAT_1:6;
hence
opp h in Hom (d,c)
; for k being Morphism of C st k in Hom (d,c) holds
( ( for x being set st x in I holds
(F /. x) (*) k = F9 /. x ) iff opp h = k )
let k be Morphism of C; ( k in Hom (d,c) implies ( ( for x being set st x in I holds
(F /. x) (*) k = F9 /. x ) iff opp h = k ) )
assume A32:
k in Hom (d,c)
; ( ( for x being set st x in I holds
(F /. x) (*) k = F9 /. x ) iff opp h = k )
then A33:
k opp in Hom ((c opp),(d opp))
by OPPCAT_1:5;
thus
( ( for x being set st x in I holds
(F /. x) (*) k = F9 /. x ) implies opp h = k )
( opp h = k implies for x being set st x in I holds
(F /. x) (*) k = F9 /. x )proof
assume A34:
for
x being
set st
x in I holds
(F /. x) (*) k = F9 /. x
;
opp h = k
now for x being set st x in I holds
F9opp /. x = (k opp) (*) ((F opp) /. x)let x be
set ;
( x in I implies F9opp /. x = (k opp) (*) ((F opp) /. x) )assume A35:
x in I
;
F9opp /. x = (k opp) (*) ((F opp) /. x)reconsider gg =
F /. x as
Morphism of
dom (F /. x),
cod (F /. x) by CAT_1:4;
A36:
Hom (
(dom gg),
(cod gg))
<> {}
by CAT_1:2;
then A37:
gg opp = (F /. x) opp
by OPPCAT_1:def 6;
F opp is
Injections_family of
c opp ,
I
by A22;
then
cod ((F opp) /. x) = c opp
by A35, Th62;
then
cod (gg opp) = c opp
by A35, Def3, A37;
then
dom (F /. x) = c
by A36, OPPCAT_1:10;
then A38:
cod k = dom (F /. x)
by A32, CAT_1:1;
reconsider ff =
k as
Morphism of
dom k,
cod k by CAT_1:4;
reconsider gg =
F /. x as
Morphism of
cod k,
cod (F /. x) by A38, CAT_1:4;
A39:
(
Hom (
(dom k),
(cod k))
<> {} &
Hom (
(dom (F /. x)),
(cod (F /. x)))
<> {} )
by CAT_1:2;
then A40:
ff opp = k opp
by OPPCAT_1:def 6;
A41:
gg opp = (F /. x) opp
by A39, A38, OPPCAT_1:def 6;
(F /. x) (*) k = F9 /. x
by A34, A35;
then
(k opp) (*) ((F /. x) opp) = (F9 /. x) opp
by A38, A40, A41, A39, OPPCAT_1:16;
hence F9opp /. x =
(k opp) (*) ((F /. x) opp)
by A35, Def3
.=
(k opp) (*) ((F opp) /. x)
by A35, Def3
;
verum end;
hence
opp h = k
by A31, A33;
verum
end;
assume A42:
opp h = k
; for x being set st x in I holds
(F /. x) (*) k = F9 /. x
let x be set ; ( x in I implies (F /. x) (*) k = F9 /. x )
assume A43:
x in I
; (F /. x) (*) k = F9 /. x
reconsider gg = F /. x as Morphism of dom (F /. x), cod (F /. x) by CAT_1:4;
A44:
Hom ((dom gg),(cod gg)) <> {}
by CAT_1:2;
then A45:
gg opp = (F /. x) opp
by OPPCAT_1:def 6;
F opp is Injections_family of c opp ,I
by A22;
then
cod ((F opp) /. x) = c opp
by A43, Th62;
then
cod (gg opp) = c opp
by A43, Def3, A45;
then
dom (F /. x) = c
by A44, OPPCAT_1:10;
then A46:
cod k = dom (F /. x)
by A32, CAT_1:1;
reconsider ff = k as Morphism of dom k, cod k by CAT_1:4;
reconsider gg = F /. x as Morphism of cod k, cod (F /. x) by A46, CAT_1:4;
A47:
( Hom ((dom k),(cod k)) <> {} & Hom ((dom (F /. x)),(cod (F /. x))) <> {} )
by CAT_1:2;
then A48:
ff opp = k opp
by OPPCAT_1:def 6;
A49:
gg opp = (F /. x) opp
by A47, A46, OPPCAT_1:def 6;
(k opp) (*) ((F opp) /. x) = F9opp /. x
by A31, A33, A43, A42;
then
(k opp) (*) ((F opp) /. x) = (F9 /. x) opp
by A43, Def3;
hence F9 /. x =
(k opp) (*) ((F /. x) opp)
by A43, Def3
.=
((F /. x) (*) k) opp
by A46, A48, A49, A47, OPPCAT_1:16
.=
(F /. x) (*) k
;
verum