## Stream: maths

### Topic: Representation Theory

#### 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 $\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).

#### Patrick Massot (May 21 2020 at 10:42):

Could we move this thread to the math stream?

#### Notification Bot (May 21 2020 at 16:18):

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

Thanks Mario.

#### 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.)

#### 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 (-;

#### 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.

#### Scott Morrison (May 22 2020 at 09:33):

There are a lot of ways to talk about semisimplicity!

#### 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

#### Kevin Buzzard (May 22 2020 at 09:33):

Yeah what Scott said

#### Kevin Buzzard (May 22 2020 at 09:34):

They won't be hard

#### 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

#### 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.

#### 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.

#### 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.

#### 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.

#### 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.

#### 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?

#### Aaron Anderson (Mar 23 2021 at 03:42):

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

#### Aaron Anderson (Mar 23 2021 at 03:43):

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

#### 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.

#### 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).

#### 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.

#### 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

#### 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.)

#### Scott Morrison (Mar 26 2021 at 02:44):

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

#### 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.

#### Scott Morrison (Mar 26 2021 at 03:19):

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

#### 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.

#### Aaron Anderson (Mar 26 2021 at 03:46):

Does the existence of smul_comm_class help with that?

#### Hanting Zhang (Mar 26 2021 at 03:51):

Pushed here: branch#acxxa/representation

#### Aaron Anderson (Mar 26 2021 at 03:53):

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

#### Hanting Zhang (Mar 26 2021 at 03:55):

Oops. It should be there now.

#### 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?

#### 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...)

#### Johan Commelin (Mar 26 2021 at 05:16):

Yes, this probably should use both is_scalar_tower and smul_comm_class

#### Eric Wieser (Mar 26 2021 at 09:00):

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

#### 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?"

#### 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.

#### Johan Commelin (Mar 26 2021 at 09:27):

And G also acts on k[G]

#### Johan Commelin (Mar 26 2021 at 09:27):

So we want is_scalar_tower G (monoid_algebra k G) M

#### Kevin Buzzard (Mar 26 2021 at 10:01):

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

#### 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)  #### Kevin Buzzard (Mar 26 2021 at 10:09): You also want a distrib mul action of G on M #### 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  #### 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 #### 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 #### 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 #### Kevin Buzzard (Mar 26 2021 at 10:13): Mathematicians pass freely between the two points of view #### 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]  #### 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]  #### Johan Commelin (Mar 26 2021 at 10:15): And probably an is_smul_comm_class for good measurer? #### 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 #### Johan Commelin (Mar 26 2021 at 10:17): aah, right. So that should be fine #### Johan Commelin (Mar 26 2021 at 10:18): So clearly we are approaching the limit of comfy variable lines. #### Johan Commelin (Mar 26 2021 at 10:18): You just want to say: "Let M be a k-linear G-module." #### Eric Wieser (Mar 26 2021 at 10:29): Wait, actually I think you can do that #### Eric Wieser (Mar 26 2021 at 10:29): Certainly the module (monoid_algebra k G) M instance is inferred already #### Eric Wieser (Mar 26 2021 at 10:30): (my orange bars conspired against me again) #### 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. #### Johan Commelin (Mar 26 2021 at 10:32): Because $k[G] \otimes_k R = R[G]$, but Lean will not believe that equality. #### 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  #### 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]? #### Scott Morrison (Mar 26 2021 at 10:41): Maybe Eric's suggestion is better. #### 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 #### 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. #### 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. #### 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 }  #### 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! #### 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 #### 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,
zero_smul := λ _, add_monoid_hom.map_zero _,
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.

#### 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! :)

#### 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 _ _).

#### Scott Morrison (Apr 26 2021 at 05:21):

Do you see any obstacle to doing that?

#### 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.)

#### 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.)

#### 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.

#### 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)

#### 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.

#### 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.

#### 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

#### 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".

#### Scott Morrison (Apr 27 2021 at 08:15):

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

#### 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.

#### 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.

#### 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.

#### 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.

#### 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.

#### 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.

#### 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.

#### 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.

#### 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

#### 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...)

#### 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

#### 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

#### 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

#### 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

#### Aaron Anderson (Apr 27 2021 at 16:28):

Perhaps as simple as ρ k M g...

#### 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

#### 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?

#### 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

#### 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

#### 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)

#### 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...

#### 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!

#### Hanting Zhang (Apr 27 2021 at 17:06):

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

#### 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

#### 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

#### 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

#### 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?

#### 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: )

#### 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...

#### 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

#### 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

#### Eric Wieser (Apr 27 2021 at 17:49):

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

#### 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]?

#### 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)

#### 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

#### 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.

#### 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.

#### Eric Wieser (Apr 28 2021 at 11:11):

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

#### Johan Commelin (Apr 28 2021 at 11:12):

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

#### Kevin Buzzard (Apr 28 2021 at 11:23):

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

#### 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)

#### Johan Commelin (Apr 28 2021 at 11:31):

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

#### Johan Commelin (Apr 28 2021 at 11:31):

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

#### 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.

#### 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

#### Riccardo Brasca (Apr 28 2021 at 11:34):

It really makes things confusing

#### Kevin Buzzard (Apr 28 2021 at 11:34):

Is that a good reason to avoid it?

#### Kevin Buzzard (Apr 28 2021 at 11:35):

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

#### 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

#### Kevin Buzzard (Apr 28 2021 at 11:36):

Yes, that's a fair point.

#### 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