Direct Sum of Representations

Stream: Is there code for X?

[Atticus Kuhn]

It is a fact in representation theory that the direct sum of representations is a representation. I am trying to prove this fact. I looked in /representation_theory/* , but could not find it, so I decided to try proving it myself. Here is what I have so far

import algebra.module.linear_map
import representation_theory.basic


variables (k G : Type) [comm_semiring k] [monoid G]

def direct_sum_of_representations (i :Type ) (M : i → Type)
[decidable_eq i]
[ Π (j : i), add_comm_monoid (M j) ] [Π (j : i), module k (M j) ] [Π (j : i), representation k G (M j)]
: representation k G (direct_sum i (λ (j : i), M j)) := begin
 exact ⟨λg, sorry, sorry, sorry⟩,
end

What is the best way to prove this? I tried using direct_sum.lmk. Any help would be appreciated.

[Kevin Buzzard]

It's arguably a construction (ie a definition) rather than a fact (a theorem). You're missing a definition, not a proof.

[Kevin Buzzard]

You'll have to look in the API for direct sums to see how to define maps out of and into them

[Eric Wieser]

I would guess this is easiest to prove/construct by unfolding docs#representation

[Eric Wieser]

import algebra.module.linear_map
import representation_theory.basic

variables {k G : Type} [comm_semiring k] [monoid G]

/-- A more bundled version of `dfinsupp.map_range.linear_map`. -/
def dfinsupp.map_range.module_End {ι : Type*} {M : ι → Type*}
  [decidable_eq ι] [Π j, add_comm_monoid (M j)] [Π j, module k (M j)] :
  (Π i, module.End k (M i)) →* module.End k (Π₀ i, M i) :=
{ to_fun := dfinsupp.map_range.linear_map,
  map_one' := dfinsupp.map_range.linear_map_id,
  map_mul' := dfinsupp.map_range.linear_map_comp }

def direct_sum_of_representations (i :Type*) (M : i → Type*)
  [decidable_eq i]
  [Π j, add_comm_monoid (M j)] [Π j, module k (M j)]
  (r : Π j, representation k G (M j)) :
  representation k G (direct_sum i (λ (j : i), M j)) :=
dfinsupp.map_range.module_End.comp (pi.monoid_hom r)

[Atticus Kuhn]

Thank you both for your help. I can see that I will have to look more into dfinsupp in the future.

[Eric Wieser]

Note that docs#direct_sum is just a thin layer on top of docs#dfinsupp; if the API you want is missing for direct_sum, it probably exists for dfinsupp instead

[Atticus Kuhn]

Do you think I should make a PR to mathlib with this? representation_theory.basic has the tensor product of representations, but not the direct sum of representations.

[Kevin Buzzard]

We're in the middle of a big port right now, which makes things a bit more complicated than usual.

[Eric Wieser]

It's also worth asking whether by "direct sum" you perhaps actually want representation k G (Π i, M j), which I think we have somewhere too