Order and cyclicity of a cyclotomic Galois group, and embeddings of cyclotomic extensions

For an n-th cyclotomic extension L / K whose cyclotomic polynomial Φ_n is irreducible over K, the Galois group has exactly φ n elements. Over any base, the Galois group embeds in the unit group (ZMod n)ˣ through the action on a primitive n-th root of unity, so it is cyclic whenever (ZMod n)ˣ is — for instance whenever n is a power of an odd prime. When Φ_n is irreducible, a primitive n-th root of unity in L is sent to any primitive n-th root of unity in a domain containing K by exactly one K-algebra map.

Main results

• IsCyclotomicExtension.card_aut_eq_totient: #Gal(L / K) = φ n when Φ_n is irreducible.
• IsCyclotomicExtension.isCyclic_aut: the group is cyclic when (ZMod n)ˣ is.
• IsPrimitiveRoot.existsUnique_algHom_apply_eq: exactly one K-algebra map sends a given primitive root to any other when Φ_n is irreducible.

Implementation notes

Nat.card is used rather than Fintype.card so that no finiteness instance is demanded of the caller; the finiteness is supplied locally (irreducibility of Φ_n forces n ≠ 0).

References

The Birkbeck--Brasca Chebotarev development, CBirkbeck/chebotarev-density (Apache-2.0), performs the φ n count inline over ℚ on branch development at commit 8575c9df1ae0a61120ab5c964c7911414254bec7. In CebotarevDensity/Main.lean it sets E := IsCyclotomicExtension.autEquivPow L hirr and rewrites with Nat.card_congr E.toEquiv, Nat.card_eq_fintype_card and ZMod.card_units_eq_totient, as a step inside the consumer of chebotarev_cyclotomic rather than as a named result. card_aut_eq_totient is that step named and stated over an arbitrary base field. isCyclic_aut does not appear in the source.

theorem IsCyclotomicExtension.card_aut_eq_totient {n : ℕ} (K : Type u_1) [Field K] (L : Type u_2) [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] (h : Irreducible (Polynomial.cyclotomic n K)) : Nat.card (L ≃ₐ[K] L) = n.totient

The order of a cyclotomic Galois group. If Φ_n is irreducible over K then the Galois group of an n-th cyclotomic extension of K has exactly φ n elements.

At a prime q this reads q - 1, via Nat.totient_prime.

theorem IsCyclotomicExtension.isCyclic_aut {n : ℕ} (K : Type u_1) [Field K] (L : Type u_2) [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] [IsCyclic (ZMod n)ˣ] : IsCyclic (L ≃ₐ[K] L)

A cyclotomic Galois group is cyclic when the unit group is. The hypothesis holds at every power of an odd prime, where it is ZMod.isCyclic_units_of_prime_pow.

theorem IsPrimitiveRoot.existsUnique_algHom_apply_eq {n : ℕ} {K : Type u_1} [Field K] {L : Type u_2} [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] {ζ : L} (hζ : IsPrimitiveRoot ζ n) (hirr : Irreducible (Polynomial.cyclotomic n K)) {C : Type u_3} [CommRing C] [IsDomain C] [Algebra K C] {ω : C} (hω : IsPrimitiveRoot ω n) : ∃! ι : L →ₐ[K] C, ι ζ = ω

If Φ_n is irreducible over K, a primitive n-th root of unity in an n-th cyclotomic extension of K is sent to any given primitive n-th root of unity in a domain containing K by exactly one K-algebra map.