Stack Exchange network consists of 183 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.
If we have the first two, I believe that we need results about realisability to find what we want. Again, there is nothing wrong with this. Just it seems like "to kill a fly with a cannon", and least in my opinion.
4) I will surely read Fabio's preprint as soon as possible. Still, I have already discussed with him about his summary. It seems to me that he presents relations between global freeness and locally freeness (so with semi-completions), and between locally freeness and freeness in the local case, but not bewteen freeness in the global and local case.
3) Ok so with probably just one exception, where there is a proof in the global case, there is also a direct proof of a local case. Also, thank to Henniart's result, now we know that this is always true when $p\ne 2$, and there is no need to prove again directly the case also in the local setting. This is great.
For example, in the preface of Childs' book "Taming wild extensions: Hopf algebras and local Galois module theory", published in 2000, Childs says that the global case "immediately implies the corresponding result for abelian extensions of $\mathbb{Q}_p$.
2) There is no problem a priori in the use of Henniart's result (except when $p=2$ clearly), and of course, once you have this result, the proof in the local case is immediate and direct. But this result is quite complicated, it seems to need a big machinery behind, and finally, I am quite sure that this is not the result that other mathematicians had in mind when they used global to deduce local.
I have asked this question in MSE, but I had no replies, and I was suggested to ask the question here. The link is the following: math.stackexchange.com/questions/4131623/…