Monogenicity criteria for finite extensions of local rings

This file develops the local-ring steps in the monogenicity argument for finite extensions of discrete valuation rings. The Newton step produces an element whose polynomial value generates a principal maximal ideal. A residue-field generator then meets every residue class, and propagation through powers of the maximal ideal lets Nakayama's lemma prove algebra generation. Assembling them proves that a module-finite extension of local rings with principal maximal ideal upstairs and separable residue extension is generated by a single element.

Main results

• TauCeti.IsLocalRing.exists_span_eval_eq_maximalIdeal: the Newton step at a principal maximal ideal.
• TauCeti.IsLocalRing.residue_comp_algebraMap: reduction modulo the maximal ideals commutes with algebraMap.
• TauCeti.IsLocalRing.adjoin_toSubmodule_sup_maximalIdeal_eq_top_of_adjoin_residue_eq_top: a lift of a residue-field generator meets every residue class.
• TauCeti.IsLocalRing.exists_maximalIdeal_pow_le_map: some power of 𝓂(S) lies in 𝓂(R) S.
• TauCeti.IsLocalRing.adjoin_eq_top_of_span_eval_eq_maximalIdeal: the generation criterion.
• TauCeti.IsLocalRing.exists_adjoin_eq_top_of_span_eq_maximalIdeal: existence of a generator.
• TauCeti.IsLocalRing.adjoin_eq_top_of_algebraMap_residueField_surjective_of_span_eq_maximalIdeal: the criterion for a generator of the maximal ideal when the residue extension is trivial.

References

• J.-P. Serre, Corps locaux, Chapter III, §6, Proposition 12.

theorem TauCeti.IsLocalRing.exists_span_eval_eq_maximalIdeal {S : Type u_1} [CommRing S] [IsLocalRing S] {f : Polynomial S} {a π : S} (hπ : Ideal.span {π} = IsLocalRing.maximalIdeal S) (ha : Polynomial.eval a f ∈ IsLocalRing.maximalIdeal S) (ha' : IsUnit (Polynomial.eval a (Polynomial.derivative f))) : ∃ (b : S), b - a ∈ IsLocalRing.maximalIdeal S ∧ Ideal.span {Polynomial.eval b f} = IsLocalRing.maximalIdeal S

Newton step at a principal maximal ideal. If π generates the maximal ideal of a local ring S, and f : S[X] has a simple root at a modulo 𝓂(S), then f takes a value generating 𝓂(S) at some b congruent to a modulo 𝓂(S): either a itself works, or a + π does.

theorem TauCeti.IsLocalRing.residue_comp_algebraMap {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] : (algebraMap (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S)).comp (IsLocalRing.residue R) = (IsLocalRing.residue S).comp (algebraMap R S)

Reduction modulo the maximal ideals commutes with algebraMap, as a square of ring homomorphisms. This is Mathlib's IsLocalRing.ResidueField.algebraMap_residue in the form Polynomial.map_aeval_eq_aeval_map takes.

theorem TauCeti.IsLocalRing.adjoin_toSubmodule_sup_maximalIdeal_eq_top_of_adjoin_residue_eq_top {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] {β : S} (hβ : (IsLocalRing.ResidueField R)[(IsLocalRing.residue S) β] = ⊤) : Subalgebra.toSubmodule R[β] ⊔ Submodule.restrictScalars R (IsLocalRing.maximalIdeal S) = ⊤

If the residue of β generates the residue field extension, then R[β] meets every residue class of S modulo the maximal ideal: R[β] and 𝓂(S) together span S over R. This is the residue-class step of the generation criterion TauCeti.IsLocalRing.adjoin_eq_top_of_span_eval_eq_maximalIdeal. It is the ramified counterpart of the forward half of Mathlib's IsLocalRing.adjoin_residue_eq_top_iff_adjoin_eq_top, which spans modulo 𝓂(R) S instead and so is available only when the two ideals agree.

theorem TauCeti.IsLocalRing.exists_maximalIdeal_pow_le_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] [Algebra R S] [Module.Finite R S] : ∃ (n : ℕ), IsLocalRing.maximalIdeal S ^ n ≤ Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R)

The maximal ideal of S is nilpotent modulo the ideal generated by the maximal ideal of R: some power of 𝓂(S) lies in 𝓂(R) S. For discrete valuation rings the exponent that works is the ramification index.

theorem TauCeti.IsLocalRing.adjoin_eq_top_of_span_eval_eq_maximalIdeal {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] [Module.Finite R S] {β : S} {g : Polynomial R} (hres : (IsLocalRing.ResidueField R)[(IsLocalRing.residue S) β] = ⊤) (hgen : Ideal.span {(Polynomial.aeval β) g} = IsLocalRing.maximalIdeal S) : R[β] = ⊤

The generation criterion. An element β of S generates S as an R-algebra as soon as its residue generates the residue field extension and some polynomial in β with coefficients in R generates the maximal ideal of S.

theorem TauCeti.IsLocalRing.exists_adjoin_eq_top_of_span_eq_maximalIdeal {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] [Module.Finite R S] [Algebra.IsSeparable (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S)] {π : S} (hπ : Ideal.span {π} = IsLocalRing.maximalIdeal S) : ∃ (β : S), R[β] = ⊤

Existence of a generator. If the maximal ideal of S is principal and the residue extension is separable, then S is generated over R by a single element. This is the monogenicity statement that the discrete-valuation-ring results specialize, a discrete valuation ring being a local ring whose maximal ideal is generated by a uniformizer.

theorem TauCeti.IsLocalRing.adjoin_eq_top_of_algebraMap_residueField_surjective_of_span_eq_maximalIdeal {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] [Module.Finite R S] (hsurj : Function.Surjective ⇑(algebraMap (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S))) {π : S} (hπ : Ideal.span {π} = IsLocalRing.maximalIdeal S) : R[π] = ⊤

The totally ramified case. If the residue extension is trivial, every generator of the maximal ideal of S generates S over R. This is the direction of the Eisenstein description of a totally ramified extension that produces an integral power basis.