Monogenicity of completed integer rings

Let L/K be an extension of fraction fields of Dedekind domains, and let w be a height-one prime of the top ring above a height-one prime v of the base. When the residue fields are finite, the ring of integers 𝒪_w is generated by one element over 𝒪_v.

The generator can simultaneously be viewed as an integral element which generates the local field extension. This is the form needed to apply formulas for the different which use a generator of both the integer ring and its fraction field.

Main results

• The theorem adjoin_adicCompletion_eq_top_of_adjoin_adicCompletionIntegers_eq_top promotes any generator of the completed integer extension to a generator of the completed field extension.
• The theorem exists_adjoin_adicCompletionIntegers_eq_top_and_isIntegral_and_adjoin_adicCompletion_eq_top gives one element which generates the completed integer ring and the completed field extension, and is integral over the base completed integer ring.

References

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

theorem IsDedekindDomain.HeightOneSpectrum.adjoin_adicCompletion_eq_top_of_adjoin_adicCompletionIntegers_eq_top {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {B : Type u_3} [CommRing B] [IsDedekindDomain B] [Algebra R B] {L : Type u_4} [Field L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [Algebra B L] [IsFractionRing B L] [IsScalarTower R B L] (v : HeightOneSpectrum R) (w : HeightOneSpectrum B) [w.asIdeal.LiesOver v.asIdeal] [Finite (R ⧸ v.asIdeal)] [Finite (B ⧸ w.asIdeal)] (x : ↥(adicCompletionIntegers L w)) (hx : (↥(adicCompletionIntegers K v))[x] = ⊤) : (adicCompletion K v)[↑x] = ⊤

A generator of the completed integer extension also generates the completed field extension.

theorem IsDedekindDomain.HeightOneSpectrum.exists_adjoin_adicCompletionIntegers_eq_top_and_isIntegral_and_adjoin_adicCompletion_eq_top {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {B : Type u_3} [CommRing B] [IsDedekindDomain B] [Algebra R B] {L : Type u_4} [Field L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [Algebra B L] [IsFractionRing B L] [IsScalarTower R B L] (v : HeightOneSpectrum R) (w : HeightOneSpectrum B) [w.asIdeal.LiesOver v.asIdeal] [Finite (R ⧸ v.asIdeal)] [Finite (B ⧸ w.asIdeal)] : ∃ (x : ↥(adicCompletionIntegers L w)), (↥(adicCompletionIntegers K v))[x] = ⊤ ∧ IsIntegral (↥(adicCompletionIntegers K v)) x ∧ (adicCompletion K v)[↑x] = ⊤

When both residue fields are finite, the completed integer ring 𝒪_w is generated over 𝒪_v by an element which is also an integral generator of the field extension.