# Zulip Chat Archive

## Stream: FLT-regular

### Topic: Ramification

#### Thomas Browning (Dec 17 2023 at 20:08):

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 (Dec 17 2023 at 20:24):

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 (Dec 17 2023 at 20:26):

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 (Dec 17 2023 at 20:27):

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 (Dec 17 2023 at 20:30):

Note that the different will soon be in mathlib #9063

#### Thomas Browning (Dec 17 2023 at 21:05):

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 (Dec 17 2023 at 21:09):

Well, if you need a precise result you can just `sorry`

it, and we can see if it follows from what we have

Last updated: Dec 20 2023 at 11:08 UTC