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

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

proof end;

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 :: YONEDA_1:2

canceled;

theorem Th3: :: YONEDA_1:3

for A being Category
for f being Morphism of A holds <|(cod f),?> is_naturally_transformable_to <|(dom f),?>

proof end;

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 b₁ being natural_transformation of <|(cod f),?>,<|(dom f),?> st
for o being Object of A holds b₁ . o = [[(Hom (cod f),o),(Hom (dom f),o)],(hom f,(id o))]

proof end;

uniqueness
for b₁, b₂ being natural_transformation of <|(cod f),?>,<|(dom f),?> st ( for o being Object of A holds b₁ . o = [[(Hom (cod f),o),(Hom (dom f),o)],(hom f,(id o))] ) & ( for o being Object of A holds b₂ . o = [[(Hom (cod f),o),(Hom (dom f),o)],(hom f,(id o))] ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines <| YONEDA_1:def 3 :

for A being Category
for f being Morphism of A
for b₃ being natural_transformation of <|(cod f),?>,<|(dom f),?> holds
( b₃ = <|f,?> iff for o being Object of A holds b₃ . o = [[(Hom (cod f),o),(Hom (dom f),o)],(hom f,(id o))] );

theorem Th4: :: YONEDA_1:4

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))

proof end;

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 b₁ being Contravariant_Functor of A, Functors A,(EnsHom A) st
for f being Morphism of A holds b₁ . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>]

proof end;

uniqueness
for b₁, b₂ being Contravariant_Functor of A, Functors A,(EnsHom A) st ( for f being Morphism of A holds b₁ . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] ) & ( for f being Morphism of A holds b₂ . f = [[<|(cod f),?>,<|(dom f),?>],<|f,?>] ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines Yoneda YONEDA_1:def 4 :

for A being Category
for b₂ being Contravariant_Functor of A, Functors A,(EnsHom A) holds
( b₂ = Yoneda A iff for f being Morphism of A holds b₂ . 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;
func F . 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:5

for A being Category
for F being Functor of A, Functors A,(EnsHom A) st Obj F is one-to-one & F is faithful holds
F is one-to-one

proof end;

definition

let C, D be Category;
let T be Contravariant_Functor of C,D;
attr T is faithful means :Def6: :: YONEDA_1:def 6
for c, c' being Object of C st Hom c,c' <> {} holds
for f1, f2 being Morphism of c,c' 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, c' being Object of C st Hom c,c' <> {} holds
for f1, f2 being Morphism of c,c' st T . f1 = T . f2 holds
f1 = f2 );

theorem Th6: :: YONEDA_1:6

for A being Category
for F being Contravariant_Functor of A, Functors A,(EnsHom A) st Obj F is one-to-one & F is faithful holds
F is one-to-one

proof end;

theorem Th7: :: YONEDA_1:7

for A being Category holds Yoneda A is faithful

proof end;

theorem :: YONEDA_1:8

for A being Category holds Yoneda A is one-to-one

proof end;

definition

let C, D be Category;
let T be Contravariant_Functor of C,D;
attr T is full means :Def7: :: YONEDA_1:def 7
for c, c' being Object of C st Hom (T . c'),(T . c) <> {} holds
for g being Morphism of T . c',T . c holds
( Hom c,c' <> {} & ex f being Morphism of c,c' 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, c' being Object of C st Hom (T . c'),(T . c) <> {} holds
for g being Morphism of T . c',T . c holds
( Hom c,c' <> {} & ex f being Morphism of c,c' st g = T . f ) );

theorem :: YONEDA_1:9

for A being Category holds Yoneda A is full

proof end;