:: Yoneda Embedding :: by Miros{\l}aw Wojciechowski :: :: Received June 12, 1997 :: Copyright (c) 1997-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies CAT_1, ENS_1, FUNCT_1, GRAPH_1, RELAT_1, SUBSET_1, MCART_1, NATTRA_1, STRUCT_0, XBOOLE_0, PZFMISC1, TARSKI, OPPCAT_1, CAT_2, FUNCT_2, YONEDA_1, MONOID_0, PARTFUN1; notations TARSKI, XBOOLE_0, XTUPLE_0, XFAMILY, SUBSET_1, MCART_1, RELAT_1, FUNCT_1, BINOP_1, FUNCT_2, STRUCT_0, GRAPH_1, CAT_1, CAT_2, OPPCAT_1, ENS_1, CAT_3, NATTRA_1; constructors DOMAIN_1, NATTRA_1, ENS_1, RELSET_1, CAT_3, XTUPLE_0, XFAMILY; registrations XBOOLE_0, FUNCT_1, RELSET_1, ENS_1, STRUCT_0, FUNCT_2, CAT_1, XTUPLE_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; definition let A,a; func <|a,?> -> Functor of A,EnsHom(A) equals :: YONEDA_1:def 2 hom?-(a); end; theorem :: YONEDA_1:2 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:3 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)); 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:4 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,c9 being Object of C st Hom(c,c9) <> {} for f1,f2 being Morphism of c,c9 holds T.f1 = T.f2 implies f1 = f2; end; theorem :: YONEDA_1:5 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; registration let A; cluster Yoneda A -> faithful; end; registration let A; cluster Yoneda A -> one-to-one; end; 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,c9 being Object of C st Hom(T.c9,T.c) <> {} for g being Morphism of T.c9,T.c holds Hom(c,c9) <> {} & ex f being Morphism of c,c9 st g = T.f; end; registration let A; ::\$N Yoneda Lemma cluster Yoneda A -> full; end;