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