let A, B be non empty transitive with_units reflexive AltCatStr ; for F being feasible FunctorStr over A,B st F is bijective holds
for G being feasible FunctorStr over B,A st FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " holds
F * G = id B
set I1 = [: the carrier of A, the carrier of A:];
set I2 = [: the carrier of B, the carrier of B:];
let F be feasible FunctorStr over A,B; ( F is bijective implies for G being feasible FunctorStr over B,A st FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " holds
F * G = id B )
assume A1:
F is bijective
; for G being feasible FunctorStr over B,A st FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " holds
F * G = id B
consider k being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F such that
A2:
k = the MorphMap of F
and
A3:
the MorphMap of (F ") = (k "") * ( the ObjectMap of F ")
by A1, FUNCTOR0:def 38;
F is injective
by A1;
then
F is one-to-one
;
then A4:
the ObjectMap of F is one-to-one
;
set OM = the ObjectMap of F;
F is surjective
by A1;
then
F is onto
;
then
the ObjectMap of F is onto
;
then A5:
rng the ObjectMap of F = [: the carrier of B, the carrier of B:]
by FUNCT_2:def 3;
F is injective
by A1;
then A6:
F is faithful
;
then A7:
the MorphMap of F is "1-1"
;
F is surjective
by A1;
then
( F is full & F is onto )
;
then consider f being ManySortedFunction of the Arrows of A, the Arrows of B * the ObjectMap of F such that
A8:
f = the MorphMap of F
and
A9:
f is "onto"
;
let G be feasible FunctorStr over B,A; ( FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F " implies F * G = id B )
assume A10:
FunctorStr(# the ObjectMap of G, the MorphMap of G #) = F "
; F * G = id B
A11:
the ObjectMap of G = the ObjectMap of F "
by A1, A10, FUNCTOR0:def 38;
FunctorStr(# the ObjectMap of G, the MorphMap of G #) is bijective
by A1, A10, FUNCTOR0:35;
then
FunctorStr(# the ObjectMap of G, the MorphMap of G #) is surjective
;
then
( FunctorStr(# the ObjectMap of G, the MorphMap of G #) is full & FunctorStr(# the ObjectMap of G, the MorphMap of G #) is onto )
;
then A12:
the ObjectMap of G is onto
;
set OMG = the ObjectMap of G;
A13:
dom the ObjectMap of F = [: the carrier of A, the carrier of A:]
by FUNCT_2:def 1;
reconsider OM = the ObjectMap of F as bifunction of the carrier of A, the carrier of B ;
A14:
[: the carrier of B, the carrier of B:] = dom ((f * the ObjectMap of G) ** ((k "") * the ObjectMap of G))
by PARTFUN1:def 2;
A15:
for i being object st i in [: the carrier of B, the carrier of B:] holds
((f * the ObjectMap of G) ** ((k "") * the ObjectMap of G)) . i = (id the Arrows of B) . i
proof
let i be
object ;
( i in [: the carrier of B, the carrier of B:] implies ((f * the ObjectMap of G) ** ((k "") * the ObjectMap of G)) . i = (id the Arrows of B) . i )
assume A16:
i in [: the carrier of B, the carrier of B:]
;
((f * the ObjectMap of G) ** ((k "") * the ObjectMap of G)) . i = (id the Arrows of B) . i
A17:
dom the
ObjectMap of
G = [: the carrier of B, the carrier of B:]
by FUNCT_2:def 1;
then A18:
(f * the ObjectMap of G) . i = k . ( the ObjectMap of G . i)
by A2, A8, A16, FUNCT_1:13;
rng the
ObjectMap of
G = [: the carrier of A, the carrier of A:]
by A12, FUNCT_2:def 3;
then A19:
the
ObjectMap of
G . i in [: the carrier of A, the carrier of A:]
by A16, A17, FUNCT_1:def 3;
then A20:
rng (f . ( the ObjectMap of G . i)) =
( the Arrows of B * the ObjectMap of F) . ( the ObjectMap of G . i)
by A9
.=
the
Arrows of
B . ( the ObjectMap of F . ( the ObjectMap of G . i))
by A13, A19, FUNCT_1:13
;
A21: the
ObjectMap of
F . ( the ObjectMap of G . i) =
(OM * (OM ")) . i
by A11, A16, A17, FUNCT_1:13
.=
(id [: the carrier of B, the carrier of B:]) . i
by A4, A5, FUNCT_1:39
.=
i
by A16, FUNCT_1:18
;
(
f is
"1-1" &
dom f = [: the carrier of A, the carrier of A:] )
by A6, A8, PARTFUN1:def 2;
then A22:
f . ( the ObjectMap of G . i) is
one-to-one
by A19;
((k "") * the ObjectMap of G) . i =
(k "") . ( the ObjectMap of G . i)
by A16, A17, FUNCT_1:13
.=
(k . ( the ObjectMap of G . i)) "
by A7, A2, A8, A9, A19, MSUALG_3:def 4
;
then ((f * the ObjectMap of G) ** ((k "") * the ObjectMap of G)) . i =
(f . ( the ObjectMap of G . i)) * ((f . ( the ObjectMap of G . i)) ")
by A2, A8, A14, A16, A18, PBOOLE:def 19
.=
id ( the Arrows of B . i)
by A22, A20, A21, FUNCT_1:39
.=
(id the Arrows of B) . i
by A16, MSUALG_3:def 1
;
hence
((f * the ObjectMap of G) ** ((k "") * the ObjectMap of G)) . i = (id the Arrows of B) . i
;
verum
end;
the MorphMap of (F * G) = (f * the ObjectMap of G) ** ((k "") * the ObjectMap of G)
by A10, A3, A8, A11, FUNCTOR0:def 36;
then A23:
the MorphMap of (F * G) = id the Arrows of B
by A15;
the ObjectMap of (F * G) = the ObjectMap of F * the ObjectMap of G
by FUNCTOR0:def 36;
then
the ObjectMap of (F * G) = the ObjectMap of F * ( the ObjectMap of F ")
by A1, A10, FUNCTOR0:def 38;
then
the ObjectMap of (F * G) = id [: the carrier of B, the carrier of B:]
by A4, A5, FUNCT_1:39;
hence
F * G = id B
by A23, FUNCTOR0:def 29; verum