begin
:: deftheorem defines EnsHom YONEDA_1:def 1 :
for A being Category holds EnsHom A = Ens (Hom A);
theorem Th1:
:: deftheorem defines <| YONEDA_1:def 2 :
for A being Category
for a being Object of A holds <|a,?> = hom?- a;
theorem
canceled;
theorem Th3:
definition
let A be
Category;
let f be
Morphism of
A;
func <|f,?> -> natural_transformation of
<|(cod f),?>,
<|(dom f),?> means :
Def3:
for
o being
Object of
A holds
it . o = [[(Hom (cod f),o),(Hom (dom f),o)],(hom f,(id o))];
existence
ex b1 being natural_transformation of <|(cod f),?>,<|(dom f),?> st
for o being Object of A holds b1 . o = [[(Hom (cod f),o),(Hom (dom f),o)],(hom f,(id o))]
uniqueness
for b1, b2 being natural_transformation of <|(cod f),?>,<|(dom f),?> st ( for o being Object of A holds b1 . o = [[(Hom (cod f),o),(Hom (dom f),o)],(hom f,(id o))] ) & ( for o being Object of A holds b2 . o = [[(Hom (cod f),o),(Hom (dom f),o)],(hom f,(id o))] ) holds
b1 = b2
end;
:: deftheorem Def3 defines <| YONEDA_1:def 3 :
for A being Category
for f being Morphism of A
for b3 being natural_transformation of <|(cod f),?>,<|(dom f),?> holds
( b3 = <|f,?> iff for o being Object of A holds b3 . o = [[(Hom (cod f),o),(Hom (dom f),o)],(hom f,(id o))] );
theorem Th4:
definition
let A be
Category;
func Yoneda A -> Contravariant_Functor of
A,
Functors A,
(EnsHom A) means :
Def4:
for
f being
Morphism of
A holds
it . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>];
existence
ex b1 being Contravariant_Functor of A, Functors A,(EnsHom A) st
for f being Morphism of A holds b1 . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>]
uniqueness
for b1, b2 being Contravariant_Functor of A, Functors A,(EnsHom A) st ( for f being Morphism of A holds b1 . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] ) & ( for f being Morphism of A holds b2 . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] ) holds
b1 = b2
end;
:: deftheorem Def4 defines Yoneda YONEDA_1:def 4 :
for A being Category
for b2 being Contravariant_Functor of A, Functors A,(EnsHom A) holds
( b2 = Yoneda A iff for f being Morphism of A holds b2 . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] );
:: deftheorem defines . YONEDA_1:def 5 :
for A, B being Category
for F being Contravariant_Functor of A,B
for c being Object of A holds F . c = (Obj F) . c;
theorem
:: deftheorem Def6 defines faithful YONEDA_1:def 6 :
for C, D being Category
for T being Contravariant_Functor of C,D holds
( T is faithful iff for c, c9 being Object of C st Hom c,c9 <> {} holds
for f1, f2 being Morphism of c,c9 st T . f1 = T . f2 holds
f1 = f2 );
theorem Th6:
:: deftheorem Def7 defines full YONEDA_1:def 7 :
for C, D being Category
for T being Contravariant_Functor of C,D holds
( T is full iff for c, c9 being Object of C st Hom (T . c9),(T . c) <> {} holds
for g being Morphism of T . c9,T . c holds
( Hom c,c9 <> {} & ex f being Morphism of c,c9 st g = T . f ) );