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