The lower index of a quotient of a Galois group

Let M/K be a finite Galois extension of nonarchimedean local fields with group G, and let L be an intermediate field, normal over K, so that restriction G → Gal(L/K) identifies Gal(L/K) with the quotient G / H by H = Gal(M/L). Serre's lower index i_G(σ) = min_{x ∈ 𝒪[M]} v_M(σ x - x) (TauCeti.IsLocalRing.lowerIndex) encodes the lower ramification filtration, since σ ∈ G_i ↔ i + 1 ≤ i_G(σ). This file proves how it behaves under passage to the quotient:

e(M/L) · i_{G/H}(σ') = ∑_{σ ↦ σ'} i_G(σ),

where e(M/L) is the ramification index of M/L. The identity is stated in ℕ∞, where it holds for every σ': at σ' = 1 both sides are ⊤. It is the input from which Herbrand's theorem, the compatibility of the upper numbering with quotients, is derived.

Main results

• TauCeti.LocalFieldsRamification.ramificationIndex_mul_lowerIndex_restrictNormal_eq_sum: for σ : Gal(M/K), e(M/L) · i(σ|_L) = ∑_{τ ∈ Gal(M/L)} i(σ τ), the sum over the coset σ H.
• TauCeti.LocalFieldsRamification.ramificationIndex_mul_lowerIndex_eq_sum: for σ' : Gal(L/K), e(M/L) · i(σ') = ∑_{σ|_L = σ'} i(σ), the sum over the fibre of restriction.

References

• J.-P. Serre, Corps Locaux, Chapter IV, §1, Proposition 3.

theorem TauCeti.LocalFieldsRamification.ramificationIndex_mul_lowerIndex_restrictNormal_eq_sum {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] [Algebra K M] [ValuativeExtension K M] [Module.Finite K M] [IsScalarTower K L M] [IsGalois L M] (σ : Gal(M/K)) : ↑(ramificationIndex L M) * IsLocalRing.lowerIndex (↥(ValuativeRel.valuation L).integer) (σ.restrictNormal L) = ∑ τ : Gal(M/L), IsLocalRing.lowerIndex (↥(ValuativeRel.valuation M).integer) (σ * AlgEquiv.restrictScalars K τ)

Serre's quotient formula for the lower index, over a coset. For an intermediate field L of M/K normal over K and σ : Gal(M/K), e(M/L) · i_{L/K}(σ|_L) = ∑_{τ ∈ Gal(M/L)} i_{M/K}(σ τ).

theorem TauCeti.LocalFieldsRamification.ramificationIndex_mul_lowerIndex_eq_sum {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] [Algebra K M] [ValuativeExtension K M] [Module.Finite K M] [IsGalois K M] [IsScalarTower K L M] (σ' : Gal(L/K)) : ↑(ramificationIndex L M) * IsLocalRing.lowerIndex (↥(ValuativeRel.valuation L).integer) σ' = ∑ σ : Gal(M/K) with σ.restrictNormal L = σ', IsLocalRing.lowerIndex (↥(ValuativeRel.valuation M).integer) σ

Serre's quotient formula for the lower index. For an intermediate field L of M/K normal over K and σ' : Gal(L/K), e(M/L) · i_{L/K}(σ') = ∑_{σ|_L = σ'} i_{M/K}(σ), the sum running over the automorphisms of M/K restricting to σ'.