let A, B be non empty transitive with_units AltCatStr ; for F being feasible FunctorStr over A,B st F is bijective holds
( F " is bijective & F " is feasible )
let F be feasible FunctorStr over A,B; ( F is bijective implies ( F " is bijective & F " is feasible ) )
assume A1:
F is bijective
; ( F " is bijective & F " is feasible )
set G = F " ;
A2:
the ObjectMap of (F ") = the ObjectMap of F "
by A1, Def38;
A3:
F is injective
by A1;
then
F is one-to-one
;
then A4:
the ObjectMap of F is one-to-one
;
hence
the ObjectMap of (F ") is one-to-one
by A2; FUNCTOR0:def 6,FUNCTOR0:def 33,FUNCTOR0:def 35 ( F " is faithful & F " is surjective & F " is feasible )
F is faithful
by A3;
then A5:
the MorphMap of F is "1-1"
;
A6:
F is surjective
by A1;
then
F is onto
;
then A7:
the ObjectMap of F is onto
;
consider h being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F such that
A8:
h = the MorphMap of F
and
A9:
the MorphMap of (F ") = (h "") * ( the ObjectMap of F ")
by A1, Def38;
F is full
by A6;
then A10:
ex f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F st
( f = the MorphMap of F & f is "onto" )
;
set AA = [: the carrier of A, the carrier of A:];
set BB = [: the carrier of B, the carrier of B:];
A11:
rng the ObjectMap of F = [: the carrier of B, the carrier of B:]
by A7;
reconsider f = the MorphMap of (F ") as ManySortedFunction of the Arrows of B, the Arrows of A * the ObjectMap of (F ") by Def4;
f is "1-1"
proof
let i be
set ;
MSUALG_3:def 2 for b1 being set holds
( not i in proj1 f or not f . i = b1 or b1 is one-to-one )let g be
Function;
( not i in proj1 f or not f . i = g or g is one-to-one )
assume that A12:
i in dom f
and A13:
f . i = g
;
g is one-to-one
i in [: the carrier of B, the carrier of B:]
by A12;
then A14:
i in dom ( the ObjectMap of F ")
by A4, A11, FUNCT_1:33;
then
( the ObjectMap of F ") . i in rng ( the ObjectMap of F ")
by FUNCT_1:def 3;
then A15:
( the ObjectMap of F ") . i in dom the
ObjectMap of
F
by A4, FUNCT_1:33;
then
( the ObjectMap of F ") . i in [: the carrier of A, the carrier of A:]
;
then
( the ObjectMap of F ") . i in dom h
by PARTFUN1:def 2;
then A16:
h . (( the ObjectMap of F ") . i) is
one-to-one
by A5, A8;
g =
(h "") . (( the ObjectMap of F ") . i)
by A9, A13, A14, FUNCT_1:13
.=
(h . (( the ObjectMap of F ") . i)) "
by A5, A8, A10, A15, MSUALG_3:def 4
;
hence
g is
one-to-one
by A16;
verum
end;
hence
the MorphMap of (F ") is "1-1"
; FUNCTOR0:def 30 ( F " is surjective & F " is feasible )
thus
F " is full
FUNCTOR0:def 34 ( F " is onto & F " is feasible )proof
take
f
;
FUNCTOR0:def 32 ( f = the MorphMap of (F ") & f is "onto" )
thus
f = the
MorphMap of
(F ")
;
f is "onto"
let i be
set ;
MSUALG_3:def 3 ( not i in [: the carrier of B, the carrier of B:] or proj2 (f . i) = ( the Arrows of A * the ObjectMap of (F ")) . i )
assume A17:
i in [: the carrier of B, the carrier of B:]
;
proj2 (f . i) = ( the Arrows of A * the ObjectMap of (F ")) . i
then A18:
i in dom the
ObjectMap of
(F ")
by FUNCT_2:def 1;
A19:
i in dom ( the ObjectMap of F ")
by A4, A11, A17, FUNCT_1:33;
then
( the ObjectMap of F ") . i in rng ( the ObjectMap of F ")
by FUNCT_1:def 3;
then A20:
( the ObjectMap of F ") . i in dom the
ObjectMap of
F
by A4, FUNCT_1:33;
then
( the ObjectMap of F ") . i in [: the carrier of A, the carrier of A:]
;
then
the
ObjectMap of
(F ") . i in dom h
by A2, PARTFUN1:def 2;
then A21:
h . ( the ObjectMap of (F ") . i) is
one-to-one
by A5, A8;
set j = the
ObjectMap of
(F ") . i;
A22:
h . ( the ObjectMap of (F ") . i) is
Function of
( the Arrows of A . ( the ObjectMap of (F ") . i)),
(( the Arrows of B * the ObjectMap of F) . ( the ObjectMap of (F ") . i))
by A2, A20, PBOOLE:def 15;
consider o1,
o2 being
Element of
A such that A23:
the
ObjectMap of
(F ") . i = [o1,o2]
by A2, A20, DOMAIN_1:1;
reconsider o1 =
o1,
o2 =
o2 as
Object of
A ;
f . i =
(h "") . (( the ObjectMap of F ") . i)
by A9, A19, FUNCT_1:13
.=
(h . (( the ObjectMap of F ") . i)) "
by A5, A8, A10, A20, MSUALG_3:def 4
;
hence rng (f . i) =
dom (h . ( the ObjectMap of (F ") . i))
by A2, A21, FUNCT_1:33
.=
the
Arrows of
A . ( the ObjectMap of (F ") . i)
by A22, A24, FUNCT_2:def 1
.=
( the Arrows of A * the ObjectMap of (F ")) . i
by A18, FUNCT_1:13
;
verum
end;
thus rng the ObjectMap of (F ") =
dom the ObjectMap of F
by A2, A4, FUNCT_1:33
.=
[: the carrier of A, the carrier of A:]
by FUNCT_2:def 1
; FUNCT_2:def 3,FUNCTOR0:def 7 F " is feasible
let o1, o2 be Object of B; FUNCTOR0:def 11 ( <^o1,o2^> <> {} implies the Arrows of A . ( the ObjectMap of (F ") . (o1,o2)) <> {} )
assume
<^o1,o2^> <> {}
; the Arrows of A . ( the ObjectMap of (F ") . (o1,o2)) <> {}
then A25:
the Arrows of B . (o1,o2) <> {}
by ALTCAT_1:def 1;
A26:
[o1,o2] in [: the carrier of B, the carrier of B:]
by ZFMISC_1:87;
then consider p1, p2 being Element of A such that
A27:
the ObjectMap of (F ") . [o1,o2] = [p1,p2]
by DOMAIN_1:1, FUNCT_2:5;
reconsider p1 = p1, p2 = p2 as Object of A ;
[o1,o2] in dom the ObjectMap of (F ")
by A26, FUNCT_2:def 1;
then A28: the ObjectMap of F . (p1,p2) =
( the ObjectMap of F * the ObjectMap of (F ")) . [o1,o2]
by A27, FUNCT_1:13
.=
(id [: the carrier of B, the carrier of B:]) . [o1,o2]
by A2, A4, A11, FUNCT_1:39
.=
[o1,o2]
by A26, FUNCT_1:18
;
assume A29:
the Arrows of A . ( the ObjectMap of (F ") . (o1,o2)) = {}
; contradiction
A30:
[p1,p2] in [: the carrier of A, the carrier of A:]
by ZFMISC_1:87;
then A31:
[p1,p2] in dom the ObjectMap of F
by FUNCT_2:def 1;
h . [p1,p2] is Function of ( the Arrows of A . [p1,p2]),(( the Arrows of B * the ObjectMap of F) . [p1,p2])
by A30, PBOOLE:def 15;
then {} =
rng (h . [p1,p2])
by A27, A29
.=
( the Arrows of B * the ObjectMap of F) . [p1,p2]
by A8, A10, A30
.=
the Arrows of B . [o1,o2]
by A28, A31, FUNCT_1:13
;
hence
contradiction
by A25; verum