Existence of primitive roots of unity

Stream: Is there code for X?

[Adam Topaz]

Are we really missing the assertion that there exists a primitive root of unity of order $n$ whenever $n$ is coprime to the characteristic of the field $K$ and the correct polynomial splits in $K$?

[Riccardo Brasca]

I don't think we have a lot of existence statement about primitive roots of unity, but it should be easy using the cyclotomic stuff

[Adam Topaz]

what cyclotomic stuff?

[Riccardo Brasca]

docs#Polynomial.isRoot_cyclotomic_iff says that the roots of the cyclotomic polynomial are precisely the primitive root of unity, so it depends by what you mean with "the correct polynomial"

[Adam Topaz]

Aha that's great!

[Adam Topaz]

[NeZero ↑n] is a funny way of stating the characteristic condition :)

[Riccardo Brasca]

Yeah, I don't remember why it is spelled that way

[Adam Topaz]

I came up with the following:

theorem exists_isPrimitiveRoot {F : Type*} [Field F] [NeZero (n : F)]
    (splits : (cyclotomic n F).Splits (RingHom.id _)) : ∃ ξ : F, IsPrimitiveRoot ξ n := by
  obtain ⟨ξ,h⟩ := exists_root_of_splits _ splits <| by
    rw [Polynomial.degree_cyclotomic]
    norm_cast
    suffices 0 <  n.totient from Nat.pos_iff_ne_zero.mp this
    apply Nat.totient_pos
    exact NeZero.pos_of_neZero_natCast F
  refine ⟨ξ, ?_⟩
  rwa [← isRoot_cyclotomic_iff]

[Riccardo Brasca]

We have docs#Polynomial.degree_cyclotomic_pos to golf it

[Adam Topaz]

BTW, I'm thinking about this now because of some discussion I had with @Qi Ge yesterday about formalizing the cyclotomic character. Another question which should be answered is in what level of generality this should be done.

One approach is to take a so-called "truncation set" $S$ in the sense of big Witt vectors, which does not contain the characteristic of the field, and define a cyclotomic character associated to that. If $S$ is the set of powers of a fixed prime $p$ then this should give the $p$-adic cyclotomic character.

[Adam Topaz]

Do we have the fact that the cyclotomic polynomial is separable under the suitable characteristic assumptions?

[Adam Topaz]

Adam Topaz said:

Do we have the fact that the cyclotomic polynomial is separable under the suitable characteristic assumptions?

I coudn't find it, and came up with the following:

theorem separable_cyclotomic {K : Type*} [Field K] [NeZero (n : K)] :
    (cyclotomic n K).Separable := by
  refine Polynomial.Separable.of_dvd ?_ <| Polynomial.cyclotomic.dvd_X_pow_sub_one n K
  rw [Polynomial.X_pow_sub_one_separable_iff]
  exact NeZero.natCast_ne n K

[Kevin Buzzard]

Note that I have a branch called something like kbuzzard-cyclotomic-character which defines the mod n cyclo char but it broke after the simp refactor in core and fixing it is kind of low priority for me right now because I'm teaching and doing other things until April.

[Kevin Buzzard]

I'll get to a computer and push the partial fixes I have

[Adam Topaz]

@Kevin Buzzard we do have docs#IsPrimitiveRoot.autToPow

[Adam Topaz]

the issue @Qi Ge and I were discussing is in packaging them together as n varies

[Adam Topaz]

Then there's the issue of continuity w.r.t. the profinite topology of the absolute Galois group, but I don't think that would be too hard

[Adam Topaz]

anyway, I have to come back to this later. I pushed the few lemmas I wrote to branch#AT-cyclotomic

[Kevin Buzzard]

Adam Topaz said:

Kevin Buzzard we do have docs#IsPrimitiveRoot.autToPow

Yeah but this is a bit weird because it chooses a root of unity, which you don't have to do.

[Kevin Buzzard]

On the other hand, I did write the file before I had realised that this existed. This is the current status of my code (which I think now compiles with master):

/-
Copyright (c) 2023 Hanneke Wiersema. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kevin Buzzard, Hanneke Wiersema
-/
import Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
import Mathlib.RingTheory.RootsOfUnity.Basic

/-!

# The cyclotomic character

