Cyclotomic units.

We gather miscellaneous results about units given by sums of powers of roots of unit, the so-called cyclotomic units.

Main results

• IsPrimitiveRoot.associated_sub_one_pow_sub_one_of_coprime : given an n-th primitive root of unity ζ, we have that ζ - 1 and ζ ^ j - 1 are associated for all j coprime with n.
• IsPrimitiveRoot.associated_pow_sub_one_pow_of_coprime : given an n-th primitive root of unity ζ, we have that ζ ^ i - 1 and ζ ^ j - 1 are associated for all i and j coprime with n.
• IsPrimitiveRoot.associated_pow_add_sub_sub_one : given an n-th primitive root of unity ζ, where 2 ≤ n, we have that ζ - 1 and ζ ^ (i + j) - ζ ^ i are associated for all and j coprime with n and all i.

Implementation details

We sometimes state series of results of the form a = u * b, IsUnit u and Associated a b. Often, Associated a b is everything one needs, and it is more convenient to use, we include the other version for completeness.

theorem IsPrimitiveRoot.associated_sub_one_pow_sub_one_of_coprime {n j : ℕ} {A : Type u_1} {ζ : A} [CommRing A] [IsDomain A] (hζ : IsPrimitiveRoot ζ n) (hj : j.Coprime n) : Associated (ζ - 1) (ζ ^ j - 1)

Given an n-th primitive root of unity ζ, we have that ζ - 1 and ζ ^ j - 1 are associated for all j coprime with n. pow_sub_one_mul_geom_sum_eq_pow_sub_one_mul_geom_sum gives an explicit formula for the unit.

theorem IsPrimitiveRoot.associated_pow_sub_one_pow_of_coprime {n i j : ℕ} {A : Type u_1} {ζ : A} [CommRing A] [IsDomain A] (hζ : IsPrimitiveRoot ζ n) (hi : i.Coprime n) (hj : j.Coprime n) : Associated (ζ ^ j - 1) (ζ ^ i - 1)

Given an n-th primitive root of unity ζ, we have that ζ ^ j - 1 and ζ ^ i - 1 are associated for all i and j coprime with n.

theorem IsPrimitiveRoot.associated_sub_one_map_sub_one {A : Type u_1} {ζ : A} [CommRing A] [IsDomain A] {R : Type u_3} [CommRing R] [Algebra R A] {n : ℕ} [NeZero n] (hζ : IsPrimitiveRoot ζ n) (σ : A ≃ₐ[R] A) : Associated (ζ - 1) (σ (ζ - 1))

Given an n-th primitive root of unity ζ, we have that ζ - 1 is associated to any of its conjugate.

theorem IsPrimitiveRoot.associated_map_sub_one_map_sub_one {A : Type u_1} {ζ : A} [CommRing A] [IsDomain A] {R : Type u_3} [CommRing R] [Algebra R A] {n : ℕ} [NeZero n] (hζ : IsPrimitiveRoot ζ n) (σ τ : A ≃ₐ[R] A) : Associated (σ (ζ - 1)) (τ (ζ - 1))

Given an n-th primitive root of unity ζ, we have that two conjugates of ζ - 1 are associated.

theorem IsPrimitiveRoot.geom_sum_isUnit {n j : ℕ} {A : Type u_1} {ζ : A} [CommRing A] [IsDomain A] (hζ : IsPrimitiveRoot ζ n) (hn : 2 ≤ n) (hj : j.Coprime n) : IsUnit (∑ i ∈ Finset.range j, ζ ^ i)

Given an n-th primitive root of unity ζ, where 2 ≤ n, we have that ∑ i ∈ range j, ζ ^ i is a unit for all j coprime with n. This is the unit given by associated_pow_sub_one_pow_of_coprime (see pow_sub_one_mul_geom_sum_eq_pow_sub_one_mul_geom_sum).

theorem IsPrimitiveRoot.geom_sum_isUnit' {n j : ℕ} {A : Type u_1} {ζ : A} [CommRing A] [IsDomain A] (hζ : IsPrimitiveRoot ζ n) (hj : j.Coprime n) (hj_Unit : IsUnit ↑j) : IsUnit (∑ i ∈ Finset.range j, ζ ^ i)

Similar to geom_sum_isUnit, but instead of assuming 2 ≤ n we assume that j is a unit in A.

theorem IsPrimitiveRoot.pow_sub_one_mul_geom_sum_eq_pow_sub_one_mul_geom_sum {n i j : ℕ} {A : Type u_1} {ζ : A} [CommRing A] [IsDomain A] (hζ : IsPrimitiveRoot ζ n) (hn : 2 ≤ n) : (ζ ^ j - 1) * ∑ k ∈ Finset.range i, ζ ^ k = (ζ ^ i - 1) * ∑ k ∈ Finset.range j, ζ ^ k

The explicit formula for the unit whose existence is the content of associated_pow_sub_one_pow_of_coprime.

theorem IsPrimitiveRoot.pow_sub_one_eq_geom_sum_mul_geom_sum_inv_mul_pow_sub_one {n i j : ℕ} {A : Type u_1} {ζ : A} [CommRing A] [IsDomain A] (hζ : IsPrimitiveRoot ζ n) (hn : 2 ≤ n) (hi : i.Coprime n) (hj : j.Coprime n) : ζ ^ j - 1 = ↑⋯.unit * ↑⋯.unit⁻¹ * (ζ ^ i - 1)

theorem IsPrimitiveRoot.associated_pow_add_sub_sub_one {n j : ℕ} {A : Type u_1} {ζ : A} [CommRing A] [IsDomain A] (hζ : IsPrimitiveRoot ζ n) (hn : 2 ≤ n) (i : ℕ) (hjn : j.Coprime n) : Associated (ζ - 1) (ζ ^ (i + j) - ζ ^ i)

Given an n-th primitive root of unity ζ, where 2 ≤ n, we have that ζ - 1 and ζ ^ (i + j) - ζ ^ i are associated for all and j coprime with n and all i. See pow_sub_one_eq_geom_sum_mul_geom_sum_inv_mul_pow_sub_one for the explicit formula of the unit.

theorem IsPrimitiveRoot.ntRootsFinset_pairwise_associated_sub_one_sub_of_prime {p : ℕ} {A : Type u_1} {ζ : A} [CommRing A] [IsDomain A] (hζ : IsPrimitiveRoot ζ p) (hp : Nat.Prime p) : (↑(Polynomial.nthRootsFinset p 1)).Pairwise fun (η₁ η₂ : A) => Associated (ζ - 1) (η₁ - η₂)

If p is prime and ζ is a p-th primitive root of unit, then ζ - 1 and η₁ - η₂ are associated for all distincts p-th root of unit η₁ and η₂.