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!

[Thomas Browning]

@Andrew Yang Are these results available anywhere yet?

[Andrew Yang]

The relevant stuff is here:
https://github.com/leanprover-community/mathlib4/blob/KroneckerWeber/Mathlib/NumberTheory/KroneckerWeber/Unramified.lean

I haven’t found the time (and courage) to PR them yet but if you need them (and are willing to review them :)) then I try to start PRing them.

[Andrew Yang]

It might not be as bad as I thought: that file doesn’t seem to depend on anything else. I’ll try to open a PR when I get back to my laptop.

[Andrew Yang]

#25498 is the first PR. The connection of ramification and different will be the second.

[Andrew Yang]

Since mathlib defines unramified to be e=1 and residue field separable, the second PRs in line are
#25589: e=1 implies not divides different

[Andrew Yang]

#25591: residue field not separable implies divides different.

[Andrew Yang]

Also I saw @Riccardo Brasca assigned yourself but didn’t have a chance to leave a review on the previous PR. If you have any unsent reviews, I’m happy to address them in a separate PR.

[Riccardo Brasca]

Sorry I didn't have much time to review it. We can probably discuss them in person this week

[Andrew Yang]

#25792 is the PR linking different ideal and absolute discriminant.

[Thomas Browning]

Andrew Yang said:

#25792 is the PR linking different ideal and absolute discriminant.

Do you have a followup with "ramify iff divides discriminant" or should I make that myself? (I haven't checked, but I assume it's pretty quick from the merged PRs?)

[Andrew Yang]

Andrew Yang said:

#25591: residue field not separable implies divides different.

It is pending this PR. (Because unramified is defined to be e=1 and residue field separable in mathlib)

[Andrew Yang]

Thanks to the swift reviews of Riccardo,
#25936: ¬ P ∣ differentIdeal A B ↔ Algebra.IsUnramifiedAt A P is now dependency free.

[Junjie Bai]

Andrew Yang said:

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.

Is this proof available on Mathlib now? Or is the result available anywhere yet?

[Thomas Browning]

@Andrew Yang To add to that, do you have a definition of inertia subgroup at this point? I've been experimenting with the following definition that takes in G rather than K and L:

variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]
  (P : Ideal A) (Q : Ideal B) [Q.LiesOver P]
  (G : Type*) [Group G] [MulSemiringAction G B] [SMulCommClass G A B]

noncomputable def Ideal.inertiaSubgroup : Subgroup G :=
  (Ideal.Quotient.stabilizerHom Q P G).ker.map (MulAction.stabilizer G Q).subtype

[Andrew Yang]

I've been using docs#AddSubgroup.inertia.

[Thomas Browning]

Oh, nice. That's probably equivalent?

[Andrew Yang]

They should be. And docs#AddSubgroup.inertia has better defeqs because there's map in your definition (otherwise I like yours more).

[Andrew Yang]

Junjie Bai said:

Is this proof available on Mathlib now? Or is the result available anywhere yet?

I am slowly PRing it (sorry I forgot that people needed it :sweat_smile:). But in the mean time it is here

[Thomas Browning]

Well, the big advantage of your definition seems to be that it doesn't require specifying the base ring.

[Thomas Browning]

Also, I'm realizing now that I'm duplicating some of your results exactly. E.g., #26049 is just https://github.com/leanprover-community/mathlib4/blob/0aaa73fbf982736ed441b55a3a067383b184e342/Mathlib/NumberTheory/KroneckerWeber/IsInvariant.lean#L226C7-L226C27

[Andrew Yang]

It's probably my fault for not PRing my things sooner. What else do you have? Duplicated lemmas are easy to fix but if we have some different definitions we should probably try to unify them first.

[Thomas Browning]

I don't have that much really (#25726). Just a definition of the inertia subgroup and an attempt at computing it's cardinality where I realized that I would need the cardinality lemma in #26056 and the fact that (A/P)/(B/Q) is Galois which it looks like you also have.

[Junjie Bai]

Andrew Yang said:

Junjie Bai said:

Is this proof available on Mathlib now? Or is the result available anywhere yet?

I am slowly PRing it (sorry I forgot that people needed it :sweat_smile:). But in the mean time it is here

That will be very helpful, thank you!

[Andrew Yang]

The fact that (A/P)/(B/Q) is Galois is in #25616