The completed integer rings are an integral closure

Let R ⊆ B be Dedekind domains with fraction fields K ⊆ L, and let w be a height-one prime of B lying over the height-one prime v of R, both with finite residue fields. The completions K_v and L_w are then nonarchimedean local fields and the canonical map K_v → L_w makes L_w a valuative extension of K_v, inside which the completed integer rings sit as 𝒪_v ⊆ 𝒪_w.

This file proves that L_w is a finite extension of K_v, that 𝒪_w is the integral closure of 𝒪_v in L_w, and that 𝒪_w is a finite 𝒪_v-module of rank [L_w : K_v]. Together with the algebra structure, the scalar towers and the torsion-freeness of 𝒪_w over 𝒪_v, and with the IsFractionRing, IsIntegrallyClosed and IsDedekindDomain instances that the valuation subring of a complete discretely valued field already carries, these are the hypotheses that the different ideal and the conductor of the local extension 𝒪_w / 𝒪_v take, so that those objects can be formed at all.

The integrality criterion is that of a complete discretely valued field: the valuation of L_w is the unique extension of the valuation of K_v, so an element of L_w is integral over 𝒪_v exactly when its valuation is at most 1. The finiteness of 𝒪_w over 𝒪_v is transported from TauCeti.integerRingModuleFinite, which is proved for the ring of integers of a valuative relation, rather than deduced from the integral closure by IsIntegralClosure.finite: the latter assumes separability of L_w / K_v, which holds for a number field but not for a local field of equal characteristic, whereas the transport is unconditional.

Main results

• IsDedekindDomain.HeightOneSpectrum.adicCompletion_moduleFinite: L_w is a finite K_v-module for the canonical algebra structure.
• IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers_isIntegralClosure: 𝒪_w is the integral closure of 𝒪_v in L_w.
• IsDedekindDomain.HeightOneSpectrum.norm_mem_adicCompletionIntegers: the norm of L_w over K_v carries 𝒪_w into 𝒪_v.
• IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers_moduleFinite and IsDedekindDomain.HeightOneSpectrum.finrank_adicCompletionIntegers: 𝒪_w is a finite 𝒪_v-module, of rank [L_w : K_v].
• IsDedekindDomain.HeightOneSpectrum.integerEquivAdicCompletionIntegers_algebraMap: the identifications 𝒪[K_v] = 𝒪_v and 𝒪[L_w] = 𝒪_w commute with the two maps between the integer rings.

References

• [J. Neukirch, Algebraic Number Theory][Neukirch1992], Chapter II, §4 and §6.
• J.-P. Serre, Corps Locaux, Chapter II, §2.

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletion_moduleFinite {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)] : Module.Finite (adicCompletion K v) (adicCompletion L w)

A completion of an extension is a finite extension of completions. For the canonical algebra structure of adicCompletionExtension, L_w is a finite K_v-module. Mathlib's instance for an adic completion assumes that K and L are number fields and holds for an arbitrary compatible algebra structure; this one is about the canonical structure over an arbitrary Dedekind base.

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers_isIntegralClosure {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)] : IsIntegralClosure (↥(adicCompletionIntegers L w)) (↥(adicCompletionIntegers K v)) (adicCompletion L w)

𝒪_w is the integral closure of 𝒪_v in L_w. An element of L_w is integral over 𝒪_v exactly when its valuation is at most 1, because the valuation of L_w is the unique extension of the valuation of K_v.

theorem IsDedekindDomain.HeightOneSpectrum.norm_mem_adicCompletionIntegers {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 : adicCompletion L w} (hx : x ∈ adicCompletionIntegers L w) : (Algebra.norm (adicCompletion K v)) x ∈ adicCompletionIntegers K v

The local norm preserves integrality. The norm of L_w over K_v carries the completed integer ring 𝒪_w into 𝒪_v: an element of 𝒪_w is integral over 𝒪_v, hence so is its norm, and the integral elements of K_v are those of valuation at most 1.

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.integerEquivAdicCompletionIntegers_algebraMap {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] (x : ↥(ValuativeRel.valuation (adicCompletion K v)).integer) : w.integerEquivAdicCompletionIntegers ((algebraMap ↥(ValuativeRel.valuation (adicCompletion K v)).integer ↥(ValuativeRel.valuation (adicCompletion L w)).integer) x) = (algebraMap ↥(adicCompletionIntegers K v) ↥(adicCompletionIntegers L w)) (v.integerEquivAdicCompletionIntegers x)

The identifications of the integer rings are natural. The identifications 𝒪[K_v] = 𝒪_v and 𝒪[L_w] = 𝒪_w commute with the map 𝒪[K_v] → 𝒪[L_w] of the valuative extension and the map 𝒪_v → 𝒪_w of adicCompletionIntegersExtension, both of which are restrictions of the canonical map K_v → L_w.

theorem IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers_moduleFinite {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)] : Module.Finite ↥(adicCompletionIntegers K v) ↥(adicCompletionIntegers L w)

𝒪_w is a finite 𝒪_v-module. The identifications 𝒪[K_v] = 𝒪_v and 𝒪[L_w] = 𝒪_w carry TauCeti.integerRingModuleFinite over to the completed integer rings.

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.finrank_adicCompletionIntegers {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)] : Module.finrank ↥(adicCompletionIntegers K v) ↥(adicCompletionIntegers L w) = Module.finrank (adicCompletion K v) (adicCompletion L w)

𝒪_w is a lattice of full rank in L_w. Its rank as an 𝒪_v-module is the degree [L_w : K_v] of the local extension.