Commit 2025-02-13 06:13 e2c6f0ed

feat(NumberTheory/RamificationInertia): ramificationIdx and inertiaDeg in Galois extensions (#20899) Assume B/A is a finite extension of Dedekind domains, K is the fraction ring of A, L is the fraction ring of K. We show that if L/K is a Galois extension, then

1. All Ideal.ramificationIdx(resp. Ideal.inertiaDeg) over a fixed maximal ideal p of A are the same, which we define as Ideal.ramificationIdxIn(resp. Ideal.inertiaDegIn).
2. Let p be a maximal ideal of A, r be the number of prime ideals lying over p, e be the ramification index of p in B, and f be the inertia degree of p in B. Then r * (e * f) = [L : K]. It is the form of Ideal.sum_ramification_inertia in the case of Galois extension. This is adapted from the proof in the case of number fields.