let C be category; :: thesis: ( ( 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
; :: thesis: 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
:: thesis: verumproof
let a,
b be
object of
C;
:: thesis: for A being Morphism of a,b st <^a,b^> <> {} & <^b,a^> <> {} holds
A is iso let A be
Morphism of
a,
b;
:: thesis: ( <^a,b^> <> {} & <^b,a^> <> {} implies A is iso )
assume A2:
(
<^a,b^> <> {} &
<^b,a^> <> {} )
;
:: thesis: A is iso
A3:
A is
retraction
by A1;
A is
coretraction
proof
consider A1 being
Morphism of
b,
a such that A4:
A1 is_right_inverse_of A
by A3, Def2;
A5:
A1 is
epi
by A1, A2, Th15;
A6:
<^a,a^> <> {}
by ALTCAT_1:23;
A1 * (A * A1) = A1 * (idm b)
by A4, Def1;
then
A1 * (A * A1) = A1
by A2, ALTCAT_1:def 19;
then
(A1 * A) * A1 = A1
by A2, ALTCAT_1:25;
then
(A1 * A) * A1 = (idm a) * A1
by A2, ALTCAT_1:24;
then
A1 * A = idm a
by A5, A6, Def8;
then
A1 is_left_inverse_of A
by Def1;
hence
A is
coretraction
by Def3;
:: thesis: verum
end;
hence
A is
iso
by A2, A3, Th6;
:: thesis: verum
end;