Ramification

Stream: FLT-regular

[Thomas Browning]

I'm trying to formalize this argument: https://kconrad.math.uconn.edu/blurbs/gradnumthy/galoisselmerpoly.pdf
But I need the following fact from algebraic number theory:
If $K/\mathbb{Q}$ is Galois, then $\mathrm{Gal}(K/\mathbb{Q})$ is generated by the inertia subgroups
$I(q/p)=\{\sigma\in\mathrm{Gal}(K/\mathbb{Q}):\sigma(x)\equiv x\pmod{q}\text{ for all }x\in\mathcal O_K\}.$
I think the hardest part is already in mathlib (docs#NumberField.discr_gt_one), but a bit more is needed (e.g., glue between discriminant and ramification and the inertia group). Does FLT-regular have anything that might help?

[Riccardo Brasca]

I don't think we have the fact that an ideal ramifies if and only if it divides the discriminant, but I was planning to give it to a student.

[Chris Birkbeck]

We have the version with the relative different ideal (i.e. that its divisible by the ramified primes with the precise exponents). We also have some explicit ways to see if something is in the different ideal, from which I think you can get the link to the discriminant without too much pain.

[Chris Birkbeck]

There is also some stuff about how the Galois group permutes the ramification degrees, which might be useful for linking with inertia? probably @Andrew Yang can say more since he wrote pretty much all of the ramification stuff

[Riccardo Brasca]

Note that the different will soon be in mathlib #9063

[Thomas Browning]

Ok, thanks for the info! I'll probably hold off then, and wait for a bit more stuff to be done properly, rather than try to bodge together a solution at this point.

[Riccardo Brasca]

Well, if you need a precise result you can just sorry it, and we can see if it follows from what we have