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 )

A4: <^(F . o2),(F . o1)^> <> {} by A3, FUNCTOR0:def 18;

assume F . a is coretraction ; :: thesis: a is coretraction

then consider b being Morphism of (F . o2),(F . o1) such that

A5: F . a is_right_inverse_of b ;

Morph-Map (F,o2,o1) is onto by A1, FUNCTOR1:15;

then rng (Morph-Map (F,o2,o1)) = <^(F . o2),(F . o1)^> ;

then consider a9 being object such that

A6: a9 in dom (Morph-Map (F,o2,o1)) and

A7: b = (Morph-Map (F,o2,o1)) . a9 by A4, FUNCT_1:def 3;

reconsider a9 = a9 as Morphism of o2,o1 by A4, A6, FUNCT_2:def 1;

take a9 ; :: according to ALTCAT_3:def 3 :: thesis: a9 is_left_inverse_of a

A8: b * (F . a) = idm (F . o1) by A5;

A9: ( dom (Morph-Map (F,o1,o1)) = <^o1,o1^> & Morph-Map (F,o1,o1) is one-to-one ) by A1, FUNCTOR1:16, FUNCT_2:def 1;

(Morph-Map (F,o1,o1)) . (idm o1) = F . (idm o1) by FUNCTOR0:def 15

.= idm (F . o1) by FUNCTOR2:1

.= (F . a9) * (F . a) by A3, A8, A4, A7, FUNCTOR0:def 15

.= F . (a9 * a) by A2, A3, FUNCTOR0:def 23

.= (Morph-Map (F,o1,o1)) . (a9 * a) by FUNCTOR0:def 15 ;

hence a9 * a = idm o1 by A9, FUNCT_1:def 4; :: according to ALTCAT_3:def 1 :: thesis: verum

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 )

A4: <^(F . o2),(F . o1)^> <> {} by A3, FUNCTOR0:def 18;

assume F . a is coretraction ; :: thesis: a is coretraction

then consider b being Morphism of (F . o2),(F . o1) such that

A5: F . a is_right_inverse_of b ;

Morph-Map (F,o2,o1) is onto by A1, FUNCTOR1:15;

then rng (Morph-Map (F,o2,o1)) = <^(F . o2),(F . o1)^> ;

then consider a9 being object such that

A6: a9 in dom (Morph-Map (F,o2,o1)) and

A7: b = (Morph-Map (F,o2,o1)) . a9 by A4, FUNCT_1:def 3;

reconsider a9 = a9 as Morphism of o2,o1 by A4, A6, FUNCT_2:def 1;

take a9 ; :: according to ALTCAT_3:def 3 :: thesis: a9 is_left_inverse_of a

A8: b * (F . a) = idm (F . o1) by A5;

A9: ( dom (Morph-Map (F,o1,o1)) = <^o1,o1^> & Morph-Map (F,o1,o1) is one-to-one ) by A1, FUNCTOR1:16, FUNCT_2:def 1;

(Morph-Map (F,o1,o1)) . (idm o1) = F . (idm o1) by FUNCTOR0:def 15

.= idm (F . o1) by FUNCTOR2:1

.= (F . a9) * (F . a) by A3, A8, A4, A7, FUNCTOR0:def 15

.= F . (a9 * a) by A2, A3, FUNCTOR0:def 23

.= (Morph-Map (F,o1,o1)) . (a9 * a) by FUNCTOR0:def 15 ;

hence a9 * a = idm o1 by A9, FUNCT_1:def 4; :: according to ALTCAT_3:def 1 :: thesis: verum