paper-wlog.tex

\documentclass{amsart}

\usepackage[utf8]{inputenc}
\usepackage{amsthm,mathtools,tikz,float,caption,xspace}
\usetikzlibrary{patterns,matrix}
\usepackage[protrusion=true,expansion=true]{microtype}
\usepackage{hyperref}
\usepackage{cleveref}

\usepackage[natbib=true,style=numeric,maxnames=10]{biblatex}
\usepackage[babel]{csquotes}
\bibliography{paper-wlog.bib}

\title[Without loss of generality, any reduced ring is a field]{Without loss of generality, \\ any reduced ring is a field}
\author{Ingo Blechschmidt}

\theoremstyle{definition}
\newtheorem{defn}{Definition}[]
\newtheorem{ex}[defn]{Example}

\theoremstyle{plain}
\newtheorem{prop}[defn]{Proposition}
\newtheorem{cor}[defn]{Corollary}
\newtheorem{lemma}[defn]{Lemma}
\newtheorem{thm}[defn]{Theorem}
\newtheorem{scholium}[defn]{Scholium}

\theoremstyle{remark}
\newtheorem{rem}[defn]{Remark}
\newtheorem{question}[defn]{Question}
\newtheorem{speculation}[defn]{Speculation}
\newtheorem{caveat}[defn]{Caveat}
\newtheorem{conjecture}[defn]{Conjecture}

\crefname{defn}{Definition}{Definitions}
\crefname{thm}{Theorem}{Theorems}
\crefname{lemma}{Lemma}{Lemmas}
\crefname{prop}{Proposition}{Propositions}
\crefname{ex}{Example}{Examples}
\crefname{section}{Section}{Sections}

% Workaround from David Carlisle described at https://tex.stackexchange.com/a/316037
\makeatletter
\let\xx@thm\@thm
\AtBeginDocument{\let\@thm\xx@thm}
\makeatother

