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 Functor of C, Ens V
let C be Category; for a being Object of C st Hom C c= V holds
hom?- a is Functor of C, Ens V
let a be Object of C; ( Hom C c= V implies hom?- a is Functor of C, Ens V )
assume A1:
Hom C c= V
; hom?- a is 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 (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
T . (g (*) f) = (T . g) (*) (T . f) ) )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 (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) ) & ( for f, g being Morphism of C st dom g = cod f holds
T . (g (*) f) = (T . g) (*) (T . f) ) )thus
for
f being
Morphism of
C holds
(
T . (id (dom f)) = id (dom (T . f)) &
T . (id (cod f)) = id (cod (T . f)) )
for f, g being Morphism of C st dom g = cod f holds
T . (g (*) f) = (T . g) (*) (T . f)proof
let f be
Morphism of
C;
( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) )
set b =
dom f;
set c =
cod f;
set g =
T . f;
(
Hom (
a,
(dom f))
in Hom C &
Hom (
a,
(cod f))
in Hom C )
;
then reconsider A =
Hom (
a,
(dom f)),
B =
Hom (
a,
(cod f)) as
Element of
V by A1;
A2:
[[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))] =
@ (T . f)
by Def20
.=
[[(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 (@ A)
by A1, Lm9
.=
id (dom (T . f))
by A2, Lm1
;
T . (id (cod f)) = id (cod (T . f))
thus T . (id (cod f)) =
id (@ B)
by A1, Lm9
.=
id (cod (T . f))
by A2, Lm1
;
verum
end; let f,
g be
Morphism of
C;
( dom g = cod f implies T . (g (*) f) = (T . g) (*) (T . f) )assume A3:
dom g = cod f
;
T . (g (*) f) = (T . g) (*) (T . f)A4:
[[(Hom (a,(dom g))),(Hom (a,(cod g)))],(hom (a,g))] =
@ (T . g)
by Def20
.=
[[(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 (
a,
g)
by XTUPLE_0:1;
cod (T . g) = Hom (
a,
(cod g))
by A4, Lm1;
then A6:
cod (@ (T . g)) = Hom (
a,
(cod g))
by Def10;
A7:
dom (T . g) = Hom (
a,
(dom g))
by A4, Lm1;
then A8:
dom (@ (T . g)) = Hom (
a,
(dom g))
by Def9;
A9:
[[(Hom (a,(dom f))),(Hom (a,(cod f)))],(hom (a,f))] =
@ (T . f)
by Def20
.=
[[(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 (
a,
f)
by XTUPLE_0:1;
dom (T . f) = Hom (
a,
(dom f))
by A9, Lm1;
then A11:
dom (@ (T . f)) = Hom (
a,
(dom f))
by Def9;
A12:
cod (T . f) = Hom (
a,
(cod f))
by A9, Lm1;
then A13:
cod (@ (T . f)) = Hom (
a,
(cod f))
by Def10;
(
dom (g (*) f) = dom f &
cod (g (*) f) = cod g )
by A3, CAT_1:17;
hence T . (g (*) f) =
[[(Hom (a,(dom f))),(Hom (a,(cod g)))],(hom (a,(g (*) f)))]
by Def20
.=
[[(Hom (a,(dom f))),(Hom (a,(cod g)))],((hom (a,g)) * (hom (a,f)))]
by A3, Th44
.=
(@ (T . g)) * (@ (T . f))
by A3, A10, A11, A13, A5, A8, A6, Def6
.=
(T . g) (*) (T . f)
by A3, A12, A7, Th27
;
verum end;
hence
hom?- a is Functor of C, Ens V
by CAT_1:61; verum