5 The Partially Étale Case (Lemma 3.1)
This chapter proves the more general Lemma 3.1: monogenicity from an étale quotient through a height-one prime. The hypotheses are stronger on the rings (domains, integrally closed, UFD) but weaker on the map (only a quotient needs to be étale).
5.1 Sub-lemmas
In a UFD \(S\), every prime ideal \(\mathfrak {q}\) of height 1 is principal.
Since \(\mathfrak {q} \ne 0\), it contains an irreducible element \(p\). Then \(\operatorname {span}\{ p\} \) is prime and contained in \(\mathfrak {q}\). If \(\operatorname {span}\{ p\} \subsetneq \mathfrak {q}\), then \(\operatorname {height}(\operatorname {span}\{ p\} ) {\lt} \operatorname {height}(\mathfrak {q}) = 1\), forcing \(\operatorname {span}\{ p\} = 0\), contradicting \(p \ne 0\). Hence \(\mathfrak {q} = \operatorname {span}\{ p\} \).
For any polynomial \(f \in R[X]\) and elements \(x, h \in S\), there exists \(c \in S\) such that
Reduce modulo \(\operatorname {span}\{ h^2\} \) using \(\mathtt{Polynomial.aeval\_ add\_ of\_ sq\_ eq\_ zero}\), then lift.
Let \(R\) and \(S\) be local rings with \(S\) a finite \(R\)-algebra, and let \(\mathfrak {q} \subset S\) be a prime ideal. If the quotient map \(R/(\mathfrak {q} \cap R) \to S/\mathfrak {q}\) is étale, then
The quotient rings are local domains, and the étale condition on \(R/\mathfrak {p} \to S/\mathfrak {q}\) gives \(\mathfrak {m}_{R/\mathfrak {p}} \cdot (S/\mathfrak {q}) = \mathfrak {m}_{S/\mathfrak {q}}\) by \(\mathtt{Algebra.FormallyUnramified.map\_ maximalIdeal}\). Pulling back through the quotient maps, using \(\operatorname {map}(\operatorname {mk}\; \mathfrak {q})(\mathfrak {m}_S) = \mathfrak {m}_{S/\mathfrak {q}}\) and the analogous statement for \(R\), the equality lifts to \(\mathfrak {m}_S = \mathfrak {q} + \mathfrak {m}_R S\).
Let \(\mathfrak {q} \subset S\) be an ideal and \(\mathfrak {q} = \operatorname {span}\{ q_0\} \). Then for any \(\beta \in S\), the image of \(\beta + q_0\) in \(S/\mathfrak {q}\) is equal to the image of \(\beta \).
Since \((\beta + q_0) - \beta = q_0 \in \mathfrak {q}\), the elements are congruent modulo \(\mathfrak {q}\).
5.2 Nakayama Helpers
Let \(\mathfrak {q} \subset S\) be an ideal and \(\beta \in S\). If \(\beta \) generates \(S/\mathfrak {q}\) over \(R/(\mathfrak {q} \cap R)\), then for every \(s \in S\) there exists \(t \in R[\beta ]\) with \(s - t \in \mathfrak {q}\).
Since \((R/\mathfrak {p})[\bar\beta ] = S/\mathfrak {q}\), the map \(\operatorname {aeval}_{\bar\beta }\) is surjective. Lift a polynomial preimage of \(\bar s\) through \(\mathtt{Polynomial.map\_ surjective}\) to obtain \(t \in R[\beta ]\) with \(s - t \in \mathfrak {q}\).
Let \(R, S\) be local rings with \(S\) a finite \(R\)-algebra, and \(\mathfrak {q} \subset S\) a prime ideal. Let \(\beta \in S\) and \(\pi \in R[\beta ]\). Assume:
\(\bar\beta \) generates \(S/\mathfrak {q}\) over \(R/(\mathfrak {q} \cap R)\),
\(\mathfrak {m}_S = \operatorname {span}\{ \pi \} + \mathfrak {m}_R S\).
Then \(R[\beta ] = S\).
Set \(A = R[\beta ]\). The quotient \(S/\mathfrak {m}_R S\) is Artinian (finite over the field \(k_R\)), so \(\mathfrak {m}_S^n \subseteq \mathfrak {m}_R S\) for some \(n\).
Power bound. By induction, \(\mathfrak {m}_S^k \subseteq \operatorname {span}\{ \pi ^k\} + \mathfrak {m}_R S\), using the hypothesis on \(\mathfrak {m}_S\).
Iterative reduction. For \(x \in \mathfrak {q}\), by repeated application of quotient lifting (Lemma 13) and the power bound, we find \(a \in A\) with \(x - a \in \operatorname {span}\{ \pi ^n\} + \mathfrak {m}_R S \subseteq \mathfrak {m}_R S\).
Hence \(\mathfrak {q} \subseteq A + \mathfrak {m}_R S\) as \(R\)-submodules. Combined with the quotient lifting for general elements, \(S \subseteq A + \mathfrak {m}_R S\). By Nakayama’s lemma, \(A = S\).
5.3 Principal Adjustment Lemma
Let \((R, \mathfrak {m}_R)\) and \((S, \mathfrak {m}_S)\) be local domains with \(R\) integrally closed and \(S\) a finite \(R\)-algebra with faithful scalar action. Let \(\mathfrak {q} \subset S\) be a prime ideal with \(\mathfrak {q} = (q_0)\), and let \(\beta \in S\), \(f_1 \in R[X]\), \(a \in S\) satisfy:
\(f_1(\beta ) = q_0 \cdot a\) with \(a \in \mathfrak {m}_S\),
\(f_1'(\beta ) \notin \mathfrak {m}_S\),
\(\mathfrak {m}_S = \mathfrak {q} + \mathfrak {m}_R S\),
\(\bar\beta \) generates \(S/\mathfrak {q}\) over \(R/(\mathfrak {q} \cap R)\).
Then there exist a monic \(f \in R[X]\) and an \(\mathtt{IsAdjoinRootMonic}\) structure for \(S\) over \(f\).
Set \(\beta ' = \beta + q_0\). By Lemma 10, \(f_1(\beta ') = q_0 \cdot (a + f_1'(\beta ) + q_0 b)\) for some \(b \in S\). Since \(f_1'(\beta ) \notin \mathfrak {m}_S\) and \(a, q_0 b \in \mathfrak {m}_S\) (the former by hypothesis), the cofactor is a unit. Hence \(\operatorname {span}\{ f_1(\beta ')\} = \mathfrak {q}\), and \(\mathfrak {m}_S = \operatorname {span}\{ f_1(\beta ')\} + \mathfrak {m}_R S\).
Since \(\beta ' \equiv \beta \pmod{\mathfrak {q}}\) (Lemma 12), it still generates the quotient, so Lemma 14 gives \(R[\beta '] = S\). Finally, Theorem 2 provides the \(\mathtt{IsAdjoinRootMonic}\) structure for \(\operatorname {minpoly}_R \beta '\).
5.4 Main Theorem: Lemma 3.1
Let \((R, \mathfrak {m}_R)\) and \((S, \mathfrak {m}_S)\) be local domains with \(R\) integrally closed and \(S\) a UFD. Let \(R \to S\) be a finite injective ring homomorphism. If there exists a prime ideal \(\mathfrak {q} \subset S\) of height 1 such that the induced map \(R/(\mathfrak {q} \cap R) \to S/\mathfrak {q}\) is étale, then there exist a monic \(f \in R[X]\) and an \(\mathtt{IsAdjoinRootMonic}\) structure for \(S\) over \(f\).
Case 1: \(R \to S\) is already étale. Apply Theorem 7 to find \(\beta \) with \(R[\beta ] = S\), then Theorem 2 for the isomorphism.
Case 2: \(R \to S\) is not étale. Apply Theorem 7 to the étale quotient \(R_0 = R/\mathfrak {p} \to S_0 = S/\mathfrak {q}\) to get \(\beta _0 \in S_0\) with \(R_0[\beta _0] = S_0\). Lift to \(\beta \in S\).
By Lemma 9, \(\mathfrak {q} = (q_0)\) for some \(q_0 \in S\). Lift the minimal polynomial \(f_0 = \operatorname {minpoly}_{R_0} \beta _0\) to a monic \(f_1 \in R[X]\). By Lemma 11, \(\mathfrak {m}_S = \mathfrak {q} + \mathfrak {m}_R S\).
Sub-case 2a: If \(f_1(\beta )\) generates \(\mathfrak {m}_S\) modulo \(\mathfrak {m}_R S\), apply Lemma 14 directly to conclude \(R[\beta ] = S\).
Sub-case 2b: Otherwise, since \(f_1(\beta ) \in \mathfrak {q} = (q_0)\), write \(f_1(\beta ) = q_0 \cdot a\). If \(a\) were a unit, then \(\operatorname {span}\{ f_1(\beta )\} = \mathfrak {q}\) and Sub-case 2a would apply; so \(a \in \mathfrak {m}_S\). The derivative condition \(f_1'(\beta ) \notin \mathfrak {m}_S\) follows from Theorem 6 applied to the étale quotient. Now apply Lemma 15 with \(q_0\), \(\beta \), \(f_1\), and \(a\).