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

for f being Morphism of a,b

for T being Functor of C,D st f is coretraction holds

T /. f is coretraction

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

for T being Functor of C,D st f is coretraction holds

T /. f is coretraction

let f be Morphism of a,b; :: thesis: for T being Functor of C,D st f is coretraction holds

T /. f is coretraction

let T be Functor of C,D; :: thesis: ( f is coretraction implies T /. f is coretraction )

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 T /. f is coretraction )

given i being Morphism of b,a such that A2: i * f = id a ; :: thesis: T /. f is coretraction

thus ( Hom ((T . a),(T . b)) <> {} & Hom ((T . b),(T . a)) <> {} ) by A1, CAT_1:84; :: according to CAT_3:def 9 :: thesis: ex g being Morphism of T . b,T . a st g * (T /. f) = id (T . a)

take T /. i ; :: thesis: (T /. i) * (T /. f) = id (T . a)

thus (T /. i) * (T /. f) = T /. (id a) by A1, A2, Lm1

.= id (T . a) by Lm2 ; :: thesis: verum

for f being Morphism of a,b

for T being Functor of C,D st f is coretraction holds

T /. f is coretraction

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

for T being Functor of C,D st f is coretraction holds

T /. f is coretraction

let f be Morphism of a,b; :: thesis: for T being Functor of C,D st f is coretraction holds

T /. f is coretraction

let T be Functor of C,D; :: thesis: ( f is coretraction implies T /. f is coretraction )

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 T /. f is coretraction )

given i being Morphism of b,a such that A2: i * f = id a ; :: thesis: T /. f is coretraction

thus ( Hom ((T . a),(T . b)) <> {} & Hom ((T . b),(T . a)) <> {} ) by A1, CAT_1:84; :: according to CAT_3:def 9 :: thesis: ex g being Morphism of T . b,T . a st g * (T /. f) = id (T . a)

take T /. i ; :: thesis: (T /. i) * (T /. f) = id (T . a)

thus (T /. i) * (T /. f) = T /. (id a) by A1, A2, Lm1

.= id (T . a) by Lm2 ; :: thesis: verum