Maps determined by their value on a primitive root

In a domain the n-th roots of unity are exactly the powers of a primitive one, so a monoid endomorphism is pinned down on all of them by its value on a single primitive n-th root: if it raises that root to the j-th power, it raises every n-th root of unity to the j-th power.

The same principle characterises when the cyclotomic character IsPrimitiveRoot.autToPow is trivial: it kills an automorphism exactly when that automorphism fixes the chosen primitive root, because the character records nothing but the power the root is sent to.

Over a normal extension of a field where Φ_n is irreducible, every coprime power of a primitive n-th root is attained by an automorphism. Indeed the two primitive roots have the same cyclotomic minimal polynomial, and normality extends that conjugacy to the ambient field.

Every character of a group of order n takes values whose n-th power is 1; for n = p prime it therefore sends each element outside its kernel to a primitive p-th root of unity.

Multiplying one n-th root of a nonzero a by the powers of a primitive n-th root of unity gives n distinct n-th roots of a, and these are all of them.

If q² is a primitive l-th root of unity, then q^(l(l+1)) = (-1)^(l+1), the sign that appears when quantum binomial coefficients are evaluated at such a q.

Main results

• IsPrimitiveRoot.map_eq_pow: a monoid endomorphism sending a primitive n-th root of unity ζ to ζ ^ j sends every n-th root of unity μ to μ ^ j.
• IsPrimitiveRoot.autToPow_eq_one_iff: the cyclotomic character kills an automorphism exactly when it fixes the chosen primitive root.
• IsPrimitiveRoot.coe_autToPow_eq_natCast_iff: an automorphism has cyclotomic character k exactly when it raises the primitive root to the k-th power.
• IsPrimitiveRoot.cast_autToPow_eq_natCast_iff: modulo a divisor d of the level, the cyclotomic character is read off from the action on a primitive d-th root of unity.
• IsPrimitiveRoot.cast_autToPow_restrictNormalHom_eq: the same for the restriction of an automorphism of an extension field to a normal intermediate field containing the root.
• AlgEquiv.apply_eq_apply_of_abelianization_of_eq: two automorphisms with the same image in the abelianization agree on every root of unity.
• IsPrimitiveRoot.exists_algEquiv_apply_eq_pow_of_coprime: every coprime power of a primitive root in a normal extension is realized by an automorphism if Φ_n is irreducible.
• MonoidHom.apply_pow_eq_one_of_card_eq: a character of a group of order n takes values whose n-th power is 1.
• MonoidHom.isPrimitiveRoot_apply_of_card_eq_prime: a character of a group of prime order p sends every element outside its kernel to a primitive p-th root of unity.
• IsPrimitiveRoot.card_nthRootsFinset_of_pow_eq: in the presence of a primitive n-th root of unity, a nonzero element with one n-th root has exactly n of them.
• IsPrimitiveRoot.pow_mul_add_one_eq_neg_one_pow: if q² is a primitive l-th root of unity with l > 0, then q^(l(l+1)) = (-1)^(l+1).

References

The characterisation of the cyclotomic character's kernel by its value on a chosen primitive root is due to the Birkbeck--Brasca Chebotarev density project, CBirkbeck/chebotarev-density (Apache-2.0).

theorem IsPrimitiveRoot.map_eq_pow {R : Type u} [CommRing R] [IsDomain R] {F : Type u_1} [FunLike F R R] [MonoidHomClass F R R] {n j : ℕ} [NeZero n] {ζ : R} (hζ : IsPrimitiveRoot ζ n) (σ : F) (hσ : σ ζ = ζ ^ j) {μ : R} (hμ : μ ^ n = 1) : σ μ = μ ^ j

A monoid endomorphism that raises one primitive n-th root of unity to the j-th power raises every n-th root of unity to the j-th power, since the n-th roots of unity are exactly the powers of a primitive one.

