let A, B be non empty transitive with_units AltCatStr ; 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; 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; 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; ( 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^> <> {}
; ( not F . a is coretraction or a is coretraction )
A4:
<^(F . o2),(F . o1)^> <> {}
by A3, FUNCTOR0:def 18;
assume
F . a is coretraction
; 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
; ALTCAT_3:def 3 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; ALTCAT_3:def 1 verum