let A, B be non empty transitive with_units reflexive AltCatStr ; for F being feasible FunctorStr over 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 over 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 38;
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
object such that A7:
(
o1 in the
carrier of
A &
o2 in the
carrier of
A )
and A8:
i = [o1,o2]
by ZFMISC_1:84;
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 1
;
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:15;
hence
the
Arrows of
A . i = {}
by A9, FUNCTOR0:def 11;
verum
end;
F is injective
by A1;
then
F is faithful
;
then A10:
the MorphMap of F is "1-1"
;
for i being object 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 ""
;
F is injective
by A1;
then
F is one-to-one
;
then A13:
the ObjectMap of F is one-to-one
;
the ObjectMap of ((F ") * F) = the ObjectMap of (F ") * the ObjectMap of F
by FUNCTOR0:def 36;
then
the ObjectMap of ((F ") * F) = ( the ObjectMap of F ") * the ObjectMap of F
by A1, FUNCTOR0:def 38;
then A14:
the ObjectMap of ((F ") * F) = id [: the carrier of A, the carrier of A:]
by A13, A4, FUNCT_1:39;
F is surjective
by A1;
then
( F is full & F is onto )
;
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" )
;
the MorphMap of ((F ") * F) =
(((f "") * ( the ObjectMap of F ")) * the ObjectMap of F) ** f
by A2, A3, FUNCTOR0:def 36
.=
((f "") * (( the ObjectMap of F ") * the ObjectMap of F)) ** f
by RELAT_1:36
;
then
the MorphMap of ((F ") * F) = ((f "") * (id [: the carrier of A, the carrier of A:])) ** f
by A13, A4, FUNCT_1:39;
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 29; verum