Monogenicity from étale height-one quotients

If R and S are local integral domains with S a finite extension of R, R integrally closed, S a UFD, and there exists a height-one prime q ⊆ S such that R/(q ∩ R) → S/q is étale, then S ≅ R[X]/(f) for some monic f. This formalizes Lemma 3.1 of arXiv:2503.07846.

Main results

• Monogenic.exists_isAdjoinRootMonic_of_quotientMap_etale: the main theorem (Lemma 3.1).

Auxiliary lemmas

• Ideal.exists_span_singleton_eq_of_prime_of_height_one: in a UFD, a height-one prime ideal is principal.
• Monogenic.exists_aeval_add_eq: Taylor expansion f(x + h) = f(x) + f'(x)·h + h²·c.
• Monogenic.maximalIdeal_eq_sup_of_etale_quotient: when R/p → S/q is étale, m_S = q + m_R·S.
• Monogenic.exists_isAdjoinRootMonic_of_principal_adjust: adjusting a generator by adding a generator of q via Taylor expansion when f₁(B) = q₀ · a with a ∈ m_S.

References

• Balçik et al., Monogenic generators for étale extensions of local rings

Tags

étale, monogenic, local ring, height one, UFD

theorem Monogenic.Ideal.exists_span_singleton_eq_of_prime_of_height_one {S : Type u_3} [CommRing S] [IsDomain S] [UniqueFactorizationMonoid S] (q : Ideal S) [hq_prime : q.IsPrime] (hq_height : q.height = 1) : ∃ (q₀ : S), q = Ideal.span {q₀}

In a UFD, a height one prime ideal is principal.

theorem Monogenic.exists_aeval_add_eq {R : Type u_3} {S : Type u_4} [CommRing R] [CommRing S] [Algebra R S] (f : Polynomial R) (x h : S) : ∃ (c : S), (Polynomial.aeval (x + h)) f = (Polynomial.aeval x) f + (Polynomial.aeval x) (Polynomial.derivative f) * h + h ^ 2 * c

Taylor expansion: for any polynomial f and elements x, h, there exists c such that f(x + h) = f(x) + f'(x) · h + h² · c. Proved by lifting Polynomial.aeval_add_of_sq_eq_zero from S ⧸ ⟨h²⟩.

theorem Monogenic.maximalIdeal_eq_sup_of_etale_quotient {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] [Algebra R S] [Module.Finite R S] (q : Ideal S) [hq_prime : q.IsPrime] (hétale : (Ideal.quotientMap q (algebraMap R S) ⋯).Etale) : IsLocalRing.maximalIdeal S = q ⊔ Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R)

When the quotient map R/p → S/q is étale and both rings are local, the maximal ideal of S decomposes as m_S = q + m_R·S.

theorem Monogenic.cofactor_mem_maximalIdeal_of_not_generator {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] [Algebra R S] (f₁_B : S) (q : Ideal S) [hq_prime : q.IsPrime] (h_f₁B_in_q : f₁_B ∈ q) (h_gen : ¬(f₁_B ∈ IsLocalRing.maximalIdeal S ∧ Ideal.span {f₁_B} ⊔ Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R) • ⊤ = IsLocalRing.maximalIdeal S)) (q₀ : S) (hq₀ : q = Ideal.span {q₀}) (a : S) (ha : f₁_B = q₀ * a) (h_ms_eq : IsLocalRing.maximalIdeal S = q ⊔ Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R)) : a ∈ IsLocalRing.maximalIdeal S

theorem Monogenic.Ideal.quotient_adjust {S : Type u_2} [CommRing S] (q : Ideal S) (q₀ : S) (hq₀ : q = Ideal.span {q₀}) (B : S) : (Ideal.Quotient.mk q) (B + q₀) = (Ideal.Quotient.mk q) B

theorem Monogenic.Ideal.quotient_comp_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (q : Ideal S) : (Ideal.Quotient.mk q).comp (algebraMap R S) = (Ideal.quotientMap q (algebraMap R S) ⋯).comp (Ideal.Quotient.mk (Ideal.comap (algebraMap R S) q))

theorem Monogenic.exists_isAdjoinRootMonic_of_principal_adjust {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] [IsDomain R] [IsDomain S] [IsIntegrallyClosed R] [Algebra R S] [FaithfulSMul R S] [Module.Finite R S] (q : Ideal S) [hq_prime : q.IsPrime] (q₀ : S) (hq₀ : q = Ideal.span {q₀}) (B : S) (f₁ : Polynomial R) (a : S) (ha : (Polynomial.aeval B) f₁ = q₀ * a) (ha_mem : a ∈ IsLocalRing.maximalIdeal S) (h_deriv_not_in_ms : (Polynomial.aeval B) (Polynomial.derivative f₁) ∉ IsLocalRing.maximalIdeal S) (h_ms_eq : IsLocalRing.maximalIdeal S = q ⊔ Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R)) (h_adj : Algebra.adjoin (R ⧸ Ideal.comap (algebraMap R S) q) {(Ideal.Quotient.mk q) B} = ⊤) : ∃ (f : Polynomial R), Nonempty (IsAdjoinRootMonic S f)

When q is principal, f₁(B) = q₀ · a with a ∈ m_S, and f₁'(B) ∉ m_S, adjusting B to B + q₀ yields a monogenic extension via Taylor expansion.

theorem Monogenic.exists_isAdjoinRootMonic_of_quotientMap_etale {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] [IsDomain R] [IsDomain S] [IsIntegrallyClosed R] [UniqueFactorizationMonoid S] [Algebra R S] [FaithfulSMul R S] [Module.Finite R S] (q : Ideal S) [hq_prime : q.IsPrime] (hq_height : q.height = 1) (hétale : (Ideal.quotientMap q (algebraMap R S) ⋯).Etale) : ∃ (f : Polynomial R), Nonempty (IsAdjoinRootMonic S f)

Lemma 3.1 of arXiv:2503.07846. If R and S are local integral domains with R integrally closed, S a UFD, and R → S finite and injective, and there exists a height-one prime q ⊆ S such that R/(q ∩ R) → S/q is étale, then there exists a monic f with S ≅ R[X]/(f).