let V be non empty set ; for C being Category st Hom C c= V holds
hom?? C is Functor of [:(C opp ),C:], Ens V
let C be Category; ( Hom C c= V implies hom?? C is Functor of [:(C opp ),C:], Ens V )
A1:
for f being Morphism of (C opp ) holds opp f = f
assume A2:
Hom C c= V
; hom?? C is Functor of [:(C opp ),C:], Ens V
then
( C opp = CatStr(# the carrier of C,the carrier' of C,the Target of C,the Source of C,(~ the Comp of C),the Id of C #) & Maps (Hom C) c= Maps V )
by Th7, OPPCAT_1:def 1;
then reconsider T = hom?? C as Function of the carrier' of [:(C opp ),C:],the carrier' of (Ens V) by FUNCT_2:9;
A3:
for a being Object of (C opp ) holds opp a = a
now thus
for
c being
Object of
[:(C opp ),C:] ex
d being
Object of
(Ens V) st
T . (id c) = id d
( ( for fg being Morphism of [:(C opp ),C:] holds
( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) ) ) & ( for ff, gg being Morphism of [:(C opp ),C:] st dom gg = cod ff holds
T . (gg * ff) = (T . gg) * (T . ff) ) )proof
let c be
Object of
[:(C opp ),C:];
ex d being Object of (Ens V) st T . (id c) = id d
consider a being
Object of
(C opp ),
b being
Object of
C such that A4:
c = [a,b]
by DOMAIN_1:9;
Hom (opp a),
b in Hom C
;
then reconsider A =
Hom (opp a),
b as
Element of
V by A2;
take d =
@ A;
T . (id c) = id d
id c =
[(id a),(id b)]
by A4, CAT_2:41
.=
[(opp (id a)),(id b)]
by A1
.=
[(id (opp a)),(id b)]
by OPPCAT_1:22
;
hence
T . (id c) = id d
by A2, Lm10;
verum
end; thus
for
fg being
Morphism of
[:(C opp ),C:] holds
(
T . (id (dom fg)) = id (dom (T . fg)) &
T . (id (cod fg)) = id (cod (T . fg)) )
for ff, gg being Morphism of [:(C opp ),C:] st dom gg = cod ff holds
T . (gg * ff) = (T . gg) * (T . ff)proof
let fg be
Morphism of
[:(C opp ),C:];
( T . (id (dom fg)) = id (dom (T . fg)) & T . (id (cod fg)) = id (cod (T . fg)) )
consider f being
Morphism of
(C opp ),
g being
Morphism of
C such that A5:
fg = [f,g]
by DOMAIN_1:9;
(
Hom (cod (opp f)),
(dom g) in Hom C &
Hom (dom (opp f)),
(cod g) in Hom C )
;
then reconsider A =
Hom (cod (opp f)),
(dom g),
B =
Hom (dom (opp f)),
(cod g) as
Element of
V by A2;
set h =
T . fg;
opp f = f
by A1;
then A6:
[[(Hom (cod (opp f)),(dom g)),(Hom (dom (opp f)),(cod g))],(hom (opp f),g)] =
@ (T . fg)
by A5, Def25
.=
[[(dom (@ (T . fg))),(cod (@ (T . fg)))],((@ (T . fg)) `2 )]
by Th8
.=
[[(dom (T . fg)),(cod (@ (T . fg)))],((@ (T . fg)) `2 )]
by Def10
.=
[[(dom (T . fg)),(cod (T . fg))],((@ (T . fg)) `2 )]
by Def11
;
thus T . (id (dom fg)) =
T . (id [(dom f),(dom g)])
by A5, CAT_2:38
.=
T . [(id (dom f)),(id (dom g))]
by CAT_2:41
.=
T . [(opp (id (dom f))),(id (dom g))]
by A1
.=
T . [(id (opp (dom f))),(id (dom g))]
by OPPCAT_1:22
.=
T . [(id (cod (opp f))),(id (dom g))]
by OPPCAT_1:12
.=
id (@ A)
by A2, Lm10
.=
id (dom (T . fg))
by A6, Lm1
;
T . (id (cod fg)) = id (cod (T . fg))
thus T . (id (cod fg)) =
T . (id [(cod f),(cod g)])
by A5, CAT_2:38
.=
T . [(id (cod f)),(id (cod g))]
by CAT_2:41
.=
T . [(opp (id (cod f))),(id (cod g))]
by A1
.=
T . [(id (opp (cod f))),(id (cod g))]
by OPPCAT_1:22
.=
T . [(id (dom (opp f))),(id (cod g))]
by OPPCAT_1:12
.=
id (@ B)
by A2, Lm10
.=
id (cod (T . fg))
by A6, Lm1
;
verum
end; let ff,
gg be
Morphism of
[:(C opp ),C:];
( dom gg = cod ff implies T . (gg * ff) = (T . gg) * (T . ff) )assume A7:
dom gg = cod ff
;
T . (gg * ff) = (T . gg) * (T . ff)consider g being
Morphism of
(C opp ),
g9 being
Morphism of
C such that A8:
gg = [g,g9]
by DOMAIN_1:9;
opp g = g
by A1;
then A9:
[[(Hom (cod (opp g)),(dom g9)),(Hom (dom (opp g)),(cod g9))],(hom (opp g),g9)] =
@ (T . gg)
by A8, Def25
.=
[[(dom (@ (T . gg))),(cod (@ (T . gg)))],((@ (T . gg)) `2 )]
by Th8
.=
[[(dom (T . gg)),(cod (@ (T . gg)))],((@ (T . gg)) `2 )]
by Def10
.=
[[(dom (T . gg)),(cod (T . gg))],((@ (T . gg)) `2 )]
by Def11
;
then A10:
(@ (T . gg)) `2 = hom (opp g),
g9
by ZFMISC_1:33;
cod (T . gg) = Hom (dom (opp g)),
(cod g9)
by A9, Lm1;
then A11:
cod (@ (T . gg)) = Hom (dom (opp g)),
(cod g9)
by Def11;
A12:
dom (T . gg) = Hom (cod (opp g)),
(dom g9)
by A9, Lm1;
then A13:
dom (@ (T . gg)) = Hom (cod (opp g)),
(dom g9)
by Def10;
consider f being
Morphism of
(C opp ),
f9 being
Morphism of
C such that A14:
ff = [f,f9]
by DOMAIN_1:9;
opp f = f
by A1;
then A15:
[[(Hom (cod (opp f)),(dom f9)),(Hom (dom (opp f)),(cod f9))],(hom (opp f),f9)] =
@ (T . ff)
by A14, Def25
.=
[[(dom (@ (T . ff))),(cod (@ (T . ff)))],((@ (T . ff)) `2 )]
by Th8
.=
[[(dom (T . ff)),(cod (@ (T . ff)))],((@ (T . ff)) `2 )]
by Def10
.=
[[(dom (T . ff)),(cod (T . ff))],((@ (T . ff)) `2 )]
by Def11
;
then A16:
(@ (T . ff)) `2 = hom (opp f),
f9
by ZFMISC_1:33;
dom (T . ff) = Hom (cod (opp f)),
(dom f9)
by A15, Lm1;
then A17:
dom (@ (T . ff)) = Hom (cod (opp f)),
(dom f9)
by Def10;
A18:
cod (T . ff) = Hom (dom (opp f)),
(cod f9)
by A15, Lm1;
then A19:
cod (@ (T . ff)) = Hom (dom (opp f)),
(cod f9)
by Def11;
A20:
cod ff = [(cod f),(cod f9)]
by A14, CAT_2:38;
then A21:
cod ff =
[(opp (cod f)),(cod f9)]
by A3
.=
[(dom (opp f)),(cod f9)]
by OPPCAT_1:12
;
A22:
dom gg = [(dom g),(dom g9)]
by A8, CAT_2:38;
then A23:
dom gg =
[(opp (dom g)),(dom g9)]
by A3
.=
[(cod (opp g)),(dom g9)]
by OPPCAT_1:12
;
then A24:
cod (opp g) = dom (opp f)
by A7, A21, ZFMISC_1:33;
then A25:
(
dom ((opp f) * (opp g)) = dom (opp g) &
cod ((opp f) * (opp g)) = cod (opp f) )
by CAT_1:42;
A26:
dom g = cod f
by A7, A22, A20, ZFMISC_1:33;
A27:
dom g9 = cod f9
by A7, A23, A21, ZFMISC_1:33;
then A28:
(
dom (g9 * f9) = dom f9 &
cod (g9 * f9) = cod g9 )
by CAT_1:42;
thus T . (gg * ff) =
T . [(g * f),(g9 * f9)]
by A7, A14, A8, CAT_2:40
.=
T . [(opp (g * f)),(g9 * f9)]
by A1
.=
T . [((opp f) * (opp g)),(g9 * f9)]
by A26, OPPCAT_1:19
.=
[[(Hom (cod ((opp f) * (opp g))),(dom (g9 * f9))),(Hom (dom ((opp f) * (opp g))),(cod (g9 * f9)))],(hom ((opp f) * (opp g)),(g9 * f9))]
by Def25
.=
[[(Hom (cod (opp f)),(dom f9)),(Hom (dom (opp g)),(cod g9))],((hom (opp g),g9) * (hom (opp f),f9))]
by A24, A27, A28, A25, Th56
.=
(@ (T . gg)) * (@ (T . ff))
by A16, A17, A19, A10, A13, A11, A24, A27, Def7
.=
(T . gg) * (T . ff)
by A18, A12, A24, A27, Th28
;
verum end;
hence
hom?? C is Functor of [:(C opp ),C:], Ens V
by CAT_1:96; verum