Subfields of F(μ_m) are cut out by their rational cyclotomic part

Let F be a field of characteristic zero and M a subfield of F(μ_m) inside the algebraic closure AlgebraicClosure F. The number field ℚ(μ_m) ∩ M already determines M Galois-theoretically: an element of the absolute Galois group G_F fixing ℚ(μ_m) ∩ M fixes M, so ℚ(μ_m) ∩ M generates M over F. This lets a statement about a subfield of a local cyclotomic extension ℚ_p(μ_m) be proved on a number field, as in the cyclotomic normalization of the local Artin map.

The proof is Galois theory in the finite Galois extension ℚ(μ_m) / ℚ (IntermediateField.apply_eq_self_of_forall_mem_inf), followed by the infinite Galois correspondence for AlgebraicClosure F / F.

Main results

• TauCeti.apply_eq_self_of_forall_mem_adjoin_pow_eq_one: an element of G_F fixing ℚ(μ_m) ∩ M fixes M.
• TauCeti.le_adjoin_inf_of_le_adjoin_pow_eq_one: ℚ(μ_m) ∩ M generates M over F.

theorem TauCeti.apply_eq_self_of_forall_mem_adjoin_pow_eq_one {F : Type u_1} [Field F] [CharZero F] (m : ℕ) [NeZero m] {M : IntermediateField F (AlgebraicClosure F)} (hM : M ≤ IntermediateField.adjoin F {z : AlgebraicClosure F | z ^ m = 1}) (σ : Field.absoluteGaloisGroup F) (hσ : ∀ x ∈ IntermediateField.adjoin ℚ {z : AlgebraicClosure F | z ^ m = 1}, x ∈ M → σ.toRingEquiv x = x) (x : ↥M) : σ.toRingEquiv ↑x = ↑x

Reduction to ℚ(μ_m). Let F be a field of characteristic zero and M a subfield of F(μ_m) inside AlgebraicClosure F. An element σ ∈ G_F that fixes ℚ(μ_m) ∩ M fixes M.

theorem TauCeti.le_adjoin_inf_of_le_adjoin_pow_eq_one {F : Type u_1} [Field F] [CharZero F] (m : ℕ) [NeZero m] {M : IntermediateField F (AlgebraicClosure F)} (hM : M ≤ IntermediateField.adjoin F {z : AlgebraicClosure F | z ^ m = 1}) : M ≤ IntermediateField.adjoin F ↑(IntermediateField.adjoin ℚ {z : AlgebraicClosure F | z ^ m = 1} ⊓ IntermediateField.restrictScalars ℚ M)

ℚ(μ_m) ∩ M generates M over F, for F a field of characteristic zero and M a subfield of F(μ_m) inside AlgebraicClosure F: whatever in G_F fixes ℚ(μ_m) ∩ M fixes M.