6 Plan for Mathlib PRs

This chapter outlines a strategy for upstreaming the formalized results into Mathlib via a sequence of small, self-contained pull requests. Each PR should be independently reviewable and useful.

Throughout, we reference Mathlib file paths as of the current toolchain. The key Mathlib files involved are:

• Mathlib/RingTheory/IsAdjoinRoot.lean — defines IsAdjoinRoot, IsAdjoinRootMonic, and finrank_quotient_span_eq_natDegree’. Imports FieldTheory.Minpoly.IsIntegrallyClosed and RingTheory.PowerBasis. Does not transitively import LinearAlgebra.Charpoly.Basic.

• Mathlib/RingTheory/Etale/Basic.lean — defines Algebra.Etale.

• Mathlib/RingTheory/Etale/StandardEtale.lean — defines StandardEtalePair, StandardEtalePresentation, and Algebra.IsStandardEtale.

• Mathlib/RingTheory/Unramified/LocalRing.lean — contains FormallyUnramified.map_maximalIdeal.

• Mathlib/RingTheory/LocalRing/ResidueField/ — Defs.lean (defines residue, ResidueField), Basic.lean (surjectivity, kernel), Instances.lean (separability instances).

• Mathlib/RingTheory/LocalRing/Quotient.lean — contains finrank_quotient_map and exists_maximalIdeal_pow_le_of_isArtinianRing_quotient.

• Mathlib/RingTheory/LocalRing/Module.lean — contains Module.free_of_flat_of_isLocalRing.

• Mathlib/RingTheory/Ideal/Height.lean — defines Ideal.height.

• Mathlib/FieldTheory/PrimitiveElement.lean — contains Field.exists_primitive_element.

• Mathlib/RingTheory/Nakayama.lean — contains Submodule.le_of_le_smul_of_le_jacobson_bot.

• Mathlib/Algebra/Polynomial/Taylor.lean — contains aeval_add_of_sq_eq_zero.

6.1 PR 1: Quotient Isomorphism without Integrally Closed

Declarations

• minpoly.natDegree_le’: For a finite free extension with \(R\) nontrivial, \(\deg (\operatorname {minpoly}_R \alpha ) \le \operatorname {finrank}_R S\). Generalizes the existing minpoly.natDegree_le in FieldTheory/IntermediateField/Adjoin/Basic.lean (which requires \(K, L\) to be fields with FiniteDimensional).

• IsAdjoinRootMonic.mkOfAdjoinEqTop’: If \(R[\alpha ] = S\) and \(S\) is finite free over \(R\), then \(S\) admits an IsAdjoinRootMonic structure for \(\operatorname {minpoly}_R \alpha \).

File placement

Option A (preferred): Both declarations go into Mathlib/RingTheory/IsAdjoinRoot.lean. This is where IsAdjoinRootMonic, finrank_quotient_span_eq_natDegree’, and the existing adjoin-root machinery live.

Import issue: natDegree_le’ uses LinearMap.aeval_self_charpoly and charpoly_natDegree from Mathlib.LinearAlgebra.Charpoly.Basic, which is not a transitive import of IsAdjoinRoot.lean. Adding this import may be acceptable since the file already has heavy imports (PowerBasis, Minpoly.IsIntegrallyClosed), but reviewers may prefer a separate file.

Option B: Put natDegree_le’ in a new file Mathlib/FieldTheory/Minpoly/Basic.lean (or Mathlib/RingTheory/Polynomial/Minpoly/Degree.lean), then import it from IsAdjoinRoot.lean for mkOfAdjoinEqTop’.

Namespace and naming

• minpoly.natDegree_le’: Currently uses _root_ prefix to escape the Monogenic namespace. In Mathlib, consider renaming to minpoly.natDegree_le_finrank or similar, and whether to replace the existing field-level minpoly.natDegree_le or keep both.

• IsAdjoinRootMonic.mkOfAdjoinEqTop’: Already in the correct namespace (matching the Mathlib original IsAdjoinRootMonic.mkOfAdjoinEqTop). For Mathlib, the prime suffix should be dropped; the existing Mathlib version requires IsIntegrallyClosed, so this would replace it.

Required imports (for the declarations)

• Mathlib.LinearAlgebra.Charpoly.Basic (for aeval_self_charpoly, charpoly_natDegree, charpoly_monic).

• Mathlib.RingTheory.OrzechProperty (for injective_of_surjective_endomorphism; likely already transitive via IsAdjoinRoot).

• Mathlib.RingTheory.IsAdjoinRoot (for IsAdjoinRootMonic, AdjoinRoot.liftAlgHom, finrank_quotient_span_eq_natDegree’).

Proof adjustments for Mathlib style

