let C be Category; :: thesis: for a, b being Object of C
for f being Morphism of a,b st f is retraction & f is monic holds
f is invertible
let a, b be Object of C; :: thesis: for f being Morphism of a,b st f is retraction & f is monic holds
f is invertible
let f be Morphism of a,b; :: thesis: ( f is retraction & f is monic implies f is invertible )
assume A1: ( Hom (a,b) <> {} & Hom (b,a) <> {} ) ; :: according to CAT_3:def 8 :: thesis: ( for g being Morphism of b,a holds not f * g = id b or not f is monic or f is invertible )
given i being Morphism of b,a such that A2: f * i = id b ; :: thesis: ( not f is monic or f is invertible )
assume A3: f is monic ; :: thesis: f is invertible
thus ( Hom (a,b) <> {} & Hom (b,a) <> {} ) by A1; :: according to CAT_1:def 16 :: thesis: ex b₁ being Morphism of b,a st
( f * b₁ = id b & b₁ * f = id a )
take i ; :: thesis: ( f * i = id b & i * f = id a )
thus f * i = id b by A2; :: thesis: i * f = id a
A4: f * (i * f) = (id b) * f by A1, A2, CAT_1:25
.= f by A1, CAT_1:28
.= f * (id a) by A1, CAT_1:29 ;
Hom (a,a) <> {} ;
hence i * f = id a by A3, A4; :: thesis: verum