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 \operatorname{Aut}(L/K)\) will be to write this map as the composition \(D_Q \to \operatorname{Aut}(L/L^{D_Q}) \to \operatorname{Aut}(L/K)\).

The surjectivity of the first map is a general fact of Galois theory.

TheoremFixedPoints.toAlgAut_surjective#

Let \(H\) be a finite group acting on a field \(F\) by field automorphisms. Then the map \(H \to \operatorname{Aut}(F/F^H)\) is surjective.

Proof

This is a general fact of Galois theory and was already in mathlib.

Lean

Formalized as FixedPoints.toAlgAut_surjective.

Sources
MathlibFixedPoints.toAlgAut_surjective
Used by 1
Used byIsFractionRing.stabilizerHom_surjective

For surjectivity of the second map, we need to know that every element of \(L^{D_Q}\) is fixed by \(\operatorname{Aut}(L/K)\). We first show this for elements of \(B/Q\) fixed by \(D_Q\).

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\).

LemmaIsAlgebraic.exists_smul_eq_mul#

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\).

Proof

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.

Lean

Formalized as IsAlgebraic.exists_smul_eq_mul.

Sources
MathlibIsAlgebraic.exists_smul_eq_mul

Combining this with FixedPoints.toAlgAut_surjective finishes the proof.

Proof of main theorem: shown with Theorem IsFractionRing.stabilizerHom_surjective.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.