The local degree of a completion is e · f

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, with w of finite residue field. The completions K_v and L_w are then nonarchimedean local fields for the canonical algebra structure of the AdicCompletionExtension scope, and the degree of the second over the first is

[L_w : K_v] = e(w ∣ v) · f(w ∣ v),

the product of the ramification index and the inertia degree of w over R. Both factors on the right are global invariants of the extension R ⊆ B, so this formula turns a sum of local degrees over the primes w above v into ∑_{w ∣ v} e(w ∣ v) · f(w ∣ v), which the fundamental identity of Dedekind domains evaluates as the global degree [L : K].

Main results

• IsDedekindDomain.HeightOneSpectrum.finrank_adicCompletion: the degree of L_w over K_v is w.asIdeal.ramificationIdx R * w.asIdeal.inertiaDeg R.

References

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

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.finrank_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 (B ⧸ w.asIdeal)] : Module.finrank (adicCompletion K v) (adicCompletion L w) = w.asIdeal.ramificationIdx R * w.asIdeal.inertiaDeg R

The local degree of a completion. For w a height-one prime of B over the height-one prime v of R, with finite residue field, the degree of L_w over K_v for the canonical algebra structure of adicCompletionExtension is the product of the ramification index and the inertia degree of w over R.