The `n`th cyclotomic field has a prim. `n`th root of unity

Stream: Is there code for X?

[Michael Stoll]

Is there a better way to get the following?

import tactic.basic
import field_theory.is_alg_closed.algebraic_closure
import number_theory.cyclotomic.primitive_roots

lemma exists_primitive_root_of_unity (n : ℕ+) (F : Type) [field F] (h : (n : F) ≠ 0) :
  ∃ ζ : cyclotomic_field n F, is_primitive_root ζ n :=
begin
  set Fcyc := cyclotomic_field n F,
  have hh : (n : Fcyc) ≠ 0 :=
  begin
    intro hf,
    have hf' : (algebra_map F Fcyc) n = (algebra_map F Fcyc) 0,
    { simp only [coe_coe, map_nat_cast, map_zero],
      rw [(by norm_cast : ((n : ℕ) : Fcyc) = n)],
      exact hf, },
    exact h (ring_hom.injective (algebra_map F Fcyc) hf'),
  end,
  haveI h' : ne_zero (n : F) := {out := h},
  haveI hcyc : ne_zero (n : Fcyc) := {out := hh},
  use is_cyclotomic_extension.zeta n F Fcyc,
  exact is_cyclotomic_extension.zeta_primitive_root n F Fcyc,
end

What I find particularly painful here is the need to show that n : Fcyc is nonzero (and the fact that I didn't find a more direct proof).

[Johan Commelin]

That's a question for the FLT-regular people. cc @Riccardo Brasca @Eric Rodriguez @Alex J. Best

[Riccardo Brasca]

We have docs#is_cyclotomic_extension.zeta that is a primitive root of unity.

[Riccardo Brasca]

cyclotomic_field n F should automatically get the is_cyclotomic_extension instnce.

[Riccardo Brasca]

Ah, sorry, you are already using it. Well, then you only need to prove ne_zero ((n : ℕ) : Fcycl), and your proof can probably be golfed a little.

[Riccardo Brasca]

This works, but I suggest to have [ne_zero ...] instead of h as an assumption.

import number_theory.cyclotomic.primitive_roots

lemma exists_primitive_root_of_unity (n : ℕ+) (F : Type) [field F] (h : (n : F) ≠ 0) :
  ∃ ζ : cyclotomic_field n F, is_primitive_root ζ n :=
begin
  haveI : ne_zero (n : F) := ⟨h⟩,
  haveI : ne_zero ((n : ℕ) : (cyclotomic_field n F)) := ne_zero.of_no_zero_smul_divisors F _ n,
  exact ⟨is_cyclotomic_extension.zeta n F _, is_cyclotomic_extension.zeta_primitive_root n F _⟩
end

[Riccardo Brasca]

Note that the ne_zero assumption in docs#cyclotomic_field.is_cyclotomic_extension is probably not necessary. I wanted to remove it last week but I didn't have time. I will do it sooner or later, I promise. (But if you're interested feel free to do it...)

[Eric Rodriguez]

Also take care with zeta-note for example in the ring of integers subring, there is no reason for zeta to be the same as outside.

[Riccardo Brasca]

Yes, it's much better to prove any results for a generic primitive root, and use zeta only if you need to provide an example

[Eric Rodriguez]

Note that the ne_zero assumption in docs#cyclotomic_field.is_cyclotomic_extension is probably not necessary. I wanted to remove it last week but I didn't have time. I will do it sooner or later, I promise. (But if you're interested feel free to do it...)

for details, Michael, see https://leanprover.zulipchat.com/#narrow/stream/304774-FLT-regular/topic/ne_zero.20again

[Michael Stoll]

I've posted a comment in the FLT-regular stream.
You definitely need the ne_zero assumption for the existence of a primitive nth root of unity, which in turn is usually necessary if you want to prove some interesting statements.

[Michael Stoll]

Riccardo Brasca said:

This works, but I suggest to have [ne_zero ...] instead of h as an assumption.
<snip>

Thanks for the shorter proof!
I'll also take your advice and work with generic (primitive) roots of unity as far as possible.

[Michael Stoll]

BTW,

example {M} [monoid M] {x : M} (m n : ℕ) (h : x ^ n = 1) : x ^ m = x ^ (m % n) :=
begin
  nth_rewrite 0 [← nat.div_add_mod m n], rw [pow_add, pow_mul, h, one_pow, one_mul],
end

doesn't seem to exist in this form in mathlib. There are some variants where n is something like the order of x or the order (or exponent) of M, when M is a group, but this is sometimes less useful than the simple statement above.