Let `L` be an integral domain and let `n : ℕ+` be a positive integer. If `μₙ` is the
group of `n`th roots of unity in `L` then any field automorphism `g` of `L`
induces an automorphism of `μₙ` which, being a cyclic group, must be of
the form `ζ ↦ ζ^j` for some integer `j = j(g)`, well-defined in `ZMod d`, with
`d` the cardinality of `μₙ`. The function `j` is a group homomorphism
`(L ≃+* L) →* ZMod d`.

Future work: If `L` is separably closed (e.g. algebraically closed) and `p` is a prime
number such that `p ≠ 0` in `L`, then applying the above construction with
`n = p^i` (noting that the size of `μₙ` is `p^i`) gives a compatible collection of
group homomorphisms `(L ≃+* L) →* ZMod (p^i)` which glue to give
a group homomorphism `(L ≃+* L) →* ℤₚ`; this is the `p`-adic cyclotomic character.

## Important definitions

Let `L` be an integral domain, `g : L ≃+* L` and `n : ℕ+`. Let `d` be the number of `n`th roots
of `1` in `L`.

* `ModularCyclotomicCharacter n : L ≃+* L →* ZMod d` sends `g` to the unique `j` such
   that `g(ζ)=ζ^j` for all `ζ : rootsOfUnity n L`.

## Todo

* Prove the compatibility of `ModularCyclotomicCharacter n` and `ModularCyclotomicCharacter m`
if `n ∣ m`.

* Define the cyclotomic character.

* Prove that it's continuous.

## Tags

cyclotomic character
-/

universe u
variable {L : Type u} [CommRing L] [IsDomain L]

/-

## The mod n theory

-/

variable (n : ℕ+)

theorem rootsOfUnity.integer_power_of_ringEquiv (g : L ≃+* L) :
    ∃ m : ℤ, ∀ t : rootsOfUnity n L, g (t : Lˣ) = (t ^ m : Lˣ) := by
  obtain ⟨m, hm⟩ := MonoidHom.map_cyclic (g.restrictRootsOfUnity n).toMonoidHom
  exact ⟨m, fun t ↦ Units.ext_iff.1 <| SetCoe.ext_iff.2 <| hm t⟩

theorem rootsOfUnity.integer_power_of_ringEquiv' (g : L ≃+* L) :
    ∃ m : ℤ, ∀ t ∈ rootsOfUnity n L, g (t : Lˣ) = (t ^ m : Lˣ) := by
  obtain ⟨m, hm⟩ := MonoidHom.map_cyclic (g.restrictRootsOfUnity n).toMonoidHom
  exact ⟨m, fun t ht ↦ Units.ext_iff.1 $ SetCoe.ext_iff.2 (hm ⟨t, ht⟩)⟩

/-- `ModularCyclotomicCharacter_aux g n` is a non-canonical auxiliary integer `j`,
   only well-defined modulo the number of `n`'th roots of unity in `L`, such that `g(ζ)=ζ^j`
   for all `n`'th roots of unity `ζ` in `L`. -/
noncomputable def ModularCyclotomicCharacter_aux (g : L ≃+* L) (n : ℕ+) : ℤ :=
  (rootsOfUnity.integer_power_of_ringEquiv n g).choose

-- the only thing we know about `ModularCyclotomicCharacter_aux g n`
theorem ModularCyclotomicCharacter_aux_spec (g : L ≃+* L) (n : ℕ+) :
    ∀ t : rootsOfUnity n L, g (t : Lˣ) = (t ^ (ModularCyclotomicCharacter_aux g n) : Lˣ) :=
  (rootsOfUnity.integer_power_of_ringEquiv n g).choose_spec

/-- If `g` is a field automorphism of `L`, and `n : ℕ+`, then
  `ModularCyclotomicCharacter.toFun n g` is the `j : ZMod d` such that `g(ζ)=ζ^j` for all
  `n`'th roots of unity. Here `d` is the number of `n`th roots of unity in `L`. -/
noncomputable def ModularCyclotomicCharacter.toFun (n : ℕ+) (g : L ≃+* L) :
    ZMod (Fintype.card (rootsOfUnity n L)) :=
  ModularCyclotomicCharacter_aux g n

