Proving the roots of unity in \C are algebraic integers

Stream: new members

[Ryan Smith]

Working on proving that complex characters of a finite group are algebraic integers. Shouldn't be too hard right? Digging around I found some related theorems such as IsPrimitiveRoot.isIntegral (why do we only have this for the primitive roots?).

If we don't have a theorem ready, it should be easy enough to just show that we have a root of X^n - 1 and that is monic? What is the endgame here though? I'd thought of using IsIntegral.of_aeval_monic but I'm not sure that helps since we still need to construct (hx : IsIntegral R ((aeval x) p))?

import Mathlib

universe u

open BigOperators Group ComplexConjugate
open Module Module.End
open Multiset
open Polynomial
open LinearMap

variable {G : Type} [Group G] [Finite G]

theorem root_unity_alg_int (z : ℂ) (hz : z ^ (Nat.card G) = 1) : IsIntegral ℤ z := by
  let p : ℤ[X] := (X : ℤ[X]) ^ (Nat.card G) - 1
  have hpos : 0 < Nat.card G := Nat.card_pos
  have hnez : Nat.card G ≠ 0 := by grind
  have hm : Monic p := monic_X_pow_sub_C (1 : ℤ) hnez
  -- now what... IsIntegral.of_aeval_monic ?  AdjoinRoot.isIntegral_root' ?
  sorry

[Ryan Smith]

(deleted)

[Kenny Lau]

@Ryan Smith you've actually pointed out one of the (in my opinion) bigger flaws that exist: the underlying definition itself is not visible during Loogle search.

In this case, you need to look "under the definition" of IsIntegral and see that it is actually IsIntegralElem which is actually ∃ (p : Polynomial R), p.Monic ∧ Polynomial.eval₂ f x p = 0.

[Kenny Lau]

but even if you didn't know that, you could actually follow the path you were on, which is via IsIntegral.of_aeval_monic, because the result of aeval should be zero, and then you know that zero is integral

[Kenny Lau]

also, please PR this

[Kenny Lau]

I think @Chengyan Hu was doing something similar, you two might need to figure out what to do with the PR

[Chengyan Hu]

Yes it seems like we proved something similar.

[Chengyan Hu]

https://github.com/bourbaki120205/mathlib4/blob/project/Chengyan/Test%20copy%202.lean

[Chengyan Hu]

This is the link toward my previous work.

[Chengyan Hu]

I’m currently on holiday with my family and I’ll PR that as soon as I have time to read that long document

[Ryan Smith]

Thanks for the link, I hope the PR gets approved soon. This is so much shorter and more elegant than what I had.

How does this prove the lemma exactly? It looks like we're using a constructor, obviously we have the monic polynomial that \zeta satisfies as the first argument, and then the second is a proof that polynomials of this type are integral, but how does the third parameter fit in? What are we exact passing arguments to with these brackets?

lemma isIntegral_of_roots {n : ℕ} (hpos : 0 < n) {ζ : L} (hζ : ζ ^ n = 1) : IsIntegral ℤ ζ :=
  ⟨X ^ n - 1, monic_X_pow_sub_C 1 (Nat.ne_of_lt hpos).symm, by simp [hζ]⟩

[Ruben Van de Velde]

It's the eval_2 condition that Kenny mentions a few messages ago

[Ruben Van de Velde]

The brackets contain first the witness for the Exists and then the two proofs for each side of the And

[Ryan Smith]

I see, and the constructor separated out the And clause so we end up with three arguments.

[Ryan Smith]

One code question I've had for a while about arguments. This snippet now runs (yes!) but I find myself sometimes writing very long have blocks which I only ever use once and then throw away, like the way we do it here.

Is there a way to combine my last two statements (have and exact) together? It's not important for the correctness of this theorem but there's a lot of short hand in mathlib so I'm trying to understand.

theorem char_value_is_integral (V : FDRep ℂ G) (g : G) : IsIntegral ℤ (V.character g) := by
  rcases exists_char_eigenvalue_ms V g with ⟨s, hs⟩
  rw [char_eq_eigenvalue_ms_sum V g s hs]
  let f : ℂ × ℕ → ℂ := fun t ↦ t.1
  have : ∀ t ∈ s.toEnumFinset, IsIntegral ℤ (f t) := by
    rintro ⟨μ, n⟩ hμ
    have heig : HasEigenvalue (V.ρ g) μ := mem_eigen_ms_eigenvalue g s hs μ (Multiset.mem_of_mem_toEnumFinset hμ)
    have hrunity : μ ^ Nat.card G = 1 := eigenvalue_root_unity V g μ heig
    have hpos : 0 < Nat.card G := Nat.card_pos
    exact isIntegral_of_roots hpos hrunity
  exact IsIntegral.sum f this

[Lawrence Wu (llllvvuu)]

It's hard to say because there's no #mwe, but probably you can do something like

theorem char_value_is_integral (V : FDRep ℂ G) (g : G) : IsIntegral ℤ (V.character g) := by
  rcases exists_char_eigenvalue_ms V g with ⟨s, hs⟩
  rw [char_eq_eigenvalue_ms_sum V g s hs]
  apply IsIntegral.sum
  rintro ⟨μ, n⟩ hμ
  apply isIntegral_of_roots
  . exact Nat.card_pos
  . apply eigenvalue_root_unity
    apply mem_eigen_ms_eigenvalue

I don't think there's anything wrong with the original style though.

[Ryan Smith]

That's interesting, you can apply a function without specifying the arguments and they become goals?

[Lawrence Wu (llllvvuu)]

yes, and check out refine for a more flexible alternative

[Ryan Smith]

That's really neat, when I read about refine before it made no sense at all tbh but that's really useful. One webpage describes it as "exact with holes" which makes a lot of sense

[Rado Kirov]

One other trick that can be useful is using the short-hand anonymous function syntax (no idea if that is what it is called in lean), if you need to provide some args but let move the rest into goals, e.g. if f needs 5 args apply (f x . y . z) will provide 3 and leave the other two. But again refine f x ?_ y ?_ z is probably more ideomatic.

[Ryan Smith]

Thanks, these sort of "deferred arguments" make it easier to avoid defining stuff I'll never use again.