Conductors and cyclotomic character subfields

The Galois correspondence for a rational cyclotomic field identifies each intermediate field with a subgroup of Dirichlet characters. This file packages the conductor criterion for comparing such an intermediate field with a lower cyclotomic field: containment holds exactly when the conductor of its character subgroup divides the lower level.

The result combines Mathlib's character-subgroup correspondence IsCyclotomicExtension.Rat.intermediateFieldEquivSubgroupChar with its pointwise criterion IsCyclotomicExtension.Rat.mem_intermediateFieldEquivSubgroupChar_iff_conductor_dvd.

Main results

• Subgroup.characterSubfield_le_iff_dirichletConductor_dvd: the field cut out by a character subgroup lies in a lower cyclotomic field exactly when the subgroup conductor divides the lower level.

theorem Subgroup.characterSubfield_le_iff_dirichletConductor_dvd {n m : ℕ} [NeZero n] {K : Type u_1} [Field K] [NumberField K] [IsCyclotomicExtension {n} ℚ K] [IsAbelianGalois ℚ K] {R : Type u_2} [CommRing R] [HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)] (Y : Subgroup (DirichletCharacter R n)) [Finite ↥Y] (F : IntermediateField ℚ K) [IsCyclotomicExtension {m} ℚ ↥F] (hmn : m ∣ n) : (IsCyclotomicExtension.Rat.intermediateFieldEquivSubgroupChar n K R).symm Y ≤ F ↔ Y.dirichletConductor ∣ m

A character subfield of the n-th cyclotomic field lies in its cyclotomic subfield of level m exactly when every character in the group factors through level m, equivalently when the group conductor divides m.