group representations

Stream: maths

[Greg Conneen]

Is there any representation theory in Mathlib? I can't seem to find any. If there isn't, how would I go about defining a representation, characters, and stating/proving things like Schur's Lemma? I've been fuddling around and need a little guidance.

[Alex J. Best]

I think someone asked the same question a month back, you should be able to find the thread by searching zulip for representation theory

[Greg Conneen]

When I searched for this topic beforehand, this is all I found:

class representation (G R M : Type) [monoid G] [ring R] [add_comm_group M] [module R M]
  extends group_module G M :=
(smul_comm : ∀ (g : G) (r : R) (m : M), g • (r • m) = r • (g • m))

namespace representation
open mul_action linear_map
variables {G R M : Type}
variables [group G] [ring R] [add_comm_group M] [module R M] [representation G R M]

-- set_option trace.class_instances true

-- lemma smul_mem_fixed_points (r : R) (m : M) (hm : m ∈ fixed_points G M) :
--   r • m ∈ fixed_points G M :=
-- begin
--   simp only [mem_fixed_points] at *,
--   intro g,
--   rw [smul_comm, hm],
-- end
end representation

I read through that thread, and didn't exactly see a lot of development, just attempts at explaining the code, so it's not exactly what I'm looking for.

[Alex J. Best]

Right, I think the result of that thread is that no, there isn't any! But lots of people would be interested in seeing some.