Herbrand's theorem: the lower filtration of a quotient

Let M/K be a finite normal extension of nonarchimedean local fields with group G, and let L be an intermediate field, normal over K and with M/L Galois, so that restriction G → Gal(L/K) identifies Gal(L/K) with the quotient G / H by H = Gal(M/L). The lower numbering is not compatible with this quotient, but Herbrand's theorem says exactly how it fails: the image of G_u in Gal(L/K) is the lower ramification group at the index φ_{M/L}(u),

(G/H)_{φ_{M/L}(u)} = G_u H / H for every u ≥ -1.

This is the statement through which the Herbrand function passes to quotients: the transitivity φ_{M/K} = φ_{L/K} ∘ φ_{M/L} and the upper-numbering compatibility (G/H)^v = G^v H / H both rest on it. The file also records Serre's lemma comparing the lower indices of a lift σ of largest lower index in its coset and of its restriction σ|_L, which is the finite-index content of the theorem.

Main results

• TauCeti.LocalFieldsRamification.lowerIndex_mul_restrictScalars_of_forall_le: i_G(σ τ) = min (i_H(τ), i_G(σ)) for σ of largest lower index in its coset.
• TauCeti.LocalFieldsRamification.ramificationIndex_mul_lowerIndex_restrictNormal_eq_sum_card: e(M/L) · i_{G/H}(σ|_L) = ∑_{k < i_G(σ)} #H_k for such σ.
• TauCeti.LocalFieldsRamification.coe_herbrand_lowerIndex_sub_one: Serre's lemma φ_{M/L}(i_G(σ) - 1) = i_{G/H}(σ|_L) - 1 for such σ.
• TauCeti.LocalFieldsRamification.map_restrictNormalHom_lowerRamificationGroupReal: Herbrand's theorem, (G/H)_{φ_{M/L}(u)} = G_u H / H.
• TauCeti.LocalFieldsRamification.lowerRamificationGroupReal_eq_map_inverseHerbrand: the same statement read at v = φ_{M/L}(u), that is (G/H)_v = G_{ψ_{M/L}(v)} H / H.

References

• J.-P. Serre, Corps Locaux, Chapter IV, §3, Lemmas 4 and 5.

theorem TauCeti.LocalFieldsRamification.lowerIndex_mul_restrictScalars_of_forall_le {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] [Algebra L M] [ValuativeExtension L M] [Module.Finite L M] [Algebra K M] [ValuativeExtension K M] [Module.Finite K M] [IsScalarTower K L M] (σ : Gal(M/K)) (hσ : ∀ (τ : Gal(M/L)), IsLocalRing.lowerIndex (↥(ValuativeRel.valuation M).integer) (σ * AlgEquiv.restrictScalars K τ) ≤ IsLocalRing.lowerIndex (↥(ValuativeRel.valuation M).integer) σ) (τ : Gal(M/L)) : IsLocalRing.lowerIndex (↥(ValuativeRel.valuation M).integer) (σ * AlgEquiv.restrictScalars K τ) = min (IsLocalRing.lowerIndex (↥(ValuativeRel.valuation M).integer) τ) (IsLocalRing.lowerIndex (↥(ValuativeRel.valuation M).integer) σ)

If σ has the largest lower index in its coset σ H, H = Gal(M/L), then i_G(σ τ) = min (i_H(τ), i_G(σ)) for every τ ∈ H.