-- This appears to be missing from the library. It should not be in this file.
theorem Group.pow_eq_zpow_mod {G : Type _} [Group G] {x : G} (m : ℤ) {n : ℕ} (h : x ^ n = 1) :
    x ^ m = x ^ (m % (n : ℤ)) := by
  have h2 : x ^ m = x ^ ((n : ℤ) * (m / (n : ℤ)) + m % (n : ℤ)) :=
    congr_arg (fun a => x ^ a) ((Int.add_comm _ _).trans (Int.emod_add_ediv _ _)).symm
  simp [h, h2, zpow_add, zpow_mul]

namespace ModularCyclotomicCharacter

local notation "χ" => ModularCyclotomicCharacter.toFun

/-- The formula which characterises the output of `ModularCyclotomicCharacter g n`. -/
theorem spec (g : L ≃+* L) (n : ℕ+) :
    ∀ t : rootsOfUnity n L, g (t : Lˣ) = (t ^ (χ n g).val : Lˣ) := by
  rintro t
  rw [ModularCyclotomicCharacter_aux_spec g n t, ← zpow_ofNat, ModularCyclotomicCharacter.toFun,
    ZMod.val_int_cast, ← Subgroup.coe_zpow]
  exact Units.ext_iff.1 <| SetCoe.ext_iff.2 <| Group.pow_eq_zpow_mod _ pow_card_eq_one

