Cycle patterns are conjugation invariant

Proved

ChebotarevDensity.cyclePattern_conj

by vebis · Oct 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

galois-theorynumber-theory

Let $f\in\mathbb Z[X]$ and let $G=\operatorname{Gal}(f)$ be its Galois group, acting on the zeros of $f$ . The cycle pattern of an element $\sigma\in G$ (the multiset of cycle lengths of the permutation it induces on the zeros of $f$ , fixed points included) is invariant under conjugation:

\text{cycle pattern of }x\sigma x^{-1}=\text{cycle pattern of }\sigma\qquad(\sigma,x\in G).

Consequently the cycle pattern is a well-defined invariant of a conjugacy class of $G$ .

Preamble

import Definitions.Def_ChebotarevDensity_Defs
import Definitions.Def_ChebotarevDensity_Aux

open Polynomial NumberField

Formal statement

namespace ChebotarevDensity

theorem cyclePattern_conj (f : ℤ[X]) (g x : GalGroup f) :
    cyclePattern f (x * g * x⁻¹) = cyclePattern f g := by sorry

end ChebotarevDensity

Source

Stevenhagen–Lenstra, Chebotarëv and his density theorem, Math. Intelligencer 18 (1996), no. 2, pp. 32–34 (Theorem of Frobenius, decomposition types, cycle patterns) and Appendix, pp. 35–36

View graph