8. Miniproject: Frobenius Elements
8.1. Status
This miniproject has been a success: the main results are sorry-free and merged into mathlib. As a result there will be no more work on this miniproject in the FLT repo. Below is a fairly detailed sketch of the argument used.
8.2. Introduction And Goal
When this project started, I had thought that the existence of Frobenius elements was specific to the theory of local and global fields, and a slightly more general result held for Dedekind domains. Then Joel Riou pointed out on the Lean Zulip 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.
The goal of the mini-project is to get this theorem formalised and ideally into mathlib.
In particular, \Aut(L/K) is finite 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 or Noetherian hypotheses on the rings at
all.
8.3. 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 the
decomposition group D_Q of Q 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(L/K).
In the next definition we write down a group homomorphism \phi from D_Q
to \Aut(L/K).
-
IsFractionRing.stabilizerHom[complete]
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(L/K) (all the proofs
implicit in the definition here are straightforward).
Lean code for Definition8.3.1●1 definition
Associated Lean declarations
-
IsFractionRing.stabilizerHom[complete]
-
IsFractionRing.stabilizerHom[complete]
-
defdefined in Mathlib/RingTheory/Invariant/Basic.leancomplete
def IsFractionRing.stabilizerHom.{u_1, u_2, u_3, u_4, u_5} {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] (G : Type u_3) [Group G] [MulSemiringAction G B] [SMulCommClass G A B] (P : Ideal A) (Q : Ideal B) [Q.LiesOver P] (K : Type u_4) (L : Type u_5) [Field K] [Field L] [Algebra (A ⧸ P) K] [Algebra (B ⧸ Q) L] [Algebra (A ⧸ P) L] [IsScalarTower (A ⧸ P) (B ⧸ Q) L] [Algebra K L] [IsScalarTower (A ⧸ P) K L] [IsFractionRing (A ⧸ P) K] [IsFractionRing (B ⧸ Q) L] : ↥(MulAction.stabilizer G Q) →* Gal(L/K)
def IsFractionRing.stabilizerHom.{u_1, u_2, u_3, u_4, u_5} {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] (G : Type u_3) [Group G] [MulSemiringAction G B] [SMulCommClass G A B] (P : Ideal A) (Q : Ideal B) [Q.LiesOver P] (K : Type u_4) (L : Type u_5) [Field K] [Field L] [Algebra (A ⧸ P) K] [Algebra (B ⧸ Q) L] [Algebra (A ⧸ P) L] [IsScalarTower (A ⧸ P) (B ⧸ Q) L] [Algebra K L] [IsScalarTower (A ⧸ P) K L] [IsFractionRing (A ⧸ P) K] [IsFractionRing (B ⧸ Q) L] : ↥(MulAction.stabilizer G Q) →* Gal(L/K)
If `Q` lies over `P`, then the stabilizer of `Q` acts on `Frac(B/Q)/Frac(A/P)`.
The theorem we want in this mini-project is
-
IsFractionRing.stabilizerHom_surjective[complete]
The map g \mapsto \phi_g from D_Q to \Aut(L/K) defined above is
surjective.
Lean code for Theorem8.3.2●1 theorem
Associated Lean declarations
-
IsFractionRing.stabilizerHom_surjective[complete]
-
IsFractionRing.stabilizerHom_surjective[complete]
-
theoremdefined in Mathlib/RingTheory/Invariant/Basic.leancomplete
theorem IsFractionRing.stabilizerHom_surjective.{u_1, u_2, u_3, u_4, u_5} {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] (G : Type u_3) [Group G] [Finite G] [MulSemiringAction G B] [SMulCommClass G A B] (P : Ideal A) (Q : Ideal B) [Q.IsPrime] [Q.LiesOver P] (K : Type u_4) (L : Type u_5) [Field K] [Field L] [Algebra (A ⧸ P) K] [Algebra (B ⧸ Q) L] [Algebra (A ⧸ P) L] [IsScalarTower (A ⧸ P) (B ⧸ Q) L] [Algebra K L] [IsScalarTower (A ⧸ P) K L] [Algebra.IsInvariant A B G] [IsFractionRing (A ⧸ P) K] [IsFractionRing (B ⧸ Q) L] : Function.Surjective ⇑(IsFractionRing.stabilizerHom G P Q K L)
theorem IsFractionRing.stabilizerHom_surjective.{u_1, u_2, u_3, u_4, u_5} {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [Algebra A B] (G : Type u_3) [Group G] [Finite G] [MulSemiringAction G B] [SMulCommClass G A B] (P : Ideal A) (Q : Ideal B) [Q.IsPrime] [Q.LiesOver P] (K : Type u_4) (L : Type u_5) [Field K] [Field L] [Algebra (A ⧸ P) K] [Algebra (B ⧸ Q) L] [Algebra (A ⧸ P) L] [IsScalarTower (A ⧸ P) (B ⧸ Q) L] [Algebra K L] [IsScalarTower (A ⧸ P) K L] [Algebra.IsInvariant A B G] [IsFractionRing (A ⧸ P) K] [IsFractionRing (B ⧸ Q) L] : Function.Surjective ⇑(IsFractionRing.stabilizerHom G P Q K L)
The stabilizer subgroup of `Q` surjects onto `Aut(Frac(B/Q)/Frac(A/P))`.
The goal of this mini-project is to get this theorem formalised and ideally into mathlib.
In particular, \Aut(L/K) is finite 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 or Noetherian hypotheses on the rings at
all.
8.4. Examples
As a trivial consequence we get Frobenius elements for finite Galois extensions
in both the local and global field setting, as \Aut(L/K) 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 > 0 for the
extension L/K to be infinite (and mostly inseparable). The theorem implies
that \Aut(L/K) 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|. However, we can prove surjectivity directly without reference to
this maximal separable subextension.
8.5. 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 do not ever need the map
A \to B to be injective so we do not assume this.
We start with a construction which is fundamental to everything, and which
explains why we need G to be finite.
-
MulSemiringAction.charpoly[complete]
If b \in B then define the characteristic polynomial F_b(X) \in B[X]
of b to be \prod_{g \in G}(X - g \cdot b).
Lean code for Definition8.5.1●1 definition
Associated Lean declarations
-
MulSemiringAction.charpoly[complete]
-
MulSemiringAction.charpoly[complete]
-
defdefined in Mathlib/RingTheory/Invariant/Basic.leancomplete
def MulSemiringAction.charpoly.{u_2, u_3} {B : Type u_2} (G : Type u_3) [CommRing B] [Group G] [MulSemiringAction G B] [Fintype G] (b : B) : Polynomial B
def MulSemiringAction.charpoly.{u_2, u_3} {B : Type u_2} (G : Type u_3) [CommRing B] [Group G] [MulSemiringAction G B] [Fintype G] (b : B) : Polynomial B
Characteristic polynomial of a finite group action on a ring.
Clearly F_b is a monic polynomial.
-
MulSemiringAction.monic_charpoly[complete]
F_b is monic.
Lean code for Lemma8.5.2●1 theorem
Associated Lean declarations
-
MulSemiringAction.monic_charpoly[complete]
-
MulSemiringAction.monic_charpoly[complete]
-
theoremdefined in Mathlib/RingTheory/Invariant/Basic.leancomplete
theorem MulSemiringAction.monic_charpoly.{u_2, u_3} {B : Type u_2} (G : Type u_3) [CommRing B] [Group G] [MulSemiringAction G B] [Fintype G] (b : B) : (MulSemiringAction.charpoly G b).Monic
theorem MulSemiringAction.monic_charpoly.{u_2, u_3} {B : Type u_2} (G : Type u_3) [CommRing B] [Group G] [MulSemiringAction G B] [Fintype G] (b : B) : (MulSemiringAction.charpoly G b).Monic
Obvious.
It is 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 is not even
well-defined if the map A \to B is not injective.
-
Algebra.IsInvariant.charpoly_mem_lifts[complete]
F_b is the lift of some monic polynomial M_b in A[X].
Lean code for Lemma8.5.3●1 theorem
Associated Lean declarations
-
Algebra.IsInvariant.charpoly_mem_lifts[complete]
-
Algebra.IsInvariant.charpoly_mem_lifts[complete]
-
theoremdefined in Mathlib/RingTheory/Invariant/Basic.leancomplete
theorem Algebra.IsInvariant.charpoly_mem_lifts.{u_1, u_2, u_3} (A : Type u_1) (B : Type u_2) (G : Type u_3) [CommRing A] [CommRing B] [Algebra A B] [Group G] [MulSemiringAction G B] [Algebra.IsInvariant A B G] [Fintype G] (b : B) : MulSemiringAction.charpoly G b ∈ Polynomial.lifts (algebraMap A B)
theorem Algebra.IsInvariant.charpoly_mem_lifts.{u_1, u_2, u_3} (A : Type u_1) (B : Type u_2) (G : Type u_3) [CommRing A] [CommRing B] [Algebra A B] [Group G] [MulSemiringAction G B] [Algebra.IsInvariant A B G] [Fintype G] (b : B) : MulSemiringAction.charpoly G b ∈ Polynomial.lifts (algebraMap A B)
The coefficients of F_b are G-invariant, and thus lie in the image of
A.
-
Algebra.IsInvariant.isIntegral[complete]
B/A is integral.
Lean code for Theorem8.5.4●1 theorem
Associated Lean declarations
-
Algebra.IsInvariant.isIntegral[complete]
-
Algebra.IsInvariant.isIntegral[complete]
-
theoremdefined in Mathlib/RingTheory/Invariant/Basic.leancomplete
theorem Algebra.IsInvariant.isIntegral.{u_1, u_2, u_3} (A : Type u_1) (B : Type u_2) (G : Type u_3) [CommRing A] [CommRing B] [Algebra A B] [Group G] [MulSemiringAction G B] [Algebra.IsInvariant A B G] [Finite G] : Algebra.IsIntegral A B
theorem Algebra.IsInvariant.isIntegral.{u_1, u_2, u_3} (A : Type u_1) (B : Type u_2) (G : Type u_3) [CommRing A] [CommRing B] [Algebra A B] [Group G] [MulSemiringAction G B] [Algebra.IsInvariant A B G] [Finite G] : Algebra.IsIntegral A B
Use M_b.
If Q and Q' are two primes above p then there is 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.
8.6. The Extension (B/Q)/(A/P)
Note that P and Q are primes, so the quotients A/P and B/Q are
integral domains.
The following technical lemma constructs an element of B with nice
characteristic polynomial modulo Q.
- No associated Lean code or declarations.
There exist elements a,b \in B, with a \notin Q and a in the image
of A, such that for all g \in G:
-
If
g \cdot Q = Q, theng \cdot b \equiv a \pmod{Q}. -
If
g \cdot Q \neq Q, theng \cdot b \equiv 0 \pmod{Q}.
The ideals g \cdot Q \neq Q are not contained in Q. Since Q is a
prime ideal, this implies that the intersection of all g \cdot Q \neq Q is
still not contained in Q. Then we can find an element c \notin Q with
c \in g \cdot Q for all g \cdot Q \neq Q. Let F_c be the
characteristic polynomial of c, and write
F_c(X) \equiv X^j R(X) \pmod{Q}. Let a be the coefficient of X^j in
F_c(X), and choose R(X) so that R(0) = a. Let b = R(0) - R(c).
Note that F_c(c) = 0 and c \not\equiv 0 \pmod{Q}, so
R(c) \equiv 0 \pmod{Q}. Then b \equiv a \pmod{Q}, so
g \cdot b \equiv a \pmod{Q} whenever g \cdot Q = Q. But if
g \cdot Q \neq Q, then c \equiv 0 \pmod{g \cdot Q}. Then
b \equiv 0 \pmod{g \cdot Q}, so g \cdot b \equiv 0 \pmod{Q} whenever
g \cdot Q \neq Q.
A slight modification allows us to take an element of B fixed by D_Q as
input.
- No associated Lean code or declarations.
Let b_0 \in B. Suppose that the image of b_0 in the quotient B/Q is
fixed by the stabilizer subgroup D_Q. Then there exist elements
a,b \in B, with a \notin Q and a in the image of A, such that
for all g \in G:
-
If
g \cdot Q = Q, theng \cdot b \equiv a b_0 \pmod{Q}. -
If
g \cdot Q \neq Q, theng \cdot b \equiv 0 \pmod{Q}.
Multiply the b from Lemma 8.6.1 by b_0.
8.7. The Extension L/K
Let L^{D_Q} denote the fixed field of the action D_Q on L. Our
strategy for proving surjectivity of D_Q \to \Aut(L/K) will be to write
this map as the composition D_Q \to \Aut(L/L^{D_Q}) \to \Aut(L/K).
The surjectivity of the first map is a general fact of Galois theory.
-
FixedPoints.toAlgAut_surjective[complete]
If a finite group H acts on a field F by field automorphisms, then the
map H \to \Aut(F/F^H) is surjective.
Lean code for Theorem8.7.1●1 theorem
Associated Lean declarations
-
FixedPoints.toAlgAut_surjective[complete]
-
FixedPoints.toAlgAut_surjective[complete]
-
theoremdefined in Mathlib/FieldTheory/Fixed.leancomplete
theorem FixedPoints.toAlgAut_surjective.{u_2, u_3} (G : Type u_2) (F : Type u_3) [Group G] [Field F] [MulSemiringAction G F] [Finite G] : Function.Surjective ⇑(MulSemiringAction.toAlgAut G (↥(FixedPoints.subfield G F)) F)
theorem FixedPoints.toAlgAut_surjective.{u_2, u_3} (G : Type u_2) (F : Type u_3) [Group G] [Field F] [MulSemiringAction G F] [Finite G] : Function.Surjective ⇑(MulSemiringAction.toAlgAut G (↥(FixedPoints.subfield G F)) F)
`MulSemiringAction.toAlgAut` is surjective.
This is a general fact of Galois theory and was already in mathlib.
For surjectivity of the second map, we need to know that every element of
L^{D_Q} is fixed by \Aut(L/K). We first show this for elements of
B/Q fixed by D_Q.
Let b_0 \in B/Q. Suppose that b_0 is fixed by the stabilizer subgroup
D_Q. Then b_0 is fixed by \Aut(L/K).
Let a,b \in B be elements from fixed_of_fixed1_aux2. Let
M_b \in A[X] be the characteristic polynomial of b. We can map
M_b to L[X] in two different ways: via B[X] and via K[X].
Going via B[X] tells us that the image of M_b(X) in L[X] is exactly
(X - a b_0)^{|D_Q|} X^{|G|-|D_Q|}. But going via K[X] tells us that
this image lies in K[X], so we must have a b_0 \in K. Then
a b_0 is fixed by \Aut(L/K), and a is nonzero in L (since
a \notin Q), so b_0 is fixed by \Aut(L/K).
Now we upgrade this to elements of L fixed by D_Q. The following lemma
will allow us to lift the denominator from B/Q to A/P.
-
IsAlgebraic.exists_smul_eq_mul[complete]
If R/S is an algebraic extension of integral domains, then any fraction
a/b with a,b \in R can be written as c/d with c \in R and
d \in S.
Lean code for Lemma8.7.3●1 theorem
Associated Lean declarations
-
IsAlgebraic.exists_smul_eq_mul[complete]
-
IsAlgebraic.exists_smul_eq_mul[complete]
-
theoremdefined in Mathlib/RingTheory/Algebraic/Basic.leancomplete
theorem IsAlgebraic.exists_smul_eq_mul.{u_1, u_2} {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (a : S) {b : S} (hRb : IsAlgebraic R b) (hb : b ∈ nonZeroDivisors S) : ∃ c d, d ≠ 0 ∧ d • a = b * c
theorem IsAlgebraic.exists_smul_eq_mul.{u_1, u_2} {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (a : S) {b : S} (hRb : IsAlgebraic R b) (hb : b ∈ nonZeroDivisors S) : ∃ c d, d ≠ 0 ∧ d • a = b * c
A fraction `(a : S) / (b : S)` can be reduced to `(c : S) / (d : R)`, if `b` is algebraic over `R`.
If f \in S[X] satisfies f(b) = 0, then f(0) \in S is a multiple of
b. If f(0)=bx \in S, then a/b=(ax)/(bx) as desired.
- No associated Lean code or declarations.
Let x \in L. Suppose that x is fixed by the stabilizer subgroup D_Q.
Then x is fixed by the automorphism group \Aut(L/K).
Since (B/Q)/(A/P) is algebraic by Algebra.IsInvariant.isIntegral,
IsAlgebraic.exists_smul_eq_mul lets us write x=b/a for b \in B/Q and
a \in A/P. Then b is fixed by the stabilizer subgroup D_Q, and it
suffices to show that b is fixed by the automorphism group
\Aut(L/K). But this is exactly fixed_of_fixed1.
Combining this with Theorem 8.7.1 finishes the proof.
The map D_Q \to \Aut(L/L^{D_Q}) is surjective by
FixedPoints.toAlgAut_surjective. For surjectivity of
\Aut(L/L^{D_Q}) \to \Aut(L/K), let \sigma be a field automorphism of
L fixing K pointwise. We must show that \sigma automatically fixes
L^{D_Q} pointwise. But this is exactly fixed_of_fixed2. Thus, the
composition D_Q \to \Aut(L/L^{D_Q}) \to \Aut(L/K) is surjective.