:: Yoneda Embedding
:: by Miros{\l}aw Wojciechowski
::
:: Received June 12, 1997
:: Copyright (c) 1997-2021 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;