FrobeniusProject.tex

\chapter{A project: Frobenius elements}\label{Frobenius_project}

\section{Introduction and goal}

I had thought that the existence of Frobenius elements was specific to the theory
of local and global fields, until Joel Riou pointed out
an extremely general result from from Bourbaki's Commutative Algebra
(Chapter V, Section 2, number 2, theorem 2, part (ii)). This beautiful
result is surely what we want to see in mathlib. Before we state Bourbaki's
theorem, let us set the scene.

\section{Statement of the theorem}

The set-up throughout this project:
$G$ is a finite group acting (via ring isomorphisms) on a commutative ring $B$,
and $A$ is the subring of $G$-invariants.

Say $Q$ is a prime ideal of $B$, whose pullback to $A$ is the prime ideal $P$.
Note that $G$ naturally acts on the ideals of $B$. Let's define the
\emph{decomposition group} $D_Q$ of $Q$ to be the subgroup of $G$ which
stabilizes $Q$ (just to be clear: $g\in D_Q$ means
$\{g\cdot q\, :\, q \in Q\}=Q$, not $\forall q\in Q, g\cdot q=q$).

Let $L$ be the field of fractions of the integral domain $B/Q$, and let $K$ be the
field of fractions of the subring $A/P$. Then $L$ is naturally a $K$-algebra.
In this generality $L/K$ may not even be finite or Galois, but we can still talk about
$\Aut_K(L)$.

In the next definition we write down a group homomorphism $\phi$ from $D_Q$ to $\Aut_K(L)$.

\begin{definition}
  \label{Bourbaki52222.stabilizer.toGaloisGroup}
  \lean{Bourbaki52222.stabilizer.toGaloisGroup}
  Choose $g\in D_Q$. Then the action of $g$ on $B$ gives us an induced
  $A/P$-algebra automorphism of $B/Q$ which extends to a $K$-algebra automorphism $\phi(g)$ of $L$.
  This construction $g\mapsto \phi(g)$ defines a group homomorphism from $D_Q$
  to $\Aut_K(L)$ (all the proofs implicit in the definition here are straightforward).
  \leanok
\end{definition}

The theorem we want in this project is
\begin{theorem}
  \label{Bourbaki52222.MulAction.stabilizer_surjective_of_action}
  \lean{Bourbaki52222.MulAction.stabilizer_surjective_of_action}
  \uses{Bourbaki52222.stabilizer.toGaloisGroup}
  The map $g\mapsto \phi_g$ from $D_Q$ to $\Aut_K(L)$ defined above is surjective.
\end{theorem}

The goal of this project is to get this theorem formalised and ideally into mathlib.

In particular, $\Aut_K(L)$ is finite, although we prove this beforehand and not
as a corollary. What is so striking about this theorem to me is that the only finiteness hypothesis
is on the group $G$ which acts; there are no finiteness hypotheses on the rings at all.

As a trivial consequence we get Frobenius elements for finite Galois extensions in both
the local and global field setting, as $\Aut_K(L)$ is just a Galois group of finite fields
in these cases, so by surjectivity we can lift a Frobenius element.

Even though $G$ is finite, it is possible in characteristic p for the extension $L/K$ to be
infinite (and mostly inseparable). The theorem implies that $\Aut_K(L)$ is always finite;
what is actually happening is that $L/K$ is algebraic and normal, and its maximal separable
subextension is finite of degree at most $|G|$. We prove these results along the way to the
proof of the main theorem.

\subsection{Examples}

These do not need to be formalised.

The basic example is when $B$ is the ring of integers of a finite Galois extension of $\Q$
(or equivalently the field obtained by adjoining all of the roots of
a monic polynomial with rational coefficients).
Then the Galois group $G$ acts on $B$, and the invariants $A$ are just $B\cap\Q=\Z$. If $Q$
is a nonzero prime ideal of $B$ then a standard result is that $B/Q$ is a finite field. Let's
call this field $k$. We deduce that $P=Q\cap \Z$ is a nonzero ideal (as $\Z/P$ injects into $B/Q$)
and hence must be
the principal ideal generated by a prime number $p$. This number $p$ is ``the prime below $Q$'',
and also the characteristic of $k$.

