@MISC{GLIB_010.MIZ,
  AUTHOR = {Koch, Sebastian},
  NOTE1 = {The author is enrolled in the Johannes Gutenberg University in Mayence, Germany},
  TITLE = {About Graph Mappings},
  SECTION1 = {Preliminaries},
  SECTION2 = {Ordering of a Graph},
  SECTION3 = {Graph Mappings},
  SECTION4 = {Walks Induced by Graph Mappings},
  SECTION5 = {Graph Mappings and Graph Modes},
  DAY = {29},
  MONTH = {August},
  YEAR = {2019},
  ADDRESS1 = {Germany\\\href{mailto:skoch02@students.uni-mainz.de}{skoch02@students.uni-mainz.de}},
  SUMMARY = {Writing this article has been rather challenging. "Much of graph theory is concerned with the   study of simple graphs"\cite[p.~3]{MULTI}, so most graph theory books are only concerned with graph   homomorphisms between simple graphs, if they are concerned with anything more general than isomorphisms at     all. \cite{MULTI} writes about general graphs; isomorphisms are done in the first chapter while   homomorphisms are only looked at in the context of vertex colorings in chapter~14. The book "Graphs and   homomorphisms"\cite{HOMO} only handles (di)graphs without multiple parallel edges. The book "Graph   coloring problems"\cite{COLPROB} notes homomorphisms between loopless graphs, but doesn't elaborate.   \cite{AGT2} only handles homomorphisms between simple graphs. \cite{CAYLEY} shortly describes   homomorphisms between undirected graphs. \cite{EXPATH} handles homomorphisms between digraphs without   parallel edges. \cite{SIMPLE} writes about general graphs but, like most graph books, only about   isomorphisms. The best source so far has been \cite{AGT}, where graph homomorphisms are introduced for   digraphs possibly containing loops and multiple parallel edges (just like graphs are formalized in 
  \cite{GLIB_000.ABS}) but the focus is almost immediately shifted to homomorphisms between simple graphs.   So a quick overview of the formalized notation seems in order.\par
    A \textit{graph} $G$ consists of a non empty set $V(G)$ called vertices of $G$, a set $E(G)$ called   edges of $G$ and two functions $s(G),t(G):E(G)\rightarrow V(G)$, the source and target of $G$. For $e\in   E(G),v,w\in V(G)$ we write \textit{$e$ joins $v$ to $w$} if $s(G)(e)=v$ and $t(G)(e)=w$, and we write   \textit{$e$ joins $v$ and $w$} if $e$ joins $v$ to $w$ or $e$ joins $w$ to $v$. Let $G_1,G_2$ be graphs. A   \textit{partial graph mapping} from $G_1$ to $G_2$ is an ordered pair $F=[F_V,F_E]$ with the following   properties:
    \begin{itemize}
    \item $F_V$ is a partial function from $V(G_1)$ to $V(G_2)$.
    \item $F_E$ is a partial function from $E(G_1)$ to $E(G_2)$.
    \item For any $e\in\operatorname{dom}F_E$ holds $s(G)(e),t(G)(e)\in\operatorname{dom}F_V$.
    \item For any $e\in\operatorname{dom}F_E$ and $v,w\in\operatorname{dom}F_V$ such that $e$ joins $v$ and $w$ holds $F_E(e)$ joins $F_V(v)$ and $F_V(w)$.
  \end{itemize}
  Note that $[f,\emptyset]$ is a valid partial graph mapping for any partial function $f:V(G_1)\to V(G_2)$, especially for $f=\emptyset$. Now define the following attributes:
  \begin{itemize}
    \item $F$ is \textit{empty} if $\operatorname{dom}F_V=\emptyset$.
    \item $F$ is \textit{total} (or a homomorphism) if $\operatorname{dom}F_V=V(G_1)$ and $\operatorname{dom}F_E=E(G_1)$.
    \item $F$ is \textit{onto} (or surjective) if $\operatorname{rng}F_V=V(G_2)$ and $\operatorname{rng}F_E=E(G_2)$.
    \item $F$ is \textit{one-to-one} (or injective) if $F_V$ and $F_E$ are.
    \item $F$ is \textit{semi-continuous} if for any $e\in\operatorname{dom}F_E$ and $v,w\in\operatorname{dom}F_V$ such that $F_E(e)$ joins $F_V(v)$ and $F_V(w)$ holds $e$ joins $v$ and $w$.
    \item $F$ is \textit{continuous} if for any $\tilde{e}\in E(G_2)$ and $v,w\in\operatorname{dom}F_V$ such that $\tilde{e}$ joins $F_V(v)$ and $F_V(w)$ exists an $e\in\operatorname{dom}F_E$ such that $F_E(e)=\tilde{e}$ and $e$ joins $v$ and $w$.
    \item $F$ is a \textit{weak subgraph-embedding} if it is total and one-to-one.
    \item $F$ is a \textit{strong subgraph-embedding} if it is total, one-to-one and continuous.
    \item $F$ is an \textit{isomorphism} if it is total, one-to-one and onto.
  \end{itemize}
  Because modes in Mizar must always be inhabitated, partial graph mappings are the chosen foundation rather than homomorphisms, which may not exist between two graphs. The attributes \textit{total}, \textit{onto} and \textit{one-to-one} were named like their function analogons from \cite{FUNCT_1.ABS} and \cite{FUNCT_2.ABS}. The \textit{continuous} attribute was inspired by the continuous vertex mappings of \cite{AGT} and is in fact sometimes different from \textit{semi-continuous}. \textit{Semi-continuous} seemed like the natural generalization of \textit{continuous} for graph mappings instead of vertex mappings, but that turned out to be false. Still, a semi-continuous graph mapping already carries a lot of properties from $G_1$ to $G_2$, so the definition was kept. Corresponding attributes for directed graph mappings are given as well in this article.\par
  If $F$ is a weak subgraph-embedding, then $G_1$ is isomorphic to a subgraph of $G_2$. If $F$ is a strong subgraph-embedding, then $G_1$ is isomorphic to an induced subgraph of $G_2$. The short term \textit{embedding} was desperately avoided to be available for embeddings of graphs into the plane and other surfaces. If $F$ is one-to-one, it is also semi-continuous. If $F$ is semi-continuous and onto, it is also continuous.\par
  Originally, only an article about graph isomorphisms was planned, but it was changed to provide a solid foundation of general graph mappings. Now this article also includes
  the restriction of $F$ to subgraphs of $G_1$ or $G_2$, the domain and range of $F$
  defined as the plain subgraphs of $G_1$ and $G_2$ induced by $\operatorname{dom}F_V$, $\operatorname{dom}F_E$ and $\operatorname{rng}F_V$, $\operatorname{rng}F_E$ respectively, and the images of walks under $F$. Of course the inverse of $F$ and the composition of two graph mappings are included as well. \par
  Additionally, the ordering of a graph, which is just an enumeration of its vertices, has been introduced as yet another graph decorator. Attributes describing if $F$ preserves the weights, edge labels, vertex labels or the ordering have been added as well.
  }
}

