let C be category; ( ( for o1, o2 being Object of C
for A1 being Morphism of o1,o2 holds A1 is retraction ) implies for a, b being Object of C
for A being Morphism of a,b st <^a,b^> <> {} & <^b,a^> <> {} holds
A is iso )
assume A1:
for o1, o2 being Object of C
for A1 being Morphism of o1,o2 holds A1 is retraction
; for a, b being Object of C
for A being Morphism of a,b st <^a,b^> <> {} & <^b,a^> <> {} holds
A is iso
thus
for a, b being Object of C
for A being Morphism of a,b st <^a,b^> <> {} & <^b,a^> <> {} holds
A is iso
verumproof
let a,
b be
Object of
C;
for A being Morphism of a,b st <^a,b^> <> {} & <^b,a^> <> {} holds
A is iso let A be
Morphism of
a,
b;
( <^a,b^> <> {} & <^b,a^> <> {} implies A is iso )
assume that A2:
<^a,b^> <> {}
and A3:
<^b,a^> <> {}
;
A is iso
A4:
A is
retraction
by A1;
A is
coretraction
proof
consider A1 being
Morphism of
b,
a such that A5:
A1 is_right_inverse_of A
by A4;
A1 * (A * A1) = A1 * (idm b)
by A5;
then
A1 * (A * A1) = A1
by A3, ALTCAT_1:def 17;
then
(A1 * A) * A1 = A1
by A2, A3, ALTCAT_1:21;
then A6:
(A1 * A) * A1 = (idm a) * A1
by A3, ALTCAT_1:20;
(
A1 is
epi &
<^a,a^> <> {} )
by A1, A2, A3, Th15, ALTCAT_1:19;
then
A1 * A = idm a
by A6;
then
A1 is_left_inverse_of A
;
hence
A is
coretraction
;
verum
end;
hence
A is
iso
by A2, A3, A4, Th6;
verum
end;