The fibres of u ↦ u ^ m are the orbits of the m-th roots of unity

In a commutative group with zero M (for instance a field), the group rootsOfUnity m M acts on M by multiplication. For m ≠ 0, two elements have the same m-th power exactly when they lie in the same orbit: if u ^ m = v ^ m with u ≠ 0 then v / u is an m-th root of unity, and if u = 0 then v = 0 as well. So the map u ↦ u ^ m identifies the orbit set of this action with the set of m-th powers.

The action is free away from 0, whose stabilizer is the whole roots-of-unity group. This is the algebraic half of the local model u ↦ u ^ m for the quotient of a disc by a finite rotation group: the orbit map of the rotation action is the power map.

Main declarations

• rootsOfUnity.smul_eq_mul: an m-th root of unity acts by multiplication.
• rootsOfUnity.smul_pow: multiplication by an m-th root of unity preserves m-th powers.
• TauCeti.pow_eq_pow_iff_exists_rootsOfUnity_smul: u ^ m = v ^ m iff v = ζ • u for some ζ in rootsOfUnity m M.
• TauCeti.orbitRel_rootsOfUnity_apply: the orbit relation of the action is the kernel of u ↦ u ^ m.
• TauCeti.preimage_image_pow_eq: an invariant set is saturated for u ↦ u ^ m.
• TauCeti.stabilizer_rootsOfUnity_of_ne_zero, TauCeti.stabilizer_rootsOfUnity_zero: the stabilizer is trivial away from 0 and everything at 0.

theorem rootsOfUnity.smul_eq_mul {M : Type u_1} {m : ℕ} [CommMonoid M] (ζ : ↥(rootsOfUnity m M)) (u : M) : ζ • u = ↑↑ζ * u

An m-th root of unity acts on M by multiplication with its underlying element.

@[simp]

theorem rootsOfUnity.smul_pow {M : Type u_1} {m : ℕ} [CommMonoid M] (ζ : ↥(rootsOfUnity m M)) (u : M) : (ζ • u) ^ m = u ^ m

Multiplication by an m-th root of unity does not change the m-th power.

theorem TauCeti.pow_eq_pow_iff_exists_rootsOfUnity_smul {M : Type u_1} {m : ℕ} [CommGroupWithZero M] (hm : m ≠ 0) {u v : M} : u ^ m = v ^ m ↔ ∃ (ζ : ↥(rootsOfUnity m M)), ζ • u = v

For m ≠ 0, two elements have the same m-th power exactly when one is obtained from the other by multiplication with an m-th root of unity.

@[simp]

theorem TauCeti.orbitRel_rootsOfUnity_apply {M : Type u_1} {m : ℕ} [CommGroupWithZero M] (hm : m ≠ 0) {u v : M} : (MulAction.orbitRel (↥(rootsOfUnity m M)) M) u v ↔ u ^ m = v ^ m

For m ≠ 0, the orbit relation of the m-th roots of unity acting by multiplication is the relation of having the same m-th power.

theorem TauCeti.preimage_image_pow_eq {M : Type u_1} {m : ℕ} [CommGroupWithZero M] (hm : m ≠ 0) (s : SubMulAction (↥(rootsOfUnity m M)) M) : (fun (x : M) => x ^ m) ⁻¹' (fun (x : M) => x ^ m) '' ↑s = ↑s

For m ≠ 0, a set invariant under the m-th roots of unity is the full preimage of its image under u ↦ u ^ m.

@[simp]

theorem TauCeti.stabilizer_rootsOfUnity_of_ne_zero {M : Type u_1} {m : ℕ} [CommMonoidWithZero M] [IsRightCancelMulZero M] {u : M} (hu : u ≠ 0) : MulAction.stabilizer (↥(rootsOfUnity m M)) u = ⊥

Multiplication by the m-th roots of unity is free away from 0.

@[simp]

theorem TauCeti.stabilizer_rootsOfUnity_zero {M : Type u_1} {m : ℕ} [CommMonoidWithZero M] : MulAction.stabilizer (↥(rootsOfUnity m M)) 0 = ⊤

Every m-th root of unity fixes 0.