@MISC{GLIB_011.MIZ,
  AUTHOR = {Koch, Sebastian},
  NOTE1 = {The author is enrolled in the Johannes Gutenberg University in Mayence, Germany},
  TITLE = {About Graph Mappings},
  SECTION1 = {Vertex Mappings},
  SECTION2 = {The Relation Between Graph Mappings and Vertex Mappings},
  DAY = {29},
  MONTH = {August},
  YEAR = {2019},
  ADDRESS1 = {Germany\\\href{mailto:skoch02@students.uni-mainz.de}{skoch02@students.uni-mainz.de}},
  SUMMARY = {This article is a brief introduction to partial vertex mappings in Mizar\cite{FourDecades}. As discussed in the abstract of \cite{GLIB_010.ABS} almost no graph theory book discusses graph homomorphisms in a scope as general as it was done in \cite{AGT} and \cite{GLIB_010.ABS}. Most of the time, graph homomorphisms are only discussed in the form of vertex mappings, often only in the context of simple graphs. But of course that choice is not without reason and in many cases considering vertex mappings is enough, which is especially useful since one does not need to think about an edge mapping then. Given that the graph definitions change slightly between different authors, a quick overview of the formalized notation seems in order.\par
  A \textit{partial vertex mapping} $f$ between two graphs $G_1$, $G_2$ is a partial function of their vertex sets $V(G_1)$, $V(G_2)$ with the additional property that if vertices $v,w\in\operatorname{dom}f$ are adjacent in $G_1$, then their images $f(v)$, $f(w)$ are adjacent in $G_2$. The properties of $f$ to be \textit{total} (or a homomorphism), \textit{one-to-one} (or injective) and \textit{onto} (or surjective) have the usual meaning for $f$ as a partial function. $f$ is \textit{continuous} if for any $v,w\in\operatorname{dom}f$ such that $f(v)$ and $f(w)$ are adjacent, $v$ and $w$ are adjacent as well. $f$ is an \textit{isomorphism} if it is total, one-to-one, onto and the cardinality of edges between to vertices $v$ and $w$ of $G_1$ is the same as the cardinality of the edges between $f(v)$ and $f(w)$. Corresponding attributes for directed vertex mappings are given as well in this article.\par
  The attribute \textit{continuous} is the generalization for not necessarily simple graphs of the \textit{continuous} of \cite{AGT}. The \textit{isomorphism} attribute was inspired by \cite{DISC} and it is shown that for graphs $G_1, G_2$ without multiple edges that a total bijective and continuous vertex mapping $f$ between them is already an isomorphism, just like a graph isomorphism is usually described (cf. \cite{HOMO,SIMPLE,AGT}). This article does not go into depth like \cite{GLIB_010.ABS}, but the inverse and composition of partial vertex mappings are covered.\par
  A partial graph mapping does not always induce a partial vertex mapping (since any subset of the set of edges of $G_1$ can be mapped) and a partial vertex mapping can give rise to several partial graph mappings. In the second part of this article it is shown in which cases that the induced partial vertex mapping exists and the induced partial graph mapping is unique. Furthermore it is formally stated that for two graphs without multiple edges there exists a graph mapping that is an isomorphism iff there exists a vertex mapping that is an isomorphism.
  }
}
@Article{BancerekJAR:2018,
  author={Bancerek, Grzegorz and Byli{\'{n}}ski, Czes{\l}aw and Grabowski, Adam and Korni{\l}owicz, Artur and Matuszewski, Roman and Naumowicz, Adam and P{\k{a}}k, Karol},
  title={The Role of the {M}izar {M}athematical {L}ibrary for Interactive Proof Development in {M}izar},
  journal={Journal of Automated Reasoning},
  year={2018},
  volume={61},
  number={1},
  pages={9--32},
  doi={10.1007/s10817-017-9440-6},
  url={https://doi.org/10.1007/s10817-017-9440-6}
}
@Article{FourDecades,
  author={Grabowski, Adam and Korni{\l}owicz, Artur and Naumowicz, Adam},
  title={Four Decades of {M}izar},
  journal={Journal of Automated Reasoning},
  year={2015},
  volume={55},
  number={3},
  pages={191--198},
  issn={1573-0670},
  doi={10.1007/s10817-015-9345-1}
}
@book{AGT,
  title={Algebraic graph theory: morphisms, monoids and matrices},
  author={Knauer, Ulrich},
  volume={41},
  year={2011},
  publisher={Walter de Gruyter}
}
@book{SIMPLE,
  TITLE = {Introduction to graph theory},
  AUTHOR = {Wilson, Robin James},
  ADDRESS = {Edinburgh},
  PUBLISHER = {Oliver & Boyd},
  YEAR = {1972},
  ISBN = {0-05-002534-1},
  PAGES = {VIII, 168 S.},
  URL = {http://scans.hebis.de/HEBCGI/show.pl?10670775_toc.pdf},
}
@book{HOMO,
  title = {Graphs and homomorphisms},
  series = {Oxford lecture series in mathematics and its applications ; 28},
  author = {Hell, Pavol ; Nesetril, Jaroslav},
  address = {Oxford},
  publisher = {Oxford Univ. Press},
  year = {2004},
  ISBN = {0-19-852817-5},
  pages = {IX, 244 S.},
  url = {http://scans.hebis.de/HEBCGI/show.pl?12385357_toc.pdf}
}
@book{DISC,
  title = {A first course in discrete mathematics},
  series = {Springer undergraduate mathematics series},
  author = {Anderson, Ian},
  address = {London},
  publisher = {Springer},
  year = {2001},
  ISBN = {1-85233-236-0},
  pages = {VIII, 200 S.},
  url = {http://scans.hebis.de/HEBCGI/show.pl?09315030_vlg.html ; http://scans.hebis.de/HEBCGI/show.pl?09315030_cov.jpg ; http://scans.hebis.de/HEBCGI/show.pl?09315030_toc.pdf}
}