Weyl group is finite

Stream: new members

[Phillip Harris]

Assuming the root system itself is finite, how can I get a Fintype instance for the Weyl group, so I can sum over it?

import Mathlib.Data.Complex.Basic
import Mathlib.LinearAlgebra.RootSystem.Defs
import Mathlib.LinearAlgebra.RootSystem.WeylGroup
import Mathlib.GroupTheory.Perm.Sign

variable
  (ι : Type)
  [DecidableEq ι]
  [Fintype ι]
  {M : Type}
  {N : Type}
  [AddCommGroup M]
  [Module ℂ M]
  [AddCommGroup N]
  [Module ℂ N]
  (P : RootPairing ι ℂ M N)

def SphericalFn : M → ℂ := fun m =>
  ∑ w : P.weylGroup, 1

[Kenny Lau]

Surely it's a theorem that actually has content

[Kenny Lau]

What is the mathematical proof that the Weyl group is finite?

[Kevin Buzzard]

Doesn't it act faithfully on the roots?

[Kevin Buzzard]

So probably the question boils down to whether this is proved, and then getting the fintype instance should be "straightforward" modulo the usual decidability issues

[Kenny Lau]

yeah, we don't care about decidability

[Kenny Lau]

despite what I said in #Is there code for X? > Z[(1+sqrt(1+4k))/2] @ 💬

[Phillip Harris]

It's defined as a subgroup of RootPairing.Aut. I assumed RootPairing.Aut would have a fintype instance for the same reason ι ≃ ι has a fintype instance, but actually RootPairing.Aut is a specialization of RootPairing.Equiv which is a specialization of RootPairing.Hom etc

[Kenny Lau]

yes, and the data in RootPairing is very much not finite

[Phillip Harris]

Ok I guess this is actually untrue because RootPairing doesn't require that the roots span the modules. RootSystem does. So there could be infinitely many choices for the map between modules in RootPairing.Aut. So I should assume it's a RootSystem. And in that case I still need to prove that the map between index sets determines the other data.

[Kenny Lau]

@Phillip Harris and once you have that, https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Fintype/OfMap.html#Fintype.ofInjective

noncomputable def Fintype.ofInjective{α : Type u_1} {β : Type u_2} [Fintype β] (f : α → β) (H : Function.Injective f) :
Fintype α