theorem TauCeti.LocalFieldsRamification.exists_forall_lowerIndex_mul_restrictScalars_le {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [Field M] [ValuativeRel M] [TopologicalSpace M] [IsNonarchimedeanLocalField M] [Algebra K L] [Algebra L M] [Module.Finite L M] [Algebra K M] [ValuativeExtension K M] [Module.Finite K M] [IsScalarTower K L M] (σ : Gal(M/K)) : ∃ (τ₀ : Gal(M/L)), ∀ (τ : Gal(M/L)), IsLocalRing.lowerIndex (↥(ValuativeRel.valuation M).integer) (σ * AlgEquiv.restrictScalars K τ₀ * AlgEquiv.restrictScalars K τ) ≤ IsLocalRing.lowerIndex (↥(ValuativeRel.valuation M).integer) (σ * AlgEquiv.restrictScalars K τ₀)

Every coset σ H contains an element of largest lower index.

theorem TauCeti.LocalFieldsRamification.ramificationIndex_mul_lowerIndex_restrictNormal_eq_sum_card {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] [Normal K L] [Algebra L M] [ValuativeExtension L M] [Module.Finite L M] [IsGalois L M] [Algebra K M] [ValuativeExtension K M] [Module.Finite K M] [IsScalarTower K L M] (σ : Gal(M/K)) {j : ℕ} (hj : IsLocalRing.lowerIndex (↥(ValuativeRel.valuation M).integer) σ = ↑j) (hσ : ∀ (τ : Gal(M/L)), IsLocalRing.lowerIndex (↥(ValuativeRel.valuation M).integer) (σ * AlgEquiv.restrictScalars K τ) ≤ IsLocalRing.lowerIndex (↥(ValuativeRel.valuation M).integer) σ) : ↑(ramificationIndex L M) * IsLocalRing.lowerIndex (↥(ValuativeRel.valuation L).integer) (σ.restrictNormal L) = ∑ k ∈ Finset.range j, ↑(Nat.card ↥(lowerRamificationGroup L M ↑k))

Serre's lemma on the lower index of a quotient, in counting form. If σ has the largest lower index in its coset σ H, and i_G(σ) = j is finite, then e(M/L) · i_{G/H}(σ|_L) = ∑_{k < j} #H_k.

theorem TauCeti.LocalFieldsRamification.lowerIndex_restrictNormal_ne_top {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] [Normal K L] [Algebra L M] [ValuativeExtension L M] [Module.Finite L M] [IsGalois L M] [Algebra K M] [ValuativeExtension K M] [Module.Finite K M] [IsScalarTower K L M] (σ : Gal(M/K)) (hj : IsLocalRing.lowerIndex (↥(ValuativeRel.valuation M).integer) σ ≠ ⊤) (hσ : ∀ (τ : Gal(M/L)), IsLocalRing.lowerIndex (↥(ValuativeRel.valuation M).integer) (σ * AlgEquiv.restrictScalars K τ) ≤ IsLocalRing.lowerIndex (↥(ValuativeRel.valuation M).integer) σ) : IsLocalRing.lowerIndex (↥(ValuativeRel.valuation L).integer) (σ.restrictNormal L) ≠ ⊤

If σ has the largest lower index in its coset σ H and i_G(σ) is finite, then so is i_{G/H}(σ|_L): a restriction of largest lower index among its lifts is trivial only when the lift is.

theorem TauCeti.LocalFieldsRamification.coe_herbrand_lowerIndex_sub_one {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] [Normal K L] [Algebra L M] [ValuativeExtension L M] [Module.Finite L M] [IsGalois L M] [Algebra K M] [ValuativeExtension K M] [Module.Finite K M] [IsScalarTower K L M] (σ : Gal(M/K)) {j : ℕ} (hj : IsLocalRing.lowerIndex (↥(ValuativeRel.valuation M).integer) σ = ↑j) (hσ : ∀ (τ : Gal(M/L)), IsLocalRing.lowerIndex (↥(ValuativeRel.valuation M).integer) (σ * AlgEquiv.restrictScalars K τ) ≤ IsLocalRing.lowerIndex (↥(ValuativeRel.valuation M).integer) σ) : ↑(herbrand L M ⟨↑j - 1, ⋯⟩) = ↑(IsLocalRing.lowerIndex (↥(ValuativeRel.valuation L).integer) (σ.restrictNormal L)).toNat - 1

Serre's lemma on the lower index of a quotient. If σ has the largest lower index in its coset σ H, and i_G(σ) = j is finite, then φ_{M/L}(j - 1) = i_{G/H}(σ|_L) - 1.

theorem TauCeti.LocalFieldsRamification.restrictNormal_mem_lowerRamificationGroupReal_herbrand_iff {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] [Normal K L] [Algebra L M] [ValuativeExtension L M] [Module.Finite L M] [IsGalois L M] [Algebra K M] [ValuativeExtension K M] [Module.Finite K M] [IsScalarTower K L M] (σ : Gal(M/K)) (hσ : ∀ (τ : Gal(M/L)), IsLocalRing.lowerIndex (↥(ValuativeRel.valuation M).integer) (σ * AlgEquiv.restrictScalars K τ) ≤ IsLocalRing.lowerIndex (↥(ValuativeRel.valuation M).integer) σ) (u : ↑RamificationIndexDomain) : σ.restrictNormal L ∈ lowerRamificationGroupReal K L ↑(herbrand L M u) ↔ σ ∈ lowerRamificationGroupReal K M ↑u

For σ of largest lower index in its coset σ H, the restriction σ|_L lies in the lower ramification group of L/K at φ_{M/L}(u) exactly when σ lies in that of M/K at u.

@[simp]

theorem TauCeti.LocalFieldsRamification.map_restrictNormalHom_lowerRamificationGroupReal {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] [Normal K L] [Algebra L M] [ValuativeExtension L M] [Module.Finite L M] [IsGalois L M] [Algebra K M] [ValuativeExtension K M] [Module.Finite K M] [IsScalarTower K L M] [Normal K M] (u : ↑RamificationIndexDomain) : Subgroup.map (AlgEquiv.restrictNormalHom L) (lowerRamificationGroupReal K M ↑u) = lowerRamificationGroupReal K L ↑(herbrand L M u)

Herbrand's theorem. For M/K finite normal, L/K a normal subextension and H = Gal(M/L), the image of the lower ramification group G_u of M/K under restriction to L is the lower ramification group of L/K at φ_{M/L}(u): (G/H)_{φ_{M/L}(u)} = G_u H / H.

theorem TauCeti.LocalFieldsRamification.lowerRamificationGroupReal_eq_map_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] [Normal K L] [Algebra L M] [ValuativeExtension L M] [Module.Finite L M] [IsGalois L M] [Algebra K M] [ValuativeExtension K M] [Module.Finite K M] [IsScalarTower K L M] [Normal K M] (v : ↑RamificationIndexDomain) : lowerRamificationGroupReal K L ↑v = Subgroup.map (AlgEquiv.restrictNormalHom L) (lowerRamificationGroupReal K M ↑(inverseHerbrand L M v))

Herbrand's theorem read at v = φ_{M/L}(u): (G/H)_v = G_{ψ_{M/L}(v)} H / H.