let A, B be non empty transitive with_units AltCatStr ; :: thesis: for F being contravariant Functor of A,B st F is bijective holds
ex G being Functor of B,A st
( G = F " & G is bijective & G is contravariant )
let F be contravariant Functor of A,B; :: thesis: ( F is bijective implies ex G being Functor of B,A st
( G = F " & G is bijective & G is contravariant ) )
assume A1:
F is bijective
; :: thesis: ex G being Functor of B,A st
( G = F " & G is bijective & G is contravariant )
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-reversing
by Def28;
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 Contravariant
by Def28;
A10:
F is coreflexive
by A7, Th48;
A11:
F " is Contravariant
proof
F is
Contravariant
by Def28;
then
the
ObjectMap of
F is
Contravariant
by Def14;
then consider f being
Function of the
carrier of
A,the
carrier of
B such that A12:
the
ObjectMap of
F = ~ [:f,f:]
by Def3;
[:f,f:] is
one-to-one
by A2, A12, Th10;
then A13:
f is
one-to-one
by Th8;
then A14:
(
dom (f " ) = rng f &
rng (f " ) = dom f )
by FUNCT_1:55;
[:f,f:] is
onto
by A8, A12, Th14;
then A15:
rng [:f,f:] = [:the carrier of B,the carrier of B:]
by FUNCT_2:def 3;
rng [:f,f:] = [:(rng f),(rng f):]
by FUNCT_3:88;
then
rng f = the
carrier of
B
by A15, ZFMISC_1:115;
then reconsider g =
f " as
Function of the
carrier of
B,the
carrier of
A by A14, FUNCT_2:def 1, RELSET_1:11;
take
g
;
:: according to FUNCTOR0:def 3,
FUNCTOR0:def 14 :: thesis: the ObjectMap of (F " ) = ~ [:g,g:]
A16:
[:f,f:] " = [:g,g:]
by A13, Th7;
thus the
ObjectMap of
(F " ) =
the
ObjectMap of
F "
by A1, Def39
.=
~ [:g,g:]
by A12, A13, A16, Th11
;
:: thesis: verum
end;
A17:
F " is id-preserving
by A1, A3, A5, A10, Th38;
F " is comp-reversing
by A1, A3, A6, A9, A10, Th44;
then reconsider G = F " as Functor of B,A by A4, A11, A17, Def26;
take
G
; :: thesis: ( G = F " & G is bijective & G is contravariant )
thus
G = F "
; :: thesis: ( G is bijective & G is contravariant )
thus
G is bijective
by A1, A3, Th36; :: thesis: G is contravariant
thus
G is Contravariant
by A11; :: according to FUNCTOR0:def 28 :: thesis: G is comp-reversing
thus
G is comp-reversing
by A1, A3, A6, A9, A10, Th44; :: thesis: verum