• The current proof of natDegree_le’ uses classical and local let bindings for basis and matrix. This should be rewritten to avoid classical if possible (use Decidable instances or restructure).

• Drop the Monogenic namespace wrapper.

• Add docstrings in Mathlib format.

• The current proof uses Module.finrank_eq_card_chooseBasisIndex; check this is still the canonical spelling.

Potential issues

• Import weight: adding Charpoly.Basic to the import tree of IsAdjoinRoot.lean may increase compile times. Measure before submitting.

• The existing minpoly.natDegree_le for fields is proved via IntermediateField.adjoin.finrank. Reviewers may ask if the field version should be deduced from the ring version or kept separate.

6.2 PR 2: Residue Field Properties for Étale Local Extensions

Declarations

• adjoin_residue_eq_top_of_adjoin_eq_top: If \(R[\beta ] = S\) then \(k_R[\bar\beta ] = k_S\).

• finrank_eq_finrank_residueField: \(\operatorname {finrank}_R S = \operatorname {finrank}_{k_R} k_S\) for finite étale local extensions.

• minpoly_map_residue: For a finite étale local extension with \(R[\beta ] = S\): \((\operatorname {minpoly}_R \beta ) \bmod \mathfrak {m}_R = \operatorname {minpoly}_{k_R} \bar\beta \).

