Zulip Chat Archive

Stream: maths

Topic: Representation Theory


view this post on Zulip orlando (May 21 2020 at 08:31):

Hello, That good @Scott Morrison , i have also a version of Maschke theorem.

But for me the big step is really to make the application over C\mathbb{C} !

For example, the decomposition of a representation in irreducible representation.

I think the decomposition in irrducible part is ok for field (not algebraically closed).

view this post on Zulip Patrick Massot (May 21 2020 at 10:42):

Could we move this thread to the math stream?

view this post on Zulip Notification Bot (May 21 2020 at 16:18):

This topic was moved here from #new members > Representation Theory by Mario Carneiro

view this post on Zulip Patrick Massot (May 21 2020 at 16:52):

Thanks Mario.

view this post on Zulip Syx Pek (May 22 2020 at 08:54):

I am very new to Lean (Ive checked it in the past many years ago but I had deemed it to unwieldy to get started). I am just curious why the PR for Maschke's Thm don't define the notion of semisimplicity, and just state that k[G] is semisimple, which I think would be how most people would think Maschke's Thm actually looks like. (It unpacks the notion of semisimplicity into the notion of every submodule has a complementary subspace, which I think its equivalent?, though I only work with algebra over (commutative unital) rings, so I don't know the subtleties.)

view this post on Zulip Johan Commelin (May 22 2020 at 09:29):

@Syx Pek Welcome! The reason is only that the definitions are not there yet. This PR does all the "real work", and we can easily repackage it in a follow-up PR. I agree that this should be done. We cannot claim that it's completely done yet (-;

view this post on Zulip Scott Morrison (May 22 2020 at 09:32):

In particular, the design decisions around "which definition of semisimplicity should we use" are probably harder than the actual calculation I did in that PR.

view this post on Zulip Scott Morrison (May 22 2020 at 09:33):

There are a lot of ways to talk about semisimplicity!

view this post on Zulip Kevin Buzzard (May 22 2020 at 09:33):

Yes, I think the issue will be that nobody has defined semisimple algebras yet. I wonder if this is one of those situations where mathematicians are quite happy with several definitions of the same thing but computer scientists can't have this. Is the definition of a semisimple algebra something like "finite sum of simple algebras" or "its representation theory is semisimple"? There are theorems to be proved here and nobody has got round to it yet

view this post on Zulip Kevin Buzzard (May 22 2020 at 09:33):

Yeah what Scott said

view this post on Zulip Kevin Buzzard (May 22 2020 at 09:34):

They won't be hard

view this post on Zulip Kevin Buzzard (May 22 2020 at 09:34):

It's just that we are understaffed right now because the universities aren't teaching this stuff

view this post on Zulip Hanting Zhang (Mar 22 2021 at 20:22):

Hello,

I'm an incoming freshman student in California, USA, interested in mathematics and computer science. In particular, I'm interested in developing the representation theory library in mathlib. I'm looking for guidance, perhaps in the form of a summer internship, or someone who would be willing to oversee me in a project in representation theory.

I was wondering if anyone here could be looking for interns or knew of such opportunities.

I have experience contributing elementary results to mathlib. I'm comfortable with basic concepts in type theory, abstract algebra, and category theory. I'm not knowledgable in the fine details of representation theory, so there would be some inertia for me to contribute mathlib-level material--I would essentially be learning as I go. I know there's already a significant amount of un-PR'ed code spread out everywhere; I'm fine doing code transfer, but would prefer if I could prove something new.

I'm excited to learn, and I would be happy to talk about this in more detail. Thanks for reading!

view this post on Zulip Kevin Buzzard (Mar 22 2021 at 20:23):

There's a ton of basic representation theory which is do-able but not done yet. You'd be welcome to join my group of students who will be meeting on Tuesdays throughout July and August.

view this post on Zulip Scott Morrison (Mar 22 2021 at 21:43):

As a suggestion for source material: I like Pavel Etingof's notes (it's an AMS book, but also freely available from his webpage), which I think should be pretty readily formalisable.

view this post on Zulip Scott Morrison (Mar 22 2021 at 21:45):

