Basic results on roots of unity

This file records a criterion for a root of unity congruent to 1 modulo an ideal to equal 1, and counts the square roots of unity in a domain in which 2 ≠ 0. For a prime p it relates the triviality of the pth roots of unity to the absence of a primitive one. It also records that roots of unity, and hence the values of a character of a finite group, are integral over ℤ.

Main results

• IsOfFinOrder.isIntegral: a finite-order element of a commutative ring is integral over ℤ.

• MonoidHom.isIntegral_coe_apply: the values of a homomorphism from a finite group to the units of a commutative ring are integral over ℤ.

• TauCeti.eq_one_of_pow_eq_one_of_sub_one_mem: in a commutative ring without zero divisors, a root of unity that is congruent to 1 modulo an ideal not containing its order is 1.

• TauCeti.card_rootsOfUnity_two: in a domain in which 2 ≠ 0, the group μ₂ = {±1} has two elements.

• IsPrimitiveRoot.neg_one_of_two_ne_zero: when 2 ≠ 0, -1 is a primitive square root of unity.

• IsPrimitiveRoot.neg_of_odd: when 2 ≠ 0, the negative of a primitive root of unity of odd order n is a primitive 2n-th root of unity.

• TauCeti.rootsOfUnity_eq_bot_iff: for a prime p, the pth roots of unity are trivial exactly when there is no primitive pth root of unity.

• TauCeti.finite_torsionBy_additive_units: the n-torsion of Mˣ, written additively, is finite when the n-th roots of unity are, for instance in a domain for n ≠ 0.

theorem IsOfFinOrder.isIntegral {R : Type u_1} [CommRing R] {x : R} (hx : IsOfFinOrder x) : IsIntegral ℤ x

Every finite-order element of a commutative ring is integral over ℤ.

theorem MonoidHom.isIntegral_coe_apply {R : Type u_1} [CommRing R] {G : Type u_2} [Group G] [Finite G] (χ : G →* Rˣ) (g : G) : IsIntegral ℤ ↑(χ g)

The values of a homomorphism from a finite group to the units of a commutative ring are integral over ℤ.

theorem TauCeti.eq_one_of_pow_eq_one_of_sub_one_mem {R : Type u_1} [CommRing R] [NoZeroDivisors R] {I : Ideal R} {n : ℕ} (hn : ↑n ∉ I) {ζ : R} (hζ : ζ ^ n = 1) (hmem : ζ - 1 ∈ I) : ζ = 1

In a commutative ring without zero divisors, a root of unity that is congruent to 1 modulo an ideal not containing its order is equal to 1.

theorem IsPrimitiveRoot.neg_one_of_two_ne_zero {R : Type u_1} [CommRing R] (h2 : 2 ≠ 0) : IsPrimitiveRoot (-1) 2

In a commutative ring in which 2 ≠ 0, -1 is a primitive square root of unity.

theorem TauCeti.card_rootsOfUnity_two {R : Type u_1} [CommRing R] [IsDomain R] (h2 : 2 ≠ 0) : Nat.card ↥(rootsOfUnity 2 R) = 2

In a domain in which 2 ≠ 0, the group μ₂ = {±1} of square roots of unity has two elements.

theorem IsPrimitiveRoot.neg_of_odd {R : Type u_1} [CommRing R] {ζ : R} {n : ℕ} (hζ : IsPrimitiveRoot ζ n) (hn : Odd n) (h2 : 2 ≠ 0) : IsPrimitiveRoot (-ζ) (2 * n)

In a commutative ring in which 2 ≠ 0, the negative of a primitive n-th root of unity of odd order n is a primitive 2n-th root of unity.

theorem TauCeti.rootsOfUnity_eq_bot_iff {M : Type u_2} [CommMonoid M] {p : ℕ} [Fact (Nat.Prime p)] : rootsOfUnity p M = ⊥ ↔ ¬∃ (ζ : M), IsPrimitiveRoot ζ p

For a prime p, the pth roots of unity of a commutative monoid are trivial exactly when it has no primitive pth root of unity: a pth root of unity other than 1 has order p.

instance TauCeti.finite_torsionBy_additive_units {M : Type u_2} [CommMonoid M] (n : ℕ) [Finite ↥(rootsOfUnity n M)] : Finite ↥(Submodule.torsionBy ℤ (Additive Mˣ) ↑n)

The n-torsion of the unit group of a commutative monoid, written additively, consists of the n-th roots of unity; so it is finite when they are, for instance in a domain for n ≠ 0.