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 " ) " = FunctorStr(# the ObjectMap of F,the MorphMap of F #)
let F be feasible FunctorStr of A,B; :: thesis: ( F is bijective implies (F " ) " = FunctorStr(# the ObjectMap of F,the MorphMap of F #) )
assume A1:
F is bijective
; :: thesis: (F " ) " = FunctorStr(# the ObjectMap of F,the MorphMap of F #)
set CCA = [:the carrier of A,the carrier of A:];
set CCB = [:the carrier of B,the carrier of B:];
A2:
F " is bijective
by A1, FUNCTOR0:36;
then A3:
F " is surjective
by FUNCTOR0:def 36;
A4:
F is injective
by A1, FUNCTOR0:def 36;
then
F is one-to-one
by FUNCTOR0:def 34;
then A5:
the ObjectMap of F is one-to-one
by FUNCTOR0:def 7;
A6:
F is surjective
by A1, FUNCTOR0:def 36;
then
F is onto
by FUNCTOR0:def 35;
then
the ObjectMap of F is onto
by FUNCTOR0:def 8;
then A7:
rng the ObjectMap of F = [:the carrier of B,the carrier of B:]
by FUNCT_2:def 3;
F is faithful
by A4, FUNCTOR0:def 34;
then A8:
the MorphMap of F is "1-1"
by FUNCTOR0:def 31;
A9:
F is full
by A6, FUNCTOR0:def 35;
A10:
F " is full
by A3, FUNCTOR0:def 35;
F " is injective
by A2, FUNCTOR0:def 36;
then A11:
F " is faithful
by FUNCTOR0:def 34;
A12: the ObjectMap of (F " ) " =
(the ObjectMap of F " ) "
by A1, FUNCTOR0:def 39
.=
the ObjectMap of F
by A5, FUNCT_1:65
;
the MorphMap of ((F " ) " ) = the MorphMap of F
proof
consider f being
ManySortedFunction of the
Arrows of
B,the
Arrows of
A * the
ObjectMap of
(F " ) such that A13:
(
f = the
MorphMap of
(F " ) & the
MorphMap of
((F " ) " ) = (f "" ) * (the ObjectMap of (F " ) " ) )
by A2, FUNCTOR0:def 39;
consider g being
ManySortedFunction of the
Arrows of
A,the
Arrows of
B * the
ObjectMap of
F such that A14:
(
g = the
MorphMap of
F & the
MorphMap of
(F " ) = (g "" ) * (the ObjectMap of F " ) )
by A1, FUNCTOR0:def 39;
consider k being
ManySortedFunction of the
Arrows of
A,the
Arrows of
B * the
ObjectMap of
F such that A15:
(
k = the
MorphMap of
F &
k is
"onto" )
by A9, FUNCTOR0:def 33;
consider kk being
ManySortedFunction of the
Arrows of
B,the
Arrows of
A * the
ObjectMap of
(F " ) such that A16:
(
kk = the
MorphMap of
(F " ) &
kk is
"onto" )
by A10, FUNCTOR0:def 33;
A17:
f is
"1-1"
by A11, A13, FUNCTOR0:def 31;
for
i being
set st
i in [:the carrier of A,the carrier of A:] holds
((f "" ) * (the ObjectMap of (F " ) " )) . i = the
MorphMap of
F . i
proof
let i be
set ;
:: thesis: ( i in [:the carrier of A,the carrier of A:] implies ((f "" ) * (the ObjectMap of (F " ) " )) . i = the MorphMap of F . i )
assume A18:
i in [:the carrier of A,the carrier of A:]
;
:: thesis: ((f "" ) * (the ObjectMap of (F " ) " )) . i = the MorphMap of F . i
then A19:
the
ObjectMap of
F . i in [:the carrier of B,the carrier of B:]
by FUNCT_2:7;
the
ObjectMap of
F " is
Function of
[:the carrier of B,the carrier of B:],
[:the carrier of A,the carrier of A:]
by A5, A7, FUNCT_2:31;
then A20:
(the ObjectMap of F " ) . (the ObjectMap of F . i) in [:the carrier of A,the carrier of A:]
by A19, FUNCT_2:7;
A21:
the
ObjectMap of
F " is
Function of
[:the carrier of B,the carrier of B:],
[:the carrier of A,the carrier of A:]
by A5, A7, FUNCT_2:31;
A22:
g . i is
one-to-one
by A8, A14, A18, MSUALG_3:1;
((f "" ) * (the ObjectMap of (F " ) " )) . i =
(f "" ) . (the ObjectMap of F . i)
by A12, A18, FUNCT_2:21
.=
(the MorphMap of (F " ) . (the ObjectMap of F . i)) "
by A13, A16, A17, A19, MSUALG_3:def 5
.=
((g "" ) . ((the ObjectMap of F " ) . (the ObjectMap of F . i))) "
by A14, A18, A21, FUNCT_2:7, FUNCT_2:21
.=
((g . ((the ObjectMap of F " ) . (the ObjectMap of F . i))) " ) "
by A8, A14, A15, A20, MSUALG_3:def 5
.=
((g . i) " ) "
by A5, A18, FUNCT_2:32
.=
the
MorphMap of
F . i
by A14, A22, FUNCT_1:65
;
hence
((f "" ) * (the ObjectMap of (F " ) " )) . i = the
MorphMap of
F . i
;
:: thesis: verum
end;
hence
the
MorphMap of
((F " ) " ) = the
MorphMap of
F
by A13, PBOOLE:3;
:: thesis: verum
end;
hence
(F " ) " = FunctorStr(# the ObjectMap of F,the MorphMap of F #)
by A2, A12, FUNCTOR0:def 39; :: thesis: verum