let C be Category; for a, b being Object of C
for f being Morphism of a,b holds
( f is coretraction iff f opp is retraction )
let a, b be Object of C; for f being Morphism of a,b holds
( f is coretraction iff f opp is retraction )
let f be Morphism of a,b; ( f is coretraction iff f opp is retraction )
thus
( f is coretraction implies f opp is retraction )
( f opp is retraction implies f is coretraction )proof
assume A1:
(
Hom (
a,
b)
<> {} &
Hom (
b,
a)
<> {} )
;
CAT_3:def 9 ( for g being Morphism of b,a holds not g * f = id a or f opp is retraction )
given i being
Morphism of
b,
a such that A2:
i * f = id a
;
f opp is retraction
thus
(
Hom (
(b opp),
(a opp))
<> {} &
Hom (
(a opp),
(b opp))
<> {} )
by A1, OPPCAT_1:5;
CAT_3:def 8 ex g being Morphism of a opp ,b opp st (f opp) * g = id (a opp)
take
i opp
;
(f opp) * (i opp) = id (a opp)
thus (f opp) * (i opp) =
id a
by A1, A2, OPPCAT_1:70
.=
id (a opp)
by OPPCAT_1:71
;
verum
end;
assume A3:
( Hom ((b opp),(a opp)) <> {} & Hom ((a opp),(b opp)) <> {} )
; CAT_3:def 8 ( for g being Morphism of a opp ,b opp holds not (f opp) * g = id (a opp) or f is coretraction )
given i being Morphism of a opp ,b opp such that A4:
(f opp) * i = id (a opp)
; f is coretraction
thus A5:
( Hom (a,b) <> {} & Hom (b,a) <> {} )
by A3, OPPCAT_1:5; CAT_3:def 9 ex g being Morphism of b,a st g * f = id a
take
opp i
; (opp i) * f = id a
(opp i) opp =
opp i
by A5, OPPCAT_1:def 6
.=
i
by A3, OPPCAT_1:def 7
;
hence (opp i) * f =
(f opp) * i
by A5, OPPCAT_1:70
.=
id (a opp)
by A4
.=
id a
by OPPCAT_1:71
;
verum