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

for f being Morphism of a,b holds

( f opp is monic iff f is epi )

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

( f opp is monic iff f is epi )

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

thus ( f opp is monic implies f is epi ) :: thesis: ( f is epi implies f opp is monic )

A8: Hom (a,b) <> {} and

A9: for c being Object of C st Hom (b,c) <> {} holds

for g1, g2 being Morphism of b,c st g1 * f = g2 * f holds

g1 = g2 ; :: according to CAT_1:def 15 :: thesis: f opp is monic

thus Hom ((b opp),(a opp)) <> {} by A8, Th4; :: according to CAT_1:def 14 :: thesis: for b_{1} being Element of the carrier of (C opp) holds

( Hom (b_{1},(b opp)) = {} or for b_{2}, b_{3} being Morphism of b_{1},b opp holds

( not (f opp) * b_{2} = (f opp) * b_{3} or b_{2} = b_{3} ) )

let c be Object of (C opp); :: thesis: ( Hom (c,(b opp)) = {} or for b_{1}, b_{2} being Morphism of c,b opp holds

( not (f opp) * b_{1} = (f opp) * b_{2} or b_{1} = b_{2} ) )

assume A10: Hom (c,(b opp)) <> {} ; :: thesis: for b_{1}, b_{2} being Morphism of c,b opp holds

( not (f opp) * b_{1} = (f opp) * b_{2} or b_{1} = b_{2} )

let f1, f2 be Morphism of c,b opp ; :: thesis: ( not (f opp) * f1 = (f opp) * f2 or f1 = f2 )

assume A11: (f opp) * f1 = (f opp) * f2 ; :: thesis: f1 = f2

( f1 in Hom (c,(b opp)) & f2 in Hom (c,(b opp)) ) by A10, CAT_1:def 5;

then ( f1 in Hom ((opp (b opp)),(opp c)) & f2 in Hom ((opp (b opp)),(opp c)) ) by Th5;

then reconsider g1 = opp f1, g2 = opp f2 as Morphism of b, opp c by CAT_1:def 5;

A12: Hom ((opp (b opp)),(opp c)) <> {} by A10, Th5;

A13: g1 opp = f1 by Def6, A12;

A14: g2 opp = f2 by Def6, A12;

g1 * f = (f opp) * f2 by A11, A13, A8, Lm3, A12

.= g2 * f by A8, Lm3, A12, A14 ;

hence f1 = f2 by A9, A12; :: thesis: verum

for f being Morphism of a,b holds

( f opp is monic iff f is epi )

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

( f opp is monic iff f is epi )

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

thus ( f opp is monic implies f is epi ) :: thesis: ( f is epi implies f opp is monic )

proof

assume that
assume that

A1: Hom ((b opp),(a opp)) <> {} and

A2: for c being Object of (C opp) st Hom (c,(b opp)) <> {} holds

for f1, f2 being Morphism of c,b opp st (f opp) * f1 = (f opp) * f2 holds

f1 = f2 ; :: according to CAT_1:def 14 :: thesis: f is epi

thus A3: Hom (a,b) <> {} by A1, Th4; :: according to CAT_1:def 15 :: thesis: for b_{1} being Element of the carrier of C holds

( Hom (b,b_{1}) = {} or for b_{2}, b_{3} being Morphism of b,b_{1} holds

( not b_{2} * f = b_{3} * f or b_{2} = b_{3} ) )

let c be Object of C; :: thesis: ( Hom (b,c) = {} or for b_{1}, b_{2} being Morphism of b,c holds

( not b_{1} * f = b_{2} * f or b_{1} = b_{2} ) )

assume A4: Hom (b,c) <> {} ; :: thesis: for b_{1}, b_{2} being Morphism of b,c holds

( not b_{1} * f = b_{2} * f or b_{1} = b_{2} )

let g1, g2 be Morphism of b,c; :: thesis: ( not g1 * f = g2 * f or g1 = g2 )

assume A5: g1 * f = g2 * f ; :: thesis: g1 = g2

reconsider f1 = g1 opp , f2 = g2 opp as Morphism of c opp ,b opp ;

A6: Hom ((c opp),(b opp)) <> {} by A4, Th4;

(f opp) * f1 = g1 * f by A4, Lm3, A3

.= (f opp) * f2 by A4, Lm3, A3, A5 ;

then A7: f1 = f2 by A2, A6;

g1 = f1 by A4, Def6

.= g2 by A7, A4, Def6 ;

hence g1 = g2 ; :: thesis: verum

end;A1: Hom ((b opp),(a opp)) <> {} and

A2: for c being Object of (C opp) st Hom (c,(b opp)) <> {} holds

for f1, f2 being Morphism of c,b opp st (f opp) * f1 = (f opp) * f2 holds

f1 = f2 ; :: according to CAT_1:def 14 :: thesis: f is epi

thus A3: Hom (a,b) <> {} by A1, Th4; :: according to CAT_1:def 15 :: thesis: for b

( Hom (b,b

( not b

let c be Object of C; :: thesis: ( Hom (b,c) = {} or for b

( not b

assume A4: Hom (b,c) <> {} ; :: thesis: for b

( not b

let g1, g2 be Morphism of b,c; :: thesis: ( not g1 * f = g2 * f or g1 = g2 )

assume A5: g1 * f = g2 * f ; :: thesis: g1 = g2

reconsider f1 = g1 opp , f2 = g2 opp as Morphism of c opp ,b opp ;

A6: Hom ((c opp),(b opp)) <> {} by A4, Th4;

(f opp) * f1 = g1 * f by A4, Lm3, A3

.= (f opp) * f2 by A4, Lm3, A3, A5 ;

then A7: f1 = f2 by A2, A6;

g1 = f1 by A4, Def6

.= g2 by A7, A4, Def6 ;

hence g1 = g2 ; :: thesis: verum

A8: Hom (a,b) <> {} and

A9: for c being Object of C st Hom (b,c) <> {} holds

for g1, g2 being Morphism of b,c st g1 * f = g2 * f holds

g1 = g2 ; :: according to CAT_1:def 15 :: thesis: f opp is monic

thus Hom ((b opp),(a opp)) <> {} by A8, Th4; :: according to CAT_1:def 14 :: thesis: for b

( Hom (b

( not (f opp) * b

let c be Object of (C opp); :: thesis: ( Hom (c,(b opp)) = {} or for b

( not (f opp) * b

assume A10: Hom (c,(b opp)) <> {} ; :: thesis: for b

( not (f opp) * b

let f1, f2 be Morphism of c,b opp ; :: thesis: ( not (f opp) * f1 = (f opp) * f2 or f1 = f2 )

assume A11: (f opp) * f1 = (f opp) * f2 ; :: thesis: f1 = f2

( f1 in Hom (c,(b opp)) & f2 in Hom (c,(b opp)) ) by A10, CAT_1:def 5;

then ( f1 in Hom ((opp (b opp)),(opp c)) & f2 in Hom ((opp (b opp)),(opp c)) ) by Th5;

then reconsider g1 = opp f1, g2 = opp f2 as Morphism of b, opp c by CAT_1:def 5;

A12: Hom ((opp (b opp)),(opp c)) <> {} by A10, Th5;

A13: g1 opp = f1 by Def6, A12;

A14: g2 opp = f2 by Def6, A12;

g1 * f = (f opp) * f2 by A11, A13, A8, Lm3, A12

.= g2 * f by A8, Lm3, A12, A14 ;

hence f1 = f2 by A9, A12; :: thesis: verum