fix blueprint

Author: kbuzzard

blueprint/lean_decls

@@ -54,8 +54,6 @@ Hurwitz.canonicalForm
 Hurwitz.completed_units
 IsCentralSimple
 MatrixRing.isCentralSimple
-DedekindDomain.FiniteAdeleRing.mul_induction_on
-DedekindDomain.FiniteAdeleRing.clear_denominator
 DedekindDomain.instTopologicalRingFiniteAdeleRing
 AutomorphicForm.GLn.IsSmooth
 AutomorphicForm.GLn.IsSlowlyIncreasing

blueprint/src/chapter/ch07exampleGLn.tex

@@ -19,56 +19,8 @@ \section{The finite adeles of the rationals.}
 
 Mathlib already has the definition of the finite adeles $\A_{\Q}^f$ of the rationals as a
 commutative $\Q$-algebra. It does not yet have the topology; work on this is on PR 13703 to mathlib.
-See also the prerequisite PR 13705, which is ready for review. Note that 13703 still contains a
-{\tt sorry}, but the result is true and not too hard. I tried proving it directly though and it ended
-up a bit long. I propose the following plan. Start by proving the following induction principle for
-finite adeles:
-\begin{lemma}
-    \label{DedekindDomain.FiniteAdeleRing.mul_induction_on}
-    \lean{DedekindDomain.FiniteAdeleRing.mul_induction_on}
-    \leanok
-    If we have a predicate $P$ on the finite adeles, with the following properties:
-  \begin{enumerate}
-    \item $P(a)$ is true for $a$ any finite integral adele;
-    \item $P(a)$ and $P(b)$ implies $P(ab)$;
-    \item For every valuation $v$, $P(a)$ is true for every finite adele which is integral
-      away from $v$ and is a unit times the inverse of a uniformiser at $v$.
-  \end{enumerate}
-  Then $P$ is true for all finite adeles.
-\end{lemma}
-\begin{proof}
-  Every finite adele is integral away from a finite bad set $v\in S$. For these $v$,
-  embed the local field $K_v$ into the finite adeles by sending $x_v\in K_v$ to the
-  finite adele which is $x_v$ at $v$ and 1 elsewhere.
-
-  If $\varpi_v$ is the finite adele corresponding a uniformiser at $v$,
-  $a_v=u_v(\pi_v^{-1})^{n_v}$ for some unit $u_v$ and positive $n_v$ (the additive valuation
-  of the integer $a_v^{-1}$). Note that $P(u_v)$ by hypothesis~1, and
-  $P(\pi_v^{-1})$ by hypothesis~3.
-
-  Now if $b=(b_v)_v$ is the finite adele with $b_v=a_v$ for $v\not\in S$ and $b_v=1$ for $v\in S$,
-  then $b$ is a finite integral adele (so hypothesis 1 applies), and $a=b\prod_{v\in S}a_v$ is hence
-  a finite product of finite adeles which satisfy $P$ and thus satisfies $P$ by hypothesis 2
-  (with hypothesis 1 to deal with the base case $a=1$).
-\end{proof}
-
-Then prove the theorem.
-
-\begin{theorem}
-  \label{DedekindDomain.FiniteAdeleRing.clear_denominator}
-  \lean{DedekindDomain.FiniteAdeleRing.clear_denominator}
-  \leanok
-Let $R$ be a Dedekind domain with field of fractions $K$. Then every $x\in\A_K^f$ can
-be written as $x=st$ with $s\in\R\backslash\{0\}$ and $t\in\prod_v R_v$ a finite integral adele.
-\end{theorem}
-\begin{proof}
-  \uses{DedekindDomain.FiniteAdeleRing.mul_induction_on}
-  Use the induction procedure. The first and second hypotheses are easily checked
-  (we can let $s=1$ for the first, and take the product of the $s$s for the second).
-  For the third, if $a_v$ is integral then we use the first hypothesis,and if the
-  additive valuation of $a_v$ is $-n<0$, we let $s$ be the $n$th power of a nonzero
-  element in the prime ideal of $R$ corresponding to $v$.
-\end{proof}
+See also the prerequisite PR 13705, which is ready for review. Once these PRs are merged, we will
+have
 
 \begin{corollary}
   \label{DedekindDomain.instTopologicalRingFiniteAdeleRing}
@@ -77,7 +29,6 @@ \section{The finite adeles of the rationals.}
   The finite adeles are a topological ring.
 \end{corollary}
 \begin{proof} All this is done in the slightly technical mathlib PR 13703.
-  \uses{DedekindDomain.FiniteAdeleRing.clear_denominator}
   \leanok
 \end{proof}