let V be non empty set ; for C being Category
for a being Object of C st Hom C c= V holds
hom-? a is Contravariant_Functor of C, Ens V
let C be Category; for a being Object of C st Hom C c= V holds
hom-? a is Contravariant_Functor of C, Ens V
let a be Object of C; ( Hom C c= V implies hom-? a is Contravariant_Functor of C, Ens V )
assume A1:
Hom C c= V
; hom-? a is Contravariant_Functor of C, Ens V
then reconsider T = hom-? a as Function of the carrier' of C, the carrier' of (Ens V) by Lm8;
now ( ( for c being Object of C ex d being Object of (Ens V) st T . (id c) = id d ) & ( for f being Morphism of C holds
( T . (id (dom f)) = id (cod (T . f)) & T . (id (cod f)) = id (dom (T . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
T . (g (*) f) = (T . f) (*) (T . g) ) )thus
for
c being
Object of
C ex
d being
Object of
(Ens V) st
T . (id c) = id d
( ( for f being Morphism of C holds
( T . (id (dom f)) = id (cod (T . f)) & T . (id (cod f)) = id (dom (T . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
T . (g (*) f) = (T . f) (*) (T . g) ) )thus
for
f being
Morphism of
C holds
(
T . (id (dom f)) = id (cod (T . f)) &
T . (id (cod f)) = id (dom (T . f)) )
for f, g being Morphism of C st dom g = cod f holds
T . (g (*) f) = (T . f) (*) (T . g)proof
let f be
Morphism of
C;
( T . (id (dom f)) = id (cod (T . f)) & T . (id (cod f)) = id (dom (T . f)) )
set b =
cod f;
set c =
dom f;
set g =
T . f;
(
Hom (
(cod f),
a)
in Hom C &
Hom (
(dom f),
a)
in Hom C )
;
then reconsider A =
Hom (
(cod f),
a),
B =
Hom (
(dom f),
a) as
Element of
V by A1;
A2:
[[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] =
@ (T . f)
by Def21
.=
[[(dom (@ (T . f))),(cod (@ (T . f)))],((@ (T . f)) `2)]
by Th8
.=
[[(dom (T . f)),(cod (@ (T . f)))],((@ (T . f)) `2)]
by Def9
.=
[[(dom (T . f)),(cod (T . f))],((@ (T . f)) `2)]
by Def10
;
thus T . (id (dom f)) =
id (@ B)
by A1, Lm10
.=
id (cod (T . f))
by A2, Lm1
;
T . (id (cod f)) = id (dom (T . f))
thus T . (id (cod f)) =
id (@ A)
by A1, Lm10
.=
id (dom (T . f))
by A2, Lm1
;
verum
end; let f,
g be
Morphism of
C;
( dom g = cod f implies T . (g (*) f) = (T . f) (*) (T . g) )assume A3:
dom g = cod f
;
T . (g (*) f) = (T . f) (*) (T . g)A4:
[[(Hom ((cod g),a)),(Hom ((dom g),a))],(hom (g,a))] =
@ (T . g)
by Def21
.=
[[(dom (@ (T . g))),(cod (@ (T . g)))],((@ (T . g)) `2)]
by Th8
.=
[[(dom (T . g)),(cod (@ (T . g)))],((@ (T . g)) `2)]
by Def9
.=
[[(dom (T . g)),(cod (T . g))],((@ (T . g)) `2)]
by Def10
;
then A5:
(@ (T . g)) `2 = hom (
g,
a)
by XTUPLE_0:1;
dom (T . g) = Hom (
(cod g),
a)
by A4, Lm1;
then A6:
dom (@ (T . g)) = Hom (
(cod g),
a)
by Def9;
A7:
cod (T . g) = Hom (
(dom g),
a)
by A4, Lm1;
then A8:
cod (@ (T . g)) = Hom (
(dom g),
a)
by Def10;
A9:
[[(Hom ((cod f),a)),(Hom ((dom f),a))],(hom (f,a))] =
@ (T . f)
by Def21
.=
[[(dom (@ (T . f))),(cod (@ (T . f)))],((@ (T . f)) `2)]
by Th8
.=
[[(dom (T . f)),(cod (@ (T . f)))],((@ (T . f)) `2)]
by Def9
.=
[[(dom (T . f)),(cod (T . f))],((@ (T . f)) `2)]
by Def10
;
then A10:
(@ (T . f)) `2 = hom (
f,
a)
by XTUPLE_0:1;
cod (T . f) = Hom (
(dom f),
a)
by A9, Lm1;
then A11:
cod (@ (T . f)) = Hom (
(dom f),
a)
by Def10;
A12:
dom (T . f) = Hom (
(cod f),
a)
by A9, Lm1;
then A13:
dom (@ (T . f)) = Hom (
(cod f),
a)
by Def9;
(
dom (g (*) f) = dom f &
cod (g (*) f) = cod g )
by A3, CAT_1:17;
hence T . (g (*) f) =
[[(Hom ((cod g),a)),(Hom ((dom f),a))],(hom ((g (*) f),a))]
by Def21
.=
[[(Hom ((cod g),a)),(Hom ((dom f),a))],((hom (f,a)) * (hom (g,a)))]
by A3, Th45
.=
(@ (T . f)) * (@ (T . g))
by A3, A10, A13, A11, A5, A6, A8, Def6
.=
(T . f) (*) (T . g)
by A3, A12, A7, Th27
;
verum end;
hence
hom-? a is Contravariant_Functor of C, Ens V
by OPPCAT_1:def 9; verum