Commit 2026-02-13 12:37 972c70a9
View on Github →feat(RingTheory/Ideal): isomorphism between stabilizer G Q / inertia G Q and the Galois group of the residue fields extension (#34730)
Construct the isomorphism
MulAction.stabilizer G Q ⧸ (Q.inertia G).subgroupOf (MulAction.stabilizer G Q) ≃* Gal((B ⧸ Q)/(A ⧸ P))
where Q is a prime ideal of B above the ideal P of A.
Also included
- add the following abbreviation to make it easier to refer to the inertia group of an ideal
abbrev Ideal.inertia (I : Ideal B) : Subgroup G := AddSubgroup.inertia I.toAddSubgroup G
- golf the proofs of
ncard_primesOver_mul_card_inertia_mul_finrank - add
lemma card_stabilizer_eq :
Nat.card (MulAction.stabilizer G P) = p.ramificationIdxIn S * p.inertiaDegIn S