If $D$ is the subgroup of $G$ stabilizing $Q$ as a set, then $D$ acts on $k$, so we get
a map from $D$ to $\Gal(k/\F_p)$. The theorem states that this map is surjective.
Its kernel is the inertia subgroup of $Q$, which for all but finitely many primes of $B$
is the trivial group. So in these cases we get an \emph{isomorphism} from $D$ to $\Gal(k/\F_p)$
meaning that $D$ is cyclic, and furthermore has two canonical generators, one called $\Frob_Q$
(by Artin) and the other one unfortunately also called $\Frob_Q$ (by Deligne), which are inverses
to each other. If $Q$ and $Q'$ are two primes above $p$ then there's some $g\in G$ such that
$gQ=Q'$ and one can deduce from this that $\Frob_Q$ and $\Frob_{Q'}$ are conjugate. In particular
if $G$ is abelian then $\Frob_Q$ and $\Frob_{Q'}$ are equal, so we can call them both $\Frob_p$.

An example which demonstrates that things can get a bit stranger in characteristic $p$ is the
following (we restrict to $p=2$ but a generalisation of this pathology exists for all $p>0$).
We let $B=\mathbb{F}_2[X,Y]$ and $G=\{1,\tau\}$ with the involution $\tau$
fixing $Y$ and switching $X$, $X+Y$, i.e., $(\tau f)(X,Y)=f(X+Y, Y)$.
Hence $\tau$ fixes the sum and product of these two polynomials, and thus
$A\supset \mathbb{F}_2[X^2+XY,Y]$. One can check (and this needs checking) that this
is in fact an equality, and I believe that $B$ is free of
rank 2 over $A$ with basis $\{1,X\}$.
Now set $Q=(Y)$ so $P=YA$ and the quotient $(B/Q)/(A/P)$ is
$\mathbb{F}_2[X]/\mathbb{F}_2[X^2]$, and the corresponding extension
of the fields of fractions of these integral domains is a radical extension
$\mathbb{F}_2(X)/\mathbb{F}_2(X^2)$ of degree 2.
In other words, it is finite and normal, but not separable.

It appears that this construction behaves well with respect to tensor
products over $\mathbb{F}_2$ and filtered colimits (I have not thought about
how to make this rigorous), and assuming this is true, it will explain Bourbaki's
counterexample to the hope that $L/K$ is always finite. We now describe the counterexample
(exercise 9 of number 2)

The example is from the exercises in Bourbaki (exercise 9 of section 2 above, found at the end
of Chapter V). We let $B=\mathbb{F}_2[X_0,Y_0,X_1,Y_1,X_2,\ldots]$
be a polynomial ring in infinitely many variables $X_i$ and $Y_i$ indexed by the
naturals (or indeed by any infinite set), and $G$ is cyclic of order 2 with
the generator acting on $B$ via $X_n\mapsto X_n+Y_n$ and $Y_n\mapsto Y_n$.
If $Q$ is the ideal generated by the $Y_n$ then now $L/K$ is a radical extension of
infinite degree; the generator swaps $X_n$ and $X_n+Y_n$, so it fixes
their product $a_n\in A$, which becomes $X_n^2$ modulo $Q$, so all
of the $X_{i}$ will be algebraically independent in $L/K$ and $X_{i}^2\in K$.

\section{The extension $B/A$.}

The precise set-up we'll work in is the following. We fix $G$ a finite group acting
on $B$ a commutative ring, and we have another commutative ring $A$ such
that $B$ is an $A$-algebra and the image of $A$ in $B$ is precisely the $G$-invariant
elements of $B$. We don't ever need the map $A\to B$ to be injective so we don't assume this.

We start with a construction which is fundamental to everything,
and which explains why we need $G$ to be finite.

\begin{definition}
  \lean{MulSemiringAction.CharacteristicPolynomial.F}
  \label{MulSemiringAction.CharacteristicPolynomial.F}
  \leanok
  If $b\in B$ then define the \emph{characteristic polynomial}
  $F_b(X) \in B[X]$ of $b$ to be $\prod_{g\in G}(X-g\cdot b)$.
\end{definition}

Clearly $F_b$ is a monic polynomial of degree $|G|$. In fact this isn't clear:
if $B$ is the zero ring then $F_b=0$ has degree less than $|G|$.

\begin{lemma}
  \label{MulSemiringAction.CharacteristicPolynomial.F_degree}
  \lean{MulSemiringAction.CharacteristicPolynomial.F_degree}
  \uses{MulSemiringAction.CharacteristicPolynomial.F}
  \leanok
  If $B$ is nontrivial then $F_b$ is monic.
\end{lemma}
\begin{proof}
  \leanok
  Obvious.
\end{proof}

It's also clear that $F_b$ has degree $|G|$ and has $b$ as a root.
Also $F_b$ is $G$-invariant, because acting by some $\gamma\in G$
just permutes the order of the factors. Hence we can descend $F_b$
to a monic polynomial $M_b(X)$ of degree $|G|$ in $A[X]$. We will
also refer to $M_b$ as the characteristic polynomial of $b$, even though
it's not even well-defined if the map $A\to B$ isn't injective.

\begin{definition}
  \lean{MulSemiringAction.CharacteristicPolynomial.M}
  \label{MulSemiringAction.CharacteristicPolynomial.M}
  \uses{MulSemiringAction.CharacteristicPolynomial.F}
  \leanok
  $M_b$ is any monic degree $|G|$ polynomial in $A[X]$ whose
  image in $B[X]$ is $F_b$.
\end{definition}

\begin{lemma}
  \label{MulSemiringAction.CharacteristicPolynomial.M_eval_eq_zero}
  \lean{MulSemiringAction.CharacteristicPolynomial.M_eval_eq_zero}
  \uses{MulSemiringAction.CharacteristicPolynomial.M}
  \leanok
  $M_b$ has $b$ as a root.
\end{lemma}
\begin{proof}
  \leanok
  Follows from the fact that $F_b$ has $b$ as a root.
\end{proof}
\begin{lemma}
  \label{MulSemiringAction.CharacteristicPolynomial.M_deg}
  \lean{MulSemiringAction.CharacteristicPolynomial.M_deg}
  \uses{MulSemiringAction.CharacteristicPolynomial.M}
  \leanok
  $M_b$ has degree $n$.
\end{lemma}
\begin{proof}
  \uses{MulSemiringAction.CharacteristicPolynomial.F_degree}
  \leanok
  Exercise.
\end{proof}
\begin{lemma}
  \lean{MulSemiringAction.CharacteristicPolynomial.M_monic}
  \label{MulSemiringAction.CharacteristicPolynomial.M_monic}
  \uses{MulSemiringAction.CharacteristicPolynomial.M}
  \leanok
  $M_b$ is monic.
\end{lemma}
\begin{proof}
  \leanok
  Exercise.
\end{proof}

\begin{theorem}
  \lean{MulSemiringAction.CharacteristicPolynomial.isIntegral}
  \label{MulSemiringAction.CharacteristicPolynomial.isIntegral}
  \uses{MulSemiringAction.CharacteristicPolynomial.M}
  \leanok
  $B/A$ is integral.
\end{theorem}
\begin{proof}
  \uses{MulSemiringAction.CharacteristicPolynomial.M_monic}
  \leanok
  Use $M_b$.
\end{proof}

\section{The extension $(B/Q)/(A/P)$.}

Note that $Q$ is prime, so $B/Q$ is an integral domain and hence nontrivial.
Furthermore, all our polynomials are monic and hence nonzero (indeed they
all have degree $|G|$>0), so both Lean notions of degree coincide.

\begin{definition}
  \lean{MulSemiringAction.CharacteristicPolynomial.Mbar}
  \label{MulSemiringAction.CharacteristicPolynomial.Mbar}
  \uses{MulSemiringAction.CharacteristicPolynomial.M}
  \leanok
  If $\overline{b}\in B/Q$ then we define $\overline{M}_{\overline{b}}\in A/P[X]$
  to be the reduction of $M_b$ where $b$ is any lift of $\overline{b}$ to $B$.
\end{definition}

Say $\overline{b}\in B/Q$.

\begin{theorem}
  \lean{MulSemiringAction.CharacteristicPolynomial.Mbar_deg}
  \label{MulSemiringAction.CharacteristicPolynomial.Mbar_deg}
  \uses{MulSemiringAction.CharacteristicPolynomial.Mbar}
  \leanok
  $\overline{M}_{\overline{b}}$ has degree $|G|$.
\end{theorem}
\begin{proof}
  \uses{MulSemiringAction.CharacteristicPolynomial.M_deg,
    MulSemiringAction.CharacteristicPolynomial.M_monic}
  \leanok
  Exercise.
\end{proof}

\begin{theorem}
  \lean{MulSemiringAction.CharacteristicPolynomial.Mbar_monic}
  \label{MulSemiringAction.CharacteristicPolynomial.Mbar_monic}
  \uses{MulSemiringAction.CharacteristicPolynomial.Mbar}
  \leanok
  $\overline{M}_{\overline{b}}$ is monic.
\end{theorem}
\begin{proof}
  \uses{MulSemiringAction.CharacteristicPolynomial.M_monic}
  \leanok
  Exercise (note that integral domains are nontrivial).
\end{proof}

\begin{theorem}
  \lean{MulSemiringAction.CharacteristicPolynomial.Mbar_eval_eq_zero}
  \label{MulSemiringAction.CharacteristicPolynomial.Mbar_eval_eq_zero}
  \uses{MulSemiringAction.CharacteristicPolynomial.Mbar}
  \leanok
  $\overline{M}_{\overline{b}}$ has $\overline{b}$ as a root.
\end{theorem}
\begin{proof}
  \uses{MulSemiringAction.CharacteristicPolynomial.M_eval_eq_zero}
  \leanok
  Exercise.
\end{proof}

\begin{theorem}
  \lean{MulSemiringAction.reduction_isIntegral}
  \label{MulSemiringAction.reduction_isIntegral}
  \uses{MulSemiringAction.CharacteristicPolynomial.Mbar}
  \leanok
  $(B/Q)/(A/P)$ is an integral extension.
\end{theorem}
\begin{proof}
  \uses{MulSemiringAction.CharacteristicPolynomial.Mbar_monic,
    MulSemiringAction.CharacteristicPolynomial.Mbar_eval_eq_zero}
  Use $\overline{M}_{\overline{b}}$.
\end{proof}

Here is a corollary of this result: every nonzero element of $B/Q$ divides
a nonzero element of $A/P$.
\begin{corollary}
  \lean{Algebra.exists_dvd_nonzero_if_isIntegral}
  \label{Algebra.exists_dvd_nonzero_if_isIntegral}
  \leanok
  If $\beta\in B/Q$ is nonzero then there's some nonzero $\alpha\in A/P$
  such that $\beta$ divides the image of $\alpha$ in $B/Q$.
\end{corollary}
\begin{proof}
  \uses{MulSemiringAction.reduction_isIntegral}
  Note: Is this in mathlib already? This proof works for any
  integral extension if the top ring has no zero divisors.

  Let $\beta$ be nonzero, and
  consider the monic polynomial $\overline{M}_\beta(X)$, which is monic of
  degree $|G|$ and has $\beta$ as a root. Write $n=|G|$, so $f$ is monic
  of degree $n$. We cannot have $f(X)=X^n$ as this would imply that $\beta$ is
  nilpotent and hence zero, as $B/Q$ is an integral domain. Hence $f(X)=X^n+\cdots +\alpha X^d$
  for some $d<n$ and nonzero $\alpha\in A$. Again using the fact that $B/Q$ is an integral domain, we
  deduce that $\beta$ must a be root of $f/X^d=X^{n-d}+\cdots+\alpha=X(\cdots)+\alpha$, and setting
  $X=\beta$ shows that $\beta$ divides $\alpha$.
\end{proof}

\section{The extension $L/K$.}

\begin{theorem}
  \label{foo1}
If $\lambda\in L$ then there's a monic polynomial $P_\lambda\in K[X]$ of degree $|G|$
with $\lambda$ as a root, and which splits completely in $L[X]$.
\end{theorem}
\begin{proof}
  A general $\lambda\in L$ can be written as $\beta_1/\beta_2$ where $\beta_1,\beta_2\in B/Q$.
  The previous corollary showed that there's some nonzero $\alpha\in A/P$ such that $\beta_2$
  divides $\alpha$, and hence $\alpha\lambda\in B/Q$ (we just cleared denominators).
  Thus $\alpha\lambda$ is a root of some monic polynomial $f(x)\in (A/P)[X]$,
  by~\ref{MulSemiringAction.CharacteristicPolynomial.Mbar_eval_eq_zero}.
  The polynomial $f(\alpha x)\in (A/P)[X]$ thus
  has $\lambda$ as a root, but it is not monic; its leading term is $\alpha^n$.
  Dividing through in $K[X]$ gives us the polynomial we seek.
\end{proof}

\begin{corollary} The extension $L/K$ is algebraic and normal.
\end{corollary}
\begin{proof} \uses{foo1}
  Exercise using the previous theorem.
\end{proof}

Note that $L/K$ might not be separable and might have infinite degree. However

\begin{corollary} Any subextension of $L/K$ which is finite and separable over $K$
  has degree at most $|G|$.
\end{corollary}
\begin{proof}
  Finite and separable implies simple, and we've already seen that any
  element of $L$ has degree at most $|G|$ over $K$.
\end{proof}

\begin{corollary} The maximal separable subextension $M$ of $L/K$ has degree at most $|G|$.
\end{corollary}
\begin{proof} If it has dimension greater than $|G|$ over $K$, then it has a finitely-generated
  subfeld of $K$-dimension greater than $|G|$, and is finite and separable, contradicting
  the previous result.
\end{proof}

\begin{corollary} $\Aut_K(L)$ is finite.
\end{corollary}
\begin{proof} Any $K$-automorphism of $L$ is determined by where it sends $M$.
\end{proof}

\begin{corollary} $\Aut_{A/P}(B/Q)$ is finite.
\end{corollary}
\begin{proof}
  Two elements of $\Aut_{A/P}(B/Q)$ which agree once extended to automorphisms of $L$
  must have already been equal, as $B/Q\subseteq L$. Hence the canonical map
  from $\Aut_{A/P}(B/Q)$ to $\Aut_K(L)$ is injective.
\end{proof}

\section{Proof of surjectivity.}

\begin{definition} We fix once and for all some nonzero $y\in B/Q$ such that $M=K(y)$,
  with $M$ the maximal separable subextension of $L/K$.
\end{definition}

NB we do use nonzeroness at some point, and $y$ can be zero in the case $L=K$
(this seems to have been missed by Bourbaki).

Note that the existence of some $\lambda\in L$ with this property just comes from finite
and separable implies simple; we can use the ``clear denominator'' technique introduced
earlier to scale this by some nonzero $\alpha\in A$ into $B/Q$, as
$K(\lambda)=K(\alpha\lambda)$.

Our next goal is the following result:
\begin{theorem} There exists some $x\in B$ and $\alpha\in A$ with the following
  properties.
  \begin{enumerate}
  \item $x=\alpha y$ mod $Q$ and $\alpha$ isn't zero mod $P$.
  \item $x\in Q'$ for all $Q'\not=Q$ in the $G$-orbit of $Q$.
  \end{enumerate}
\end{theorem}

Bourbaki only prove this in the case that $P$ is maximal (and implicitly use $\alpha=1$),
but this generalisation seems to be fine. To prove it, we need to talk a little about localization.

Let $S$ be the complement of $P$, so $S$ is a multiplicative subset of $A$.
Write $A[1/S]$ for the localisation of $A$ at $S$, and write $B[1/S]$
for the localisation of $B$ at (the image of) $S$. I suspect that this is the
same as $B\otimes_AA[1/S]$.

\begin{lemma}
  The prime ideals of $B[1/S]$ over $P[1/S] \subseteq A[1/S]$ biject naturally with
  the prime ideals of $B$ over $P$. More precisely, the $B$-algebra $B[1/S]$
  gives a canonical map $B\to B[1/S]$ and hence a canonical map from prime ideals
  of $B[1/S]$ to prime ideals of $B$. The claim is that this map induces
  a bijection between the primes of $B[1/S]$ above $P[1/S]$ and the primes
  of $B$ above $P$.
\end{lemma}
\begin{proof}
  Hopefully this is in mathlib in some form already. In general $\Spec(B[1/S])$ is just the subset of $\Spec(B)$
  consisting of primes of $B$ which miss $S$ (i.e., whose intersection with $A$ is a subset of $P$).
\end{proof}

\begin{lemma}
  The primes of $B[1/S]$ above $P[1/S]$ are all maximal.
\end{lemma}
\begin{proof}
  This follows from {\tt Algebra.IsIntegral.isField\_iff\_isField} and the fact
  that an ideal is maximal iff the quotient by it is a field.
\end{proof}

\begin{proof}(of theorem):
Because all these ideals of $B[1/S]$ are maximal, they're pairwise coprime.
So by the Chinese Remainder Theorem we can find an element of $B[1/S]$ which
is equal to $y$ modulo $Q[1/S]$ and equal to $0$ modulo all the other primes.
This element is of the form $x/\alpha$ for some $x\in B$ and $\alpha\in S$,
and one now checks that everything works.
\end{proof}

It is probably worth remarking that the rest of the surjectivity argument was done
by Jou Glasheen in the special case of number fields, in the file {\tt Frobenius2.lean}

Briefly: we consider the monic degree $|G|$ polynomial $f_x$ in $K[X]$ or $\overline{M}_x$ in $(A/P)[X]$,
which has $x$ and its G-conjugates as roots. If $\sigma\in\Aut_K(L)$ then $\sigma(\overline{x})$
is a root of $f$ as $\sigma$ fixes $K$ pointwise. Hence $\sigma(\overline{x})=\overline{g(x)}$
for some $g\in G$ (because we're over an integral domain), and because $\sigma(\overline{x})\not=0$ we have $\overline{g(x)}\not=0$
and hence $g(x)\notin Q[1/S]$. Hence $x\notin g^{-1} Q[1/S]$ and thus $g^{-1}Q=Q$ and $g\in SD_Q$.
Finally we have $\phi_g=\sigma$ on $K$ and on $y$, so they are equal on $M$ and hence on $L$ as
$L/M$ is purely inseparable.

TODO: break this up into smaller pieces.