The upper numbering in a Galois tower

Let M/K be a finite Galois extension of nonarchimedean local fields with group G, and let H ≤ G be a normal subgroup, with fixed field L = M^H, so that restriction identifies G / H with Gal(L/K). The lower numbering is not compatible with this quotient, but the upper numbering is:

(G/H)^v = G^v H / H for every v ≥ -1.

This is Herbrand's theorem (G/H)_{φ_{M/L}(u)} = G_u H / H read through the transitivity ψ_{M/K} = ψ_{M/L} ∘ ψ_{L/K} of the inverse Herbrand functions: both give φ_{M/L}(ψ_{M/K}(v)) = ψ_{L/K}(v). It is the reason upper numbering is the one that is functorial in quotients, and hence the one that defines a filtration of an infinite Galois group; and it transports the upper breaks along the prime-order quotient series in the proof of the Hasse–Arf theorem.

The statement is given in three forms.

• For a tower M/L/K with L/K Galois, the image of G^v under restriction to L is the upper ramification group of L/K at v.
• For a normal subgroup H, define the quotient filtration upperRamificationGroupQuotient H of G ⧸ H as the image of G^v and express it as G^v H / H.
• For every compatible local-field structure on M^H, the restriction equivalence IsGalois.normalAutEquivQuotient carries this quotient filtration to the upper filtration of M^H/K.

As a consequence, every upper break of L/K is an upper break of M/K.

On the subgroup side, the upper filtration of H = Gal(M/L) is the trace of that of G, after reindexing by ψ_{L/K}: H ∩ G^v = H^{ψ_{L/K}(v)}. The two compatibilities together describe the upper breaks of M/K completely: they are the upper breaks of L/K together with the images under φ_{L/K} of the upper breaks of M/L. Along a prime-degree tower of an abelian extension, this reduces the integrality of the upper breaks to the integrality of φ_{L/K} at the single break of each prime-degree step.

Main definitions

• Subgroup.upperRamificationGroupQuotient: the upper ramification filtration of G ⧸ H.

Main results

• TauCeti.LocalFieldsRamification.map_restrictNormalHom_upperRamificationGroup: G^v restricts onto Gal(L/K)^v.
• TauCeti.LocalFieldsRamification.UpperJump.of_tower: an upper break of L/K is an upper break of M/K.
• TauCeti.LocalFieldsRamification.comap_restrictScalarsHom_upperRamificationGroup: H ∩ G^v = H^{ψ_{L/K}(v)}.
• TauCeti.LocalFieldsRamification.upperJump_iff_upperJump_or_upperJump_inverseHerbrand: v is an upper break of M/K exactly when it is one of L/K or ψ_{L/K}(v) is one of M/L.
• Subgroup.upperRamificationGroup_fixedField: the quotient filtration maps to Gal(M^H/K)^v under G ⧸ H ≃* Gal(M^H/K).
• Subgroup.upperRamificationGroup_quotient: the defined quotient filtration equals G^v H / H.
• Subgroup.upperRamificationGroupQuotient_antitone: the quotient filtration is decreasing.

The quotient API takes the normal subgroup H as its first explicit argument, so it lives in Mathlib's Subgroup namespace and is available as H.upperRamificationGroupQuotient v.

References

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

@[simp]

theorem TauCeti.LocalFieldsRamification.map_restrictNormalHom_upperRamificationGroup (K : Type u_1) (L : Type u_2) (M : Type u_3) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Field M] [ValuativeRel M] [TopologicalSpace M] [IsNonarchimedeanLocalField M] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] [Algebra L M] [ValuativeExtension L M] [Module.Finite L M] [Algebra K M] [ValuativeExtension K M] [IsScalarTower K L M] [IsGalois K L] [IsGalois K M] (v : ↑RamificationIndexDomain) : Subgroup.map (AlgEquiv.restrictNormalHom L) (upperRamificationGroup K M v) = upperRamificationGroup K L v

Herbrand's theorem in the upper numbering. For a tower M/L/K of Galois extensions, the image of the upper ramification group G^v of M/K under restriction to L is the upper ramification group of L/K at the same index: (G/H)^v = G^v H / H for H = Gal(M/L).

