let C be Category; 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; for f being Morphism of a,b holds
( f opp is monic iff f is epi )
let f be Morphism of a,b; ( f opp is monic iff f is epi )
thus
( f opp is monic implies f is epi )
( f is epi implies f opp is monic )proof
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
;
CAT_1:def 14 f is epi
thus A3:
Hom (
a,
b)
<> {}
by A1, Th4;
CAT_1:def 15 for b1 being Element of the carrier of C holds
( Hom (b,b1) = {} or for b2, b3 being Morphism of b,b1 holds
( not b2 * f = b3 * f or b2 = b3 ) )
let c be
Object of
C;
( Hom (b,c) = {} or for b1, b2 being Morphism of b,c holds
( not b1 * f = b2 * f or b1 = b2 ) )
assume A4:
Hom (
b,
c)
<> {}
;
for b1, b2 being Morphism of b,c holds
( not b1 * f = b2 * f or b1 = b2 )
let g1,
g2 be
Morphism of
b,
c;
( not g1 * f = g2 * f or g1 = g2 )
assume A5:
g1 * f = g2 * f
;
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
;
verum
end;
assume that
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
; CAT_1:def 15 f opp is monic
thus
Hom ((b opp),(a opp)) <> {}
by A8, Th4; CAT_1:def 14 for b1 being Element of the carrier of (C opp) holds
( Hom (b1,(b opp)) = {} or for b2, b3 being Morphism of b1,b opp holds
( not (f opp) * b2 = (f opp) * b3 or b2 = b3 ) )
let c be Object of (C opp); ( Hom (c,(b opp)) = {} or for b1, b2 being Morphism of c,b opp holds
( not (f opp) * b1 = (f opp) * b2 or b1 = b2 ) )
assume A10:
Hom (c,(b opp)) <> {}
; for b1, b2 being Morphism of c,b opp holds
( not (f opp) * b1 = (f opp) * b2 or b1 = b2 )
let f1, f2 be Morphism of c,b opp ; ( not (f opp) * f1 = (f opp) * f2 or f1 = f2 )
assume A11:
(f opp) * f1 = (f opp) * f2
; 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; verum