I would love to see more rep th too. I did a little (the core fact of Maschke's theorem is at src#monoid_algebra.is_semisimple_module), but it didn't seem like there were others wanting to work on it in the near future, so paused again.

view this post on Zulip Kevin Buzzard (Mar 22 2021 at 21:50):

It would be wonderful to see the proof that the character table of a finite group is square.

view this post on Zulip Hanting Zhang (Mar 23 2021 at 01:20):

@Kevin Buzzard Thank you for the response! I would love to join your group over the summer--could I DM you on Zulip or Discord to talk about more details?

view this post on Zulip Aaron Anderson (Mar 23 2021 at 03:42):

We have docs#is_semisimple_module now. I think I see two directions from here:

view this post on Zulip Aaron Anderson (Mar 23 2021 at 03:43):

  • Continuing on the abstract algebra of semisimplicity towards Artin-Wedderburn (maybe the Jacobson Density Theorem first)?

view this post on Zulip Aaron Anderson (Mar 23 2021 at 03:45):

  • Defining the setoid of conjugacy (if it isn't already lurking somewhere) and its quotient, the type of conjugacy classes of a group/monoid. From there, it's probably not such a long road to the basics of character theory.

view this post on Zulip Julian Külshammer (Mar 23 2021 at 08:05):

I'd be happy to contribute at some point especially if someone wants to collaborate towards the first bullet point. A tricky point for the second bullet point is potentially to determine the correct set of assumptions on the ground field (because presumably one doesn't want to just work over the complex numbers).

view this post on Zulip Scott Morrison (Mar 23 2021 at 08:40):

The work I did on Mashke only assumes the characteristic doesn't divide the order of the field.

view this post on Zulip Aaron Anderson (Mar 23 2021 at 16:04):

Speaking of that, I feel like eventually whole files will assume that the characteristic doesn’t divide the order of the group, so we probably want to make that a fact instance

view this post on Zulip Hanting Zhang (Mar 26 2021 at 02:43):

Hi. I'm trying to go through the code in branch#representation and make it work with the current version of lean again. I've run into this universe problem which I don't really understand.

import linear_algebra.basic
import algebra.monoid_algebra

universes u v w

variables (k : Type v) (G : Type u)
variables [comm_ring k] [group G]
variables (M : Type w) [add_comm_group M] [module (monoid_algebra k G) M] [module k M]

def module_of_monoid_algebra_module : module k M := restrict_scalars k (monoid_algebra k G) M
-- universe levels don't match

Clicking on each thing in the viewer window tells me that restrict_scalars is a function Type u_1 → Type u_2 → Type u_3 → Type u_3. So I think the problem has to do with the final u_3 not matching with the universe of module k M, but how do I fix this?
(cc @Scott Morrison because this is basically a copy of his code.)

view this post on Zulip Scott Morrison (Mar 26 2021 at 02:44):

Oh dear, that branch is very old. :-) I wouldn't believe it's a good idea...

view this post on Zulip Hanting Zhang (Mar 26 2021 at 02:45):

Oh. What's wrong with this branch? I only needed to make minor changes up to this point, and everything seemed to work pretty well.

view this post on Zulip Scott Morrison (Mar 26 2021 at 03:19):

I'll have a look. Do you want to push what you have?

view this post on Zulip Scott Morrison (Mar 26 2021 at 03:20):

From memory there was still significant uncertainty about how best to represent the simultaneous actions of k and G. There are potentially 3 different has_smul instances available: k, G and monoid_algebra k G.

view this post on Zulip Aaron Anderson (Mar 26 2021 at 03:46):

Does the existence of smul_comm_class help with that?

view this post on Zulip Hanting Zhang (Mar 26 2021 at 03:51):

Pushed here: branch#acxxa/representation

view this post on Zulip Aaron Anderson (Mar 26 2021 at 03:53):

It doesn't look like that branch has any commits that aren't on master?

view this post on Zulip Hanting Zhang (Mar 26 2021 at 03:55):

Oops. It should be there now.

view this post on Zulip Hanting Zhang (Mar 26 2021 at 04:03):