theorem TauCeti.LocalFieldsRamification.UpperJump.of_tower {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Field M] [ValuativeRel M] [TopologicalSpace M] [IsNonarchimedeanLocalField M] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] [Algebra L M] [ValuativeExtension L M] [Module.Finite L M] [Algebra K M] [ValuativeExtension K M] [IsScalarTower K L M] [IsGalois K L] [IsGalois K M] {v : ↑RamificationIndexDomain} (h : UpperJump K L v) : UpperJump K M v

In a tower M/L/K of Galois extensions, every upper break of L/K is an upper break of M/K.

@[simp]

theorem TauCeti.LocalFieldsRamification.comap_restrictScalarsHom_upperRamificationGroup (K : Type u_1) (L : Type u_2) (M : Type u_3) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Field M] [ValuativeRel M] [TopologicalSpace M] [IsNonarchimedeanLocalField M] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] [Algebra L M] [ValuativeExtension L M] [Module.Finite L M] [Algebra K M] [ValuativeExtension K M] [IsScalarTower K L M] [IsGalois K L] [IsGalois K M] (v : ↑RamificationIndexDomain) : Subgroup.comap (AlgEquiv.restrictScalarsHom K) (upperRamificationGroup K M v) = upperRamificationGroup L M (inverseHerbrand K L v)

The upper numbering of a normal subgroup. For a tower M/L/K of Galois extensions, the upper filtration of H = Gal(M/L) is the trace of that of G = Gal(M/K), reindexed by the inverse Herbrand function of L/K: H ∩ G^v = H^{ψ_{L/K}(v)}.

theorem TauCeti.LocalFieldsRamification.map_restrictScalarsHom_upperRamificationGroup (K : Type u_1) (L : Type u_2) (M : Type u_3) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Field M] [ValuativeRel M] [TopologicalSpace M] [IsNonarchimedeanLocalField M] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] [Algebra L M] [ValuativeExtension L M] [Module.Finite L M] [Algebra K M] [ValuativeExtension K M] [IsScalarTower K L M] [IsGalois K L] [IsGalois K M] (v : ↑RamificationIndexDomain) : Subgroup.map (AlgEquiv.restrictScalarsHom K) (upperRamificationGroup L M (inverseHerbrand K L v)) = (AlgEquiv.restrictScalarsHom K).range ⊓ upperRamificationGroup K M v

The image of Gal(M/L)^{ψ_{L/K}(v)} in Gal(M/K) is the trace H ∩ G^v of the upper filtration of M/K on the image H of Gal(M/L).

theorem TauCeti.LocalFieldsRamification.upperJump_iff_upperJump_or_upperJump_inverseHerbrand (K : Type u_1) (L : Type u_2) (M : Type u_3) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Field M] [ValuativeRel M] [TopologicalSpace M] [IsNonarchimedeanLocalField M] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] [Algebra L M] [ValuativeExtension L M] [Module.Finite L M] [Algebra K M] [ValuativeExtension K M] [IsScalarTower K L M] [IsGalois K L] [IsGalois K M] (v : ↑RamificationIndexDomain) : UpperJump K M v ↔ UpperJump K L v ∨ UpperJump L M (inverseHerbrand K L v)

Upper breaks in a tower. For a tower M/L/K of Galois extensions, v is an upper break of M/K exactly when it is an upper break of L/K or ψ_{L/K}(v) is an upper break of M/L. Thus the upper breaks of M/K are those of L/K together with the images under φ_{L/K} of those of M/L.

noncomputable def Subgroup.upperRamificationGroupQuotient {K : Type u_1} {M : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field M] [ValuativeRel M] [TopologicalSpace M] [IsNonarchimedeanLocalField M] [Algebra K M] [ValuativeExtension K M] [Module.Finite K M] [IsGalois K M] (H : Subgroup Gal(M/K)) [H.Normal] (v : ↑TauCeti.LocalFieldsRamification.RamificationIndexDomain) : Subgroup (Gal(M/K) ⧸ H)

