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.

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.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} [(↑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.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} [(↑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.

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 ⊥ 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) [(↑w).LiesOver ↑v] : v.inertiaDeg w = ⊥.inertiaDeg ⊥

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) [(↑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.