Complex roots of unity as a finset

Stream: Is there code for X?

[Eric Wieser]

Do we have a result that expresses the nth roots of unity as exp (2 * π * I * (↑(i : ℕ) / n) over the obvious choice of i?

docs#complex.mem_roots_of_unity is obviously close, but I want it as an equality of finsets.

My attempt was:

import analysis.complex.roots_of_unity

namespace complex

open_locale real

lemma exp_two_pi_mul_div_inj_on (n : ℕ+):
  (set.Iio (n : ℕ)).inj_on (λ i, exp (2 * π * I * (↑(i : ℕ) / n))) :=
λ i (hi : i < n) j (hj : j < n) h, begin
  dsimp at h,
  simp_rw [exp_eq_exp_iff_exists_int, mul_comm _ (2 * ↑π * I), ←mul_add] at h,
  obtain ⟨k, h⟩ := h,
  rw mul_right_inj' at h,
  field_simp at h,
  norm_cast at h,
  obtain ⟨_ | k, hk⟩ := int.eq_coe_or_neg k,
  { simp * at * },
  exfalso,
  obtain ⟨rfl | rfl⟩ := hk,
  { rw hk at h,
    norm_cast at h,
    rw [nat.succ_mul, ←add_assoc] at h,
    subst h,
    apply hi.not_le,
    apply self_le_add_left },
  { rw [hk, neg_mul, ←sub_eq_add_neg, eq_sub_iff_add_eq] at h,
    norm_cast at h,
    rw [nat.succ_mul, ←add_assoc] at h,
    subst h,
    apply hj.not_le,
    apply self_le_add_left },
  norm_num [real.pi_ne_zero, complex.ext_iff],
end

/-- The nth roots of `1 : ℂ` are all of the form `exp (2 * π * I * (↑(i : ℕ) / n)` -/
lemma roots_of_unity_to_finset (n : ℕ+) :
  (polynomial.nth_roots_finset n ℂ) =
    (finset.univ : finset (fin n)).map
      ⟨λ i, exp (2 * π * I * (↑(i : ℕ) / n)),
        λ i j h, fin.ext $ exp_two_pi_mul_div_inj_on n i.prop j.prop h⟩ :=
begin
  ext,
  simp only [fin.exists_iff, polynomial.mem_nth_roots_finset, pnat.pos, finset.mem_map,
    finset.mem_univ, function.embedding.coe_fn_mk, exists_true_left, fin.coe_mk],
  by_cases ha : a = 0,
  { simp [ha, exp_ne_zero] },
  lift a to ℂˣ using (is_unit.mk0 _ ha),
  rw [←complex.mem_roots_of_unity n a, _root_.mem_roots_of_unity,
    ←units.coe_pow, units.coe_eq_one],
end

end complex

Is there a faster way to get there via docs#is_cyclic and showing that exp (2 * π * I / n) is the generator of the group?

[Junyan Xu]

If you use docs#finset.image you don't have to prove it's injective right? We also have docs#pow_injective_of_lt_order_of but you need to first show that the order_of exp(2πI/n) is n.

[Johan Commelin]

Hasn't that been done yet???

[Junyan Xu]

Actually I think docs#is_primitive_root can simply be defined to be order_of ζ = k.

[Johan Commelin]

I don't remember, but I think I used stuff like that when I did things with Chebyshev polynomials. Those things have later been generalised. So maybe those ingredients didn't survive. But the bare result about e ^ (2pi i / n) is probably still there.

[Junyan Xu]

Indeed we have docs#is_primitive_root.not_iff but not the version without not on both sides ... but you may use docs#is_primitive_root.eq_order_of for the direction you want.

[Eric Rodriguez]

there's also docs#is_primitive_root.unique somewhere

[Eric Rodriguez]

oh that different nvm

[Eric Rodriguez]

docs#is_primitive_root.order_of

[Yaël Dillies]

At least, its proof through the order_of spelling would be much shorter.

[Eric Wieser]

If you use docs#finset.image you don't have to prove it's injective right?

Sure, but then you end up needing to prove it's injective downstream if you want to talk about finset.sum or similar

[Junyan Xu]

Indeed and I think the problem arises earlier, because finset.image requires decidable_eq ℂ. But if you're satisfied with a multiset then multiset.map should be good enough.

[Yaël Dillies]

Surely we have that as a (noncomputable) instance?

[Junyan Xu]

docs#complex.decidable_eq :exploding_head:

[Eric Wieser]

image would be easier, but only because it puts off proving other helpful results. But both would work here

[Eric Wieser]

Thanks for the suggestions @Junyan Xu , this is certainly better:

lemma exp_two_pi_mul_div_inj_on (n : ℕ):
  (set.Iio (n : ℕ)).inj_on (λ i, exp (2 * π * I * (↑(i : ℕ) / n))) :=
λ i (hi : i < n) j (hj : j < n) h, begin
  have : order_of (units.mk0 (exp (2 * π * I / n)) (exp_ne_zero _)) = n,
  { rw [←order_of_units, units.coe_mk0],
    refine (is_primitive_root_exp _ $ ne_zero_of_lt hi).eq_order_of.symm },
  refine pow_injective_of_lt_order_of _ (hi.trans_eq this.symm) (hj.trans_eq this.symm) _,
  ext1,
  simp_rw [units.coe_pow, units.coe_mk0],
  simp_rw [←exp_nat_mul, mul_comm (i : ℂ), mul_comm (j : ℂ),
    div_eq_mul_inv, mul_right_comm _ (n⁻¹ : ℂ) _, mul_assoc _ _ (n⁻¹ : ℂ), ←div_eq_mul_inv],
  exact h,
end

[Eric Rodriguez]

shouldn't there be glue between nth_roots_finset and roots_of_unity.to_finset?

[Eric Wieser]

docs#roots_of_unity.fintype already exists, but I don't think you can use to_finset in a sensible way