-- this is in the wrong place I guess
lemma ext {G : Type _} [Group G] [Fintype G] [IsCyclic G]
    {d : ℕ} {a b : ZMod d} (hGcard : Fintype.card G = d) (h : ∀ t : G, t^a.val = t^b.val) :
  a = b := by
  obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := G)
  have hgord := orderOf_eq_card_of_forall_mem_zpowers hg
  specialize h g
  rw [pow_eq_pow_iff_modEq, hgord, hGcard, ← ZMod.nat_cast_eq_nat_cast_iff] at h
  subst hGcard
  simpa [ZMod.nat_cast_val, ZMod.cast_id'] using h

lemma id : χ n (RingEquiv.refl L) = 1 := by
  refine ext (G := rootsOfUnity n L) rfl ?_
  intro ζ
  ext
  rw [Subgroup.coe_pow, ← spec]
  have : 1 ≤ Fintype.card { x // x ∈ rootsOfUnity n L } := Fin.size_positive'
  obtain (h | h) := this.lt_or_eq
  · have := Fact.mk h
    simp [ZMod.val_one]
  · have := Fintype.card_le_one_iff_subsingleton.mp h.ge
    obtain rfl : ζ = 1 := Subsingleton.elim ζ 1
    simp

lemma comp (g h : L ≃+* L) : χ n (g * h) =
    χ n g * χ n h := by
  refine ext (G := rootsOfUnity n L) rfl ?_
  intro ζ
  ext
  rw [Subgroup.coe_pow, ← spec]
  change g (h (ζ : Lˣ)) = _
  rw [spec, ← Subgroup.coe_pow, spec, mul_comm, Subgroup.coe_pow, ← pow_mul, ← Subgroup.coe_pow]
  congr 2
  simp only [pow_eq_pow_iff_modEq, ← ZMod.nat_cast_eq_nat_cast_iff, SubmonoidClass.coe_pow,
    ZMod.nat_cast_val, Nat.cast_mul, ZMod.cast_mul (m := orderOf ζ) orderOf_dvd_card]

end ModularCyclotomicCharacter

-- see also `IsPrimitiveRoot.autToPow`, which is the same construction under the more
-- restrictive condition that there exists a primitive n'th root of unity.
/-- Given a positive integer `n`, `ModularCyclotomicCharacter n` is a
multiplicative homomorphism from the automorphisms of a field `L` to `ℤ/dℤ`,
where `d` is the number of `n`'th roots of unity in `L`. It is uniquely
characterised by the property that `g(ζ)=ζ^(ModularCyclotomicCharacter n g)`
for `g` an automorphism of `L` and `ζ` an `n`th root of unity. -/
noncomputable
def ModularCyclotomicCharacter (n : ℕ+) :
    (L ≃+* L) →* (ZMod (Fintype.card { x // x ∈ rootsOfUnity n L }))ˣ := MonoidHom.toHomUnits
  { toFun := ModularCyclotomicCharacter.toFun n
    map_one' := ModularCyclotomicCharacter.id n
    map_mul' := ModularCyclotomicCharacter.comp n }

[Kevin Buzzard]

Now it's compiling again, my next job was going to be to figure out how to adapt it given that I now know about IsPrimitiveRoot.autToPow. Note that this started off as Hanneke Wiersema's project from the Leiden workshop. What I want to be able to do is to state that the determinant of the n-torsion of an elliptic curve is the mod n cyclo char but we are way way off this (we don't even know that the n-torsion is a finite object, and to define the Weil pairing we will probably need some form of Riemann-Roch for elliptic curves)

[Adam Topaz]

BTW, why is this our definition of the abs gal group?

def absoluteGaloisGroup := AlgebraicClosure K ≃ₐ[K] AlgebraicClosure K

as opposed to using the separable closure?

[Kevin Buzzard]

They're the same thing, right?

[Kevin Buzzard]

So perhaps the answer is "the separable closure did not exist at that time"

[Adam Topaz]

Yeah, sure, but the Galois correspondence is wonky

[Kevin Buzzard]

We don't have the galois correspondence for infinite extensions so this is not yet an issue

[Adam Topaz]

I.e. the fixed fields of the algebraic closure will be the perfect closures of the corresponding extensions of k

[Kevin Buzzard]

Yeah the definition sounds like a terrible idea now we actually have some theory of separable extensions.

[Kevin Buzzard]

The other issue is that should we really be choosing a geometric point anyway? But this is a separate discussion. I still don't have a clear idea how we're doing to do Frobenius elements -- one wacky idea I had was to literally choose an element of the absolute Galois group and call it Frob_P and then have an IsFrobenius P g which is true iff g is conjugate to an element which differs from Frob_P by an element of the equally noncanonical inertia subgroup.

[Kevin Buzzard]

Because I want to talk about traces of Frobenius on Galois reps without jumping through hoops

[Adam Topaz]

If you work in $Prof_{out}$ then there’s no issue!

[Kevin Buzzard]

There's still the inertia group issue -- am I allowed to take the trace of Frobenius at a ramified extension?

[Adam Topaz]

@Kevin Buzzard In case it helps, the branch mentioned above now has a sorry-free proof of the following:

theorem exists_isPrimitiveRoot_of_isSepClosed (n : ℕ) [IsSepClosed K] [NeZero (n : K)] :
    ∃ (ξ : K), IsPrimitiveRoot ξ n := ...

noncomputable
def cyclotomicCharacter (n : ℕ+) [IsSepClosure k K] [NeZero (n : K)] :
    (K ≃ₐ[k] K) →* (ZMod n)ˣ := ...

lemma cyclotomicCharacter_spec (n : ℕ+) [IsSepClosure k K] [NeZero (n : K)]
    (ξ : Kˣ) (hξ : ξ ∈ rootsOfUnity n K) (σ : (K ≃ₐ[k] K)) :
    ξ ^ (cyclotomicCharacter k K n σ : ZMod n).val = σ ξ := ...

lemma cyclotomicCharacter_unique (n : ℕ+) [IsSepClosure k K] [NeZero (n : K)]
    (χ : (K ≃ₐ[k] K) →* (ZMod n)ˣ)
    (hχ : ∀ (ξ : Kˣ) (_ : ξ ∈ rootsOfUnity n K) (σ : (K ≃ₐ[k] K)),
      ξ ^ (χ σ : ZMod n).val = σ ξ) :
    χ = cyclotomicCharacter k K n := ...

[Adam Topaz]

But it still needs a bit of cleanup before I open a PR

[Adam Topaz]

With those and the (seemingly nonexistent) obvious morphisms $(\Z/n)^\times \to (\Z/m)^\times$ when $m$ divides $n$, it should be easy to show compatibility and take limits

[Michael Stoll]

Use docs#Units.map and the underlying ring hom?

[Adam Topaz]

the underlying ring hom seems to be missing!

[Adam Topaz]

If you know otherwise, then I would love an answer here: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/ZMod.2Elift.20for.20ring.20homs/near/413234717 :)

[Eric Rodriguez]

I thought monnet did infinite galois?

[Kevin Buzzard]

Just the definition of the topology, so we could state the correspondence. The proof is pretty hairy IIRC

[Kevin Buzzard]

You would imagine it all "just follows by taking the limit of the finite case" but I'm not sure I ever figured out a satisfactory one line translation of this