Transitivity of the Herbrand functions

Let M/K be a finite Galois extension of nonarchimedean local fields with group G, and let L be an intermediate field Galois over K, so that H = Gal(M/L) is normal in G and restriction to L identifies Gal(L/K) with G / H. Herbrand's theorem (G/H)_{φ_{M/L}(u)} = G_u H / H has a counting form, #(G/H)_{φ_{M/L}(u)} · #H_u = #G_u, because H_u = H ∩ G_u. Both φ_{M/K} and φ_{L/K} ∘ φ_{M/L} are affine on each interval [m, m + 1], and the counting form says that their slopes #G_{m+1} / #G_0 and (#H_{m+1} / #H_0) · (#(G/H)_{φ_{M/L}(m+1)} / #(G/H)_0) agree; since both functions are the identity on [-1, 0], this gives the transitivity of the Herbrand functions

φ_{M/K} = φ_{L/K} ∘ φ_{M/L} and ψ_{M/K} = ψ_{M/L} ∘ ψ_{L/K},

together with its integral form ψℕ_{M/K} = ψℕ_{M/L} ∘ ψℕ_{L/K}.

Main results

All declarations live in the namespace TauCeti.LocalFieldsRamification.

• natCard_lowerRamificationGroupReal_herbrand_mul: Herbrand's theorem in counting form, #(G/H)_{φ_{M/L}(u)} · #H_u = #G_u.
• lowerRamificationGroupReal_eq_of_forall_eq_of_herbrand_lt_of_le_herbrand: the filtration of L/K is constant on (φ_{M/L}(a), φ_{M/L}(b)] when that of M/K is constant on (a, b].
• herbrand_tower: φ_{M/K} = φ_{L/K} ∘ φ_{M/L}, as the identity herbrandOrderIso K M = (herbrandOrderIso L M).trans (herbrandOrderIso K L) of bundled order isomorphisms.
• inverseHerbrand_tower: ψ_{M/K} = ψ_{M/L} ∘ ψ_{L/K}, as the identity of the inverse order isomorphisms.
• psiNat_tower: ψℕ_{M/K} = ψℕ_{M/L} ∘ ψℕ_{L/K}.

References

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

Herbrand's theorem in counting form

Finiteness of M/K follows from that of L/K and M/L (Module.Finite.trans), but instance synthesis cannot recover it, since L is not determined by K and M; the statements therefore install Module.Finite K M with haveI rather than assuming it separately.

theorem TauCeti.LocalFieldsRamification.natCard_lowerRamificationGroupReal_herbrand_mul (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] [Normal K L] [IsGalois L M] [Normal K M] (u : ↑RamificationIndexDomain) : Nat.card ↥(lowerRamificationGroupReal K L ↑(herbrand L M u)) * Nat.card ↥(lowerRamificationGroupReal L M ↑u) = Nat.card ↥(lowerRamificationGroupReal K M ↑u)

Herbrand's theorem in counting form. For G = Gal(M/K), H = Gal(M/L) and G/H = Gal(L/K), the orders satisfy #(G/H)_{φ_{M/L}(u)} · #H_u = #G_u: the lower ramification group of the quotient at φ_{M/L}(u) is the image of G_u under restriction to L, and the kernel of restriction on G_u is H ∩ G_u = H_u.

theorem TauCeti.LocalFieldsRamification.lowerRamificationGroupReal_eq_of_forall_eq_of_herbrand_lt_of_le_herbrand (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] [Normal K L] [IsGalois L M] [Normal K M] {a b : ↑RamificationIndexDomain} {t : ℝ} (ht₁ : ↑(herbrand L M a) < t) (ht₂ : t ≤ ↑(herbrand L M b)) : (∀ (s : ℝ), ↑a < s → s ≤ ↑b → lowerRamificationGroupReal K M s = lowerRamificationGroupReal K M ↑b) → lowerRamificationGroupReal K L t = lowerRamificationGroupReal K L ↑(herbrand L M b)

Through Herbrand's theorem, the lower filtration of L/K is constant on the interval (φ_{M/L}(a), φ_{M/L}(b)] as soon as that of M/K is constant on (a, b].

Transitivity of the Herbrand functions

Here L/K and M/K are Galois, so M/L is Galois as well (IsGalois.tower_top_of_isGalois). Since L is an arbitrary field rather than an IntermediateField K M, instance synthesis cannot recover IsGalois L M from [IsGalois K M]; the statements below therefore install it with haveI as well.

theorem TauCeti.LocalFieldsRamification.herbrand_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] : herbrandOrderIso K M = (herbrandOrderIso L M).trans (herbrandOrderIso K L)

Transitivity of the Herbrand function in a tower M/L/K of Galois extensions: φ_{M/K} = φ_{L/K} ∘ φ_{M/L}, as an identity of the bundled order isomorphisms of RamificationIndexDomain.

theorem TauCeti.LocalFieldsRamification.inverseHerbrand_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] : (herbrandOrderIso K M).symm = (herbrandOrderIso K L).symm.trans (herbrandOrderIso L M).symm

Transitivity of the inverse Herbrand function in a tower M/L/K of Galois extensions: ψ_{M/K} = ψ_{M/L} ∘ ψ_{L/K}, as an identity of the inverse order isomorphisms. Inverting the composite φ_{L/K} ∘ φ_{M/L} reverses its order.

theorem TauCeti.LocalFieldsRamification.psiNat_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] : psiNat K M = psiNat L M ∘ psiNat K L

Transitivity of the integral inverse Herbrand function: ψℕ_{M/K} = ψℕ_{M/L} ∘ ψℕ_{L/K}.