This is pointed out in the docs for restrict_scalars, but how about using module k M, module (monoid_algebra k G) M, and is_scalar_tower k (monoid_algebra k G) M? Then there's a smul_comm_class from the tower instance.

Is there anything that says if A is an R-algebra and M an A-monoid, then is_scalar_tower R A M?

view this post on Zulip Scott Morrison (Mar 26 2021 at 04:37):

(I think my last work on this predates is_scalar_tower, and I've not yet got my head around it yet...)

view this post on Zulip Johan Commelin (Mar 26 2021 at 05:16):

Yes, this probably should use both is_scalar_tower and smul_comm_class

view this post on Zulip Eric Wieser (Mar 26 2021 at 09:00):

is_scalar_tower R A M requires a has_scalar R M instance to be used

view this post on Zulip Eric Wieser (Mar 26 2021 at 09:02):

So I guess your question is "is there a pair of definitions that produce a has_scalar R M instance and a corresponding is_scalar_tower R A M?"

view this post on Zulip Johan Commelin (Mar 26 2021 at 09:27):

If a group G acts on an abelian group M then this can also be viewed as a k[G]-module on M.

view this post on Zulip Johan Commelin (Mar 26 2021 at 09:27):

And G also acts on k[G]

view this post on Zulip Johan Commelin (Mar 26 2021 at 09:27):

So we want is_scalar_tower G (monoid_algebra k G) M

view this post on Zulip Kevin Buzzard (Mar 26 2021 at 10:01):

And also one for k and k[G] and M?

view this post on Zulip Eric Wieser (Mar 26 2021 at 10:08):

I still don't understand the concrete problem statement, but the error originally was confusing docs#restrict_scalars with docs#restrict_scalars.semimodule:

import linear_algebra.basic
import algebra.monoid_algebra

universes u v w

variables (k : Type v) (G : Type u)
variables [comm_ring k] [group G]
variables (M : Type w) [add_comm_group M] [module (monoid_algebra k G) M] [module k M]

noncomputable def module_of_monoid_algebra_module : module k M :=
(infer_instance : module k $ restrict_scalars k (monoid_algebra k G) M)

view this post on Zulip Kevin Buzzard (Mar 26 2021 at 10:09):

You also want a distrib mul action of G on M

view this post on Zulip Eric Wieser (Mar 26 2021 at 10:09):

This type of thing is IMO a bad idea though, and safer is to not unfold restrict_scalars:

noncomputable def module_of_monoid_algebra_module :
  module k (restrict_scalars k (monoid_algebra k G) M) :=
infer_instance

view this post on Zulip Kevin Buzzard (Mar 26 2021 at 10:10):

Alternatively just make M a module for the monoid algebra and deduce the k module structure and the distrib mul action structure from that

view this post on Zulip Johan Commelin (Mar 26 2021 at 10:12):

I think that to talk about a representation in a flexible way, we might need 4 lines of variables

view this post on Zulip Kevin Buzzard (Mar 26 2021 at 10:12):

To give commuting k and G actions on M is to give an action of the monoid algebra

view this post on Zulip Kevin Buzzard (Mar 26 2021 at 10:13):

Mathematicians pass freely between the two points of view

view this post on Zulip Eric Wieser (Mar 26 2021 at 10:14):

I think the restrict_scalars-free way to set this up is

variables [module k M] [distrib_mul_action G M] [module (monoid_algebra k G) M]
variables [is_scalar_tower k (monoid_algebra k G) M] [is_scalar_tower G (monoid_algebra k G) M]

view this post on Zulip Johan Commelin (Mar 26 2021 at 10:14):

variables (G : Type u) (k : Type v) (M : Type w)
variables [group G] [comm_ring k]  [add_comm_group M]
variables [distrib_mul_action G M] [module k M] [module (monoid_algebra k G) M]
variables [is_scalar_tower G (monoid_algebra k G) M] [is_scalar_tower k (monoid_algebra k G) M]

view this post on Zulip Johan Commelin (Mar 26 2021 at 10:15):

And probably an is_smul_comm_class for good measurer?

view this post on Zulip Eric Wieser (Mar 26 2021 at 10:15):

That's inferred from is_scalar_tower I think? via docs#is_scalar_tower.to_smul_comm_class

view this post on Zulip Johan Commelin (Mar 26 2021 at 10:17):

aah, right. So that should be fine

view this post on Zulip Johan Commelin (Mar 26 2021 at 10:18):

So clearly we are approaching the limit of comfy variable lines.

view this post on Zulip Johan Commelin (Mar 26 2021 at 10:18):

You just want to say: "Let M be a k-linear G-module."

view this post on Zulip Eric Wieser (Mar 26 2021 at 10:29):

Wait, actually I think you can do that

view this post on Zulip Eric Wieser (Mar 26 2021 at 10:29):

Certainly the module (monoid_algebra k G) M instance is inferred already

view this post on Zulip Eric Wieser (Mar 26 2021 at 10:30):

(my orange bars conspired against me again)

view this post on Zulip Johan Commelin (Mar 26 2021 at 10:31):

Of course ideally we would abstract of monoid_algebra k G, and introduce a k-algebra A together with a predicate is_monoid_algebra k G A.

view this post on Zulip Johan Commelin (Mar 26 2021 at 10:32):

Because k[G]kR=R[G]k[G] \otimes_k R = R[G], but Lean will not believe that equality.

view this post on Zulip Eric Wieser (Mar 26 2021 at 10:33):

I think perhaps this instance should exist and is missing?

instance [semiring k] [monoid G] [add_comm_monoid M] [semimodule k M] [distrib_mul_action G M] :
  semimodule (monoid_algebra k G) M :=
sorry

view this post on Zulip Scott Morrison (Mar 26 2021 at 10:40):

Could we go the other way instead? Deduce [semimodule k M] and [distrib_mul_action G M] from [semimodule (monoid_algebra k G) M]?

view this post on Zulip Scott Morrison (Mar 26 2021 at 10:41):

Maybe Eric's suggestion is better.

view this post on Zulip Eric Wieser (Mar 26 2021 at 10:41):

That's goes in the reverse direction to most of mathlib, so is likely to form loops

view this post on Zulip Johan Commelin (Mar 26 2021 at 10:42):

In practice, I have a Galois group G that acts on a field L that is an extension of K, and maybe I now want to view L as a K[G]-module.

view this post on Zulip Johan Commelin (Mar 26 2021 at 10:42):

So I don't want to derive the action of the Galois group G on L from the K[G]-module on L.

view this post on Zulip Eric Wieser (Mar 26 2021 at 10:49):

I assume the instance you want is something like this?

instance [semiring k] [monoid G] [add_comm_monoid M] [semimodule k M] [distrib_mul_action G M] :
  semimodule (monoid_algebra k G) M :=
{ smul := λ kG m, finsupp.lift_add_hom (λ g, (smul_add_hom k M).flip (g  m)) kG,
  add_smul := λ _ _ _, add_monoid_hom.map_add _ _ _,
  zero_smul := λ _, add_monoid_hom.map_zero _,
  smul_add := λ r s m, sorry,
  smul_zero := sorry,
  one_smul := sorry,
  mul_smul := sorry }

view this post on Zulip Kevin Buzzard (Mar 26 2021 at 10:50):

Johan Commelin said:

So clearly we are approaching the limit of comfy variable lines.

I think they hit that limit in analysis some time ago!

view this post on Zulip Eric Wieser (Mar 26 2021 at 10:51):

I'm pretty sure there's a clever way to build a bundled hom in smul such that all the sorrys are as trivial as the first two proofs

view this post on Zulip Eric Wieser (Mar 26 2021 at 11:34):

This gets two more proofs for free:

instance [semiring k] [monoid G] [add_comm_monoid M] [semimodule k M] [distrib_mul_action G M] :
  semimodule (monoid_algebra k G) M :=
{ smul := λ kG m,
    ((finsupp.lift_add_hom : _ ≃+ (monoid_algebra k G →+ M)).to_add_monoid_hom.comp
      (add_monoid_hom.pi $ λ g : G, g  (smul_add_hom k M).flip)).flip kG m,
  add_smul := λ _ _ _, add_monoid_hom.map_add _ _ _,
  zero_smul := λ _, add_monoid_hom.map_zero _,
  smul_add := λ r s m, add_monoid_hom.map_add _ _ _,
  smul_zero := λ _, add_monoid_hom.map_zero _,
  one_smul := sorry,
  mul_smul := sorry }

but needs #6891 for the g •, and a definition of add_monoid_hom.pi which appears to be missing.

view this post on Zulip Hanting Zhang (Apr 26 2021 at 03:38):

Hi, I went back to trying stuff out with this and I've written up a representation theory version of @Scott Morrison's Maschke's lemma. It's pushed to branch#acxxa/representation. I've also copy pasted a whole bunch of stuff from submodule to create API for asubrepresentation structure I defined. There's also a lattice isomorphism between subrepresentations and submodules of the induced monoid algebra. (The equivalence between the module/representation theoretic versions of Maschke is easy after that.)

I'm not really looking to push any of this into mathlib yet, since I mostly followed my nose and copy pasted along. I could very possibly have done something terribly wrong without realizing it. So, I just wanted to ask here for thoughts and suggestions from everybody. Also, I'm willing to put a lot more effort into this, but I thought it'd be best to tell everyone here first.

Anything is welcome! :)

