The fixed field of a subgroup meeting the cyclotomic fixers trivially

If M contains a primitive m-th root of unity and a subgroup H ≤ Gal(M/K) meets Gal(M/K(μ_m)) trivially, then M is an m-th cyclotomic extension of the fixed field M ^ H.

Only M / K is assumed finite and Galois. The root of unity enters as a hypothesis rather than through an ambient cyclotomic tower, so no separately quantified intermediate field or cyclotomic tower appears among the arguments — the fixed field itself is of course an IntermediateField K M, being the base of the conclusion.

Nothing here needs H to be cyclic. The Chebotarev application takes H = Subgroup.zpowers (σ, τ), but the argument is the Galois correspondence and uses neither a generator nor cyclicity.

Main results

• IsPrimitiveRoot.fixedField_isCyclotomicExtension_of_inf_fixingSubgroup_eq_bot

Provenance

The proof is adapted from the private compositum_isCyclotomic_over_fixedField in CebotarevDensity/Abelian.lean of CBirkbeck/chebotarev-density (Apache-2.0, Birkbeck--Brasca) at commit 8575c9df1ae0a61120ab5c964c7911414254bec7. That version is stated for a cyclic subgroup over a tower K ⊆ L ⊆ M of number fields; the hypotheses here are weaker.

theorem IsPrimitiveRoot.fixedField_isCyclotomicExtension_of_inf_fixingSubgroup_eq_bot {K : Type u_1} {M : Type u_2} [Field K] [Field M] [Algebra K M] [FiniteDimensional K M] [IsGalois K M] {m : ℕ} [NeZero m] {ζ : M} (hζ : IsPrimitiveRoot ζ m) (H : Subgroup Gal(M/K)) (hmeet : H ⊓ (IntermediateField.adjoin K {b : M | b ^ m = 1}).fixingSubgroup = ⊥) : IsCyclotomicExtension {m} (↥(IntermediateField.fixedField H)) M

The fixed field of H carries the cyclotomic extension, whenever H meets the fixers of K(μ_m) trivially.

The trivial meet says exactly that M ^ H and K(μ_m) generate M, so adjoining a primitive root to M ^ H recovers all of M.