let C be Category; :: thesis: for a, b being Object of C

for f being Morphism of a,b st f is coretraction & f is epi holds

f is invertible

let a, b be Object of C; :: thesis: for f being Morphism of a,b st f is coretraction & f is epi holds

f is invertible

let f be Morphism of a,b; :: thesis: ( f is coretraction & f is epi implies f is invertible )

assume A1: ( Hom (a,b) <> {} & Hom (b,a) <> {} ) ; :: according to CAT_3:def 9 :: thesis: ( for g being Morphism of b,a holds not g * f = id a or not f is epi or f is invertible )

given i being Morphism of b,a such that A2: i * f = id a ; :: thesis: ( not f is epi or f is invertible )

assume A3: f is epi ; :: 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 )

A4: (f * i) * f = f * (id a) by A1, A2, CAT_1:25

.= f by A1, CAT_1:29

.= (id b) * f by A1, CAT_1:28 ;

Hom (b,b) <> {} ;

hence f * i = id b by A3, A4; :: thesis: i * f = id a

thus i * f = id a by A2; :: thesis: verum

for f being Morphism of a,b st f is coretraction & f is epi holds

f is invertible

let a, b be Object of C; :: thesis: for f being Morphism of a,b st f is coretraction & f is epi holds

f is invertible

let f be Morphism of a,b; :: thesis: ( f is coretraction & f is epi implies f is invertible )

assume A1: ( Hom (a,b) <> {} & Hom (b,a) <> {} ) ; :: according to CAT_3:def 9 :: thesis: ( for g being Morphism of b,a holds not g * f = id a or not f is epi or f is invertible )

given i being Morphism of b,a such that A2: i * f = id a ; :: thesis: ( not f is epi or f is invertible )

assume A3: f is epi ; :: 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 )

A4: (f * i) * f = f * (id a) by A1, A2, CAT_1:25

.= f by A1, CAT_1:29

.= (id b) * f by A1, CAT_1:28 ;

Hom (b,b) <> {} ;

hence f * i = id b by A3, A4; :: thesis: i * f = id a

thus i * f = id a by A2; :: thesis: verum