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_{1} being Morphism of b,a st

( f * b_{1} = id b & b_{1} * 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

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

( f * b

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