@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{GERWAG,
  title = {Graphentheorie},
  series = {B.I-Hochschultaschenbücher ; 248},
  author = {Wagner, Klaus},
  address = {Mannheim [u.a.]},
  publisher = {Bibliograph. Inst.},
  year = {1970},
  ISBN = {3-411-00248-4},
  pages = {220 S.}
}
@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{MULTI,
  TITLE = {Graph theory},
  SERIES = {Graduate texts in mathematics ; 244},
  AUTHOR = {Bondy, John Adrian ; Murty, U. S. R.},
  ADDRESS = {New York, NY},
  PUBLISHER = {Springer},
  YEAR = {2008},
  ISBN = {978-1-84628-969-9},
  PAGES = {XII, 652 S.},
  URL = {http://scans.hebis.de/HEBCGI/show.pl?19542627_toc.pdf ; http://scans.hebis.de/HEBCGI/show.pl?19542627_kap-2.pdf ; http://scans.hebis.de/HEBCGI/show.pl?19542627_ein-1.pdf}
}
@book{SELECTED,
  TITLE = {Selected topics in graph theory},
  EDITOR = {Beineke, Lowell W.},
  ADDRESS = {London [et al.]},
  PUBLISHER = {Academic Press},
  YEAR = {1978},
  ISBN = {0-12-086250-6},
  pages = {IX, 451 S.}
}
@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{COLPROB,
  title = {Graph coloring problems},
  series = {Wiley-Interscience series in discrete mathematics and optimization},
  author = {Jensen, Tommy R. ; Toft, Bjarne},
  address = {New York [u.a.]},
  publisher = {Wiley},
  year = {1995},
  ISBN = {0-471-02865-7},
  pages = {XIX, 295 S.},
  url = {http://scans.hebis.de/HEBCGI/show.pl?04673951_toc.pdf}
}
@book{AGT2,
  title = {Algebraic graph theory},
  series = {Graduate texts in mathematics ; 207},
  author = {Godsil, Christopher David ; Royle, Gordon},
  address = {New York [u.a.]},
  publisher = {Springer},
  year = {2001},
  ISBN = {0-387-95220-9 ; 0-387-95241-1},
  pages = {XIX, 439 S.},
  url = {http://scans.hebis.de/HEBCGI/show.pl?09922696_ein-1.pdf ; http://scans.hebis.de/HEBCGI/show.pl?09922696_kap-1.pdf ; http://scans.hebis.de/HEBCGI/show.pl?09922696_toc.pdf ; http://scans.hebis.de/HEBCGI/show.pl?09922696_cov.jpg},
}
@book{CAYLEY,
  title = {Expander families and Cayley graphs : a beginners guide},
  author = {Krebs, Mike ; Shaheen, Anthony},
  address = {Oxford [u.a.]},
  publisher = {Oxford University Press},
  year = {2011},
  ISBN = {0-19-976711-4 ; 978-0-19-976711-3},
  pages = {XXIV, 258 S.}
}
@book{EXPATH,
  title = {Extremal paths in graphs : foundations, search strategies, and related topics},
  series = {Mathematical topics ; 10},
  author = {Huckenbeck, Ulrich},
  address = {Berlin},
  publisher = {Akademie-Verl.},
  year = {1997},
  edition = {1. ed.},
  ISBN = {3-05-501658-0 ; 978-3-05-501658-5},
  pages = {480 S.},
  url = {http://scans.hebis.de/HEBCGI/show.pl?05834025_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}
}