\newcommand{\XXX}[1]{\textbf{XXX: #1}}
\newcommand{\aaa}{\mathfrak{a}}
\newcommand{\bbb}{\mathfrak{b}}
\newcommand{\mmm}{\mathfrak{m}}
\newcommand{\ppp}{\mathfrak{p}}
\newcommand{\I}{\mathcal{I}}
\newcommand{\J}{\mathcal{J}}
\newcommand{\ZZ}{\mathbb{Z}}
\newcommand{\defeq}{\vcentcolon=}
\DeclareMathOperator{\Spec}{Spec}
\DeclareMathOperator{\Quot}{Quot}
\newcommand{\?}{\,{:}\,}
\newcommand{\notnot}{\emph{not not}\xspace}
\newcommand{\negg}{\neg\!\!\!\neg}

\newcommand{\stacksproject}[1]{\cite[{\href{https://stacks.math.columbia.edu/tag/#1}{Tag~#1}}]{stacks-project}}

\begin{document}

\begin{abstract}
  XXX
\end{abstract}

\maketitle
\thispagestyle{empty}

\noindent
XXX


\section{Case studies}

\subsection{Linear surjections between finite free modules}

\begin{prop}\label{surjection}
Let~$M \in A^{n \times m}$ be a matrix over a ring~$A$ such that~$n
> m$. Assume that the induced linear map~$A^m \to A^n$ is surjective. Then~$1 =
0 \in A$.
\end{prop}

\begin{proof}[Proof~A (classical)]Assume to the contrary that~$1 \neq 0 \in A$.
Then there exists a maximal ideal~$\mmm \subseteq A$. Tensoring the given linear map
over~$A$ with~$A/\mmm$ yields a linear map~$(A/\mmm)^m \to (A/\mmm)^n$ which is
still surjective, since tensoring is right exact. Since~$A/\mmm$ is a field,
this is a contradiction by basic linear algebra.
\end{proof}

This proof uses the axiom of choice in the guise of the lemma that nontrivial
rings contain maximal ideals in order to reduce from general rings to
fields.\footnote{It's possible to avoid the full axiom of choice here and only
assume the Boolean Prime Ideal Theorem, at the expense of slightly complicating
the proof. This theorem is strong enough to conclude that a nontrivial ring has
a prime ideal~$\ppp$. One then first passes to the quotient~$A/\ppp$, where
surjectivity is preserved thanks to right-exactness of tensoring, and then to
the field of fractions~$\Quot(A/\ppp)$, where surjectivity is preserved thanks
to exactness of localization.} In fact, the statement even admits a fully
constructive proof. It's not hard to give such a proof explicitly, for instance
using determinants~\cite{richman:trivial-rings}, but in this section we want to
see how the forcing technique can be used to translate the classical proof into
a constructive one.

Starting point is the observation that \Cref{surjection} admits an easy proof
in the case that the ring~$A$ is local:

\begin{proof}[Proof~B (constructive, but only of the special case
that~$A$ is a local ring)]
Since~$M$ is surjective, some linear combination of its columns sums to the
first canonical basis vector~$e_1$. Since~$A$ is local, some entry of the first row
is invertible. By employing elementary row and column transformations, we can
change this entry to the unit of the ring, move it to the top left, and kill
any remaining entries in the first row and in the first column. Continuing in
this fashion, we can assume~$A$ to be a rectangular diagonal matrix. Since~$A$
has more rows than columns, all entries in the last row are zero. On the other
hand, one of its entries is the unit. Thus~$1 = 0$.
\end{proof}

\begin{proof}[Proof~C (constructive, general case)]
By~XXX, the given matrix~$M$ is also surjective as a matrix over~$A^\sim$.
Since~$A^\sim$ is a local ring, the previous proof applies and shows
that~$A^\sim \models 1 = 0 \? A^\sim$. This is equivalent to~$1 = 0 \in A$ by
definition.
\end{proof}

This attempt succeeds in eliminating the axiom of choice and the law of
excluded middle; but it isn't yet a faithful translation of Proof~A, since the
standard linear algebra proof referenced in Proof~A proceeds slightly
differently than Proof~B. To obtain such a translation, we use the special
field property of~$A^\sim$.

\begin{proof}[Proof~D (constructive, general case)]
By passing from~$A$ to its quotient ring~$A/\sqrt{(0)}$, which preserves
surjectivity since tensoring is right-exact, we may assume that~$A$ is a
reduced ring. Thus~$A^\sim$ is a field in the sense that non-invertible
elements are zero. It therefore suffices to give a constructive proof of
\Cref{surjection} in the special that~$A$ is such a kind of field.

Every entry of the given matrix is \notnot invertible or not invertible. Since
the statement we want to verify,~$1 = 0$, is~$\neg\neg$-stable, we may
assume that every entry is actually invertible or not invertible. If
one of the entries is invertible, we can change it to the unit, move it to the
top left, kill the remaining entries in the first row and in the first
column, and then continue in this fashion. We may thus assume that~$M$ is a
rectangular diagonal matrix having only zeros and ones on the diagonal.

XXX
\end{proof}


\subsection{Linear injections between finite free modules: McCoy's theorem}

\begin{prop}\label{injection}
Let~$M \in A^{n \times m}$ be a matrix over a ring~$A$ such that~$n
< m$. Assume that the induced linear map~$A^m \to A^n$ is injective. Then~$1 =
0 \in A$.
\end{prop}

\begin{proof}[Proof~A (classical)]
Assume to the contrary that~$1 \neq 0 \in A$. Then there exists a minimal prime
ideal~$\ppp$. Since localization is exact, the induced linear map~$A_\ppp^m \to
A_\ppp^n$ is still injective. Since the stalk~$A_\ppp$ has precisely one prime
ideal, any element of~$A_\ppp$ is either invertible or nilpotent.

If~$A$ happens to be reduced, a shortcut is available: In this case~$A_\ppp$ is
also reduced, therefore a field. Thus injectivity of the linear map~$A_\ppp^m
\to A_\ppp^n$ is a contradiction to basic linear algebra.

In the general case, we argue as follows. Any entry of the matrix is invertible
or nilpotent as an element of~$A_\ppp$. If the former case occurs for at least
one entry, we can employ elementary row and column transformations to change it
into the unit, move it to the top left, kill the remaining entries in the first
row and in the first column, and continue in this fashion with the
resulting~$((n-1) \times (m-1))$-submatrix.

We eventually obtain a matrix of the
form~$\left(\begin{smallmatrix}I&0\\0&M'\end{smallmatrix}\right)$, where~$I$ is
an identity matrix of appropriate size, the submatrix~$M'$ is still injective,
and all entries of~$M'$ are nilpotent. Let~$\aaa$ be the ideal of~$A_\ppp$
generated by the entries of~$M'$. Since all generators of~$\aaa$ are nilpotent,
there is a natural number~$n \geq 0$ such that~$\aaa^n = (0)$.

If~$n \geq 1$, then in fact~$\aaa^{n-1} = (0)$, since if~$x \in \aaa^{n-1}$,
then~$M' \cdot (x,0,\ldots,0)^t = 0$ (the coefficients of the resulting vector are
elements of~$\aaa^n$) and thus~$x = 0$ by injectivity. Repeating this argument
yields~$(1) = \aaa^0 = (0)$, thus~$1 = 0 \in A_\ppp$; a contradiction.
\end{proof}

\begin{proof}[Proof B (constructive)]By XXX, the given matrix~$M$ is also
injective as a matrix over~$A^\sim$. We may therefore pass from~$A$ to the
forcing model~$A^\sim$, allowing us to assume that that~$A$ is almost a field
in the sense that any element is \notnot invertible or nilpotent.

Since the statement we want to verify,~$1 = 0 \? A^\sim$, is~$\neg\neg$-stable,
we may assume that any entry of the matrix is invertible or nilpotent. We can
therefore proceed exactly as in Proof~A, only referring to~$A^\sim$ where that
proof refers to the stalk~$A_\ppp$.
\end{proof}

\begin{prop}Let~$M \in A^{n \times m}$ be a matrix over a ring~$A$. Assume that
the induced linear map~$A^m \to A^n$ is injective. Then~$(\Lambda^m M)$, the
ideal of~$m$-minors of~$M$, is regular.
\end{prop}

\begin{proof}Let~$a \? A^\sim$ be such that~$a \cdot (\Lambda^m M) = (0)$. We want
to verify that~$a = 0$. Instead of employing~$\neg\neg$ like on previous
occasions, we employ~$\negg\negg$, where~$\negg\varphi$ doesn't mean~$(\varphi
\Rightarrow \bot)$, but~$(\varphi \Rightarrow a = 0)$.

For any entry~$M_{ij}$ of the matrix, we~$\negg\negg$-have that it's invertible
or~$\negg($invertible$)$. The latter is equivalent to some power XXX
\end{proof}


\subsection{Nilpotent polynomials}

\begin{prop}Let~$f \in A[X]$ be a nilpotent polynomial over a ring~$A$. Then
the coefficients of~$f$ are nilpotent as elements of~$A$.
\end{prop}

\begin{proof}[Proof A (classical)]It suffices to show that the coefficients
of~$f$ are contained in every prime ideal of~$A$. Thus let~$\ppp$ be an
arbitrary prime ideal. Since some power of~$f$ is zero as an element of~$A[X]$,
a~forteriori it is zero as an element of~$(A/\ppp)[X]$. Since~$A/\ppp$ is an
integral domain, so is~$(A/\ppp)[X]$ (this requires a quick verification using
induction). Thus~$f$ is zero as an element of~$(A/\ppp)[X]$, so all of its
coefficients are elements of~$\ppp$.
\end{proof}

Proof~A is ineffective: It doesn't give any bounds on the indices of nilpotency
of the coefficients in terms of the index of nilpotency of~$f$.\footnote{The
proof does tell us that there is \emph{some} uniform bound, since we can apply
it to the generic situation, that is the polynomial~$f = \sum_i A_i X^i$ over the
ring~$\ZZ[A_0,\ldots,A_d]/(\ldots)$, where we put the individual coefficients of~$(\sum_i
A_i X^i)^n$ at~``$\ldots$''.} The standard way to mine Proof~A for effective
content is to employ a technique suitable for capturing the \emph{generic prime
ideal}, for instance \cite{XXXcoquand} or \cite{XXXschuster}. These techniques
come down to the forcing language of the space~$\Spec(A)$, but equipped with
the \emph{flat topology} (also called \emph{co-Zariski topology}), and allow
for a constructive interpretation of a verbatim copy of Proof~A.

The forcing language of the usual Zariski spectrum can also be used to XXX

\begin{proof}[Proof B (constructive)]
\end{proof}

\subsection{Grothendieck's generic freeness lemma}

XXX

\end{document}