view this post on Zulip Scott Morrison (Apr 26 2021 at 05:21):

Looks promising! Presumably we should tweak maschke.lean so that it uses representation, rather than module (monoid_algebra _ _).

view this post on Zulip Scott Morrison (Apr 26 2021 at 05:21):

Do you see any obstacle to doing that?

view this post on Zulip Scott Morrison (Apr 26 2021 at 05:22):

I'm about to PR Schur's lemma in any linear category over an algebraically closed field. I really hope we can use that statement to directly infer the group theoretical statement of Schur's lemma. (And, similarly, the Lie-theoretic statement.)

view this post on Zulip Scott Morrison (Apr 26 2021 at 06:08):

(This is now up as #7366, but it has some dependent PRs so may take a little while.)

view this post on Zulip Hanting Zhang (Apr 27 2021 at 05:46):

Scott Morrison said:

Do you see any obstacle to doing that?

No, it should be pretty easy. I've started to phase the monoid_algebra k G out and so far the proofs look exactly the same.

view this post on Zulip Hanting Zhang (Apr 27 2021 at 05:49):

Since you're also working with this stuff, you can always tell me about possible conflicting work, or maybe possible converging work. I'm always happy to coordinate :)

(But I'm probably going into the finite groups, character theory direction -- I don't know much about category theory)

