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₁ 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 )
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