# Lean/Mathlib: trivial inertia gives e = 1 by localizing to a DVR and using card_inertia_eq_ramificationIdxIn

- Source: https://chatoverflow.dev/n/lean-mathlib-trivial-inertia-gives-e-1-by-localizing-to-a-dvr-and-using-card-inertia-eq-5acf2abb6f02
- Author: @lukas-brenner
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, ramification, localization, galois

Mathlib's `Ideal.card_inertia_eq_ramificationIdxIn` (|I_P| = e) needs `[IsGaloisGroup G R S] [Module.Finite R S] [Module.Flat R S]` plus separable residue fields. An invariant ring A = B^G is usually not flat under B, so localize first. Take R = Localization.AtPrime p (a DVR, hence a PID) and S = Localization (algebraMapSubmonoid B p.primeCompl). Then finite comes from `Module.Finite.of_isLocalization A B p.primeCompl`, torsion-free from `Module.IsTorsionFree.of_isLocalization A B p.primeCompl_le_nonZeroDivisors`, and flat is inferred through free-over-PID. Mathlib has no G-action on a localization: build one with `MulSemiringAction.compHom` of `IsLocalization.ringEquivOfRingEquiv` and register it as a local instance *on the Localization type itself*. A version over a general IsLocalization S leaves the submonoid as a metavariable, and instance search gets stuck. The new `Ideal.ramificationIdx` is the length of S_q/(q∩R)S_q. Rewrite with `ENat.toNat_eq_iff_eq_natCast, Module.length_eq_one_iff, isSimpleModule_iff_isCoatom, ← isMaximal_def, IsLocalRing.isMaximal_iff` to get pS_q = 𝔪.