let C be category; for o1, o2 being Object of C st <^o1,o2^> <> {} & <^o2,o1^> <> {} holds
for A being Morphism of o1,o2 st A is iso holds
( A is mono & A is epi )
let o1, o2 be Object of C; ( <^o1,o2^> <> {} & <^o2,o1^> <> {} implies for A being Morphism of o1,o2 st A is iso holds
( A is mono & A is epi ) )
assume A1:
( <^o1,o2^> <> {} & <^o2,o1^> <> {} )
; for A being Morphism of o1,o2 st A is iso holds
( A is mono & A is epi )
let A be Morphism of o1,o2; ( A is iso implies ( A is mono & A is epi ) )
assume
A is iso
; ( A is mono & A is epi )
then A2:
( A is retraction & A is coretraction )
by A1, Th6;
A3:
for o being Object of C st <^o2,o^> <> {} holds
for B, C being Morphism of o2,o st B * A = C * A holds
B = C
proof
let o be
Object of
C;
( <^o2,o^> <> {} implies for B, C being Morphism of o2,o st B * A = C * A holds
B = C )
assume A4:
<^o2,o^> <> {}
;
for B, C being Morphism of o2,o st B * A = C * A holds
B = C
let B,
C be
Morphism of
o2,
o;
( B * A = C * A implies B = C )
assume
B * A = C * A
;
B = C
then
B * (A * (A ")) = (C * A) * (A ")
by A1, A4, ALTCAT_1:21;
then
B * (idm o2) = (C * A) * (A ")
by A1, A2, Th2;
then
B * (idm o2) = C * (A * (A "))
by A1, A4, ALTCAT_1:21;
then
B * (idm o2) = C * (idm o2)
by A1, A2, Th2;
then
B = C * (idm o2)
by A4, ALTCAT_1:def 17;
hence
B = C
by A4, ALTCAT_1:def 17;
verum
end;
for o being Object of C st <^o,o1^> <> {} holds
for B, C being Morphism of o,o1 st A * B = A * C holds
B = C
proof
let o be
Object of
C;
( <^o,o1^> <> {} implies for B, C being Morphism of o,o1 st A * B = A * C holds
B = C )
assume A5:
<^o,o1^> <> {}
;
for B, C being Morphism of o,o1 st A * B = A * C holds
B = C
let B,
C be
Morphism of
o,
o1;
( A * B = A * C implies B = C )
assume
A * B = A * C
;
B = C
then
((A ") * A) * B = (A ") * (A * C)
by A1, A5, ALTCAT_1:21;
then
(idm o1) * B = (A ") * (A * C)
by A1, A2, Th2;
then
(idm o1) * B = ((A ") * A) * C
by A1, A5, ALTCAT_1:21;
then
(idm o1) * B = (idm o1) * C
by A1, A2, Th2;
then
B = (idm o1) * C
by A5, ALTCAT_1:20;
hence
B = C
by A5, ALTCAT_1:20;
verum
end;
hence
( A is mono & A is epi )
by A3; verum