Ramification quotients for subgroups

Let a group G act on a nonarchimedean local field L, preserving its integer ring, and let H ≤ G. The ramification filtration for the restricted action is the intersection of H with the filtration for G. Consequently, inclusion induces an injective homomorphism

H_i / H_{i+1} → G_i / G_{i+1}.

This file constructs that homomorphism and proves that the ramification-quotient embedding θ_i : G_i / G_{i+1} → U(L,i) / U(L,i+1) is natural for it. Thus passing to a subgroup does not change the uniformizer ratio representing a ramification class. This is the subgroup counterpart to the quotient behavior used by Herbrand theory.

Main results

• TauCeti.IsLocalRing.ramificationGroupGradedSubgroupHom: the injective map on successive ramification quotients induced by subgroup inclusion.
• TauCeti.ramificationGroupGradedToUnitFiltrationGraded_comp_subgroupHom: the embeddings θ_i commute with passage to H.

References

• J.-P. Serre, Corps Locaux, Chapter IV, §2.

theorem TauCeti.ramificationGroupGradedToUnitFiltrationGraded_comp_subgroupHom {L : Type u_1} [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] {G : Type u_2} [Group G] [MulSemiringAction G L] [IsInvariantSubring G (ValuativeRel.valuation L).integer] {H : Subgroup G} (n : ℕ) {ϖ : ↥(ValuativeRel.valuation L).integer} (hϖ : Irreducible ϖ) : (ramificationGroupGradedToUnitFiltrationGraded n hϖ).comp (IsLocalRing.ramificationGroupGradedSubgroupHom G (↥(ValuativeRel.valuation L).integer) H ↑n) = ramificationGroupGradedToUnitFiltrationGraded n hϖ

Naturality of the ramification-quotient embedding under subgroups. Including H_i/H_{i+1} into G_i/G_{i+1} and then applying θ_i gives the same class in U(L,i)/U(L,i+1) as applying the quotient embedding for the restricted H-action.