Formalizing Ramification Groups

Stream: maths

[Jiang Jiedong]

Hi everyone,

I have a preliminary plan for formalizing the ramification groups, which I will outline below. I would be grateful to receive any of your comments and advice for refinement!

The main motivation of formalizing ramification groups for me is extending current formalization work of local fields and contribute towards the formalization of p-adic Hodge theory. The main reference I use is Serre's book Local Fields.

1. The initial problem is that for what kind of extension should we define the ramification group. My current answer is for ring extension $L/K$ that has valued instance on K and a special valued instance [vL : Valued L ℤₘ₀] on L and an instance [ValAlgebra K L] (meaning that valuation on L is an extension of valuation on K in a suitable sense, see this post). This is a compromising choice for notations to be aligned with the literature. $G_i = \{s | v (s(x) - x) \ge i + 1, \forall x \in L \text{ s.t. } v(x) \ge 0 \, \}$ is used commonly in the literature, and this $+1$ restricts our definition to ℤₘ₀ only.
2. I will define the type of algebra homomorphism that is compatible the Valued structures, L ≃ₐv[K] L. (Together with ValRingHom, ValAlgebra to support it.) For local fields, this would be the same as the Galois group L ≃ₐ[K] L, due to the uniqueness of extension of valuation. However, when $L = \mathbb{C}_p, \widehat{\mathbb{Q}}_p^{ur}, \widehat{\mathbb{Q}_p^{cyc}}, ...$, this type is more natural than the algebra homomorphisms. (This would be the same as continuous algebra homomorphisms in above cases). In the case of number fields extension $L / K$, if we manually fill in the valued instance defined by some prime ideal $\mathfrak{P}$, L ≃ₐv[K] L will be isomorphic to the decomposition group of $\mathfrak{P}$, $G_0$ will correspond to the inertia subgroup. In my plan, the lower ramification group will be a ℤ-indexed filtration of subgroups of L ≃ₐv[K] L (just OrderHom(ℤᵒᵈ , Subgroup (L ≃ₐv[K] L))), as a filtration of subgroups of L ≃ₐ[K] L under coercion. I will mainly use the case of finite extension of local fields for now. (So an alternative is that I just ignore L ≃ₐv[K] L and define everything just using L ≃ₐ[K] L.)
3. The Herbrand function $\varphi_{L/K}, \psi_{L/K}$ and the index function $i_{L/K}(s) = \min_{x \in \mathcal{O}_L} {s(x) - x}$ could be defined as general as the lower ramification group. Many properties only holds in the case of finite extension of local fields. The upper numbering ramification group is defined using Herbrand function (only for finite extension of local fields first) and will be a $\mathbb{Q}$-indexed filtration of subgroups of L ≃ₐv[K] L. After proving the property of $G^u H /H = (G/H)^u$, the definition of upper numbering ramification group can be extended to arbitrary (possibly infinite) algebraic extension of a local field.
4. If needed in future work, I will define a renomalizing of ramification group, making both lower and upper numbering start from 0 instead of -1. This will also extends the definition of lower numbering ramification group to extension $L/K$ for arbitrary value group on $L$ instead of only ℤₘ₀, as a filtration of subgroups indexed by elements in the value group.

[Kevin Buzzard]

1. Probably you should make thsi definition for all $i\in\Z$ because the literature insists on starting at $-1$. The alternative is WithBot Nat, because with the lower numbering $G_u=G_0$ for $-1<u\leq 0$ and with the upper numbering $G^u=G^0=G_0$ for $-1<u\leq 0$. I agree it's fine to stick to top field having a discrete valuation.

2. You're now talking about $\mathbb{C}_p$ so I guess you've dropped the hypothesis that $v$ is discrete. Another possibility is to consider the preorder on $L$ associated to the valuation ($a\leq b\iff v(a)\leq v(b)$) and look at $K$-algebra morphisms which preserve the preorder. But my instinct is that whilst this might boil down to the same thing, your approach is probably easier to understand and I doubt the preorder approach will buy you anything: you can't use order-preserving maps because you need them to be $K$-algebra maps so you'll have to make a new structure anyway. Re your comments on restricting to the local case: I think this is unwise. Serre allows the global case quite a lot at the beginning of his his book even though the title is local fields, and Serre thinks in a Bourbaki style.

3. yeah

4. This renormalisation has made me quite angry recently. The normalisation in the literature seems to be a completely ridiculous choice. The only thing which one might think it has going for it is that some filtration on $K^\times$ corresponds to the upper numbering on the abelianisation of the Weil group via the class field theory isomorphism, but when you write down what the theorem is (involving something called $U_K^n$ on Wikipedia) this (a) does not even make sense for $n=-1$ (b) is arbitrarily defined to be $\mathcal{O}_K^\times$ for $n=0$ (c) is $1+(\pi)$ for $n=1$ (d) is not $(1+(\pi))^n$ for $n>1$, it's instead $1+(\pi^n)$, which doesn't coincide in general. So it's not the $n$ th power of anything. However I think it's important we stick to the literature.

norm1.png

This looks like a Lean beginner definition :-)

[Adam Topaz]

I still think the lower numbering should be defined for an arbitrary Galois extension $L|K$ of valued fields (meaning that the valuation of L restricts to the valuation of K), and that the lower numbering should be indexed by the upward closed subsets of the value group (assuming they're wrriten aditively and that $v(0) = \infty$).

[Adam Topaz]

At the very least, the wild ramification group is an object that does make sense (and is quite important in general valuation theory) for arbitrary valuations, not just rank 1.

[Jiang Jiedong]

Adam Topaz said:

I still think the lower numbering should be defined for an arbitrary Galois extension $L|K$ of valued fields (meaning that the valuation of L restricts to the valuation of K), and that the lower numbering should be indexed by the upward closed subsets of the value group (assuming they're wrriten aditively and that $v(0) = \infty$).

Maybe this can be done in 4th part, and add theorems comparing between this and Serre's notation of lower ramification group? I agree with that this "upward closed subsets" indexed should be done for general Galois extension of valued fields.

[Kevin Buzzard]

For general valuations, do people use any concepts beyond decomposition, inertia and wild inertia? I'm unclear about whether having a filtration in the general case is just generalisation for generalisation's sake and will slow down the journey towards the integer indexed lower numbering in the discrete case.

[Antoine Chambert-Loir]

Adam Topaz said:

I still think the lower numbering should be defined for an arbitrary Galois extension $L|K$ of valued fields (meaning that the valuation of L restricts to the valuation of K), and that the lower numbering should be indexed by the upward closed subsets of the value group (assuming they're wrriten aditively and that $v(0) = \infty$).

It could probably be defined in an even greater generality: one has an action of a group on a “filtered space”, and one considers the greatest stratum which is invariant under a given element.