let C be Category; :: thesis: for a, b being Object of C

for f being Morphism of a,b holds

( f is retraction iff f opp is coretraction )

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

( f is retraction iff f opp is coretraction )

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

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

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

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

take opp i ; :: thesis: f * (opp i) = id b

A6: (opp i) opp = opp i by A5, OPPCAT_1:def 6

.= i by A3, OPPCAT_1:def 7 ;

thus f * (opp i) = id (b opp) by A4, A6, A5, OPPCAT_1:70

.= id b by OPPCAT_1:71 ; :: thesis: verum

for f being Morphism of a,b holds

( f is retraction iff f opp is coretraction )

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

( f is retraction iff f opp is coretraction )

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

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

proof

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

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

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

take i opp ; :: thesis: (i opp) * (f opp) = id (b opp)

thus (i opp) * (f opp) = id b by A1, A2, OPPCAT_1:70

.= id (b opp) by OPPCAT_1:71 ; :: thesis: verum

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

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

take i opp ; :: thesis: (i opp) * (f opp) = id (b opp)

thus (i opp) * (f opp) = id b by A1, A2, OPPCAT_1:70

.= id (b opp) by OPPCAT_1:71 ; :: thesis: verum

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

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

take opp i ; :: thesis: f * (opp i) = id b

A6: (opp i) opp = opp i by A5, OPPCAT_1:def 6

.= i by A3, OPPCAT_1:def 7 ;

thus f * (opp i) = id (b opp) by A4, A6, A5, OPPCAT_1:70

.= id b by OPPCAT_1:71 ; :: thesis: verum