jonmsterling.com
this repo has no description
Construction 32, Computation 33: path object => reflexive graph
From Ian Ray.
+3
-3
+3
-3
nodes/rx-gph-constructions.tex
+3
-3
nodes/rx-gph-constructions.tex
···
74
74
% \begin{example}[Exponential]
75
75
% Let $\gA$ and $\gB$ be two reflexive graphs; the \DefEmph{exponential} reflexive graph $\gA\Rightarrow \gB$ is defined as follows:
76
76
% \begin{align*}
77
-
% &\vrt{\gA\Rightarrow\gB} :\equiv \hom\prn{\gA,\gB}\\
77
+
% &\vrt{\gA\Rightarrow\gB} :\equiv \hom\prn{\gA,\gB}\\
78
78
% &f \Edge{\gA\Rightarrow\gB} g :\equiv
79
79
% \end{align*}
80
80
% \end{example}
···
149
149
150
150
151
151
\begin{construction}[Restriction of iterated displayed reflexive graphs]\label[construction]{con:rst-disp-rx-gph}
152
-
Let $\gA$ be a path object, and let $\gB$ be a displayed path object over $\gA$, and let $\gC$ be a displayed path object over $\gA.\gB$. Then for any $x:\vrt{\gA}$, we may define a displayed path object $\gC\Sub{\vert \gB\prn{x}}$ over the component $\gB\prn{x}$ with vertices given as follows:
152
+
Let $\gA$ be a reflexive graph object, and let $\gB$ be a displayed reflexive graph over $\gA$, and let $\gC$ be a displayed reflexive graph over $\gA.\gB$. Then for any $x:\vrt{\gA}$, we may define a displayed reflexive graph $\gC\Sub{\vert \gB\prn{x}}$ over the component $\gB\prn{x}$ with vertices given as follows:
153
153
154
154
\iblock{
155
155
\mrow{
···
188
188
\end{construction}
189
189
190
190
\begin{computation}[Components of the restriction]\label[computation]{cmp:component-of-rst-disp-rx-gph}
191
-
Let $\gA$ be a path object, and let $\gB$ be a displayed path object over $\gA$, and let $\gC$ be a displayed path object over $\gA.\gB$. Given $x:\vrt{\gB}$ and $u:\vrt{\gB}\prn{x}$, the component $\prn{\gC\Sub{\vert \gB\prn{x}}}\prn{u}$ of the restriction of $\gC$ to $\gB\prn{x}$ at $u$ is definitionally equal to the component $\gC\prn{\prn{x,u}}$ of $\gC$ at $\prn{x,u}:\vrt{\gA.\gB}$.
191
+
Let $\gA$ be a reflexive graph, and let $\gB$ be a displayed reflexive graph over $\gA$, and let $\gC$ be a displayed reflexive graph over $\gA.\gB$. Given $x:\vrt{\gB}$ and $u:\vrt{\gB}\prn{x}$, the component $\prn{\gC\Sub{\vert \gB\prn{x}}}\prn{u}$ of the restriction of $\gC$ to $\gB\prn{x}$ at $u$ is definitionally equal to the component $\gC\prn{\prn{x,u}}$ of $\gC$ at $\prn{x,u}:\vrt{\gA.\gB}$.
192
192
\end{computation}
193
193
194
194
\end{xsect}