Galois group of completion

Stream: Is there code for X?

[Andrew Yang]

Let $K$ be a number field and $v$ be a finite place of $K$. Do we know that $\mathrm{Gal}(\overline{K}_v/K_v)$ is isomorphic to the decomposition group of $v$?

[Kevin Buzzard]

There is some content here: it's not too difficult to write down the map from the local Galois group to the global one, but the claim that it's injective boils down to the statement that any field automorphism of $\overline{K}_v$ fixing $\overline{K}$ and $K_v$ is trivial. The proof I know of this uses that $\overline{K}$ is dense in $\overline{K}_v$ but that sentence doesn't even make sense until $\overline{K}_v$ has a topology and #23301 is not merged yet (the 7 PRs it depends on are all merged though and the PR itself is very close, I reviewed it earlier this week and I think it will be ready after Maria Ines responds). Even when the question makes sense we'll need to prove some form of Krasner's lemma and I don't think we have that. Do you need the injectivity though in your application though? (if it is what I think it is then maybe you don't)

[Andrew Yang]

Yeah I only need the map.
The map from the decomposition to the local Galois isn’t hard too. It’s the fact that the two constructions are inverse to another that is hard. So I figured I should ask for both and see if we have any.

[Kevin Buzzard]

I don't see how to get the map from the decomposition to the local Galois without using Maria-Ines' work. What am I missing?

[Andrew Yang]

I thought that $\bigcup_{L/F\text{ finite}} L_w = \overline{F}_v$ but after thinking about it a bit more I can only prove that it is dense.

[Kevin Buzzard]

Right, I think this is Krasner, which in some sense we are only able to state once #23301 goes in (take generators for the finite local extension, approximate their min polys by elements of F etc)

[Johan Commelin]

@Jiang Jiedong did Krasner

[Jz Pan]

Kevin Buzzard said:

it's not too difficult to write down the map from the local Galois group to the global one

I think you need to fix an embedding of $\overline K$ to $\overline K_v$ (which can be given by IsAlgClosed.lift I think?).

[Jz Pan]

And the "decomposition group of $v$" itself requires to fix an extension $\overline v$ of $v$ to $\overline F$ I think? This should be equivalent to fix an embedding of $\overline K$ to $\overline K_v$?