closes #121

Author: ecpeterson

finite.tex

@@ -546,10 +546,11 @@ \section{The structure of \texorpdfstring{\(\moduli{fg}\)}{Mfg} II: Large scales
 \end{definition}
 
 \begin{lemma}[{\cite[Theorem 15.2.9]{Hazewinkel}}]\label{EveryLogHaspTypification}\label{EveryFGLIsPTypical}
-Every formal group law \(+_\phi\) over a torsion--free \(\Z_{(p)}\)--algebra is naturally isomorphic to a \(p\)--typical formal group law, called the \textit{\(p\)--typification} of \(+_\phi\).
+Let \(\G\) be a formal group \(\G\) over a torsion--free \(\Z_{(p)}\)--algebra, and let \(x\) be a coordinate with associated invariant differential \(\sum_{j=1}^\infty a_j x^{j-1} \dx\).
+There is then an isomorphic \(p\)--typical coordinate \(y\) on \(\G\), called the \textit{\(p\)--typification} of \(x\), whose invariant differential is given by \(\sum_{n=0}^\infty a_{p^n} y^{p^n - 1} \dy\) (i.e., by ``removing terms'').
 \end{lemma}
 \begin{proof}
-Let \(\G\) be the formal group associated to \(+_\phi\), denote its inherited parameter by \[g_0\co \A^1 \xrightarrow{\cong} \G,\] so that \(\omega_0(x) = (g_0^* \omega)(x) = \sum_{n=1}^\infty a_n x^{n-1} \dx\) is the invariant differential associated to \(+_\phi\).  Our goal is to perturb this parameter to a new parameter \(g_\infty\) so that its associated invariant differential has the form \[\sum_{n=0}^\infty a_{p^n} x^{p^n-1} \dx.\]  To do this, we introduce four operators on functions\footnote{Unfortunately, it is standard in the literature to call these parameters ``curves'', which does not fit well with our previous use of the term in \Cref{ComplexBordismChapter}.} \(\A^1 \to \G\):
+Denote the parameter associated to \(x\) by \[g_0\co \A^1 \xrightarrow{\cong} \G,\] so that \(\omega_0(x) = (g_0^* \omega)(x) = \sum_{n=1}^\infty a_n x^{n-1} \dx\) is the associated invariant differential.  Our goal is to perturb this parameter to a new parameter \(g_\infty\) so that its associated invariant differential has the form \[\sum_{n=0}^\infty a_{p^n} y^{p^n-1} \dy.\]  To do this, we introduce four operators on functions\footnote{Unfortunately, it is standard in the literature to call these parameters ``curves'', which does not fit well with our previous use of the term in \Cref{ComplexBordismChapter}.} \(\A^1 \to \G\):
 \begin{itemize}
 \item Given \(r \in R\), we can define a \index{homothety}\textit{homothety} by rescaling the coordinate by \(r\): \[(\theta_r^* g_0^* \omega)(x) = \omega_0(rx) = \sum_{n=1}^\infty (a_n r^n) x^{n-1} \dx.\]
 \item For \(\ell \in \N\), we can define a shift operator (or \index{Verschiebung}\textit{Verschiebung}) by \[(V_\ell^* g_0^* \omega)(x) = \omega_0(x^\ell) = \sum_{n=1}^\infty a_n \ell x^{n \ell - 1} \dx.\]

preamble.tex

@@ -296,6 +296,7 @@
 \newcommand{\spin}{\mathit{spin}}
 \newcommand{\EinftyRings}{E_\infty\CatOf{RingSpectra}}
 \newcommand{\dx}{\operatorname{d\mathit{x}}}
+\newcommand{\dy}{\operatorname{d\mathit{y}}}
 \newcommand{\cts}{\mathrm{cts}}
 
 \DeclareMathOperator{\Fix}{Fix}