let A, B be non empty transitive with_units reflexive AltCatStr ; for F being feasible FunctorStr of A,B st F is bijective holds
(F " ) * F = id A
set I1 = [:the carrier of A,the carrier of A:];
let F be feasible FunctorStr of A,B; ( F is bijective implies (F " ) * F = id A )
assume A1:
F is bijective
; (F " ) * F = id A
consider f being ManySortedFunction of the Arrows of A,the Arrows of B * the ObjectMap of F such that
A2:
f = the MorphMap of F
and
A3:
the MorphMap of (F " ) = (f "" ) * (the ObjectMap of F " )
by A1, FUNCTOR0:def 39;
set OM = the ObjectMap of F;
A4:
dom the ObjectMap of F = [:the carrier of A,the carrier of A:]
by FUNCT_2:def 1;
A5:
the Arrows of A is_transformable_to the Arrows of B * the ObjectMap of F
proof
let i be
set ;
PZFMISC1:def 3 ( not i in [:the carrier of A,the carrier of A:] or not (the Arrows of B * the ObjectMap of F) . i = {} or the Arrows of A . i = {} )
assume A6:
i in [:the carrier of A,the carrier of A:]
;
( not (the Arrows of B * the ObjectMap of F) . i = {} or the Arrows of A . i = {} )
then consider o1,
o2 being
set such that A7:
(
o1 in the
carrier of
A &
o2 in the
carrier of
A )
and A8:
i = [o1,o2]
by ZFMISC_1:103;
reconsider o1 =
o1,
o2 =
o2 as
object of
A by A7;
A9: the
Arrows of
A . i =
the
Arrows of
A . o1,
o2
by A8
.=
<^o1,o2^>
by ALTCAT_1:def 2
;
assume
(the Arrows of B * the ObjectMap of F) . i = {}
;
the Arrows of A . i = {}
then
the
Arrows of
B . (the ObjectMap of F . o1,o2) = {}
by A6, A8, FUNCT_2:21;
hence
the
Arrows of
A . i = {}
by A9, FUNCTOR0:def 12;
verum
end;
F is injective
by A1, FUNCTOR0:def 36;
then
F is faithful
by FUNCTOR0:def 34;
then A10:
the MorphMap of F is "1-1"
by FUNCTOR0:def 31;
for i being set st i in [:the carrier of A,the carrier of A:] holds
((f "" ) * (id [:the carrier of A,the carrier of A:])) . i = (f "" ) . i
then A12:
(f "" ) * (id [:the carrier of A,the carrier of A:]) = f ""
by PBOOLE:3;
F is injective
by A1, FUNCTOR0:def 36;
then
F is one-to-one
by FUNCTOR0:def 34;
then A13:
the ObjectMap of F is one-to-one
by FUNCTOR0:def 7;
the ObjectMap of ((F " ) * F) = the ObjectMap of (F " ) * the ObjectMap of F
by FUNCTOR0:def 37;
then
the ObjectMap of ((F " ) * F) = (the ObjectMap of F " ) * the ObjectMap of F
by A1, FUNCTOR0:def 39;
then A14:
the ObjectMap of ((F " ) * F) = id [:the carrier of A,the carrier of A:]
by A13, A4, FUNCT_1:61;
F is surjective
by A1, FUNCTOR0:def 36;
then
( F is full & F is onto )
by FUNCTOR0:def 35;
then A15:
ex k being ManySortedFunction of the Arrows of A,the Arrows of B * the ObjectMap of F st
( k = the MorphMap of F & k is "onto" )
by FUNCTOR0:def 33;
the MorphMap of ((F " ) * F) =
(((f "" ) * (the ObjectMap of F " )) * the ObjectMap of F) ** f
by A2, A3, FUNCTOR0:def 37
.=
((f "" ) * ((the ObjectMap of F " ) * the ObjectMap of F)) ** f
by RELAT_1:55
;
then
the MorphMap of ((F " ) * F) = ((f "" ) * (id [:the carrier of A,the carrier of A:])) ** f
by A13, A4, FUNCT_1:61;
then
the MorphMap of ((F " ) * F) = id the Arrows of A
by A5, A2, A10, A15, A12, Lm1;
hence
(F " ) * F = id A
by A14, FUNCTOR0:def 30; verum