let C be Category; :: thesis: 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; :: thesis: for f being Morphism of a,b holds

( f is coretraction iff f opp is retraction )

let f be Morphism of a,b; :: thesis: ( f is coretraction iff f opp is retraction )

thus ( f is coretraction implies f opp is retraction ) :: thesis: ( f opp is retraction implies f is coretraction )

given i being Morphism of a opp ,b opp such that A4: (f opp) * i = id (a opp) ; :: thesis: f is coretraction

thus A5: ( Hom (a,b) <> {} & Hom (b,a) <> {} ) by A3, OPPCAT_1:5; :: according to CAT_3:def 9 :: thesis: ex g being Morphism of b,a st g * f = id a

take opp i ; :: thesis: (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 ;

:: thesis: verum

for f being Morphism of a,b holds

( f is coretraction iff f opp is retraction )

let a, b be Object of C; :: thesis: for f being Morphism of a,b holds

( f is coretraction iff f opp is retraction )

let f be Morphism of a,b; :: thesis: ( f is coretraction iff f opp is retraction )

thus ( f is coretraction implies f opp is retraction ) :: thesis: ( f opp is retraction implies f is coretraction )

proof

assume A3:
( Hom ((b opp),(a opp)) <> {} & Hom ((a opp),(b opp)) <> {} )
; :: according to CAT_3:def 8 :: thesis: ( for g being Morphism of a opp ,b opp holds not (f opp) * g = id (a opp) or f is coretraction )
assume A1:
( Hom (a,b) <> {} & Hom (b,a) <> {} )
; :: according to CAT_3:def 9 :: thesis: ( 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 ; :: thesis: f opp is retraction

thus ( Hom ((b opp),(a opp)) <> {} & Hom ((a opp),(b opp)) <> {} ) by A1, OPPCAT_1:5; :: according to CAT_3:def 8 :: thesis: ex g being Morphism of a opp ,b opp st (f opp) * g = id (a opp)

take i opp ; :: thesis: (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 ; :: thesis: verum

end;given i being Morphism of b,a such that A2: i * f = id a ; :: thesis: f opp is retraction

thus ( Hom ((b opp),(a opp)) <> {} & Hom ((a opp),(b opp)) <> {} ) by A1, OPPCAT_1:5; :: according to CAT_3:def 8 :: thesis: ex g being Morphism of a opp ,b opp st (f opp) * g = id (a opp)

take i opp ; :: thesis: (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 ; :: thesis: verum

given i being Morphism of a opp ,b opp such that A4: (f opp) * i = id (a opp) ; :: thesis: f is coretraction

thus A5: ( Hom (a,b) <> {} & Hom (b,a) <> {} ) by A3, OPPCAT_1:5; :: according to CAT_3:def 9 :: thesis: ex g being Morphism of b,a st g * f = id a

take opp i ; :: thesis: (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 ;

:: thesis: verum