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 ") " = 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 of 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, FUNCTOR0:def 36;
then
F is one-to-one
by FUNCTOR0:def 34;
then A3:
the ObjectMap of F is one-to-one
by FUNCTOR0:def 7;
A4:
F " is bijective
by A1, FUNCTOR0:36;
then
F " is surjective
by FUNCTOR0:def 36;
then A5:
F " is full
by FUNCTOR0:def 35;
F " is injective
by A4, FUNCTOR0:def 36;
then A6:
F " is faithful
by FUNCTOR0:def 34;
A7: the ObjectMap of (F ") " =
( the ObjectMap of F ") "
by A1, FUNCTOR0:def 39
.=
the ObjectMap of F
by A3, FUNCT_1:65
;
F is faithful
by A2, FUNCTOR0:def 34;
then A8:
the MorphMap of F is "1-1"
by FUNCTOR0:def 31;
A9:
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 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, FUNCTOR0:def 35;
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, FUNCTOR0:def 33;
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, FUNCTOR0:def 33;
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 39;
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 39;
A18:
f is
"1-1"
by A6, A14, 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
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:31;
let i be
set ;
( 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: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 A3, A10, FUNCT_2:31;
then A22:
( the ObjectMap of F ") . ( the ObjectMap of F . i) in [: the carrier of A, the carrier of A:]
by A21, FUNCT_2:7;
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:21
.=
( the MorphMap of (F ") . ( the ObjectMap of F . i)) "
by A14, A12, A18, A21, MSUALG_3:def 5
.=
((g "") . (( the ObjectMap of F ") . ( the ObjectMap of F . i))) "
by A17, A20, A19, FUNCT_2:7, FUNCT_2:21
.=
((g . (( the ObjectMap of F ") . ( the ObjectMap of F . i))) ") "
by A8, A16, A13, A22, MSUALG_3:def 5
.=
((g . i) ") "
by A3, A20, FUNCT_2:32
.=
the
MorphMap of
F . i
by A16, A23, FUNCT_1:65
;
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, PBOOLE:3;
verum
end;
hence
(F ") " = FunctorStr(# the ObjectMap of F, the MorphMap of F #)
by A4, A7, FUNCTOR0:def 39; verum