Ramification Index equal to the card of inertia group

Stream: maths

[Junjie Bai]

I want to formalize the theorem that the ramification Index is equal to the card of inertia group. We define the inertia group consisted of the elements that member to the decomposition group and acts on the uniformizer trivially (mod the maximal ideal). Is there any elementary proof of this theorem? Because some definitions and theorems are missing in Mathlib, I can't finish the proof in current way.

[Andrew Yang]

I have a formalized proof of this, and the proof goes through

1. $g = |G/D|$ by orbit-stabilizer (and docs#Algebra.IsInvariant.exists_smul_of_under_eq)
2. $f = |D/I|$ by docs#Ideal.Quotient.stabilizerHom_surjective
3. $efg = |G| = |I||D/I||G/D|$ by docs#Ideal.ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn

Hopefully everything will go public in a week so that I can actually point you to some lean code.

[Junjie Bai]

That's really encouraging! I sincerely hope your code will be accepted!

[Thomas Browning]

@Andrew Yang Are you also working on the connection with the discriminant, or is that still untouched?

[Andrew Yang]

Yeah I also have a proof that $P\nmid\mathcal{D}_{S/R} \iff P$ is unramified and that the absolute norm of $\mathcal{D}_{\mathcal{O}/\mathbb{Z}}$ is the discriminant. The full $P^e|\mathcal{D}_{S/R} \iff p | e$ needs more work and (hopefully) I don't need it for now.

[Thomas Browning]

Oh, fantastic! Looking forward to the PRs!