3 The Étale Case (Lemma 3.2)

We now prove the main result for finite étale extensions of local rings: such extensions are monogenic, and the minimal polynomial has unit derivative.

3.1 Generator Descends to Residue Field

Lemma 3 Generator descends to residue fields

✓

If \(\beta \) generates \(S\) over \(R\) (i.e., \(R[\beta ] = S\)), then \(\bar\beta = \beta \bmod \mathfrak {m}_S\) generates \(k_S\) over \(k_R\).

Proof ▶

Given \(x \in k_S\), lift to \(s \in S\), express \(s = p(\beta )\) for some \(p \in R[X]\), then \(x = \bar{p}(\bar\beta )\) where \(\bar{p} = p \bmod \mathfrak {m}_R \in k_R[X]\). The key commutativity (\(\operatorname {residue}_S \circ \varphi = \operatorname {algebraMap}_{k_R \to k_S} \circ \operatorname {residue}_R\)) is used via \(\mathtt{map\_ aeval\_ eq\_ aeval\_ map}\).

3.2 Rank Equality across Residue Fields

Lemma 4 Rank preserved by residue field base change

✓

If \(R \to S\) is a finite étale extension of local rings with faithful scalar action, then

\[ \operatorname {finrank}_R S = \operatorname {finrank}_{k_R} k_S. \]

Proof ▶

Since \(R \to S\) is étale, it is smooth, hence flat. Finite + flat over a local ring implies free (\(\mathtt{Module.free\_ of\_ flat\_ of\_ isLocalRing}\)).

The étale condition gives \(\mathfrak {m}_R \cdot S = \mathfrak {m}_S\) (\(\mathtt{Algebra.FormallyUnramified.}\allowbreak \mathtt{map\_ maximalIdeal}\)), so \(S / \mathfrak {m}_R S \cong k_S\). By \(\mathtt{IsLocalRing.finrank\_ quotient\_ map}\), \(\operatorname {finrank}_{k_R}(S/\mathfrak {m}_R S) = \operatorname {finrank}_R S\). The quotient equivalence from \(\mathfrak {m}_R S = \mathfrak {m}_S\) transfers the finrank.

3.3 Minimal Polynomial Descends to Residue Field

Lemma 5 Minimal polynomial maps to residue minimal polynomial

✓

Let \(R \to S\) be a finite étale extension of local rings with faithful scalar action, and \(\beta \in S\) with \(R[\beta ] = S\). Then

\[ (\operatorname {minpoly}_R \beta ) \bmod \mathfrak {m}_R = \operatorname {minpoly}_{k_R} \bar\beta . \]

Proof ▶

Set \(f = \operatorname {minpoly}_R \beta \), \(\bar f = f \bmod \mathfrak {m}_R\), \(g = \operatorname {minpoly}_{k_R} \bar\beta \).

Since \(\bar\beta \) is a root of \(\bar f\) (by \(\mathtt{hom\_ eval_2}\)), we have \(g \mid \bar f\). Both \(f\) and \(g\) are monic, and \(\bar f\) is monic.

The degree chain:

\begin{align*} \deg \bar f & = \deg f & & \text{(monic polynomial preserves degree under reduction)} \\ & = \operatorname {finrank}_R S & & \text{(Theorem~ \ref{thm:mkOfAdjoinEqTop})} \\ & = \operatorname {finrank}_{k_R} k_S & & \text{(Lemma~ \ref{lem:finrank_eq_finrank_residueField})} \\ & = [k_R(\bar\beta ) : k_R] & & \text{(Lemma~ \ref{lem:adjoin_residue_eq_top}: } k_R[\bar\beta ] = k_S \text{)} \\ & = \deg g & & \text{(degree of minimal polynomial = extension degree)} \end{align*}

Since \(g \mid \bar f\), both are monic, and they have the same degree, \(\bar f = g\).

3.4 Unit Derivative Condition

Theorem 6 Derivative of minimal polynomial is a unit

✓

Let \(R \to S\) be a finite étale extension of local rings with faithful scalar action, and \(\beta \in S\) with \(R[\beta ] = S\). Then

\[ f'(\beta ) \in S^\times \]

where \(f = \operatorname {minpoly}_R \beta \).

Proof ▶

Since \(S\) is a local ring, it suffices to show \(\overline{f'(\beta )} \ne 0\) in \(k_S\) (\(\mathtt{IsLocalRing.}\allowbreak \mathtt{residue\_ ne\_ zero\_ iff\_ isUnit}\)).

Since \(R \to S\) is étale, the residue field extension \(k_R \to k_S\) is separable. By Lemma 5, \(\bar f = \operatorname {minpoly}_{k_R} \bar\beta \), so \(\bar f\) is separable (\(\mathtt{Algebra.IsSeparable.isSeparable}\)). This means \(\bar{f'}(\bar\beta ) \ne 0\) (\(\mathtt{Separable.aeval\_ derivative\_ ne\_ zero}\)).

By \(\mathtt{hom\_ eval_2}\), \(\overline{f'(\beta )} = \bar{f'}(\bar\beta ) \ne 0\).

3.5 Existence of Generator (Nakayama Argument)

Theorem 7 Finite étale local extensions are monogenic

✓

Let \(R \to S\) be a finite étale extension of local rings with faithful scalar action. Then there exists \(\beta \in S\) such that \(R[\beta ] = S\).

Proof ▶

By the primitive element theorem (\(\mathtt{Field.exists\_ primitive\_ element}\)), there exists \(\beta _0 \in k_S\) with \(k_R[\beta _0] = k_S\). Lift \(\beta _0\) to \(\beta \in S\) via \(\mathtt{Ideal.Quotient.mk\_ surjective}\).

It suffices to show \(\operatorname {Algebra.adjoin} R \{ \beta \} = \top \). By Nakayama’s lemma (\(\mathtt{Submodule.}\allowbreak \mathtt{le\_ of\_ le\_ smul\_ of\_ le\_ jacobson\_ bot}\)), it suffices to show \(S \subseteq R[\beta ] + \mathfrak {m}_R \cdot S\).

For any \(s \in S\), the residue \(\bar s \in k_S = k_R[\beta _0]\), so there exists \(t_0 \in R[\beta ]\) with \(\overline{t_0} = \bar s\). Then \(s - t_0 \in \mathfrak {m}_S = \mathfrak {m}_R \cdot S\) (using the étale condition \(\mathtt{Algebra.FormallyUnramified.map\_ maximalIdeal}\)).