Ramification theory of completions of number fields

This file studies the ramification of completions of number fields.

Main definitions

• NumberField.InfinitePlace.inertiaDeg : the inertia degree of a place w of L over a place v of K, defined as the local degree of the extension of completions at w and v if w lies over v and zero otherwise. The v.Completion-algebra structure on w.Completion used here is AbsoluteValue.Completion.algebraOfLiesOver, which is the unique one compatible with K → L and having continuous scalar action, see AbsoluteValue.Completion.algebra_eq_of_liesOver.

Main results

• NumberField.InfinitePlace.sum_inertiaDeg_eq_finrank : the degree of L over K is equal to the sum of the inertia degrees of the places of L over v.

Tags

number field, infinite places, ramification

theorem NumberField.InfinitePlace.IsRamified.finrank_eq_two {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) {w : InfinitePlace L} [Algebra v.Completion w.Completion] [IsScalarTower K v.Completion w.Completion] [ContinuousSMul v.Completion w.Completion] [w.LiesOver v] (h : IsRamified K w) : Module.finrank v.Completion w.Completion = 2

If w is a ramified place over v then w.Completion has v.Completion dimension two.

theorem NumberField.InfinitePlace.IsUnramified.finrank_eq_one {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) {w : InfinitePlace L} [Algebra v.Completion w.Completion] [IsScalarTower K v.Completion w.Completion] [ContinuousSMul v.Completion w.Completion] [w.LiesOver v] (h : IsUnramified K w) : Module.finrank v.Completion w.Completion = 1

If w is an unramified place over v then w.Completion has v.Completion dimension one.

@[deprecated NumberField.InfinitePlace.IsRamified.finrank_eq_two (since := "2026-07-10")]

theorem NumberField.InfinitePlace.Completion.finrank_eq_two_of_isRamified {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) {w : InfinitePlace L} [Algebra v.Completion w.Completion] [IsScalarTower K v.Completion w.Completion] [ContinuousSMul v.Completion w.Completion] [w.LiesOver v] (h : IsRamified K w) : Module.finrank v.Completion w.Completion = 2

Alias of NumberField.InfinitePlace.IsRamified.finrank_eq_two.

---

If w is a ramified place over v then w.Completion has v.Completion dimension two.

@[deprecated NumberField.InfinitePlace.IsUnramified.finrank_eq_one (since := "2026-07-10")]

theorem NumberField.InfinitePlace.Completion.finrank_eq_one_of_isUnramified {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) {w : InfinitePlace L} [Algebra v.Completion w.Completion] [IsScalarTower K v.Completion w.Completion] [ContinuousSMul v.Completion w.Completion] [w.LiesOver v] (h : IsUnramified K w) : Module.finrank v.Completion w.Completion = 1

Alias of NumberField.InfinitePlace.IsUnramified.finrank_eq_one.

---

If w is an unramified place over v then w.Completion has v.Completion dimension one.

theorem NumberField.InfinitePlace.mult_mul_finrank {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) (w : InfinitePlace L) [Algebra v.Completion w.Completion] [IsScalarTower K v.Completion w.Completion] [ContinuousSMul v.Completion w.Completion] [w.LiesOver v] : v.mult * Module.finrank v.Completion w.Completion = w.mult

noncomputable def NumberField.InfinitePlace.inertiaDeg {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) (w : InfinitePlace L) : ℕ

The inertia degree of w over v.

Equations

• v.inertiaDeg w = if x : w.LiesOver v then ⊥.inertiaDeg v.Completion else 0

theorem NumberField.InfinitePlace.inertiaDeg_of_liesOver {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) (w : InfinitePlace L) [Algebra v.Completion w.Completion] [IsScalarTower K v.Completion w.Completion] [ContinuousSMul v.Completion w.Completion] [w.LiesOver v] : v.inertiaDeg w = ⊥.inertiaDeg v.Completion

theorem NumberField.InfinitePlace.inertiaDeg_eq_finrank {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) (w : InfinitePlace L) [Algebra v.Completion w.Completion] [IsScalarTower K v.Completion w.Completion] [ContinuousSMul v.Completion w.Completion] [w.LiesOver v] : v.inertiaDeg w = Module.finrank v.Completion w.Completion

theorem NumberField.InfinitePlace.inertiaDeg_eq_one {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {v : InfinitePlace K} {w : InfinitePlace L} (hw : w ∈ unramifiedPlacesOver L v) : v.inertiaDeg w = 1

theorem NumberField.InfinitePlace.inertiaDeg_eq_two {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {v : InfinitePlace K} {w : InfinitePlace L} (hw : w ∈ ramifiedPlacesOver L v) : v.inertiaDeg w = 2

theorem NumberField.InfinitePlace.sum_inertiaDeg_eq_finrank (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] (v : InfinitePlace K) [NumberField K] [NumberField L] : ∑ w ∈ (placesOver L v).toFinset, v.inertiaDeg w = Module.finrank K L

The degree of L over K is equal to the sum of the inertia degrees of the places over v.