Dependency graph

Legend

Boxes: definitions
Ellipses: theorems and lemmas
Blue border: the statement of this result is ready to be formalized; all prerequisites are done
Orange border: the statement of this result is not ready to be formalized; the blueprint needs more work
Blue background: the proof of this result is ready to be formalized; all prerequisites are done
Green border: the statement of this result is formalized
Green background: the proof of this result is formalized
Dark green background: the proof of this result and all its ancestors are formalized
Dark green border: this is in Mathlib

Lemma 14Nakayama argument for quotient generation

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

LaTeX Lean

Lemma 3Generator 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\).

LaTeX Lean

Lemma 13Quotient lifting

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

LaTeX Lean

Lemma 15Adjustment by principal generator

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

LaTeX Lean

Lemma 4Rank 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. \]

LaTeX Lean

Lemma 9Height-one primes are principal in UFDs

In a UFD \(S\), every prime ideal \(\mathfrak {q}\) of height 1 is principal.

LaTeX Lean

Lemma 11Maximal ideal decomposition from étale quotient

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

\[ \mathfrak {m}_S = \mathfrak {q} + \mathfrak {m}_R \cdot S. \]

LaTeX Lean

Lemma 5Minimal 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 . \]

LaTeX Lean

Lemma 1Minimal polynomial degree bound

Let \(R \to S\) be a finite free extension with \(R\) nontrivial. For any \(\alpha \in S\),

\[ \deg (\operatorname {minpoly}_R \alpha ) \le \operatorname {finrank}_R S. \]

LaTeX Lean

Lemma 12Quotient adjustment

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

LaTeX Lean

Lemma 10Taylor expansion for polynomial evaluation

For any polynomial \(f \in R[X]\) and elements \(x, h \in S\), there exists \(c \in S\) such that

\[ f(x + h) = f(x) + f'(x) \cdot h + h^2 \cdot c. \]

LaTeX Lean

Theorem 8Standard étale from monogenic with unit derivative

Let \(f \in R[X]\) be monic with \(S \cong R[X]/(f)\) (via an \(\mathtt{IsAdjoinRootMonic}\) structure). If \(f'(\beta ) \in S^\times \) where \(\beta \) is the image of \(X\), then \(R \to S\) is étale.

LaTeX Lean

Theorem 7Finite é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\).

LaTeX Lean

Theorem 16Monogenicity from étale height-one quotient

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

LaTeX Lean

Theorem 6Derivative 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 \).

LaTeX Lean

Theorem 2Quotient isomorphism without integrally closed hypothesis

Let \(R \to S\) be a finite free extension with \(R\) nontrivial, and let \(\alpha \in S\) with \(R[\alpha ] = S\). Then \(f = \operatorname {minpoly}_R \alpha \) is monic, and the natural map

\[ \varphi \colon R[X]/(f) \longrightarrow S, \qquad X \mapsto \alpha \]

is an \(R\)-algebra isomorphism. In particular, \(S\) admits an \(\mathtt{IsAdjoinRootMonic}\) structure for \(f\).

LaTeX Lean