Tame inertia of an abelian number field at $q$ embeds in $(\mathbb{Z}/q)^\times$

Let $K$ be a finite abelian extension of $\mathbb{Q}$ with group $G = \mathrm{Gal}(K/\mathbb{Q})$, let $q$ be a prime number, and let $Q$ be a prime ideal of the ring of integers $\mathcal{O}_K$ over $q$. Let

be the inertia group. Assume that $q$ does not divide $|I|$ (the ramification at $Q$ is tame). The statement asserts that there is an injective group homomorphism

Thus $I$ is cyclic and $|I|$ divides $q - 1$.

Proof idea. Let $\pi$ be a uniformizer at $Q$ and let $k = \mathcal{O}_K/Q$. The tame character $\theta(\sigma) = \sigma(\pi)/\pi \bmod Q$ is a homomorphism $I \to k^\times$ that does not depend on $\pi$. Its kernel is the wild inertia group, a $q$-group, which is trivial because $q \nmid |I|$. For $\tau$ in the decomposition group, $\theta(\tau\sigma\tau^{-1}) = \bar\tau(\theta(\sigma))$. The group $G$ is abelian, so $\theta(\sigma)$ is fixed by the image of the decomposition group, which is all of $\mathrm{Gal}(k/\mathbb{F}_q)$. Hence $\theta(\sigma) \in \mathbb{F}_q^\times$.

Use. This is the main missing piece of the tame step NumberField.exists_isUnramifiedIn_le_sup_of_prime_ne of the Kronecker-Weber theorem: it gives $|I| \mid q - 1$ for an abelian field of degree prime to $q$.

Formalization Note. Q.inertia (K ≃ₐ[ℚ] K) is Mathlib's Ideal.inertia for the action of the Galois group on 𝓞 K. The hypothesis hq is not necessary for the truth of the statement (a prime ideal over span {q} exists only when q is prime or zero). Mathlib at this revision has Ideal.card_inertia_eq_ramificationIdxIn, the surjection from the decomposition group to the residue Galois group (Ideal.Quotient.stabilizerHom_surjective), and no higher ramification groups and no tame character. An alternative route: the Frobenius relation and commutativity give $\sigma^{q-1} = 1$ on the tame quotient, and the tame inertia group is cyclic.