Volume 9, 1997

University of Bialystok

Copyright (c) 1997 Association of Mizar Users

### The abstract of the Mizar article:

### Yoneda Embedding

**by****Miroslaw Wojciechowski**- Received June 12, 1997
- 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;

Back to top