Journal of Formalized Mathematics
Volume 9, 1997
University of Bialystok
Copyright (c) 1997 Association of Mizar Users

### Yoneda Embedding

by
Miroslaw Wojciechowski

MML identifier: YONEDA_1
[ Mizar article, MML identifier index ]

```environ

vocabulary CAT_1, ENS_1, FUNCT_1, RELAT_1, MCART_1, NATTRA_1, BOOLE, OPPCAT_1,
CAT_2, FUNCT_2, YONEDA_1;
notation TARSKI, XBOOLE_0, SUBSET_1, MCART_1, RELAT_1, FUNCT_1, FUNCT_2,
CAT_1, CAT_2, OPPCAT_1, ENS_1, NATTRA_1;
constructors DOMAIN_1, ENS_1, NATTRA_1, PARTFUN1;
clusters FUNCT_1, RELSET_1, ENS_1, XBOOLE_0;
requirements SUBSET, BOOLE;

begin

reserve y for set;
reserve A for Category, a,o for Object of A;
reserve f for Morphism of A;

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

theorem :: YONEDA_1:1
for f,g being Function, 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;

theorem :: YONEDA_1:2
hom?-(a) is Functor of A,EnsHom(A);

definition let A,a;
func <|a,?> -> Functor of A,EnsHom(A) equals
:: YONEDA_1:def 2
hom?-(a);
end;

theorem :: YONEDA_1:3
for f being Morphism of A holds
<|cod f,?> is_naturally_transformable_to <|dom f,?>;

definition let A,f;
func <|f,?> -> natural_transformation of <|cod f,?>, <|dom f,?> means
:: YONEDA_1:def 3
for o be Object of A holds
it.o = [[Hom(cod f,o),Hom(dom f,o)],hom(f,id o)];
end;

theorem :: YONEDA_1:4
for f being Element of the Morphisms of A holds
[[<|cod f,?>,<|dom f,?>],<|f,?>] is Element of the Morphisms of
Functors(A,EnsHom(A));

definition let A;
func Yoneda(A) -> Contravariant_Functor of A,Functors(A,EnsHom(A)) means
:: YONEDA_1:def 4
for f being Morphism of A holds
it.f = [[<|cod f,?>,<|dom f,?>],<|f,?>];
end;

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;
end;

theorem :: YONEDA_1:5
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;

definition let C,D be Category;
let T be Contravariant_Functor of C,D;
attr T is faithful means
:: YONEDA_1:def 6
for c,c' being Object of C st Hom(c,c') <> {}
for f1,f2 being Morphism of c,c' holds T.f1 = T.f2 implies f1 = f2;
end;

theorem :: YONEDA_1:6
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;

theorem :: YONEDA_1:7
Yoneda A is faithful;

theorem :: YONEDA_1:8
Yoneda A is one-to-one;

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

theorem :: YONEDA_1:9
Yoneda A is full;

```