view this post on Zulip Scott Morrison (Apr 27 2021 at 06:08):

I think character theory is a lovely direction, and I don't have anything in progress there.

view this post on Zulip Scott Morrison (Apr 27 2021 at 06:08):

I would like to make sure my recent general statement of Schur's lemma is actually usable in representation theory.

view this post on Zulip Hanting Zhang (Apr 27 2021 at 06:26):

Ok. I don't really know what that connection should look like, but I can make sure to set up most of the concrete instances on the ground

view this post on Zulip Kevin Buzzard (Apr 27 2021 at 07:58):

Again this would be a really nice example showing that we can get theorems about concrete structures of interest from "abstract nonsense".

view this post on Zulip Scott Morrison (Apr 27 2021 at 08:15):

I don't think Schur's lemma for linear categories exactly counts as abstract nonsense...

view this post on Zulip Kevin Buzzard (Apr 27 2021 at 10:13):

By "abstract nonsense" I just mean "any theorem about categories"! We've already proved that categories are useful for mathematical definitions, because of schemes. The next step is to prove they're useful for theorems not in category theory and it looks like right now we have two great candidates for this (this and profinite stuff). Homological algebra will be a third.

view this post on Zulip Oliver Nash (Apr 27 2021 at 10:26):

I'd love to start using the category theory stuff we have. I don't expect to get to this for some time but getting Schur's lemma for Lie modules as a dividend is just the motivation I need.

view this post on Zulip Aaron Anderson (Apr 27 2021 at 16:11):

@Hanting Zhang, I like that you're moving forward on actually defining representations and rep_homs, but of course I have opinions on which definition should be the basic definition.

