let A, B be non empty transitive with_units AltCatStr ; for F being covariant Functor of A,B st F is bijective holds
ex G being Functor of B,A st
( G = F " & G is bijective & G is covariant )
let F be covariant Functor of A,B; ( F is bijective implies ex G being Functor of B,A st
( G = F " & G is bijective & G is covariant ) )
assume A1:
F is bijective
; ex G being Functor of B,A st
( G = F " & G is bijective & G is covariant )
then
F is injective
by Def36;
then
F is one-to-one
by Def34;
then A2:
the ObjectMap of F is one-to-one
by Def7;
A3:
F is feasible
by Def26;
then A4:
( F " is bijective & F " is feasible )
by A1, Th36;
A5:
F is id-preserving
by Def26;
A6:
F is comp-preserving
by Def27;
F is surjective
by A1, Def36;
then A7:
F is onto
by Def35;
then A8:
the ObjectMap of F is onto
by Def8;
A9:
F is Covariant
by Def27;
A10:
F is coreflexive
by A7, Th47;
A11:
F " is Covariant
proof
F is
Covariant
by Def27;
then
the
ObjectMap of
F is
Covariant
by Def13;
then consider f being
Function of the
carrier of
A, the
carrier of
B such that A12:
the
ObjectMap of
F = [:f,f:]
by Def2;
A13:
f is
one-to-one
by A2, A12, Th8;
then A14:
dom (f ") = rng f
by FUNCT_1:33;
A15:
rng (f ") = dom f
by A13, FUNCT_1:33;
A16:
rng [:f,f:] = [: the carrier of B, the carrier of B:]
by A8, A12, FUNCT_2:def 3;
rng [:f,f:] = [:(rng f),(rng f):]
by FUNCT_3:67;
then
rng f = the
carrier of
B
by A16, ZFMISC_1:92;
then reconsider g =
f " as
Function of the
carrier of
B, the
carrier of
A by A14, A15, FUNCT_2:def 1, RELSET_1:4;
take
g
;
FUNCTOR0:def 1,
FUNCTOR0:def 12 the ObjectMap of (F ") = [:g,g:]
[:f,f:] " = [:g,g:]
by A13, Th7;
hence
the
ObjectMap of
(F ") = [:g,g:]
by A1, A12, Def39;
verum
end;
A17:
F " is id-preserving
by A1, A3, A5, A10, Th38;
F " is comp-preserving
by A1, A3, A6, A9, A10, Th43;
then reconsider G = F " as Functor of B,A by A4, A11, A17, Def26;
take
G
; ( G = F " & G is bijective & G is covariant )
thus
G = F "
; ( G is bijective & G is covariant )
thus
G is bijective
by A1, A3, Th36; G is covariant
thus
G is Covariant
by A11; FUNCTOR0:def 26 G is comp-preserving
thus
G is comp-preserving
by A1, A3, A6, A9, A10, Th43; verum