theorem IsPrimitiveRoot.exists_algEquiv_apply_eq_pow_of_coprime {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [Normal K L] {n j : ℕ} [NeZero n] {ζ : L} (hζ : IsPrimitiveRoot ζ n) (hj : n.Coprime j) (hirr : Irreducible (Polynomial.cyclotomic n K)) : ∃ (σ : Gal(L/K)), σ ζ = ζ ^ j

If Φ_n is irreducible over K, every coprime power of a primitive root in a normal extension is the image of that root under a K-algebra automorphism.

theorem MonoidHom.apply_pow_eq_one_of_card_eq {n : ℕ} {G : Type u_1} {M : Type u_2} [Group G] [Monoid M] (χ : G →* M) (hG : Nat.card G = n) (g : G) : χ g ^ n = 1

A character of a group of order n takes values whose n-th power is 1.

theorem MonoidHom.isPrimitiveRoot_apply_of_card_eq_prime {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} {M : Type u_2} [Group G] [CommMonoid M] (χ : G →* M) (hG : Nat.card G = p) {g : G} (hg : χ g ≠ 1) : IsPrimitiveRoot (χ g) p

A character of a group of prime order p sends every element outside its kernel to a primitive p-th root of unity.

theorem IsPrimitiveRoot.card_nthRootsFinset_of_pow_eq {R : Type u} [CommRing R] [IsDomain R] {n : ℕ} {ζ α a : R} (hζ : IsPrimitiveRoot ζ n) (hα : α ^ n = a) (ha : a ≠ 0) : (Polynomial.nthRootsFinset n a).card = n

If R has a primitive n-th root of unity, then a nonzero a with one n-th root α has exactly n distinct n-th roots, namely α times the n-th roots of unity. This generalizes Mathlib's IsPrimitiveRoot.card_nthRootsFinset from a = 1.

theorem IsPrimitiveRoot.pow_mul_add_one_eq_neg_one_pow {R : Type u} [CommRing R] [IsDomain R] {q : R} {l : ℕ} (hq : IsPrimitiveRoot (q ^ 2) l) (hl : 0 < l) : q ^ (l * (l + 1)) = (-1) ^ (l + 1)

If q² is a primitive l-th root of unity with l > 0, then q^(l(l+1)) = (-1)^(l+1): for even l, q^l = (q²)^(l/2) = -1, while for odd l the exponent l(l+1) is a multiple of 2l.

theorem IsPrimitiveRoot.coe_autToPow_eq_natCast_iff {K : Type u_1} {M : Type u_2} [CommRing K] [CommRing M] [IsDomain M] [Algebra K M] {m : ℕ} [NeZero m] {ζ : M} (hζ : IsPrimitiveRoot ζ m) {x : M ≃ₐ[K] M} {k : ℕ} : ↑((autToPow K hζ) x) = ↑k ↔ x ζ = ζ ^ k

The cyclotomic character from the action on ζ. An automorphism has cyclotomic character k modulo m exactly when it raises the primitive m-th root of unity ζ to the k-th power.

@[simp]

theorem IsPrimitiveRoot.autToPow_eq_one_iff {K : Type u_1} {M : Type u_2} [CommRing K] [CommRing M] [IsDomain M] [Algebra K M] {m : ℕ} [NeZero m] {ζ : M} (hζ : IsPrimitiveRoot ζ m) (x : M ≃ₐ[K] M) : (autToPow K hζ) x = 1 ↔ x ζ = ζ

The cyclotomic character detects fixing ζ. autToPow sends x to 1 exactly when x fixes the chosen primitive root, since autToPow is defined by the power x sends it to.

theorem IsPrimitiveRoot.cast_autToPow_eq_natCast_iff {K : Type u_1} {M : Type u_2} [CommRing K] [CommRing M] [IsDomain M] [Algebra K M] {m d : ℕ} [NeZero m] (hd : d ∣ m) {ζ : M} (hζ : IsPrimitiveRoot ζ m) {x : M ≃ₐ[K] M} {k : ℕ} : (↑((autToPow K hζ) x)).cast = ↑k ↔ x (ζ ^ (m / d)) = (ζ ^ (m / d)) ^ k

The cyclotomic character modulo a divisor. Let d ∣ m. An automorphism has cyclotomic character congruent to k modulo d exactly when it raises the primitive d-th root of unity ζ ^ (m / d) to the k-th power.

theorem IsPrimitiveRoot.cast_autToPow_restrictNormalHom_eq {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {m : ℕ} [NeZero m] {E : IntermediateField K L} [Normal K ↥E] {ζ' : ↥E} (hζ' : IsPrimitiveRoot ζ' m) {d c : ℕ} (hd : d ∣ m) (κ : Gal(L/K)) (hκ : ∀ (t : L), t ^ d = 1 → κ t = t ^ c) : (↑((autToPow K hζ') ((AlgEquiv.restrictNormalHom ↥E) κ))).cast = ↑c

The cyclotomic character of a restriction. Let E be a normal intermediate field of a field extension L / K containing a primitive m-th root of unity ζ', and d ∣ m. If an automorphism κ of L over K raises the d-th roots of unity to the c-th power, then the cyclotomic character of its restriction to E is congruent to c modulo d.

theorem AlgEquiv.apply_eq_apply_of_abelianization_of_eq {K : Type u_1} {M : Type u_2} [CommRing K] [CommRing M] [IsDomain M] [Algebra K M] {σ τ : M ≃ₐ[K] M} (h : Abelianization.of σ = Abelianization.of τ) {n : ℕ} (hn : n ≠ 0) {μ : M} (hμ : μ ^ n = 1) : σ μ = τ μ

Roots of unity only see the abelianization. Two automorphisms with the same image in the abelianization agree on every root of unity: on the roots of unity of order d they act through the commutative group (ZMod d)ˣ (IsPrimitiveRoot.autToPow).