The local ramification index of a completion is the global one

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 nonarchimedean local fields, and the canonical continuous map K_v → L_w makes L_w a valuative extension of K_v in the AdicCompletionExtension scope. This file proves that the ramification index of that extension of local fields is the ramification index of w over R:

IsDedekindDomain.HeightOneSpectrum.ramificationIndex_adicCompletion v w identifies TauCeti.ramificationIndex K_v L_w with w.asIdeal.ramificationIdx R.

So the local invariant, defined through the normalized valuations of K_v and L_w alone, is the global one, defined as a length of a localization of B. In particular, when B is essentially of finite type over R, a place unramified over the base completes to an unramified extension of local fields.

Main results

• IsDedekindDomain.HeightOneSpectrum.ramificationIndex_adicCompletion: the ramification index of L_w / K_v is w.asIdeal.ramificationIdx R.
• IsDedekindDomain.HeightOneSpectrum.isTamelyRamified_adicCompletion_iff and IsDedekindDomain.HeightOneSpectrum.isWildlyRamified_adicCompletion_iff: L_w / K_v is tamely (wildly) ramified exactly when w.asIdeal.ramificationIdx R is nonzero (zero) in R ⧸ v.
• IsDedekindDomain.HeightOneSpectrum.isUnramified_adicCompletion_of_isUnramifiedAt: for B essentially of finite type over R, unramifiedness of w over R gives unramifiedness of L_w / K_v.

References

• [J. Neukirch, Algebraic Number Theory][Neukirch1992], Chapter II, §8.

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.ramificationIndex_adicCompletion {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)] : TauCeti.ramificationIndex (adicCompletion K v) (adicCompletion L w) = w.asIdeal.ramificationIdx R

The local ramification index is the global one. For w a height-one prime of B over the height-one prime v of R, with finite residue fields, the ramification index of the extension of local fields L_w / K_v, for the canonical algebra structure of adicCompletionExtension, is the ramification index of w over R.

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.isTamelyRamified_adicCompletion_iff {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)] : TauCeti.IsTamelyRamified (adicCompletion K v) (adicCompletion L w) ↔ ↑(w.asIdeal.ramificationIdx R) ≠ 0

Tameness of the completed extension. The extension of local fields L_w / K_v is tamely ramified exactly when the ramification index of w over R is nonzero in the residue field R ⧸ v.

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.isWildlyRamified_adicCompletion_iff {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)] : TauCeti.IsWildlyRamified (adicCompletion K v) (adicCompletion L w) ↔ ↑(w.asIdeal.ramificationIdx R) = 0

Wildness of the completed extension. The extension of local fields L_w / K_v is wildly ramified exactly when the ramification index of w over R vanishes in the residue field R ⧸ v.

theorem IsDedekindDomain.HeightOneSpectrum.isUnramified_adicCompletion_of_isUnramifiedAt {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)] [Algebra.EssFiniteType R B] [Algebra.IsUnramifiedAt R w.asIdeal] : TauCeti.IsUnramified (adicCompletion K v) (adicCompletion L w)

An unramified place gives an unramified completed extension. If B is essentially of finite type over R and w is unramified over R, the extension of local fields L_w / K_v is unramified.