let V be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: ( Hom C c= V implies hom?- a is Functor of C, Ens V )
assume A1: Hom C c= V ; :: thesis: 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 :: thesis: ( ( 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 :: thesis: ( ( 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 c be Object of C; :: thesis: ex d being Object of (Ens V) st T . (id c) = id d
Hom (a,c) in Hom C ;
then reconsider A = Hom (a,c) as Element of V by A1;
take d = @ A; :: thesis: T . (id c) = id d
thus T . (id c) = id d by A1, Lm9; :: thesis: verum
end;
thus for f being Morphism of C holds
( T . (id (dom f)) = id (dom (T . f)) & T . (id (cod f)) = id (cod (T . f)) ) :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: verum
end;
let f, g be Morphism of C; :: thesis: ( dom g = cod f implies T . (g (*) f) = (T . g) (*) (T . f) )
assume A3: dom g = cod f ; :: thesis: 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 ;
:: thesis: verum
end;
hence hom?- a is Functor of C, Ens V by CAT_1:61; :: thesis: verum