Global and local ramification groups

Let L/K be an extension of number fields, v a finite place of K, and w a finite place of L above v. The decomposition group of w, the stabilizer of w in Aut(L/K), acts on the completion L_w through decompositionHom v w. This file proves that this action matches the two ramification filtrations: the global ramification groups G_i of the prime w of 𝓞 L, cut out by congruences modulo w ^ (i + 1), and the lower-numbering ramification groups of the local extension L_w/K_v, cut out by congruences modulo the powers of the maximal ideal of the ring of integers 𝒪[L_w].

The comparison is an equality of subgroups along the named map decompositionHom v w, not an abstract isomorphism, so that elements can be moved across it. It rests on two facts. An element of 𝓞 L lies in w ^ n exactly when its image in L_w has valuation at most exp (-n), so the global congruences are the local ones restricted to 𝓞 L. Conversely 𝓞 L is dense in 𝒪[L_w] modulo every power of the maximal ideal, and the action of the decomposition group preserves the valuation, so a congruence that holds on 𝓞 L holds on all of 𝒪[L_w].

For L/K Galois, decompositionHom v w is an isomorphism onto Aut(L_w/K_v), and the global and local ramification groups have the same orders. In particular the global wild inertia group G_1 of w is trivial exactly when L_w/K_v is tamely ramified, that is, when the residue characteristic does not divide e(w/v). The reading on the different exponent is in TauCeti.NumberTheory.NumberField.LocalGlobal.Different.Tame.

Main results

• IsDedekindDomain.HeightOneSpectrum.mem_ramificationGroup_iff_decompositionHom_mem: an element of the decomposition group of w lies in the i-th global ramification group of w exactly when its action on L_w lies in the i-th local ramification group.
• IsDedekindDomain.HeightOneSpectrum.ramificationGroup_stabilizer_eq_comap_decompositionHom: the same statement as an equality of subgroups of the decomposition group.
• IsDedekindDomain.HeightOneSpectrum.map_ramificationGroup_decompositionHom: for L/K Galois, decompositionHom v w carries the global ramification groups onto the local ones.
• IsDedekindDomain.HeightOneSpectrum.card_ramificationGroup_eq_card_lowerRamificationGroup: for L/K Galois, the global and local ramification groups have the same orders.
• IsDedekindDomain.HeightOneSpectrum.ramificationGroup_one_eq_bot_iff_isTamelyRamified and ramificationGroup_one_eq_bot_iff_natCast_ramificationIdx_ne_zero: for L/K Galois, G_1 is trivial exactly when w is tamely ramified, read on the completion and on the ramification index in the residue field of v.

References

• J.-P. Serre, Corps Locaux, Chapter IV, §1.
• [J. Neukirch, Algebraic Number Theory][Neukirch1992], Chapter II, §9.

theorem IsDedekindDomain.HeightOneSpectrum.mem_ramificationGroup_iff_decompositionHom_mem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) {w : HeightOneSpectrum (NumberField.RingOfIntegers L)} [w.asIdeal.LiesOver v.asIdeal] (i : ℕ) (σ : ↥(MulAction.stabilizer Gal(L/K) w.asIdeal)) : ↑σ ∈ Ideal.ramificationGroup Gal(L/K) w.asIdeal i ↔ (v.decompositionHom w) σ ∈ TauCeti.LocalFieldsRamification.lowerRamificationGroup (adicCompletion K v) (adicCompletion L w) ↑i

The global and local ramification groups agree. An element σ of the decomposition group of w lies in the i-th ramification group of the prime w of 𝓞 L exactly when its continuous extension to L_w lies in the i-th lower-numbering ramification group of L_w/K_v.

theorem IsDedekindDomain.HeightOneSpectrum.ramificationGroup_stabilizer_eq_comap_decompositionHom {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) {w : HeightOneSpectrum (NumberField.RingOfIntegers L)} [w.asIdeal.LiesOver v.asIdeal] (i : ℕ) : Ideal.ramificationGroup (↥(MulAction.stabilizer Gal(L/K) w.asIdeal)) w.asIdeal i = Subgroup.comap (v.decompositionHom w) (TauCeti.LocalFieldsRamification.lowerRamificationGroup (adicCompletion K v) (adicCompletion L w) ↑i)

The global ramification groups are the local ones, pulled back along decompositionHom. Inside the decomposition group of w, the i-th ramification group of w is the preimage of the i-th lower-numbering ramification group of L_w/K_v.

theorem IsDedekindDomain.HeightOneSpectrum.map_ramificationGroup_decompositionHom {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] [IsGalois K L] (i : ℕ) : Subgroup.map (v.decompositionHom w) (Ideal.ramificationGroup (↥(MulAction.stabilizer Gal(L/K) w.asIdeal)) w.asIdeal i) = TauCeti.LocalFieldsRamification.lowerRamificationGroup (adicCompletion K v) (adicCompletion L w) ↑i

The decomposition group carries the global ramification groups onto the local ones. For L/K Galois, the image of the i-th ramification group of w in Aut(L_w/K_v) is the i-th lower-numbering ramification group of L_w/K_v.

theorem IsDedekindDomain.HeightOneSpectrum.card_ramificationGroup_eq_card_lowerRamificationGroup {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] [IsGalois K L] (i : ℕ) : Nat.card ↥(Ideal.ramificationGroup Gal(L/K) w.asIdeal i) = Nat.card ↥(TauCeti.LocalFieldsRamification.lowerRamificationGroup (adicCompletion K v) (adicCompletion L w) ↑i)

The global and local ramification groups have the same order. For L/K Galois, the i-th ramification group of w has as many elements as the i-th lower-numbering ramification group of L_w/K_v.

theorem IsDedekindDomain.HeightOneSpectrum.ramificationGroup_one_eq_bot_iff_isTamelyRamified {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] [IsGalois K L] : Ideal.ramificationGroup Gal(L/K) w.asIdeal 1 = ⊥ ↔ TauCeti.IsTamelyRamified (adicCompletion K v) (adicCompletion L w)

Wild inertia is trivial exactly at tame primes. For L/K Galois, the first ramification group G_1 of w is trivial if and only if the completed extension L_w/K_v is tamely ramified.

theorem IsDedekindDomain.HeightOneSpectrum.ramificationGroup_one_eq_bot_iff_natCast_ramificationIdx_ne_zero {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] [IsGalois K L] : Ideal.ramificationGroup Gal(L/K) w.asIdeal 1 = ⊥ ↔ ↑(w.asIdeal.ramificationIdx (NumberField.RingOfIntegers K)) ≠ 0

For L/K Galois, the first ramification group G_1 of w is trivial if and only if the ramification index e(w/v) is nonzero in the residue field of v, that is, not divisible by the residue characteristic.