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 ") " = 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:];
let F be feasible FunctorStr over A,B; ( F is bijective implies (F ") " = FunctorStr(# the ObjectMap of F, the MorphMap of F #) )
assume A1:
F is bijective
; (F ") " = FunctorStr(# the ObjectMap of F, the MorphMap of F #)
A2:
F is injective
by A1;
then
F is one-to-one
;
then A3:
the ObjectMap of F is one-to-one
;
A4:
F " is bijective
by A1, FUNCTOR0:35;
then
F " is surjective
;
then A5:
F " is full
;
F " is injective
by A4;
then A6:
F " is faithful
;
A7: the ObjectMap of (F ") " =
( the ObjectMap of F ") "
by A1, FUNCTOR0:def 38
.=
the ObjectMap of F
by A3, FUNCT_1:43
;
F is faithful
by A2;
then A8:
the MorphMap of F is "1-1"
;
A9:
F is surjective
by A1;
then
F is onto
;
then
the ObjectMap of F is onto
;
then A10:
rng the ObjectMap of F = [: the carrier of B, the carrier of B:]
by FUNCT_2:def 3;
A11:
F is full
by A9;
the MorphMap of ((F ") ") = the MorphMap of F
proof
A12:
ex
kk being
ManySortedFunction of the
Arrows of
B, the
Arrows of
A * the
ObjectMap of
(F ") st
(
kk = the
MorphMap of
(F ") &
kk is
"onto" )
by A5;
A13:
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 A11;
consider f being
ManySortedFunction of the
Arrows of
B, the
Arrows of
A * the
ObjectMap of
(F ") such that A14:
f = the
MorphMap of
(F ")
and A15:
the
MorphMap of
((F ") ") = (f "") * ( the ObjectMap of (F ") ")
by A4, FUNCTOR0:def 38;
consider g being
ManySortedFunction of the
Arrows of
A, the
Arrows of
B * the
ObjectMap of
F such that A16:
g = the
MorphMap of
F
and A17:
the
MorphMap of
(F ") = (g "") * ( the ObjectMap of F ")
by A1, FUNCTOR0:def 38;
A18:
f is
"1-1"
by A6, A14;
for
i being
object st
i in [: the carrier of A, the carrier of A:] holds
((f "") * ( the ObjectMap of (F ") ")) . i = the
MorphMap of
F . i
proof
A19:
the
ObjectMap of
F " is
Function of
[: the carrier of B, the carrier of B:],
[: the carrier of A, the carrier of A:]
by A3, A10, FUNCT_2:25;
let i be
object ;
( i in [: the carrier of A, the carrier of A:] implies ((f "") * ( the ObjectMap of (F ") ")) . i = the MorphMap of F . i )
assume A20:
i in [: the carrier of A, the carrier of A:]
;
((f "") * ( the ObjectMap of (F ") ")) . i = the MorphMap of F . i
then A21:
the
ObjectMap of
F . i in [: the carrier of B, the carrier of B:]
by FUNCT_2:5;
the
ObjectMap of
F " is
Function of
[: the carrier of B, the carrier of B:],
[: the carrier of A, the carrier of A:]
by A3, A10, FUNCT_2:25;
then A22:
( the ObjectMap of F ") . ( the ObjectMap of F . i) in [: the carrier of A, the carrier of A:]
by A21, FUNCT_2:5;
A23:
g . i is
one-to-one
by A8, A16, A20, MSUALG_3:1;
((f "") * ( the ObjectMap of (F ") ")) . i =
(f "") . ( the ObjectMap of F . i)
by A7, A20, FUNCT_2:15
.=
( the MorphMap of (F ") . ( the ObjectMap of F . i)) "
by A14, A12, A18, A21, MSUALG_3:def 4
.=
((g "") . (( the ObjectMap of F ") . ( the ObjectMap of F . i))) "
by A17, A20, A19, FUNCT_2:5, FUNCT_2:15
.=
((g . (( the ObjectMap of F ") . ( the ObjectMap of F . i))) ") "
by A8, A16, A13, A22, MSUALG_3:def 4
.=
((g . i) ") "
by A3, A20, FUNCT_2:26
.=
the
MorphMap of
F . i
by A16, A23, FUNCT_1:43
;
hence
((f "") * ( the ObjectMap of (F ") ")) . i = the
MorphMap of
F . i
;
verum
end;
hence
the
MorphMap of
((F ") ") = the
MorphMap of
F
by A15;
verum
end;
hence
(F ") " = FunctorStr(# the ObjectMap of F, the MorphMap of F #)
by A4, A7, FUNCTOR0:def 38; verum