Adjoining a primitive root of unity adjoins all of them

The n-th roots of unity in a domain are exactly the powers of a primitive one, so adjoining a single primitive n-th root of unity already produces a subalgebra containing every n-th root of unity. For a field extension, the same holds for the generated intermediate field. The additive retraction from ℤ[ζ] to ℤ lets cyclotomic coefficients descend to integral coefficients in induction arguments.

Main results

• IsPrimitiveRoot.mem_algebraAdjoin_of_pow_eq_one: an n-th root of unity lies in the subalgebra generated by a primitive n-th root of unity.
• IsPrimitiveRoot.mem_adjoin_of_pow_eq_one: the analogous intermediate-field statement.
• IsPrimitiveRoot.adjoin_eq_top_of_natCard_sub_one: a primitive (q - 1)-st root of unity of a finite field with q elements generates it as an algebra.
• IsPrimitiveRoot.exists_additive_retraction: the subalgebra generated by a primitive root of unity retracts additively onto ℤ.

theorem IsPrimitiveRoot.mem_algebraAdjoin_of_pow_eq_one {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommRing S] [IsDomain S] [Algebra R S] {n : ℕ} [NeZero n] {ζ : S} (hζ : IsPrimitiveRoot ζ n) {μ : S} (hμ : μ ^ n = 1) : μ ∈ R[ζ]

Every n-th root of unity in a domain lies in the subalgebra generated by a primitive n-th root of unity, being one of its powers.

theorem IsPrimitiveRoot.adjoin_eq_top_of_natCard_sub_one {R : Type u_1} {F : Type u_2} [CommSemiring R] [Field F] [Finite F] [Algebra R F] {ζ : F} (hζ : IsPrimitiveRoot ζ (Nat.card F - 1)) : R[ζ] = ⊤

A primitive (q - 1)-st root of unity generates a finite field with q elements, as an algebra over any commutative semiring: every nonzero element is one of its powers.

theorem IsPrimitiveRoot.exists_additive_retraction {S : Type u_1} [CommRing S] [IsDomain S] [CharZero S] {n : ℕ} [NeZero n] {ζ : S} (hζ : IsPrimitiveRoot ζ n) : ∃ (t : ↥ℤ[ζ] →+ ℤ), t 1 = 1

The subalgebra generated by a primitive n-th root of unity in a characteristic-zero domain admits an additive retraction onto ℤ that sends 1 to 1.

theorem IsPrimitiveRoot.mem_adjoin_of_pow_eq_one {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] {n : ℕ} [NeZero n] {ζ : K} (hζ : IsPrimitiveRoot ζ n) {μ : K} (hμ : μ ^ n = 1) : μ ∈ F⟮ζ⟯

Every n-th root of unity of a field extension K of F lies in the intermediate field generated over F by a primitive n-th root of unity, being one of its powers.