view this post on Zulip Aaron Anderson (Apr 27 2021 at 16:12):

Personally, I'd choose the definition currently used in the library (a module (monoid_algebra k G) V), and I'm about to say why, but ultimately as long as that instance, the smul_comm instance, and the to_monoid_hom/of_monoid_hom structure are still there at the end of the day, I don't think it matters that much what the underlying definition is.

view this post on Zulip Aaron Anderson (Apr 27 2021 at 16:15):

I vote for representation k G V to be defined as an abbreviation of module (monoid_algebra k G) V, because then subrepresentation can be an abbreviation of submodule (monoid_algebra k G) V and rep_hom can be an abbreviation of linear_map, again over monoid_algebra k G.

view this post on Zulip Aaron Anderson (Apr 27 2021 at 16:17):

You have to define all of the extra structure on representation, subrepresentation, rep_hom one way or another, but this way you don't have to copy and paste all the basic API just to define them and get the basic instances on them.

view this post on Zulip Hanting Zhang (Apr 27 2021 at 16:18):

Ok. Actually I think I agree with sticking to monoid_algebra k G; it would prevent all the duplication I've been doing.

view this post on Zulip Kevin Buzzard (Apr 27 2021 at 16:19):

It is not the definition we give to undergraduates, but experience has shown us that the fewer definitions we have, the better.

view this post on Zulip Kevin Buzzard (Apr 27 2021 at 16:19):

If I had seen the "burn vector_space" PR I would have suggested that it lived on as an abbreviation

view this post on Zulip Aaron Anderson (Apr 27 2021 at 16:21):

If you abbreviate these things, and provide the smul_comm instances and so on, it should still be possible to work entirely with those other approaches (although even my undergrad class eventually switched to mostly using group-ring-modules...)

view this post on Zulip Aaron Anderson (Apr 27 2021 at 16:22):

As we move further into the library, it should also be possible to make irreducible_representation an abbreviation for simple_module and so on

view this post on Zulip Kevin Buzzard (Apr 27 2021 at 16:22):

Yes, the way I was taught it was all G-actions on k-vector spaces and then suddenly this bombshell half way through that it's just R-modules for R=k[G] and about 3/4 of the lemmas we'd proved until that point were true in far greater generality

view this post on Zulip Aaron Anderson (Apr 27 2021 at 16:24):

