feat(data/representation): definition of group representation and representation k G M ≃ module (monoid_algebra k G) M (blocked by #2366)
#2431
Conversation
Some functions and lemmas in `polynomial` now take bundled homomorphisms as arguments.
semorrison
added
RFC
semorrison
changed the title
representation k G M ≃ module (monoid_algebra k G) M (blocked by #2417 and #2366)
| def smul.linear_map [representation k G M] (g : G) : M →ₗ[k] M := | ||
| { to_fun := λ m, g • m, | ||
| add := λ m m', by simp [smul_add], | ||
| smul := λ r m, by simp [representation.smul_smul], } |
There was a problem hiding this comment.
Setting up things like this, using representation as a class, means that (a) there will be trouble when we want more than one action of G on M (which can surely happen) and (b) we can't say "Let pi be a representation of G on V" without breaking the rules of the class instance game. This is a big design decision. is it the right one?
| def as_monoid_hom [representation k G M] : G →* (M →ₗ[k] M) := | ||
| { to_fun := λ g, smul.linear_map g, | ||
| map_one' := by { ext, simp, }, | ||
| map_mul' := λ g g', by { ext, simp [mul_smul], }, } |
There was a problem hiding this comment.
In the Langlands programme it is very common to let pi be a representation of G on V. Note that pi is not G or V, it's the name of the structure in question, although it has a coercion to a function G -> End(V). Currently this function is called as_monoid_hom [representation k G M] in Lean. Giving this data is equivalent to giving the representation and pi is a very common interface in modern representation theory.
| mul_smul := λ g g' m, by { simp, erw [monoid_hom.map_mul ρ], simp, }, -- FIXME: here to | ||
| smul_zero := λ g, by { simp, }, | ||
| smul_add := λ g m m', by { simp, }, | ||
| smul_smul := λ g r m, by { simp, }, } |
There was a problem hiding this comment.
I see -- so I can use "rho". Then what is the point of representation k G M?
There was a problem hiding this comment.
To be honest, I'm pretty unconvinced by the usefulness of this definition. The main thing I was aiming for here was to make it easy to use g • m to talk about the actual action in terms of elements.
In a separate branch (not depending on this one) I've just proved Maschke's theorem, completely staying in the world of module (monoid_algebra k G). As I discovered there, writing things out in terms of elements was not actually very useful! Much more useful was being able to talk about "multiplication by g as a k-linear map", i.e. exactly the ρ : G →* (M →ₗ[k] M) interpretation.
There was a problem hiding this comment.
I wonder if sometime soon we (you, me, anyone interested) could have a "meeting", whether just on zulip or with screen sharing, to go over the possibilities. I'd be happy to go through my proof of Maschke's theorem and explain what felt most painful there.
There was a problem hiding this comment.
I wonder if sometime soon we (you, me, anyone interested) could have a "meeting", whether just on zulip or with screen sharing, to go over the possibilities. I'd be happy to go through my proof of Maschke's theorem and explain what felt most painful there.
@semorrison I'm only seeing this comment now... but I think such a meeting is a great idea.
There was a problem hiding this comment.
I'm going to close this PR in the meantime. I've been meaning to write some notes about my other experiments so far. In any case, I don't think this PR is a particularly good approach.
semorrison
changed the title
representation k G M ≃ module (monoid_algebra k G) M (blocked by #2417 and #2366)representation k G M ≃ module (monoid_algebra k G) M (blocked by #2417)
semorrison
changed the title
representation k G M ≃ module (monoid_algebra k G) M (blocked by #2417)representation k G M ≃ module (monoid_algebra k G) M (blocked by #2366)
Introduces
representation k G M, taking a[module k M]typeclass and extendingdistrib_mul_action, and proves the equivalences (roughly, see the module-doc) betweenrepresentation k G MG →* (M →ₗ[k] M)module (monoid_algebra k G) MSorry, this is stacked on top of two other open PRs (#2366
and #2417), so it's a bit hard to see what's going on, but as it seems several people are working on similar material I thought it best to get this public earlier rather than later.