The p-primary part of upper ramification

Let L/K be a finite Galois extension of nonarchimedean local fields, and let p be the residue characteristic. Every positive upper ramification group is contained in the first lower ramification group G₁, hence is a p-group. This isolates the wild part of a positive upper break.

For a cyclic extension, quotient the Galois group by the subgroup generated by the prime-to-p part of a generator. That subgroup has order prime to p, so it is disjoint from every positive upper ramification group. The upper-numbering quotient theorem then shows that a positive upper break remains a break in the resulting cyclic p-extension. This is the cyclic-to-p-primary reduction in the Hasse--Arf theorem.

At the other end of the filtration, an upper break at a nonpositive index is necessarily -1 or 0. Together, these results separate the elementary integral breaks from the positive wild breaks that require the norm-conductor argument.

Main results

• TauCeti.LocalFieldsRamification.isPGroup_upperRamificationGroup_of_pos: a positive upper ramification group is a p-group.
• TauCeti.LocalFieldsRamification.UpperJump.eq_neg_one_or_eq_zero_of_nonpos: the only nonpositive upper breaks are -1 and 0.
• TauCeti.LocalFieldsRamification.UpperJump.fixedField_of_disjoint: quotienting by a subgroup disjoint from the upper group at a break preserves that break in the fixed field.
• TauCeti.LocalFieldsRamification.UpperJump.exists_isPGroup_intermediateField_of_isCyclic_of_pos: a positive upper break of a cyclic extension is detected in a cyclic p-subextension.

References

• J.-P. Serre, Corps Locaux, Chapter IV, §§2--3, and Chapter V, §7.

theorem TauCeti.LocalFieldsRamification.upperRamificationGroup_le_lowerRamificationGroup_one (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] [IsGalois K L] {u : ↑RamificationIndexDomain} (hu : 0 < ↑u) : upperRamificationGroup K L u ≤ lowerRamificationGroup K L 1

A positive upper ramification group is contained in the first lower ramification group. Indeed, the inverse Herbrand value of a positive index is positive, so its ceiling is at least one.

theorem TauCeti.LocalFieldsRamification.isPGroup_upperRamificationGroup_of_pos (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] [IsGalois K L] {u : ↑RamificationIndexDomain} (p : ℕ) [CharP (IsLocalRing.ResidueField ↥(ValuativeRel.valuation L).integer) p] (hu : 0 < ↑u) : IsPGroup p ↥(upperRamificationGroup K L u)

Every positive upper ramification group is a p-group for the residue characteristic p. This is the upper-numbering form of the fact that G₁ is wild inertia.

theorem TauCeti.LocalFieldsRamification.UpperJump.eq_neg_one_or_eq_zero_of_nonpos {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] [IsGalois K L] {u : ↑RamificationIndexDomain} (hu : UpperJump K L u) (hu0 : ↑u ≤ 0) : ↑u = -1 ∨ ↑u = 0

The only nonpositive upper ramification breaks are -1 and 0. Between these two indices the upper filtration equals the constant lower filtration G₀.

theorem TauCeti.LocalFieldsRamification.UpperJump.fixedField_of_disjoint {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] [IsGalois K L] (H : Subgroup Gal(L/K)) [H.Normal] [ValuativeRel ↥(IntermediateField.fixedField H)] [TopologicalSpace ↥(IntermediateField.fixedField H)] [IsNonarchimedeanLocalField ↥(IntermediateField.fixedField H)] [ValuativeExtension K ↥(IntermediateField.fixedField H)] {u : ↑RamificationIndexDomain} (hu : UpperJump K L u) (hdisjoint : Disjoint H (upperRamificationGroup K L u)) : UpperJump K (↥(IntermediateField.fixedField H)) u

An upper break survives in the fixed field of a normal subgroup that is disjoint from the upper ramification group at that break. The quotient map is injective on that upper group, so it preserves every strict drop after the break.

theorem TauCeti.LocalFieldsRamification.UpperJump.exists_isPGroup_intermediateField_of_isCyclic_of_pos {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] [IsGalois K L] [IsCyclic Gal(L/K)] (p : ℕ) [CharP (IsLocalRing.ResidueField ↥(ValuativeRel.valuation L).integer) p] {u : ↑RamificationIndexDomain} (hu : UpperJump K L u) (hupos : 0 < ↑u) : ∃ (F : IntermediateField K L) (hF : IsGalois K ↥F), IsCyclic Gal(↥F/K) ∧ IsPGroup p Gal(↥F/K) ∧ UpperJump K (↥F) u

A positive upper break of a cyclic extension is detected in a cyclic p-subextension, for the residue characteristic p. The subextension is the fixed field of the prime-to-p part of the original cyclic Galois group. Its local-field structures are the canonical ones induced from K.