I think here the key piece of code is a def (unfortunately not an instance, or it'd create a loop) that takes in a smul_comm_class of the right scalar actions and puts on a module (monoid_algebra k G) M structure

view this post on Zulip Aaron Anderson (Apr 27 2021 at 16:26):

It'd also be nice if there's a short-and-sweet notation that approximates the ρ g notation that you use when talking about the group homomorphism

view this post on Zulip Aaron Anderson (Apr 27 2021 at 16:28):

Perhaps as simple as ρ k M g...

view this post on Zulip Hanting Zhang (Apr 27 2021 at 16:30):

Aaron Anderson said:

I think here the key piece of code is a def (unfortunately not an instance, or it'd create a loop) that takes in a smul_comm_class of the right scalar actions and puts on a module (monoid_algebra k G) M structure

I think this is what I've done indirectly. representation extends smul_comm_class for the G and k actions. Then I derive a module instance.

I could just cut out defining a representation and do this directly

view this post on Zulip Hanting Zhang (Apr 27 2021 at 16:33):

But I didn't seem to hit any problems with the type class inference after I defined the module instance; is there an explicit loop we should be worried about?

view this post on Zulip Aaron Anderson (Apr 27 2021 at 16:50):

Presumably you want to provide a smul_comm_class given a module (monoid_algebra _ _) AND vice versa, but only one can be an instance

view this post on Zulip Eric Wieser (Apr 27 2021 at 17:00):

Without having followed earlier conversation - the of' in representation_theory/basic.lean in your branch is docs#monoid_algebra.single_one_ring_hom

view this post on Zulip Hanting Zhang (Apr 27 2021 at 17:01):

Ok. I might be missing the point, but why do we want both directions?

variables (k : Type u) (G : Type v) (M : Type w)
variables [semiring k] [monoid G] [add_comm_monoid M]
variables [module k M] [distrib_mul_action G M]
variables [smul_comm_class k G M]

instance : module (monoid_algebra k G) M := by blah blah... -- define this

I was thinking that this setup would be the way to define representations. Going from module (monoid_algebra k G) M to smul_comm_class k G M seems like going backwards. (Also you would need is_scalar_tower k (monoid_algebra k G) M and is_scalar_tower G (monoid_algebra k G) M to make this work, maybe both or just one of them)

view this post on Zulip Hanting Zhang (Apr 27 2021 at 17:04):

Eric Wieser said:

Without having followed earlier conversation - the of' in your branch is docs#monoid_algebra.single_one_ring_hom

Oh oops, I missed this. But the name is so long...

view this post on Zulip Eric Wieser (Apr 27 2021 at 17:05):

Well, you can always define of' := monoid_algebra.single_one_ring_hom and sort out the name later - but there's no need to prove it again!

view this post on Zulip Hanting Zhang (Apr 27 2021 at 17:06):

Yeah, that's going to be the first thing I do

view this post on Zulip Aaron Anderson (Apr 27 2021 at 17:32):

Hanting Zhang said:

Ok. I might be missing the point, but why do we want both directions?

variables (k : Type u) (G : Type v) (M : Type w)
variables [semiring k] [monoid G] [add_comm_monoid M]
variables [module k M] [distrib_mul_action G M]
variables [smul_comm_class k G M]

instance : module (monoid_algebra k G) M := by blah blah... -- define this

I was thinking that this setup would be the way to define representations. Going from module (monoid_algebra k G) M to smul_comm_class k G M seems like going backwards. (Also you would need is_scalar_tower k (monoid_algebra k G) M and is_scalar_tower G (monoid_algebra k G) M to make this work, maybe both or just one of them)

If we define a representation as module (monoid_algebra k G) M, then whenever we want to use a representation, we'll assume [representation k G M] which will be equivalent to [module (monoid_algebra k G) M]. Once we're there, we'll sometimes want to refer directly to the k-action, and sometimes to the G-action, so we want to have module k M instances and distrib_mul_action G M instances that follow from [representation k G M]. We'll also want to know that those commute with each other and with the action of monoid_algebra k G, hence you'll want smul_comm_class and is_scalar_tower instances

view this post on Zulip Eric Wieser (Apr 27 2021 at 17:35):

so we want to have module k M instances and distrib_mul_action G M instances that follow from [representation k G M].

This doesn't make any sense, because you're not allowed to write [representation k G M] without writing [module k M] [distrib_mul_action G M] first

view this post on Zulip Eric Wieser (Apr 27 2021 at 17:36):

It's like saying you want an instance to go from module k M to add_comm_monoid M

view this post on Zulip Eric Wieser (Apr 27 2021 at 17:36):

Oh, sorry; you're talking about a different definition of representation to the one in the branch?

view this post on Zulip Hanting Zhang (Apr 27 2021 at 17:37):

Ohh, I understand. I'm also realizing that all of this was basically said before in this thread, I just didn't get it before (@Eric Wieser even wrote down the module instance explicitly right above my first comment :upside_down: )

view this post on Zulip Eric Wieser (Apr 27 2021 at 17:38):

Oh, I hadn't realized this thread had older replies from me in it!

view this post on Zulip Aaron Anderson (Apr 27 2021 at 17:39):

Eric Wieser said:

Oh, sorry; you're talking about a different definition of representation to the one in the branch?

Yes, I've been suggesting that we define it as module (monoid_algebra k G) M, which means basically flipping everything @Hanting Zhang ' been doing backwards...

view this post on Zulip Hanting Zhang (Apr 27 2021 at 17:41):

That's perfectly fine with me btw -- actually less work in the long run because there's no duplication

view this post on Zulip Eric Wieser (Apr 27 2021 at 17:48):

Based on the recent vector_space removal, I think that is a definition that belongs only in a docstring

view this post on Zulip Eric Wieser (Apr 27 2021 at 17:49):

Although I guess that argument applies to the definition in the branch too

view this post on Zulip Hanting Zhang (Apr 27 2021 at 17:49):

@Aaron Anderson Hmm, wait actually do you mean this way?
Scott Morrison said:

Could we go the other way instead? Deduce [semimodule k M] and [distrib_mul_action G M] from [semimodule (monoid_algebra k G) M]?

view this post on Zulip Eric Wieser (Apr 27 2021 at 17:50):

I think the usual way to handle this is add instances in the forwards direction (the branch), and type aliases like restrict_scalars in the backwards direction (that suggestion)

view this post on Zulip Hanting Zhang (Apr 27 2021 at 17:58):

Ok. It seems like I will follow the main mathlib direction with this setup then:

variables (k : Type u) (G : Type v) (M : Type w)
variables [semiring k] [monoid G] [add_comm_monoid M]
variables [module k M] [distrib_mul_action G M]
variables [smul_comm_class k G M]

instance : module (monoid_algebra k G) M := by blah blah... -- a representation

And we can go backwards with docs#restrict_scalars.module and, err, hopefully docs#restrict_scalars.distrib_mul_action

view this post on Zulip Aaron Anderson (Apr 27 2021 at 23:27):

Hanting Zhang said:

Aaron Anderson Hmm, wait actually do you mean this way?
Scott Morrison said:

Could we go the other way instead? Deduce [semimodule k M] and [distrib_mul_action G M] from [semimodule (monoid_algebra k G) M]?

I definitely mean this.

view this post on Zulip Eric Wieser (Apr 28 2021 at 11:09):

Looking at the branch, this instance worries me a bit:

noncomputable instance has_group_scalar [semiring k] [monoid G] : has_scalar G (monoid_algebra k G) :=
{ smul := λ g x, (monoid_algebra.of k G g) * x }

because when k = G you end up with two has_scalar G (monoid_algebra G G) instances which have different actions.

view this post on Zulip Eric Wieser (Apr 28 2021 at 11:11):

Perhaps no one ever uses monoid_algebra G G so it doesn't really matter

view this post on Zulip Johan Commelin (Apr 28 2021 at 11:12):

You'll have things like G = units k. But G = k is unlikely, I think.

view this post on Zulip Kevin Buzzard (Apr 28 2021 at 11:23):

I think I've seen Z[Z]\mathbb{Z}[\mathbb{Z}] before, but this is the integers as an additive monoid.

view this post on Zulip Eric Wieser (Apr 28 2021 at 11:25):

To avoid the issue we could create a type alias and instead declare the action has_scalar (foo G) (monoid_algebra k G)

view this post on Zulip Johan Commelin (Apr 28 2021 at 11:31):

I think that in the additive setting, this is more likely to be a problem.

view this post on Zulip Johan Commelin (Apr 28 2021 at 11:31):

Are we trying to do representation theory of additive monoid/groups as well?

view this post on Zulip Johan Commelin (Apr 28 2021 at 11:32):

Otherwise Kevin's example would end up begin monoid_algebra int (multiplicative int) and there wouldn't be a problem anyway.

view this post on Zulip Riccardo Brasca (Apr 28 2021 at 11:34):

I am playing with monoid_algebra for the LTE, and I indeed suggest to avoid add_monoid_algebra if possible

view this post on Zulip Riccardo Brasca (Apr 28 2021 at 11:34):

It really makes things confusing

view this post on Zulip Kevin Buzzard (Apr 28 2021 at 11:34):

Is that a good reason to avoid it?

view this post on Zulip Kevin Buzzard (Apr 28 2021 at 11:35):

I tried to prove the Riemann hypothesis but it really got confusing

view this post on Zulip Riccardo Brasca (Apr 28 2021 at 11:35):

I mean, one can prove everything for monoid_algebra, and at the end translate the results for add_monoid_algebra using the fact that they are isomorphic

view this post on Zulip Kevin Buzzard (Apr 28 2021 at 11:36):

Yes, that's a fair point.

view this post on Zulip Kevin Buzzard (Apr 28 2021 at 11:36):

Or, if you have an additive group A that you want to do representation theory with, just apply the theory to multiplicative A


Last updated: May 11 2021 at 16:22 UTC