The automorphisms fixing the roots of unity

The K-automorphisms of M fixing K(μ_m) pointwise are exactly the kernel of the cyclotomic character IsPrimitiveRoot.autToPow. No Galois, normality or separability hypothesis is needed — only that M contains a primitive m-th root of unity — although when M / K is Galois this subgroup is Gal(M/K(μ_m)), which is the reading the crossing argument uses.

Without a primitive root, the same subgroup is the kernel of the action of Aut(M/K) on the group μ_m(M). The index divides φ(#μ_m(M)) for every m: if μ_m(M) is finite it is cyclic, and φ(#μ_m(M)) is the order of its automorphism group; otherwise #μ_m(M) = 0 and φ 0 = 0. For a prime p this index is prime to p: adjoining the p-th roots of unity is a step of degree prime to p, the reduction step in the Kummer-theoretic proofs of class field theory.

Main results

• IsPrimitiveRoot.fixingSubgroup_adjoin_nth_roots_eq_ker_autToPow
• IsPrimitiveRoot.isOpen_ker_autToPow, IsPrimitiveRoot.isOpen_ker_comp_autToPow: the kernel of the cyclotomic character, and of every additive character read on it, is open in the Krull topology.
• IntermediateField.fixingSubgroup_adjoin_nth_roots_eq_ker: the fixers of K(μ_m) are the automorphisms acting trivially on μ_m(M).
• IntermediateField.index_fixingSubgroup_adjoin_nth_roots_dvd_totient: their index divides φ(#μ_m(M)).
• IntermediateField.coprime_index_fixingSubgroup_adjoin_nth_roots: for a prime p, their index is prime to p.

References

The identification of Gal(M/K(μ_m)) with the G × 1 factor of a Galois splitting is due to the Birkbeck--Brasca Chebotarev development, CBirkbeck/chebotarev-density (Apache-2.0).

theorem IsPrimitiveRoot.fixingSubgroup_adjoin_nth_roots_eq_ker_autToPow {K : Type u_1} {M : Type u_2} [Field K] [Field M] [Algebra K M] {m : ℕ} [NeZero m] {ζ : M} (hζ : IsPrimitiveRoot ζ m) : (IntermediateField.adjoin K {b : M | b ^ m = 1}).fixingSubgroup = (autToPow K hζ).ker

The fixers of K(μ_m) are the kernel of the cyclotomic character.

Use it to move between a condition on Gal(M/K(μ_m)) and one on the cyclotomic character, which is the form a Galois splitting presents.

theorem IsPrimitiveRoot.isOpen_ker_autToPow {K : Type u_1} {M : Type u_2} [Field K] [Field M] [Algebra K M] {m : ℕ} [NeZero m] {ζ : M} (hζ : IsPrimitiveRoot ζ m) : IsOpen ↑(autToPow K hζ).ker

The kernel of the cyclotomic character is open in the Krull topology: it fixes the finite extension K(μ_m) = K(ζ).

theorem IsPrimitiveRoot.isOpen_ker_comp_autToPow {K : Type u_1} {M : Type u_2} {A : Type u_3} [Field K] [Field M] [Algebra K M] [AddZeroClass A] {m : ℕ} [NeZero m] {ζ : M} (hζ : IsPrimitiveRoot ζ m) (ψ : Additive (ZMod m)ˣ →+ A) : IsOpen ↑(ψ.comp (MonoidHom.toAdditive (autToPow K hζ))).ker

A character of (ℤ / m)ˣ read on the cyclotomic character has open kernel: its kernel contains the open kernel of the cyclotomic character (IsPrimitiveRoot.isOpen_ker_autToPow). Use it to feed such a character to constructions that require a continuous character of Gal(M/K).

theorem IntermediateField.fixingSubgroup_adjoin_nth_roots_eq_ker {K : Type u_1} {M : Type u_2} [Field K] [Field M] [Algebra K M] (m : ℕ) : (adjoin K {b : M | b ^ m = 1}).fixingSubgroup = (MulDistribMulAction.toMulAut Gal(M/K) ↥(rootsOfUnity m M)).ker

The fixers of K(μ_m) are the automorphisms acting trivially on μ_m(M). Unlike IsPrimitiveRoot.fixingSubgroup_adjoin_nth_roots_eq_ker_autToPow, this needs no primitive root: the action on the group μ_m(M) replaces the cyclotomic character.

theorem IntermediateField.index_fixingSubgroup_adjoin_nth_roots_dvd_totient {K : Type u_1} {M : Type u_2} [Field K] [Field M] [Algebra K M] (m : ℕ) : (adjoin K {b : M | b ^ m = 1}).fixingSubgroup.index ∣ (Nat.card ↥(rootsOfUnity m M)).totient

The index of Aut(M/K(μ_m)) divides φ(#μ_m(M)). When μ_m(M) is finite it is cyclic, and φ(#μ_m(M)) is the order of its automorphism group, through whose action Aut(M/K(μ_m)) is the kernel; otherwise #μ_m(M) = 0 and φ 0 = 0, so the statement holds trivially.

theorem IntermediateField.coprime_index_fixingSubgroup_adjoin_nth_roots {K : Type u_1} {M : Type u_2} [Field K] [Field M] [Algebra K M] {p : ℕ} (hp : Nat.Prime p) : (adjoin K {b : M | b ^ p = 1}).fixingSubgroup.index.Coprime p

Adjoining the p-th roots of unity is a step of degree prime to p: for a prime p, the index of Aut(M/K(μ_p)) in Aut(M/K) is prime to p. It divides φ(#μ_p(M)), and #μ_p(M) ≤ p.