let A, B be non empty transitive with_units AltCatStr ; 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; ( 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
; ex G being Functor of B,A st
( G = F " & G is bijective & G is contravariant )
then
F is injective
;
then
F is one-to-one
;
then A2:
the ObjectMap of F is one-to-one
;
A3:
F is feasible
by Def25;
then A4:
( F " is bijective & F " is feasible )
by A1, Th35;
A5:
F is id-preserving
by Def25;
A6:
F is comp-reversing
by Def27;
F is surjective
by A1;
then A7:
F is onto
;
then A8:
the ObjectMap of F is onto
;
A9:
F is Contravariant
by Def27;
A10:
F is coreflexive
by A7, Th47;
A11:
F " is Contravariant
proof
F is
Contravariant
by Def27;
then
the
ObjectMap of
F is
Contravariant
;
then consider f being
Function of the
carrier of
A, the
carrier of
B such that A12:
the
ObjectMap of
F = ~ [:f,f:]
;
[:f,f:] is
one-to-one
by A2, A12, Th9;
then A13:
f is
one-to-one
by Th7;
then A14:
dom (f ") = rng f
by FUNCT_1:33;
A15:
rng (f ") = dom f
by A13, FUNCT_1:33;
[:f,f:] is
onto
by A8, A12, Th13;
then A16:
rng [:f,f:] = [: the carrier of B, the carrier of B:]
;
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 2,
FUNCTOR0:def 13 the ObjectMap of (F ") = ~ [:g,g:]
A17:
[:f,f:] " = [:g,g:]
by A13, Th6;
thus the
ObjectMap of
(F ") =
the
ObjectMap of
F "
by A1, Def38
.=
~ [:g,g:]
by A12, A13, A17, Th10
;
verum
end;
A18:
F " is id-preserving
by A1, A3, A5, A10, Th37;
F " is comp-reversing
by A1, A3, A6, A9, A10, Th43;
then reconsider G = F " as Functor of B,A by A4, A11, A18, Def25;
take
G
; ( G = F " & G is bijective & G is contravariant )
thus
G = F "
; ( G is bijective & G is contravariant )
thus
G is bijective
by A1, A3, Th35; G is contravariant
thus
G is Contravariant
by A11; FUNCTOR0:def 27 G is comp-reversing
thus
G is comp-reversing
by A1, A3, A6, A9, A10, Th43; verum