:: Yoneda Embedding
:: by Miros{\l}aw Wojciechowski
::
:: Received June 12, 1997
:: Copyright (c) 1997-2012 Association of Mizar Users


begin

definition
let A be Category;
func EnsHom A ->  Category equals :: YONEDA_1:def 1
 Ens (Hom A);
correctness
coherence
Ens (Hom A) is Category;
;
end;

:: deftheorem  defines EnsHom YONEDA_1:def_1_:_
 for A being Category holds EnsHom A = Ens (Hom A);

theorem Th1: :: YONEDA_1:1
for A being Category
for f, g being Function
for m1, m2 being Morphism of (EnsHom A) st cod m1 = dom m2 & [[(dom m1),(cod m1)],f] = m1 & [[(dom m2),(cod m2)],g] = m2 holds
[[(dom m1),(cod m2)],(g * f)] = m2 (*) m1
proofend;

definition
let A be Category;
let a be Object of A;
func<|a,?> ->  Functor of A, EnsHom A equals :: YONEDA_1:def 2
 hom?- a;
coherence
 hom?- a is Functor of A, EnsHom A by ENS_1:49;
end;

:: deftheorem  defines <| YONEDA_1:def_2_:_
 for A being Category
for a being Object of A holds <|a,?> = hom?- a;

theorem Th2: :: YONEDA_1:2
for A being Category
for f being Morphism of A holds <|(cod f),?> is_naturally_transformable_to <|(dom f),?>
proofend;

definition
let A be Category;
let f be Morphism of A;
func<|f,?> ->  natural_transformation of <|(cod f),?>,<|(dom f),?> means :Def3: :: YONEDA_1:def 3
 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)))]
proofend;
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)))] ) &amp; ( for o being Object of A holds b2 . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] ) holds
b1 = b2
proofend;
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 Th3: :: YONEDA_1:3
for A being Category
for f being Element of the carrier' of A holds [[<|(cod f),?>,<|(dom f),?>],<|f,?>] is Element of the carrier' of (Functors (A,(EnsHom A)))
proofend;

definition
let A be Category;
func Yoneda A ->  Contravariant_Functor of A, Functors (A,(EnsHom A)) means :Def4: :: YONEDA_1:def 4
 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,?>]
proofend;
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,?>] ) &amp; ( for f being Morphism of A holds b2 . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] ) holds
b1 = b2
proofend;
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,?>] );

definition
let A, B be Category;
let F be Contravariant_Functor of A,B;
let c be Object of A;
funcF . c ->  Object of B equals :: YONEDA_1:def 5
(Obj F) . c;
correctness
coherence
(Obj F) . c is Object of B;
;
end;

:: 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 :: YONEDA_1:4
for A being Category
for F being Functor of A, Functors (A,(EnsHom A)) st Obj F is one-to-one &amp; F is faithful holds
F is one-to-one
proofend;

definition
let C, D be Category;
let T be Contravariant_Functor of C,D;
attrT is faithful  means :Def6: :: YONEDA_1:def 6
 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;
end;

:: 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 Th5: :: YONEDA_1:5
for A being Category
for F being Contravariant_Functor of A, Functors (A,(EnsHom A)) st Obj F is one-to-one &amp; F is faithful holds
F is one-to-one
proofend;

registration
let A be Category;
cluster Yoneda A ->  faithful ;
coherence
 Yoneda A is faithful
proofend;
end;

registration
let A be Category;
cluster Yoneda A ->  one-to-one ;
coherence
 Yoneda A is one-to-one
proofend;
end;

definition
let C, D be Category;
let T be Contravariant_Functor of C,D;
attrT is full  means :Def7: :: YONEDA_1:def 7
 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) <> {} &amp; ex f being Morphism of c,c9 st g = T . f );
end;

:: 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) <> {} &amp; ex f being Morphism of c,c9 st g = T . f ) );

registration
let A be Category;
cluster Yoneda A ->  full ;
coherence
 Yoneda A is full
proofend;
end;