The upper ramification filtration of the quotient G ⧸ H, for a normal subgroup H of G = Gal(M/K): the image of G^v under the quotient map G → G ⧸ H.

Equations

• H.upperRamificationGroupQuotient v = Subgroup.map (QuotientGroup.mk' H) (TauCeti.LocalFieldsRamification.upperRamificationGroup K M v)

theorem Subgroup.upperRamificationGroup_quotient {K : Type u_1} {M : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field M] [ValuativeRel M] [TopologicalSpace M] [IsNonarchimedeanLocalField M] [Algebra K M] [ValuativeExtension K M] [Module.Finite K M] [IsGalois K M] (H : Subgroup Gal(M/K)) [H.Normal] (v : ↑TauCeti.LocalFieldsRamification.RamificationIndexDomain) : H.upperRamificationGroupQuotient v = map (QuotientGroup.mk' H) (TauCeti.LocalFieldsRamification.upperRamificationGroup K M v ⊔ H)

For a normal subgroup H of G = Gal(M/K), the defined quotient filtration is G^v H / H.

@[simp]

theorem Subgroup.mem_upperRamificationGroupQuotient_mk_iff {K : Type u_1} {M : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field M] [ValuativeRel M] [TopologicalSpace M] [IsNonarchimedeanLocalField M] [Algebra K M] [ValuativeExtension K M] [Module.Finite K M] [IsGalois K M] (H : Subgroup Gal(M/K)) [H.Normal] (v : ↑TauCeti.LocalFieldsRamification.RamificationIndexDomain) (σ : Gal(M/K)) : ↑σ ∈ H.upperRamificationGroupQuotient v ↔ σ ∈ TauCeti.LocalFieldsRamification.upperRamificationGroup K M v ⊔ H

A representative belongs to the quotient upper ramification group exactly when it belongs to G^v H.

theorem Subgroup.upperRamificationGroupQuotient_antitone {K : Type u_1} {M : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field M] [ValuativeRel M] [TopologicalSpace M] [IsNonarchimedeanLocalField M] [Algebra K M] [ValuativeExtension K M] [Module.Finite K M] [IsGalois K M] (H : Subgroup Gal(M/K)) [H.Normal] : Antitone H.upperRamificationGroupQuotient

The upper ramification filtration on a quotient is decreasing.

instance Subgroup.instNormalUpperRamificationGroupQuotient {K : Type u_1} {M : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field M] [ValuativeRel M] [TopologicalSpace M] [IsNonarchimedeanLocalField M] [Algebra K M] [ValuativeExtension K M] [Module.Finite K M] [IsGalois K M] (H : Subgroup Gal(M/K)) [H.Normal] (v : ↑TauCeti.LocalFieldsRamification.RamificationIndexDomain) : (H.upperRamificationGroupQuotient v).Normal

Each upper ramification group in the quotient is normal.

@[simp]

theorem Subgroup.upperRamificationGroup_fixedField {K : Type u_1} {M : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field M] [ValuativeRel M] [TopologicalSpace M] [IsNonarchimedeanLocalField M] [Algebra K M] [ValuativeExtension K M] [Module.Finite K M] [IsGalois K M] (H : Subgroup Gal(M/K)) [H.Normal] [ValuativeRel ↥(IntermediateField.fixedField H)] [TopologicalSpace ↥(IntermediateField.fixedField H)] [IsNonarchimedeanLocalField ↥(IntermediateField.fixedField H)] [ValuativeExtension K ↥(IntermediateField.fixedField H)] (v : ↑TauCeti.LocalFieldsRamification.RamificationIndexDomain) : map (↑(IsGalois.normalAutEquivQuotient H)) (H.upperRamificationGroupQuotient v) = TauCeti.LocalFieldsRamification.upperRamificationGroup K (↥(IntermediateField.fixedField H)) v

The upper numbering of a quotient, field-theoretically. For a normal subgroup H of G = Gal(M/K) and any local-field structure on the fixed field M^H compatible with K, the restriction isomorphism G ⧸ H ≃* Gal(M^H/K) maps the quotient upper ramification group at v onto the upper ramification group of M^H/K.