let A, B be non empty transitive with_units AltCatStr ; for F being contravariant Functor of A,B
for o1, o2 being object of
for a being Morphism of , st F is full & F is faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F . a is retraction holds
a is coretraction
let F be contravariant Functor of A,B; for o1, o2 being object of
for a being Morphism of , st F is full & F is faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F . a is retraction holds
a is coretraction
let o1, o2 be object of ; for a being Morphism of , st F is full & F is faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F . a is retraction holds
a is coretraction
let a be Morphism of ,; ( F is full & F is faithful & <^o1,o2^> <> {} & <^o2,o1^> <> {} & F . a is retraction implies a is coretraction )
assume that
A1:
( F is full & F is faithful )
and
A2:
<^o1,o2^> <> {}
and
A3:
<^o2,o1^> <> {}
; ( not F . a is retraction or a is coretraction )
A4:
<^(F . o1),(F . o2)^> <> {}
by A3, FUNCTOR0:def 20;
assume
F . a is retraction
; a is coretraction
then consider b being Morphism of , such that
A5:
b is_right_inverse_of F . a
by ALTCAT_3:def 2;
Morph-Map F,o2,o1 is onto
by A1, Th14;
then
rng (Morph-Map F,o2,o1) = <^(F . o1),(F . o2)^>
by FUNCT_2:def 3;
then consider a' being set such that
A6:
a' in dom (Morph-Map F,o2,o1)
and
A7:
b = (Morph-Map F,o2,o1) . a'
by A4, FUNCT_1:def 5;
reconsider a' = a' as Morphism of , by A4, A6, FUNCT_2:def 1;
take
a'
; ALTCAT_3:def 3 a' is_left_inverse_of a
A8:
(F . a) * b = idm (F . o1)
by A5, ALTCAT_3:def 1;
A9:
( dom (Morph-Map F,o1,o1) = <^o1,o1^> & Morph-Map F,o1,o1 is one-to-one )
by A1, Th15, FUNCT_2:def 1;
(Morph-Map F,o1,o1) . (idm o1) =
F . (idm o1)
by FUNCTOR0:def 17
.=
idm (F . o1)
by Th13
.=
(F . a) * (F . a')
by A3, A8, A4, A7, FUNCTOR0:def 17
.=
F . (a' * a)
by A2, A3, FUNCTOR0:def 25
.=
(Morph-Map F,o1,o1) . (a' * a)
by FUNCTOR0:def 17
;
hence
a' * a = idm o1
by A9, FUNCT_1:def 8; ALTCAT_3:def 1 verum