• isUnit_aeval_derivative_minpoly_of_adjoin_eq_top: For a finite étale local extension with \(R[\beta ] = S\), \(f'(\beta ) \in S^\times \) where \(f = \operatorname {minpoly}_R \beta \).

File placement

Preferred: A new file Mathlib/RingTheory/LocalRing/ResidueField/Minpoly.lean or Mathlib/RingTheory/Etale/Monogenic.lean that collects these cohesive residue field properties for étale local extensions.

Namespace

IsLocalRing or Algebra.Etale namespace.

Required imports

• Mathlib.RingTheory.LocalRing.ResidueField.Defs (for residue, ResidueField).

• Mathlib.RingTheory.Unramified.LocalRing (for FormallyUnramified.map_maximalIdeal, used by finrank_eq_finrank_residueField).

• Mathlib.RingTheory.Smooth.Flat (for Algebra.Smooth.flat, used in the étale \(\Rightarrow \) free chain).

• Mathlib.RingTheory.LocalRing.Module (for free_of_flat_of_isLocalRing).

• Mathlib.RingTheory.LocalRing.Quotient (for finrank_quotient_map).

• IsAdjoinRootMonic.mkOfAdjoinEqTop’ from PR 1 (used in the degree chain: \(\deg f = \operatorname {finrank}_R S\) via .finrank).

• Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (for IntermediateField.adjoin.finrank, adjoin_simple_toSubalgebra_of_isAlgebraic).

• Mathlib.FieldTheory.Separable (for Algebra.IsSeparable.isSeparable, Separable.aeval_derivative_ne_zero).

Proof structure

• Residue generator & rank: finrank_eq_finrank_residueField uses étale \(\Rightarrow \) smooth \(\Rightarrow \) flat \(\Rightarrow \) free.

• Minimal polynomial descent: minpoly_map_residue compares degrees: \(g \mid \bar f\), both monic, same degree \(\Rightarrow \) equal. The degree chain uses mkOfAdjoinEqTop’.finrank (PR 1), finrank_eq_finrank_residueField, and IntermediateField.adjoin.finrank (Mathlib).

• Unit derivative: Reduce to residue field via minpoly_map_residue, apply separability of \(k_R \to k_S\) (from étale), conclude \(\bar{f'}(\bar\beta ) \ne 0\), lift back to unit via IsLocalRing.residue_ne_zero_iff_isUnit.

Potential issues

• finrank_eq_finrank_residueField uses the étale \(\Rightarrow \) smooth \(\Rightarrow \) flat chain. Consider whether to state it more generally for “finite free local extensions where \(\mathfrak {m}_R S = \mathfrak {m}_S\)”.

• The étale hypothesis is used only to get \(\operatorname {finrank}_R S = \operatorname {finrank}_{k_R} k_S\). If this equality holds more generally, the minpoly_map_residue lemma could be stated without Algebra.Etale. Reviewers may ask for this generalization.

• The hypothesis chain étale \(\Rightarrow \) separable residue field should be automatic, but verify the instance path works: Algebra.Etale R S \(\Rightarrow \) Algebra.FormallyUnramified R S \(\Rightarrow \) Algebra.IsSeparable kR kS.

• Uses eq_of_monic_of_dvd_of_natDegree_le — verify this is still the canonical Mathlib name.

6.3 PR 3: Finite Étale Local Extensions are Monogenic

Declarations

• exists_adjoin_eq_top: For a finite étale local extension \(R \to S\) with faithful scalar action, \(\exists \beta \in S,\; R[\beta ] = S\).

File placement

Preferred: New file Mathlib/RingTheory/Etale/Monogenic.lean or Mathlib/RingTheory/Etale/LocalRing.lean. This is a natural home for étale-specific results about local rings.

Namespace

Algebra.Etale.exists_adjoin_eq_top or just in the root namespace with appropriate variable scoping.

Required imports

• Mathlib.FieldTheory.PrimitiveElement (for Field.exists_primitive_element).

• Mathlib.RingTheory.Unramified.LocalRing (for FormallyUnramified.map_maximalIdeal).

• Mathlib.RingTheory.Nakayama (for Submodule.le_of_le_smul_of_le_jacobson_bot).

• Mathlib.RingTheory.LocalRing.ResidueField.Defs (for residue, ResidueField).

Proof structure

Primitive element theorem gives \(\beta _0 \in k_S\) with \(k_R[\beta _0] = k_S\). Lift to \(\beta \in S\). Show \(S \subseteq R[\beta ] + \mathfrak {m}_R S\): for each \(s \in S\), lift a polynomial preimage of \(\bar s\) through \(\mathtt{Polynomial.map\_ surjective}\) to find \(t \in R[\beta ]\) with \(s - t \in \mathfrak {m}_S = \mathfrak {m}_R S\). Conclude by Nakayama.

Potential issues

• This PR is independent of PRs 1 and 2. It does not need mkOfAdjoinEqTop’ or minpoly_map_residue; it only produces a generator \(\beta \), not an isomorphism \(S \cong R[X]/(f)\).

• The proof uses IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic to convert between Algebra.adjoin and IntermediateField.adjoin in the residue field. This is a common pattern but sometimes fragile with universe issues.

• The FaithfulSMul R S hypothesis is equivalent to injectivity of \(\varphi \). Reviewers may prefer IsLocalHom (algebraMap R S) or just Function.Injective (algebraMap R S). Note faithfulSMul_iff_algebraMap_injective exists in Mathlib.

6.4 PR 4: Converse — Standard Étale from Unit Derivative

Declarations

• IsAdjoinRootMonic.algebra_etale: If \(S \cong R[X]/(f)\) (via IsAdjoinRootMonic) and \(f'(\beta ) \in S^\times \), then \(R \to S\) is étale.

File placement

Preferred: Mathlib/RingTheory/Etale/StandardEtale.lean, directly after the definition of StandardEtalePair and Algebra.IsStandardEtale. This is where the standard étale machinery lives and the proof constructs a StandardEtalePair.

Namespace

IsAdjoinRootMonic.algebra_etale (already correctly namespaced).

Required imports

• Mathlib.RingTheory.Etale.StandardEtale (for StandardEtalePair, HasMap, lift, hom_ext, Algebra.IsStandardEtale).

• Mathlib.RingTheory.IsAdjoinRoot (for IsAdjoinRootMonic, adjoinRootAlgEquiv, map_surjective).

Both of these should already be in the import tree of StandardEtale.lean, so no new imports are needed if placed there.

Proof structure

Construct StandardEtalePair R with \(f, f', 1, 0, 1\) and the trivial Bézout relation \(f' \cdot 1 + f \cdot 0 = (f')^1\). Build an explicit inverse of P.lift by composing AdjoinRoot.liftAlgHom with adjoinRootAlgEquiv.symm. Verify left/right inverse on generators via P.hom_ext.

Potential issues

• This theorem essentially says “standard étale presentations arise from adjoin-root-monic with unit derivative.” Mathlib may already have something close or the reviewers may want to restructure. Check for overlap with existing material in StandardEtale.lean.

• The proof uses AdjoinRoot.liftAlgHom which was recently introduced as a replacement for the deprecated AdjoinRoot.liftHom. Verify this is still the current API.

6.5 PR 5: Nakayama Helpers and Partially Étale Case (Lemma 3.1)

This is the most complex PR. It should likely be split into several sub-PRs.

Sub-PR 5a: Height-One Primes in UFDs are Principal

Declaration: Ideal.exists_span_singleton_eq_of_prime_of_height_one

File: Mathlib/RingTheory/Ideal/Height.lean (append to existing file).

Imports: Only needs Ideal.height, IsPrime, UniqueFactorizationMonoid. All already in that file’s import tree.

Notes: Self-contained, no dependencies on other PRs. This is a basic fact about UFDs that should be independently useful. The proof uses IsPrime.exists_mem_prime_of_ne_bot, height_strict_mono_of_is_prime, and primeHeight_eq_zero_iff.

Sub-PR 5b: Taylor Expansion for Polynomial Evaluation

Declaration: exists_aeval_add_eq: \(f(x+h) = f(x) + f'(x)h + h^2 c\).

File: Mathlib/Algebra/Polynomial/Taylor.lean (append to existing file, which already has aeval_add_of_sq_eq_zero).

Imports: Only needs Polynomial.Taylor (already there) and Ideal.Quotient basics.

Notes: Self-contained. The proof reduces mod \(\langle h^2 \rangle \) using aeval_add_of_sq_eq_zero, then lifts via Ideal.mem_span_singleton. Very clean.

Sub-PR 5c: Maximal Ideal Decomposition and Quotient Lifting

Declarations:

• maximalIdeal_eq_sup_of_etale_quotient: If \(R/\mathfrak {p} \to S/\mathfrak {q}\) is étale, then \(\mathfrak {m}_S = \mathfrak {q} + \mathfrak {m}_R S\).

• exists_adjoin_sub_mem: Quotient lifting.

• adjoin_eq_top_of_quotient: Nakayama with quotient generation.

File: New file, perhaps Mathlib/RingTheory/LocalRing/Quotient/Etale.lean or Mathlib/RingTheory/Etale/LocalRing.lean.

Imports:

• Mathlib.RingTheory.Unramified.LocalRing (for FormallyUnramified.map_maximalIdeal).

• Mathlib.RingTheory.RingHom.Etale (for RingHom.Etale).

• Mathlib.RingTheory.LocalRing.Quotient (for exists_maximalIdeal_pow_le_of_isArtinianRing_quotient).

• Mathlib.RingTheory.Nakayama.

Notes:

• maximalIdeal_eq_sup_of_etale_quotient has a somewhat long proof involving quotient maps and the commutative square \(\operatorname {map}(\operatorname {mk}\; \mathfrak {q})\). It uses Ideal.map_eq_iff_sup_ker_eq_of_surjective which may be fragile.

• adjoin_eq_top_of_quotient is the most intricate proof in the project (Artinian descent + iterative reduction + Nakayama). It is already decomposed into helper lemmas: Ideal.pow_le_span_pow_sup (pure ideal arithmetic) and exists_sub_mem_adjoin_of_pow (iterative approximation).

• exists_adjoin_sub_mem lifts polynomials through the quotient map via Polynomial.map_surjective.

Sub-PR 5d: Main Theorem (Lemma 3.1)

Declarations:

• exists_isAdjoinRootMonic_of_principal_adjust: The principal adjustment sub-case (Case 2b), extracted as a standalone lemma.

• exists_isAdjoinRootMonic_of_quotientMap_etale: The main theorem.

File: Same as 5c, or a dedicated file Mathlib/RingTheory/Etale/Monogenic.lean.

Dependencies: PRs 1, 2, 3, and sub-PRs 5a–5c.

Imports (beyond 5c):

• Mathlib.RingTheory.Ideal.Height (for height-one primes, 5a).

• Mathlib.Algebra.Polynomial.Taylor (for Taylor expansion, 5b).

• Mathlib.Algebra.Polynomial.Lifts (for lifts_and_degree_eq_and_monic, used to lift \(f_0 \in R_0[X]\) to monic \(f_1 \in R[X]\)).

• PR 1 (mkOfAdjoinEqTop’, used to build the isomorphism).

• PR 2 (isUnit_aeval_derivative_minpoly_of_adjoin_eq_top, for the derivative non-vanishing in Case 2b).

• PR 3 (exists_adjoin_eq_top, applied to the étale quotient).

Proof structure: Case split on whether \(R \to S\) is already étale. Case 1 uses PR 3 + PR 1 directly. Case 2 lifts a generator from the étale quotient, then either (2a) applies the Nakayama argument directly, or (2b) extracts \(a\) with \(f_1(\beta ) = q_0 \cdot a\) and shows \(a \in \mathfrak {m}_S\) (if \(a\) were a unit, Sub-case 2a would apply), then delegates to exists_isAdjoinRootMonic_of_principal_adjust.

Notes:

• The hypotheses include IsIntegrallyClosed R and UniqueFactorizationMonoid S. These are strong; reviewers may ask whether they can be weakened.

• An alternative formulation with an explicit ring homomorphism (transferring between \(\operatorname {Algebra.adjoin}\; R\) and \(\operatorname {Algebra.adjoin}\; \varphi (R)\)) could be added as a trivial corollary if needed.

6.6 Dependency Graph Summary

The PR dependency structure is:

PRs 1, 3, and 4 can be submitted independently and in parallel. PR 2 depends on PR 1. PR 5 depends on PRs 1, 2, and 3. Sub-PRs 5a and 5b are fully independent and can be submitted first.