The quotient embeddings of the ramification filtration #
Let L be a nonarchimedean local field and let a group G act on L by ring automorphisms
preserving the ring of integers, so that both the ramification filtration
G_i = TauCeti.IsLocalRing.ramificationGroup G 𝒪[L] i and the unit filtration
U(L,i) = TauCeti.unitFiltration L i are defined. The motivating case is the Galois group
L ≃ₐ[K] L of a finite extension of local fields, for which
TauCeti.integerRingIsInvariantSubring supplies the invariance hypothesis.
Fixing a uniformizer ϖ, that is an irreducible element of 𝒪[L], this file compares the two
filtrations through the ratio σ ϖ / ϖ. An element of G_i moves ϖ by a factor lying in
U(L,i), and the class of that factor modulo U(L,i+1)
- does not depend on the choice of
ϖ, - is multiplicative in
σ, and - is trivial on
G_{i+1},
so it defines θ_i : G_i / G_{i+1} → U(L,i) / U(L,i+1). The map θ_i is injective: an element
of G_0 fixes every Teichmüller representative, and every integer of L is a Teichmüller
representative plus ϖ times an integer, so membership of an element of G_0 in G_{i+1} is
decided at ϖ alone.
At depth zero, composing with the reduction isomorphism U(L,0) / U(L,1) ≃ 𝓀[L]ˣ
gives the tame character G_0 → 𝓀[L]ˣ, which kills G_1; the induced map on G_0 / G_1 is
injective, so the tame quotient is cyclic of order dividing q - 1, where q is the cardinality
of the residue field. At positive depth U(L,i) / U(L,i+1) has q elements, so every
G_i / G_{i+1} with i ≥ 1 is a p-group for the residue characteristic p; when the action is
faithful and G_0 is finite, the filtration reaches 1, and every G_i with i ≥ 1, in
particular the wild inertia group G_1, is a p-group.
Main definitions #
TauCeti.uniformizerRatio: the ratioσ ϖ / ϖ, as an element ofU(L,i).TauCeti.ramificationGroupToUnitFiltrationGraded: the homomorphismG_i → U(L,i) / U(L,i+1), andTauCeti.ramificationGroupGradedToUnitFiltrationGraded: the inducedθ_ionG_i / G_{i+1}.TauCeti.ramificationGroupGradedToResidueField: the positive-depth quotient embedding composed with the additive residue-field coordinate determined by a uniformizer.TauCeti.tameCharacter: the depth-zero homomorphismG_0 → 𝓀[L]ˣ, andTauCeti.tameCharacterGraded: the map it induces onG_0 / G_1.
Main results #
TauCeti.mem_ramificationGroup_natCast_iff_valuation_le: the valuation form of the ramification filtration,v(σ x - x) ≤ v(ϖ)^(i+1)for every integerx.TauCeti.ramificationGroupToUnitFiltrationGraded_eq_of_irreducible,TauCeti.ramificationGroupGradedToUnitFiltrationGraded_eq_of_irreducible,TauCeti.tameCharacter_eq_of_irreducibleandTauCeti.tameCharacterGraded_eq_of_irreducible: independence of the choice of uniformizer.TauCeti.smul_teichmullerLift_of_mem_ramificationGroup_zero:G_0fixes every Teichmüller representative.TauCeti.mem_ramificationGroup_natCast_iff_smul_sub_mem: an element ofG_0lies inG_nexactly when it moves a uniformizer by an element of𝓂[L] ^ (n + 1).TauCeti.smul_div_mem_unitFiltration: forσ ∈ G_i, every ratioσ y / ylies inU(L,i).TauCeti.mem_ramificationGroup_one_of_valuation_pow_sub_one_lt_one: an element ofG_0lies inG_1once ap-power ofσ ϖ / ϖis congruent to1.TauCeti.valuation_smul_div_pow_sub_one_lt_one: ifσ ∈ G_0fixes an element of valuationv(a) ^ n, then(σ a / a) ^ nis congruent to1.TauCeti.ker_ramificationGroupToUnitFiltrationGradedandTauCeti.ramificationGroupGradedToUnitFiltrationGraded_injective: the kernel is exactlyG_{i+1}, andθ_iis injective.TauCeti.ramificationGroupGradedToResidueField_change: changing the uniformizer in the positive-depth residue coordinate multiplies it by the corresponding residue-field unit.TauCeti.isCyclic_ramificationGroupGraded_zeroandTauCeti.card_ramificationGroupGraded_zero_dvd_card_residueField_sub_one: the tame quotient is cyclic, of order dividingq - 1.TauCeti.isPGroup_ramificationGroupGraded_natCast_succandTauCeti.isPGroup_ramificationGroup: the positive-depth graded pieces, and, for a faithful action with finiteG_0, the positive-depth ramification groups, arep-groups.TauCeti.ramificationGroupOneSylowandTauCeti.eq_ramificationGroupOneSylow: the wild inertia groupG_1, viewed insideG_0, is its unique normal Sylowp-subgroup.TauCeti.natCard_ramificationGroup_one: the order ofG_1is thep-part of the order ofG_0.TauCeti.ramificationGroup_one_eq_bot_iff_not_dvd_card_ramificationGroup_zero:G_1is trivial exactly whenpdoes not divide the order ofG_0, the tame case.
Implementation notes #
The ramification groups are indexed by ℤ and the unit filtration by ℕ. Every general statement
below therefore fixes a natural index i and reads the ramification group at (i : ℤ), whereas
the depth-zero declarations fix the index (0 : ℤ), the spelling in which a statement about
G_0 / G_1 is met.
References #
- J.-P. Serre, Corps Locaux, Chapter IV, §2, Proposition 5.
The valuation form of the ramification filtration #
Serre's valuation form of the ramification filtration: σ lies in G_i exactly when it
moves every integer of L by an element of valuation at most v(ϖ) ^ (i + 1), for ϖ a
uniformizer. The left-hand side does not mention ϖ, so neither side depends on the choice.
The same condition read through the additive valuation of the discrete valuation ring 𝒪[L] is
TauCeti.IsLocalRing.mem_ramificationGroup_iff_le_addVal; the multiplicative form below is the
one in which the unit filtration is stated.
The action preserves the valuation of a uniformizer: the image of an irreducible element of
𝒪[L] is irreducible, hence associated to it.
The ratio of a uniformizer #
For σ in the i-th ramification group and x a unit of 𝒪[L], the ratio σ x / x lies
one step deeper in the unit filtration, in U(L, i+1).
For σ in the i-th ramification group and ϖ a uniformizer, the ratio σ ϖ / ϖ lies in
the i-th step U(L,i) of the unit filtration.
The ratio σ ϖ / ϖ of a uniformizer ϖ and its image under an element σ of the i-th
ramification group, as an element of the i-th step U(L,i) of the unit filtration.
Instances For
For σ in the i-th ramification group, the ratio σ y / y of any nonzero y lies in the
i-th step U(L,i) of the unit filtration. For a uniformizer this is
TauCeti.mem_unitFiltration_of_val_eq_smul_div, and for a unit it is one step deeper, by
TauCeti.mem_unitFiltration_succ_of_val_eq_smul_div.
The quotient homomorphism #
The quotient homomorphism attached to a uniformizer ϖ: the homomorphism
G_i → U(L,i) / U(L,i+1) carrying σ to the class of σ ϖ / ϖ. It kills G_{i+1}, so it may
fail to be injective; the map it induces on G_i / G_{i+1} is the embedding θ_i of
TauCeti.ramificationGroupGradedToUnitFiltrationGraded.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The quotient homomorphism does not depend on the choice of uniformizer: two uniformizers
differ by a unit of 𝒪[L], and σ moves that unit inside U(L,i+1).
Membership decided at a uniformizer #
An element of the inertia group G_0 fixes every Teichmüller representative: its image is
again fixed by the q-th power map and has the same residue.
Membership in the ramification filtration is decided at a uniformizer: an element σ of
the inertia group G_0 lies in G_n exactly when σ ϖ ≡ ϖ modulo 𝓂[L] ^ (n + 1). Writing an
integer as a Teichmüller representative, which σ fixes, plus ϖ times an integer, the
congruence propagates from ϖ to every integer one power of 𝓂[L] at a time.
An element of the inertia group G_0 lies in G_1 as soon as the ratio σ ϖ / ϖ of a
uniformizer ϖ has a p-power congruent to 1 modulo the maximal ideal, for p the residue
characteristic.
For σ in the inertia group G_0 fixing an element b of valuation v(a) ^ n, the n-th
power of the ratio σ a / a is congruent to 1 modulo the maximal ideal.
The kernel #
The kernel of the quotient homomorphism, as a valuation condition at the chosen uniformizer:
σ is killed exactly when it moves ϖ one step deeper than membership in G_i requires.
The next step G_{i+1} of the ramification filtration is killed by the quotient
homomorphism.
The kernel of the quotient homomorphism is exactly G_{i+1}, which is what makes the
induced θ_i on G_i / G_{i+1} an embedding: membership of an element of G_0 in G_{i+1} is
decided at ϖ (TauCeti.mem_ramificationGroup_natCast_iff_smul_sub_mem).
The embedding of the graded pieces #
The quotient map θ_i : G_i / G_{i+1} →* U(L,i) / U(L,i+1), induced by
σ ↦ σ ϖ / ϖ for a uniformizer ϖ. It is an embedding
(TauCeti.ramificationGroupGradedToUnitFiltrationGraded_injective).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The quotient embeddings are injective.
The descended quotient map does not depend on the choice of uniformizer.
Positive-depth residue-field coordinates #
The positive-depth embedding of G_{n+1}/G_{n+2} into the additive residue field, in the
coordinate determined by a uniformizer π.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The positive-depth ramification quotient embeds in the additive residue field.
Compute a positive-depth residue coordinate from the displacement of a representative.
Change the uniformizer used for a positive-depth ramification coordinate.
The tame character #
The tame character θ_0 : G_0 →* 𝓀[L]ˣ: the depth-zero quotient homomorphism composed
with the identification of U(L,0) / U(L,1) with the multiplicative group of the residue
field. It carries σ to the residue of σ ϖ / ϖ. It kills G_1, hence factors through
TauCeti.tameCharacterGraded.
Equations
Instances For
The tame character does not depend on the choice of uniformizer.
The tame character read on the quotient G_0 / G_1 it factors through. It is injective
(TauCeti.tameCharacterGraded_injective).
Equations
Instances For
The graded tame character does not depend on the choice of uniformizer.
The tame character is injective on G_0 / G_1.
The tame quotient is cyclic: G_0 / G_1 embeds into the multiplicative group of the
residue field, which is cyclic because the residue field is finite.
The order of the tame quotient G_0 / G_1 divides q - 1, for q the cardinality of the
residue field.
Wild inertia is a p-group #
At positive depth i, the graded piece G_i / G_{i+1} is a p-group for the residue
characteristic p: it embeds into U(L,i) / U(L,i+1), which has q elements.
The positive-depth ramification groups are p-groups, for p the residue
characteristic, whenever the action is faithful and G_0 is finite; in particular the wild
inertia group G_1 is a p-group. The filtration reaches 1, and each positive-depth step
G_i / G_{i+1} is a p-group (TauCeti.isPGroup_ramificationGroupGraded_natCast_succ).
Wild inertia as the Sylow subgroup of inertia #
The index of G_1 in G_0 is prime to the residue characteristic p. This is the
order-theoretic consequence of the tame-character embedding G_0/G_1 → 𝓀[L]ˣ.
Wild inertia is the Sylow p-subgroup of inertia. For the residue characteristic p,
the first ramification group G_1, viewed as a subgroup of G_0, is a Sylow p-subgroup.
The two inputs are the positive-depth p-group theorem and the tame-character embedding, which
shows that the index #(G_0/G_1) divides #𝓀[L] - 1 and is therefore prime to p.
Equations
Instances For
The subgroup underlying ramificationGroupOneSylow is G_1 viewed inside G_0.
The wild inertia Sylow subgroup is normal in inertia.
The wild inertia Sylow subgroup is the unique Sylow p-subgroup of inertia.
The order of wild inertia is the residue-characteristic part of the order of inertia:
#G_1 = p ^ (v_p #G_0).
Wild inertia is trivial exactly in the tame case. For the residue characteristic p, the
first ramification group G_1 is trivial if and only if p does not divide the order of the
inertia group G_0: G_1 is the Sylow p-subgroup of G_0.