let C, D be Category; 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; 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; for T being Functor of C,D st f is coretraction holds
T /. f is coretraction
let T be Functor of C,D; ( f is coretraction implies T /. f is coretraction )
assume A1:
( Hom (a,b) <> {} & Hom (b,a) <> {} )
; CAT_3:def 9 ( 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
; T /. f is coretraction
thus
( Hom ((T . a),(T . b)) <> {} & Hom ((T . b),(T . a)) <> {} )
by A1, CAT_1:84; CAT_3:def 9 ex g being Morphism of T . b,T . a st g * (T /. f) = id (T . a)
take
T /. i
; (T /. i) * (T /. f) = id (T . a)
thus (T /. i) * (T /. f) =
T /. (id a)
by A1, A2, Lm1
.=
id (T . a)
by Lm2
; verum