Representation Theory

Stream: maths

[orlando]

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]

Could we move this thread to the math stream?

[Notification Bot]

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

[Patrick Massot]

Thanks Mario.

[Syx Pek]

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]

@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]

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]

There are a lot of ways to talk about semisimplicity!

[Kevin Buzzard]

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]

Yeah what Scott said

[Kevin Buzzard]

They won't be hard

[Kevin Buzzard]

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

[Hanting Zhang]

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!

[Kevin Buzzard]

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]

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]

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]

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

[Hanting Zhang]

@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]

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

[Aaron Anderson]

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

[Aaron Anderson]

• 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]

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]

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

[Aaron Anderson]

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]

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]

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

[Hanting Zhang]

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]

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

[Scott Morrison]

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]

Does the existence of smul_comm_class help with that?

[Hanting Zhang]

Pushed here: branch#acxxa/representation

[Aaron Anderson]

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

[Hanting Zhang]

Oops. It should be there now.

[Hanting Zhang]

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]

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

[Johan Commelin]

Yes, this probably should use both is_scalar_tower and smul_comm_class

[Eric Wieser]

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

[Eric Wieser]

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]

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]

And G also acts on k[G]

[Johan Commelin]

So we want is_scalar_tower G (monoid_algebra k G) M

[Kevin Buzzard]

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

[Eric Wieser]

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]

You also want a distrib mul action of G on M

[Eric Wieser]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

Mathematicians pass freely between the two points of view

[Eric Wieser]

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]

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]

And probably an is_smul_comm_class for good measurer?

[Eric Wieser]

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

[Johan Commelin]

aah, right. So that should be fine

[Johan Commelin]

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

[Johan Commelin]

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

[Eric Wieser]

Wait, actually I think you can do that

[Eric Wieser]

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

[Eric Wieser]

(my orange bars conspired against me again)

[Johan Commelin]

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]

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

[Eric Wieser]

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]

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]

Maybe Eric's suggestion is better.

[Eric Wieser]

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

[Johan Commelin]

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]

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]

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]

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]

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]

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.

[Hanting Zhang]

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]

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

[Scott Morrison]

Do you see any obstacle to doing that?

[Scott Morrison]

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]

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

[Hanting Zhang]

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]

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]

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

[Scott Morrison]

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

[Hanting Zhang]

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]

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

[Scott Morrison]

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

[Kevin Buzzard]

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]

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]

@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]

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]

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]

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]

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]

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

[Kevin Buzzard]

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

[Aaron Anderson]

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]

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]

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]

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]

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]

Perhaps as simple as ρ k M g...

[Hanting Zhang]

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]

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]

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]

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]

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]

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]

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]

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

[Aaron Anderson]

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]

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]

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

[Eric Wieser]

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

[Hanting Zhang]

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

[Eric Wieser]

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

[Aaron Anderson]

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]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Hanting Zhang]

@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]

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]

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]

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]

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]

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Eric Wieser]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Riccardo Brasca]

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

[Riccardo Brasca]

It really makes things confusing

[Kevin Buzzard]

Is that a good reason to avoid it?

[Kevin Buzzard]

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

[Riccardo Brasca]

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]

Yes, that's a fair point.

[Kevin Buzzard]

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

[Hanting Zhang]

Hi a third time,

So I didn't do anything with representation theory for awhile, because I kind of sidetracked onto a project to prove the Artin-Wedderburn Theorem, which is finally coming along in branch#acxxa/representation. It took 1500 loc though, so knowing me it will probably be another while before I can clean it up fully.

Just posting this out here in case anyone else is planning (or already! -- that would be awkward) working on this.

[Aaron Anderson]

I was working toward this, but I PRed all the work I did manage. I’ll take a look at what you’ve done.

[Scott Morrison]

What is the maths-statement of the version of Artin-Wedderburn you're aiming at?

[Hanting Zhang]

Let $R$ be a semi-simple ring. Then $R$ decomposes as a direct sum of simple modules $\bigoplus_{i = 1}^k n_i S_i$ and there is an ring isomorphism $\text{End}_R R \simeq \prod_{i = 1}^k \mathcal {M}_{n_i} (\text{End}_R (S_i))$. Here $\mathcal M_{n} (-)$ is the ring of $n\times n$ matrices. Actually we want $R^\text{op} \simeq \text{End}_R R \simeq \prod_{i = 1}^k \mathcal {M}_{n_i} (\text{End}_R (S_i)$ but I haven't thought too hard about how the op's go yet.

The tricky part was to figure out how to write the sum properly. Because letting $i$ range from $1, \dots, k$ really means something like going through the isomorphism classes of the set of simple submodules that $R$ decomposes into. Furthermore, $n_i$ quantifies the number of submodules $S'$ such that $S' \simeq S_i$, which is the size of each isomorphism class containing $S_i$.

In direct_sum_stuff.lean, isomorphism_quot R R is the quotient of decomposition R R by an isomorphism relation. Then for any i : isomorphism_quot R R, we define quotient.class i as the class of i's representative. So isomorphism_quot R R is supposed to be 1,...,k and quotient.class i is $n_i$. The isomorphism $\text{End}_R R \simeq \prod_{i = 1}^k \mathcal {M}_{n_i} (\text{End}_R (S_i))$ looks like this:

def something [is_semisimple_module R R] :
  (Π (i : isomorphism_quot R R),
    matrix (quotient.class i) (quotient.class i) (module.End R i.out)) ≃+* module.End R R :=
sorry

[Hanting Zhang]

Hopefully this looks correct and understandable. (and sane?) I would be very happy to take any suggestions and/or talk about my code!

[Hanting Zhang]

@Aaron Anderson Thanks in advance! Sorry everything is in the wrong place right now. I will be organizing code, files, and docstrings in the next few days so it should be much clearer then

[Hanting Zhang]

Oh and it shouldn't be too hard to go from the above and prove the version where $R$ is also an algebra over some field $F$.

[Scott Morrison]

The first statement "R decomposes as a direct sum" is just the definition of semisimple, right? Or are you using "Jacobson radical is trivial"?

[Scott Morrison]

The second statement "there is a ring isomorphism ..." has nothing to do with rings or modules: this is just a fact about endomorphisms of a direct sums of simple objects. (I'm just saying this to emphasise that these two parts are essentially separate projects.)

[Scott Morrison]

I think an important part of Artin-Wedderburn is that this decomposition is unique up to relabelling.

[Scott Morrison]

I had been proving this on a branch a while ago --- the version I wanted was that if you had a collection of objects so that homs between them were either zero or isomorphisms (e.g. the set of all simple objects), then decompositions into direct sums of these objects were unique (before we even come to the question of existence).

[Hanting Zhang]

Scott Morrison said:

The first statement "R decomposes as a direct sum" is just the definition of semisimple, right? Or are you using "Jacobson radical is trivial"?

Yes, I'm just using the definition.

[Hanting Zhang]

Scott Morrison said:

The second statement "there is a ring isomorphism ..." has nothing to do with rings or modules: this is just a fact about endomorphisms of a direct sums of simple objects. (I'm just saying this to emphasise that these two parts are essentially separate projects.)

As for the second part, I think I agree that the two parts are really separate things. I'm very out of depth on your first sentence though. What more general objects are you talking about when you say "nothing to do with rings and modules"?

[Hanting Zhang]

To be honest I wasn't even thinking about the unique part but now I'm realizing that it should also be a part of the proof. It shouldn't be too hard to prove from my approach just working concretely with the modules. May I ask how you've been approaching it? I guess which way do you think is more important?

[Scott Morrison]

So we have the definition of src#category_theory.simple, which hopefully is enough to do the endomorphism ring calculation.

[Scott Morrison]

Say you have a collection of objects X i in a preadditive category such that (X i ⟶ X j) = 0 when i \ne j. Then if you have a direct sum of these objects $A = \bigoplus n_i X_i$ (quite how to state that hypothesis is actually the trickiest thing here), then it should be easy to provide the ring isomorphism from End A to the direct sum of matrices over the End (X i).

[Scott Morrison]

Then the next step is to assume something a little stronger: every nonzero morphism X i ⟶ X i is an isomorphism (e.g. this holds if you take X i to be the collection of simples). (I don't think we even need Schur's lemma yet, which says that if the category is linear over an algebraically closed field then every morphisms X i ⟶ X i is actually a multiple of the identity.)

Now you can prove inductively, by a "Gaussian elimination" type argument, that if you have $$\bigoplus n_i X_i \iso \bigoplus m_i X_i$$ then in fact $n_i = m_i$.

[Scott Morrison]

I should say I haven't actually done this. I made one aborted attempt that was unnecessarily complicated, but I would like to do this at some point.

[Scott Morrison]

A final thing that would be nice to prove:

Let's give a name to the two above conditions on a collection of X i (that (X i ⟶ X j) = 0 when i \ne j, and any nonzero endomorphism of an X i is invertible), "X are mutually simple". (Notice that the X aren't necessarily simple in this definition!)

Then you can prove that if every object Z is isomorphic to some direct sum of the X i (in fact, in a unique way by the claim above), in fact the category is semisimple, and the X i are a set of representatives of the isomorphism classes of simples.

This approach is useful for example in quantum topology: e.g. typically any "diagrammatic algebra", like the Temperley-Lieb algebra underlying the Jones polynomial, is awkward to prove semisimplicity "via algebra", and the best approach is to produce this family of mutually simple objects first, then conclude afterwards the category is semisimple. In the quantum topology literature this approach sometimes goes by the name "Müger semisimplicity", as he explained how to use it.

[Julian Külshammer]

In the literature "mutually simple" is called a "semibrick". There is a related condition of a "simple-minded collection" in a triangulated category.

[Scott Morrison]

Oh, interesting, where do people use "semibrick"? I hadn't heard that one.

[Julian Külshammer]

In representation theory of finite dimensional algebras, most recently in a generalisation of the classical theory of tilting modules called tau-tilting theory, see e.g. https://arxiv.org/abs/1610.05860

[Scott Morrison]

Here's a first cut at proving that morphisms between direct sums of hom-orthogonal objects can be decomposed into direct sums of matrix blocks:

import category_theory.preadditive
import category_theory.limits.shapes.biproducts
import data.matrix.basic

open_locale classical

open category_theory
open category_theory.limits

universes v u

variables {C : Type u} [category.{v} C]

def hom_orthogonal {ι : Type*} (s : ι → C) : Prop :=
∀ i j, i ≠ j → subsingleton (s i ⟶ s j)

variables {ι : Type*} {s : ι → C}

def hom_orthogonal.eq_zero [has_zero_morphisms C] (o : hom_orthogonal s) {i j : ι} (w : i ≠ j) (f : s i ⟶ s j) :
  f = 0 :=
by { haveI := o i j w, apply subsingleton.elim, }

variables [has_zero_morphisms C] [has_finite_biproducts C]

noncomputable
def hom_orthogonal.matrix_decomposition {α β : Type*} [fintype α] [fintype β] (f : α → ι) (g : β → ι)
  (o : hom_orthogonal s) :
  (⨁ (s ∘ f) ⟶ ⨁ (s ∘ g)) ≃ Π (i : ι), matrix (f ⁻¹' {i}) (g ⁻¹' {i}) (End (s i)) :=
{ to_fun := λ z i j k,
    eq_to_hom (by { rcases j with ⟨j, ⟨⟩⟩, simp, }) ≫
      biproduct.components z j k ≫ eq_to_hom (by { rcases k with ⟨k, ⟨⟩⟩, simp, }),
  inv_fun := λ z, biproduct.matrix (λ j k, if h : f j = g k then
      z (f j) ⟨j, by simp⟩ ⟨k, by simp [h]⟩ ≫ eq_to_hom (by simp [h])
    else
      0),
  left_inv := λ z, begin
    ext j k,
    simp only [category.assoc, biproduct.lift_π, biproduct.ι_matrix],
    split_ifs,
    { simp, refl, },
    { symmetry, apply o.eq_zero h, },
  end,
  right_inv := λ z, begin
    ext i ⟨j, ⟨⟩⟩ ⟨k, w⟩,
    simp only [set.mem_preimage, set.mem_singleton_iff],
    simp [w.symm], refl,
  end, }

-- TODO additive version? linear version?

[Scott Morrison]

unique decomposition in a semibrick (a hom_orthogonal family where each object's nonzero endomorphisms are invertible) is going to be a little bit more involved, but I'll try it soon.

[Hanting Zhang]

@Scott Morrison Thanks for all your replies! Since you're planning to work on this, I don't think my approach really makes sense anymore. Especially because mine seems to be strictly less general. Would you mind though if I tried to redo some of my work following your thoughts on the category theoretic version? To be clear I would like to try as more of a learning project rather than a for mathlib project, in case you don't want interference.

[Hanting Zhang]

Although a side effect may be that I start asking a lot of random category theory questions here.

[Scott Morrison]

Oops, sorry, I don't mean to stop you doing anything. I've been thinking about doing this for a while but haven't actually done it, so I don't want to discourage you!

[Scott Morrison]

I just didn't want to wait until you had a PR to make suggestions about how to decouple AW into smaller pieces. :-)

[Scott Morrison]

One possibility would be to clean up what I posted above and get that ready for a PR. There are obvious next steps: show the equivalence I constructed is compatible with the obvious compositions on both sides, and then deduce the ring isomorphism for an endomorphism.

[Scott Morrison]

Would you be interested in doing that?

[Hanting Zhang]

Ah, my bad for misunderstanding. I kind of read too much into what you said lol

[Scott Morrison]

You've seen all the work I've done so far! :-)

[Hanting Zhang]

Now I'm thinking I should definitely get my original code PR out so people can actually see what I'm trying to put into mathlib

[Hanting Zhang]

I would be very interested in doing a general version of Artin-Wedderburn as a follow up!

[Scott Morrison]

Yes -- it's also no problem I think if first versions of things in mathlib are not in maximal generality. If someone upgrades your content later with something more general, you shouldn't feel sad about it, but happy that you provoked someone into doing work. :-)

[Hanting Zhang]

I think I just have a bad habit of writing too much code without PRing any of it. :thinking: Time too clean up all of my code...

[Winston Yin]

I mentioned in #new members wanting to add more representation theory to mathlib. While I only learned it from Fulton & Harris, @Scott Morrison suggested Etingof. Just starting a thread here to gather some opinions and advice.

[Scott Morrison]

Others have certainly been thinking about this recently: e.g. @Hanting Zhang, myself (very slowly, sorry). I'm looking forward to more representation theory!

I'm actually doing a bunch of low-level work at the moment, generalising a lot of our code about dimensions and bases to arbitrary noetherian and/or commutative rings (where previously it was just done over a field). I'm hoping this will be useful in representation theory per se soon.

[Scott Morrison]

Higher up in this same thread there is discussion about Artin-Wedderburn.

[Scott Morrison]

We already have Maschke's theorem (src#monoid_algebra.submodule.is_complemented) and Schur's lemma.

[Scott Morrison]

Although the current statement of Maschke's theorem is the "core" fact, and often you see it stated in a form that also gives various corollaries, so this might be a good first step. (i.e. find all the statements of Maschke's theorem you can in books, and make sure they follow from the version of Maschke's theorem already in mathlib!)

[Winston Yin]

I was actually having trouble finding Schur's lemma. Could you point me to it? I was actually trying to work up to proving it myself as practice. I'm not familiar with Maschke's theorem.

[Scott Morrison]

We actually have two independent proofs of versions of Schur's lemma!

[Scott Morrison]

There is src#linear_map.bijective_of_ne_zero, which states that a nonzero morphism between simple R modules is bijective.

[Scott Morrison]

(for R any ring)

[Scott Morrison]

There is also src#category_theory.is_iso_of_hom_simple

[Scott Morrison]

which is much more general, saying that any nonzero morphism between simple objects in a preadditive category with kernels is an isomorphism.

[Scott Morrison]

We should unify these. I hadn't realised until today that the special case theorem existed in mathlib.

[Scott Morrison]

There there are also various stronger versions of Schur's lemma.

[Scott Morrison]

in a k-linear category (k an algebraically closed field), src#category_theory.finrank_hom_simple_simple_le_one says the dimension of the hom space between two simples is at most one.

[Scott Morrison]

and two lemmas immediately afterwards say that it is 1 or 0 depending on whether the simple objects are isomorphic or not.

[Scott Morrison]

(Also --- if you're having trouble finding Schur's lemma, you haven't learnt how to use the right search tools: you should have the mathlib folder open in VSCode, and in the search bar type Schur. You can't miss it.)

[Winston Yin]

I did not know there are these generalisations to Schur's lemma! As a theoretical physics person, I only know it for matrix representations.

[Winston Yin]

Ah no wonder. I've been using the documentation site's search function.

[Winston Yin]

I'll take a look at Etingof and compare with mathlib.

[Hanting Zhang]

I'm working on the Artin-Wedderburn theorem (also very slowly!) with the far-away goal to prove that character tables for finite groups are square.

[Winston Yin]

I wrote about 600 lines for some basic definitions and lemmas regarding representations of algebras, following the first few pages of Etingof. Would anyone like to give some advice/feedback? I'm getting stuck at defining the direct sum of representations and showing that decomposable representations are reducible.

[Winston Yin]

representation.lean

[Winston Yin]

The proofs are certainly not efficient, so I welcome suggestions for improvement or tricks I should know

[Winston Yin]

I have some reservation regarding the notation. Currently, representation has a coe_fn from an algebra to an endomorphism of modules, which means the representation is identified with the function. Usually however, we say "let vector space V be a representation of the algebra A", so a representation is identified with the target space. I don't have enough experience to tell which one is better for mathlib.

[Winston Yin]

Also, sorry in advance if the names don’t obey the convention

[Eric Wieser]

Winston, just in case you missed it (zulip doesn't mention if your topic title already exists), there is lots of discussion above your message

[Eric Wieser]

Also, rather than uploading the txt file to zulip, could you create a gist on github? I get encoding issues when trying to read your text file on Android, which won't be true of a gist

[Winston Yin]

@Eric Wieser I’ll do that in the morning (midnight here). Never done gist before

[Alex J. Best]

Hi @Winston Yin, cool! Here are some thoughts from just looking at the file (I didn't actually run lean, so some of my suggestions might be wrong, let me know if I can clarify anything). Its easier for people to look at if you open a PR (tagged WIP for example) or at least make a git branch on mathlib so people can check the branch out more easily, let us know if you need assistance setting that up and we can help.

• If you have multiple rewrites in a row you can combine them so

rw a,
rw b,

becomes

rw [a, b]

• If you just run one tactic with by {simp} the curly braces {} aren't needed.
• The character ᾰ is awkward to type on purpose, the idea is that you shouldn't use it! Instead give a name to the thing you want to refer to, for has_bot:

  intros,
  rw submodule.mem_bot at ᾰ,
  rw ᾰ,
  rw linear_map.map_zero (ρ a),
  rw submodule.mem_bot

you can do

  intros h,
  rw [submodule.mem_bot at h, h, linear_map.map_zero (ρ a), submodule.mem_bot]

I believe.

• You apply theorems like apply linear_map.ext you could likely replace this with just calling the ext tactic. Likewise for apply funext
• If you have multiple goals its easier to read and manage them if you separate each goal into a block with braces, so whenever you have split the next line should start with a brace { to focus the first goal only.
• There are some nice tactics for reducing repetition like tactic#all_goals or tactic#repeat, for example you have

  split,
  show A → (direct_sum ι V →ₗ[k] direct_sum ι V),
  exact direct_sum_repr.to_fun ρ,

  simp,
  apply direct_sum_repr.map_one,

  simp,
  apply direct_sum_repr.map_mul,

  simp,
  apply direct_sum_repr.map_zero,

  simp,
  apply direct_sum_repr.map_add,

  simp,
  apply direct_sum_repr.commutes

which could probably become

  split,
  show A → (direct_sum ι V →ₗ[k] direct_sum ι V),
  exact direct_sum_repr.to_fun ρ,
  all_goals { simp, },
  { apply direct_sum_repr.map_one, },
  { apply direct_sum_repr.map_mul, },
  { apply direct_sum_repr.map_zero, },
  { apply direct_sum_repr.map_add, },
  { apply direct_sum_repr.commutes }

• You have a line

  change (λ (i : ι), V i) with V,
  change (λ (i : ι), V i) with V,

probably tactic#dsimp will do this for you

[Winston Yin]

@Alex J. Best those are great suggestions. Thank you!

[Eric Rodriguez]

A coule more:

• Type _ is more usually done as Type *,

• simp not at the end of the line is usually considered bad form, as it's hard to debug when you add more @[simp] lemmata. You should squeeze_simp them, or if you can put them at the end (potentially using simpa). You can also give simp bonus lemmata in the same sort of form that you pile up lemmata on rw, e.g. simp [representation.smul_add].

• Some of your lemmas should definitely be tagged with @[simp].

• You may be able to get away with reusing some lemmata from linear_map instead of having to re-prove them; you may have to put local attribute [reducible] representation in order to do this, though.

• You usually don't have to put { name . field := ... } in the definitions of things; Lean will figure it out most of the time, and if it doesn't, it'll shout at you.

• I think the standard approach for sub-objects now is docs#set_like.

• Lean usually prefers working backwards; proofs with a lot of at this tend to be a red flag that you could write it "more idiomatically".

There's some specific thoughts, too, that would be a lot easier to talk about in a github PR (e.g. the rw is unnecessary in one_smul). Have you got an invite to contribute to mathlib?

[Winston Yin]

Not yet. I’ll try a GitHub PR in the morning and maybe get some help here

[Eric Rodriguez]

Before you go to sleep, drop your github username and maintainers should be able to give you an invite for the morning ^^

[Bryan Gin-ge Chen]

If you haven't already seen it, check out our page with tips for contributors: https://leanprover-community.github.io/contribute/index.html

[Winston Yin]

If somebody could invite me to GitHub: winstonyin@gmail.com Got too tired last night after all!

[Bryan Gin-ge Chen]

I just sent an invite to that email. You'll need to create a GitHub account if you don't already have one.

[Winston Yin]

I've pushed my commit: https://github.com/leanprover-community/mathlib/commit/9215e39164877100d8bac41d0a7c241bb75a2cb9 (<---- this is a mistake)

[Winston Yin]

I only added representation.lean, so I'm not sure why there are all these other changed files.

[Winston Yin]

I think I see the issue. There's an existing branch called representation, which I've just pushed to... I'm sorry! Please help me fix this mistake, as I'm not good with git. It also looks like that branch is trying to do some of the same things I'm doing but differently.

[Winston Yin]

Ok the correct branch I've just created: https://github.com/leanprover-community/mathlib/compare/winstonyin/representation

[Antoine Labelle]

Hi,
I would like to try to contribute to the extent of my knowledge to the representation theory project in mathlib, but I am unsure where to starts since it looks like a few people are already working on this but there's not a lot in mathlib itself. I was wondering what is the state of the project right now.
I found the pull request #2431, which seems to introduce a definition of group representations and prove equivalences with other usual definitions; it seems like a good starting point, but it has been closed without merging. Why is that so, were there fundamental flaws in the approach of this PR?

[Oliver Nash]

@Scott Morrison :point_up:

[Johan Commelin]

@Antoine Labelle Is there a particular thing in repn thy that you would like to work on?

[Antoine Labelle]

@Johan Commelin I think that working towards orthogonality for characters of finite groups could be interesting. But I don't know if there are other things we'd need to get out of the way before working on that.

[Johan Commelin]

@Antoine Labelle Sounds good. Maybe create a little mind map of the topics you would need?

[Johan Commelin]

E.g., mathlib doesn't have class functions at the moment. I guess you would want to have those

[Johan Commelin]

If you have a list of things, we can quickly tell you what is there and what is not

[Heather Macbeth]

I remember from a past discussion of representation theory is that one difficulty is the variety of different ways a representation can be expressed. As a docs#mul_action, as a homomomorphism of the group into the automorphism group of the vector space, and as a module over the docs#monoid_algebra of G. I don't even think we have glue among these different notions. Did we ever decide which one should be primary?

[Antoine Labelle]

@Heather Macbeth Yeah, that's why I asked about #2431. The primary definition it takes is a distrib_mul_action such that the action of G commutes with that of k and it proves the equivalence with the two other definitions you mention. So it seems like it's already done, but have never been merged into mathlib.

[Antoine Labelle]

And yeah, I could try to create a little list of needed topics

[Scott Morrison]

The direction mathlib has gone since is to avoid things like representation which bundles together both actions and their compatibility, and instead chooses to have three separate typeclasses for these facts.

[Scott Morrison]

i.e. use the smul_comm_class (which quite possibly didn't even exist when I closed that PR??).

[Scott Morrison]

Certainly it would be good to replace #2431 with a PR that shows the equivalence between gadgets equipped with compatible scalar actions by k and G, and gadgets equipped with an action of monoid_algebra k G.

[Scott Morrison]

Personally I hope that we will also make a bundled version, perhaps as Rep k G, and provide a categorical API for everything, too.

[Scott Morrison]

There are a lot of functors used early on in representation theory (induction and restriction, particularly), and it seems to me a great shame if we do not express these as functors!

[Antoine Labelle]

Scott Morrison said:

Certainly it would be good to replace #2431 with a PR that shows the equivalence between gadgets equipped with compatible scalar actions by k and G, and gadgets equipped with an action of monoid_algebra k G.

Ok, maybe I think I could try to do that first, since these equivalences seem to me like a necessary thing to get out of way before being able to work on interesting character theory.
I am not yet very comfortable with typeclasses and their subtleties, so would you mind explaining why it is a better approach to have separate typeclasses for the actions and their compatibilities? To make it concrete, how would you write "let V be a representation of G over k" in Lean with this approach?

[Scott Morrison]

import algebra.module.basic

variables (k G V : Type*) [comm_semiring k] [monoid G] [add_comm_monoid V]
variables [module k V] [distrib_mul_action G V] [smul_comm_class k G V]

[Scott Morrison]

So you'd want definitions (perhaps instances in one direction) translating between [module k V] [distrib_mul_action G V] [smul_comm_class k G V] and [module (monoid_algebra k G) V].

[Scott Morrison]

Some of these hopefully already exist, in the files that develop monoid_algebra.

[Scott Morrison]

But then I'd also define Rep k G to be a structure, (parametrised also be the ring structure on k and the group structure on G), which has as fields the carrier type V and the remaining type classes. Then put a category instance on that.

[Scott Morrison]

Given the way we do bundled morphisms, there is not really a good way to say "a function V to W which is both k linear and G linear". So I suspect the module (monoid_algebra k G) V version is going to be important, because we can easily talk about a function which is monoid_algebra k G-linear.

[Antoine Labelle]

Thanks! So, for the backward direction (from [module (monoid_algebra k G) V]), would we have 3 definitions, one giving [module k V], one giving [distrib_mul_action G V] and one giving [smul_comm_class k G V], or should this be all bundled together somehow? In the first case, how would we formulate that the two parts pf the correspondence are inverses of each other?

[Scott Morrison]

There would be 3 definitions. (Almost surely the first one already exists.)

[Scott Morrison]

I guess we could write an equivalence with lots of letI := ... statements on one side of the equivalence, to specifying explicitly using the instance that has gone back and forth through the equivalence.

[Antoine Labelle]

Another quick question : how can I make Lean figure out what the distrib_mul_action is in the definition of [smul_comm_class k G V]?
In other words, how to avoid the error in the second definition here?

import algebra.module.basic
import algebra.module.linear_map

variables {k G V : Type*} [comm_semiring k] [monoid G] [add_comm_monoid V] [module k V]
variables (ρ : G →* (V →ₗ[k] V))

def distrib_mul_action_of_monoid_hom : distrib_mul_action G V :=
{ to_mul_action := { to_has_scalar := { smul := λ g v, ρ g v },
                     one_smul := λ v, by simp,
                     mul_smul := λ g h v, by simp, },
  smul_add := λ g v w, by simp,
  smul_zero := λ g, by simp, }

def smul_comm_class_of_monoid_hom : smul_comm_class k G V :=
begin
  sorry,
end

[Heather Macbeth]

@Antoine Labelle One option is to use a type synonym for V, something like

import algebra.module.basic
import algebra.module.linear_map

variables {k G V : Type*} [comm_semiring k] [monoid G] [add_comm_monoid V] [module k V]
variables (ρ : G →* (V →ₗ[k] V))

@[derive [add_comm_monoid, module k]] def rep_space (ρ : G →* (V →ₗ[k] V)) : Type* := V

instance distrib_mul_action_of_monoid_hom : distrib_mul_action G (rep_space ρ) :=
{ smul := λ g v, ρ g v,
  one_smul := λ v, by simp,
  mul_smul := λ g h v, by simp,
  smul_add := λ g v w, by simp,
  smul_zero := λ g, by simp }

def smul_comm_class_of_monoid_hom : smul_comm_class k G (rep_space ρ) :=
begin
  sorry,
end

[Heather Macbeth]

(The type synonym is when I rename V as rep_space ρ.)

[Heather Macbeth]

By the way, I rearranged your distrib_mul_action_of_monoid_hom a little for conciseness, but the only substantive change was from def to instance.

[Antoine Labelle]

What's the advantage of instance over def?

[Heather Macbeth]

instance can be found by "typeclass inference", def can't. So, for example, the fact that a metric space is in a natural way a topological space is found by typeclass inference.

[Heather Macbeth]

Let me redo this for you with def rather than instance, so you can see the difference -- one sec ...

[Antoine Labelle]

Should smul_comm_class_of_monoid_hom also be an instance then?

[Heather Macbeth]

Yes!

[Johan Commelin]

Btw, @Eric Wieser is the person to talk to when it comes to scalar actions in mathlib. I'm sure he knows the best way for moving back and forth between

variables (k G V : Type*) [comm_semiring k] [monoid G] [add_comm_monoid V]
variables [module k V] [distrib_mul_action G V] [smul_comm_class k G V]

and modules over monoid_algebra k G.

[Johan Commelin]

He has been adding a lot of homomorphisms of the form G -> Aut _ or R -> End _ derived from scalar actions. So this might already be there.

[Heather Macbeth]

Heather Macbeth said:

Let me redo this for you with def rather than instance, so you can see the difference -- one sec ...

OK, I got it working without typeclass inference (but as you can see, it's painful!). Not even sure if I've missed some tricks:

import algebra.module.basic
import algebra.module.linear_map

variables {k G V : Type*} [comm_semiring k] [monoid G] [add_comm_monoid V] [module k V]
variables (ρ : G →* (V →ₗ[k] V))

def distrib_mul_action_of_monoid_hom : distrib_mul_action G V :=
{ smul := λ g v, ρ g v,
  one_smul := λ v, by simp,
  mul_smul := λ g h v, by simp,
  smul_add := λ g v w, by simp,
  smul_zero := λ g, by simp }

def smul_comm_class_of_monoid_hom :
  @smul_comm_class k G V _
    (@mul_action.to_has_scalar G V _
      (@distrib_mul_action.to_mul_action G V _ _ (distrib_mul_action_of_monoid_hom ρ))) :=
begin
  sorry,
end

[Antoine Labelle]

Oof indeed, it seems like it's much better to use typeclass inference

[Eric Wieser]

Note that we already have docs#mul_action.of_End_hom; so we could have something called docs#distrib_mul_action.of_add_monoid_End_hom similar to the distrib_mul_action_of_monoid_hom above

[Eric Wieser]

Having said that, the implementation would just be distrib_mul_action.comp_hom _ ρ:

def distrib_mul_action_of_module_End_hom : distrib_mul_action G V :=
distrib_mul_action.comp_hom _ ρ

def smul_comm_class_of_monoid_hom :
  @smul_comm_class k G V _
    (@mul_action.to_has_scalar G V _
      (@distrib_mul_action.to_mul_action G V _ _ (distrib_mul_action_of_module_End_hom ρ))) :=
by apply_instance

[Antoine Labelle]

@Eric Wieser Thanks! Is there a reason you used def instead of instance as Heather suggested?
Also is there do you know if we already have also the equivalence with modules over the monoid algebra?

[Eric Wieser]

The first one can't be an instance because it depends on ρ, while the second one already exists so you don't need it anyway

[Eric Wieser]

Also is there do you know if we already have also the equivalence with modules over the monoid algebra?

Can you give me the lean statement?

[Eric Wieser]

Is this the forward statement?

variables (k G V : Type*) [comm_semiring k] [monoid G] [add_comm_monoid V]
  [module k V] [distrib_mul_action G V] [smul_comm_class k G V]

instance : module (monoid_algebra k G) V := sorry

-- are these the defining properties of the action you want?
lemma of_smul (g : G) (v : V) : monoid_algebra.of k G g • v = g • v := sorry
lemma algebra_map_smul (r : k) (v : V) : algebra_map k (monoid_algebra k G) r • v = r • v := sorry

[Antoine Labelle]

What do you think of the proposition of Heather which is to define a vector space which is just a copy of V and put distrib_mul_action and smul_comm_class instances on it? And yes, that would be the forward statement .

[Eric Wieser]

I think that's a reasonable idea

[Eric Wieser]

Whether it's necessary depends on whether V = monoid_algebra k G would create ambiguity

[Antoine Labelle]

I don't think I understand what you mean, V is the module, not the monoid algebra

[Eric Wieser]

V is any type that satisfies the module axioms. V = monoid_algebra k G is one such type.

[Eric Wieser]

If your instance can be parameterized to give a has_scalar (monoid_algebra k G) (monoid_algebra k G) instance, it must definitionally satisfy a • b = a * b to avoid diamonds

[Oliver Nash]

Antoine Labelle said:

To make it concrete, how would you write "let V be a representation of G over k" in Lean with this approach?

In addition to the great advice, examples already provided you could also look at some of our Lie theory, at least to see one way to set things like this up in terms of typeclasses. E.g., docs#lie_module is the definition of a representation of a Lie algebra.

[Antoine Labelle]

@Eric Wieser Do you know if we have the equivalence, for an algebra A over k, of module A M with is_scalar_tower k A M and algebra maps from A to M →ₗ[k] M

[Eric Wieser]

I would guess that would be docs#module.to_module_End_hom or docs#module.to_module_End

[Eric Wieser]

It seems we have neither

[Eric Wieser]

Oh, it's docs#distrib_mul_action.to_linear_map, if you just want A → M →ₗ[R] M

[Eric Wieser]

If you want the stronger A →+* module.End R M, it's:

@[simps]
def module.to_module_End_hom {R A M}
  [semiring R] [semiring A] [add_comm_monoid M]
  [has_scalar R A] [module R M] [module A M]
  [smul_comm_class A R M] : A →+* module.End R M :=
{ to_fun := distrib_mul_action.to_linear_map R M,
  map_one' := linear_map.ext $ one_smul _,
  map_mul' := λ f g, linear_map.ext $ mul_smul _ _,
  map_zero' := linear_map.ext $ zero_smul _,
  map_add' := λ f g, linear_map.ext $ add_smul _ _, }

[Eric Wieser]

I never PR'd that because I couldn't find a good place to put it where I had all the typeclasses available

[Antoine Labelle]

Eric Wieser said:

I would guess that would be docs#module.to_module_End_hom or docs#module.to_module_End

Actually I mostly want the other direction

[Eric Wieser]

That's docs#linear_map.apply_module

[Eric Wieser]

Which probably should be renamed to module.End.apply_module

[Eric Wieser]

Or at least, it's that if you combine it with module.comp_hom f where f : A →+* module.End R M

[Eric Wieser]

Note that is_scalar_tower was the wrong condition, smul_comm_class is what you need

[Antoine Labelle]

Thanks!

[Eric Wieser]

Eric Wieser said:

If you want the stronger A →+* module.End R M, it's:

PR'd as #10300

[Nicolò Cavalleri]

@Antoine Labelle are you still working on this?

[Antoine Labelle]

@Nicolò Cavalleri I've put it on hold a little bit to do other stuff including some linear algebra which I felt would be needed for rep theory, but yes I have some stuff done and I have the intention to come back to it soonish.

[Antoine Labelle]

Hi,
I was wondering if anyone understand why the scalar action is not recognized in smul_single. It works with of k G g but not with finsupp.single g 1, which is quite annoying.

import algebra.module.basic
import data.equiv.module
import algebra.module.linear_map
import algebra.monoid_algebra.basic
import linear_algebra.trace

open monoid_algebra

namespace representation

section
variables (k G V : Type*) [comm_semiring k] [monoid G] [add_comm_monoid V]
variables [module k V] [distrib_mul_action G V] [smul_comm_class G k V]

def as_monoid_hom : G →* (V →ₗ[k] V) :=
{ to_fun := distrib_mul_action.to_linear_map k V,
  map_one' := by { ext, simp, },
  map_mul' := λ g g', by { ext, simp [mul_smul], }, }

@[simp]
lemma as_monoid_hom_apply_apply (g : G) (v : V) :
  (as_monoid_hom k G V) g v = g • v := rfl

noncomputable def as_algebra_hom : monoid_algebra k G →ₐ[k] (V →ₗ[k] V) :=
  (lift k G _) (as_monoid_hom k G V)

lemma as_algebra_hom_def :
  as_algebra_hom k G V = (lift k G _) (as_monoid_hom k G V) := rfl

@[simp]
lemma as_algebra_hom_single (g : G):
  (as_algebra_hom k G V (finsupp.single g 1)) = (as_monoid_hom k G V) g :=
by simp [as_algebra_hom_def]

noncomputable instance as_module : module (monoid_algebra k G) V :=
  module.comp_hom V (as_algebra_hom k G V).to_ring_hom

lemma as_module_apply (a : monoid_algebra k G) (v : V):
  a • v = (as_algebra_hom k G V a) v := rfl

@[simp]
lemma smul_single (g : G) (v : V) :
  (finsupp.single g 1 : monoid_algebra k G) • v =  g • v := by simp [as_module_apply]

[Kevin Buzzard]

Here's a hacky fix:

example : has_scalar (G →₀ k) V := infer_instance -- fails
noncomputable example : has_scalar (monoid_algebra k G) V := infer_instance -- works

@[simp]
lemma smul_single (g : G) (v : V) :
  (id (finsupp.single g 1) : monoid_algebra k G) • v =  g • v := by simp [as_module_apply]

[Kevin Buzzard]

Even though monoid_algebra k G and G →₀ k are definitionally equal, they are not syntactically equal, and type class inference works up to syntactic equality. What is happening in (finsupp.single g 1 : monoid_algebra k G) is that the syntactic type of finsupp.single g 1 is G →₀ k, and (finsupp.single g 1 : monoid_algebra k G) means "check finsupp.single g 1 has type monoid_algebra k G and then continue" -- but it doesn't actually syntactically change the type, so has_scalar (G →₀ k) V is what Lean ends up searching for, and it can't find it. However adding that little id hack actually does syntactically change the type of the term to monoid_algebra k G and then type class inference works. The "correct" thing to do here would be to use the appropriate monoid_algebra constructor for monoid_algebra k G as opposed to finsupp.single g 1 which is the finsupp constructor.

[Antoine Labelle]

Will the simplifier still simplify (finsupp.single g 1) • v to g • v if I add id?

[Kevin Buzzard]

Looking through the monoid algebra file it seems that the appropriate constructor is of_magma:

@[simp]
lemma smul_single (g : G) (v : V) :
  (of_magma k G g : monoid_algebra k G) • v =  g • v := by simp [as_module_apply]

[Antoine Labelle]

Kevin Buzzard said:

Looking through the monoid algebra file it seems that the appropriate constructor is of_magma:

@[simp]
lemma smul_single (g : G) (v : V) :
  (of_magma k G g : monoid_algebra k G) • v =  g • v := by simp [as_module_apply]

My first intention was to state it as (of k G g) • v = g • v but the linter complained that the LHS simplifies to (finsupp.single g 1) • v. Won't the same problem happen with of_magma?

[Kevin Buzzard]

oh I see!

[Kevin Buzzard]

Yes you're absolutely right, the simp linter doesn't like it. I think that it's a bad idea to have of = single and of_magma = single as global @[simp] lemmas. I can quite understand why one might want them locally to be simp lemmas when making the API, but for a "user" like you who doesn't ever want to see finsupps but still wants to use the simplifier, the strategy of making of = single a simp lemma is preventing you from doing this.

I saw the same phenomenon showing up in the complex number game. I wanted to make complex.ext a simp lemma, so that whenever Lean was faced with a goal z = w it would replace it with z.re = w.re and z.im = w.im. This worked great for me when I was making the API for complex numbers, because to e.g. prove that multiplication of complex numbers is associative you absolutely want to check this on real and imaginary parts. However when you go deeper into the theory and are developing complex analysis, the last thing you want the simplifier to do is to keep taking real and imaginary parts of things; you want this to be available to you as an option, but definitely not be the "this is the only sensible way to proceed" option, which is kind of what simp lemmas are.

So I would suggest that (perhaps after getting the nod from one or more maintainers) that you make a PR removing the global simp tags from the lemmas which are causing the trouble and then adding them again with local attribute [simp] of_eq_single (or whatever it's called) so that they're there for API development of monoid_algebra but don't leak out.

[Kevin Buzzard]

In my opinion monoid_algebra should be irreducible and finsupp.single G 1 : monoid_algebra should not even typecheck. I mean, it should typecheck in the file making the API for monoid_algebra, and then it should stop typechecking and the simplifier should stop trying to flow in that direction.

@[irreducible] def X := ℕ
def a : ℕ := 37
#check (a : X) -- fails

[Kevin Buzzard]

@Eric Wieser am I talking nonsense?

[Eric Wieser]

I've not read the whole of today's discussion, but yes, we shouldn't be writing finsupp.single about monoid_algebra

[Eric Wieser]

The problem is that the alternative is copying over all the lemmas about finsupp.single to a new monoid_algebra.single

[Antoine Labelle]

So @Eric Wieser should I make a PR to remove the global simp tag to lemmas like monoid_algebra.of_apply?

[Eric Wieser]

I'm not sure. I guess you could open one with the WIP tag and see what breaks

[Kevin Buzzard]

I am not convinced that there is too much stuff to be said about monoid_algebra.single. One could even get away with not having it, and just sticking with of. The big advantage of single over of is that single span G ->_0 k as an abelian group so you can use simpler induction principles, but I wonder whether we ever see these in practice.

[Eric Wieser]

I am not convinced that there is too much stuff to be said about monoid_algebra.single.

(edit: we would need lemmas saying what the) Behavior of 0, 1, addition, subtraction, negation, multiplication, nsmul, zsmul, pow, and maybe some stuff about summation is?

[Eric Wieser]

Also I think docs#add_monoid_algebra.of is nasty due to multiplicative

[Kevin Buzzard]

I don't know what you mean by all this.

[Eric Wieser]

Also of doesn't work on magma algebras, which is annoying

[Kevin Buzzard]

sure define 0 and 1 and etc in the monoid_algebra.lean API file using single, and then close it off, giving the user access to of, and a proof that of (g * h) = of g * of h

[Eric Wieser]

I think if we want to remove of_apply, we need to unbundle of

[Kevin Buzzard]

Things like addition are not about of or single

[Eric Wieser]

Ah, you're talking about the "One could even get away with not having [monoid_algebra.single]" option, which is where we are today minus the finsupp mess

[Eric Wieser]

Kevin Buzzard said:

Things like addition are not about of or single

single g r + single g s = single g (r + s) is the type of thing I'm describing

[Kevin Buzzard]

But we only want single x 1 so I'm not interested in this

[Eric Wieser]

I disagree, we need single x r for polynomial.monomial

[Eric Wieser]

Unless you also want to kill monomial at the same time

[Kevin Buzzard]

I'm well aware that we need it for G ->0 k

[Kevin Buzzard]

I'm suggesting that we forego it only for monoid_algebra because to me it looks a bit useless when we're thinking about group representation theory.

[Eric Wieser]

polynomial is (add_)monoid_algebra not ->0 though

[Kevin Buzzard]

Right. I'm suggesting we don't need single for monoid_algebra (only).

[Eric Wieser]

Are you suggesting we should have add_monoid_algebra.single but not monoid_algebra.single?

[Kevin Buzzard]

What I learnt when working on a multivariable polynomial project was that it's really handy to have single because then you can prove stuff about G ->_0 k by checking it's true on single x y and then checking that the subset where it's true is a subgroup. I'm suggesting that this is not a common method of proof for $k[G]$.

[Kevin Buzzard]

If I call it $k[G]$ then you can figure out what I mean in Lean, but I mean "the group ring". I'm not talking about subtle differences between additive and multiplicative structures. I just mean that $tg$ doesn't show up much in this theory when $t\not=1$.

[Kevin Buzzard]

So I don't care if I not only can't coerce finsupp.single x y into monoid_algebra but that there's no substitute in monoid_algebra world, because I will just do of_ring x * of_group y for the appropriate ofs (one from the ring, one from the group).

[Eric Wieser]

I think multivariate polynomials are confusing things here, since they are of type add_monoid_algebra R (σ →₀ ℕ) which has both things you're talking about in it

[Eric Wieser]

My polynomial remarks are about polynomial R = add_monoid_algebra R ℕ where polynomial.monomial = add_monoid_algebra.single (modulo structure eta)

[Eric Wieser]

If we forbid using finsupp.single with add_monoid_algebra and don't add a add_monoid_algebra.single to replace it, then we're pulling the rug out from under polynomial.

[Eric Wieser]

And if we have add_monoid_algebra.single but not monoid_algebra.single, then we're being inconsistent

[Kevin Buzzard]

I see. Do you understand #11574?

[Eric Wieser]

Yes, but unrelated to the single topic, I don't yet know how to avoid the diamonds that PR creates

[Eric Rodriguez]

do we have any diamonds that don't get fixed with definitional eta? i've often said how little I like the current diamond-fixing approach as much as I understand it's necessary

[Eric Wieser]

Yeah, these are straight-up non-equal diamonds

[Eric Rodriguez]

more type synonyms? :/ seems to be how mathcomp deal with it

[Eric Wieser]

(there are some equal-but-not-defeq diamonds that appear in that PR too, but they're not so big a deal)

[Eric Wieser]

https://github.com/leanprover-community/mathlib/blob/1b4ee53b3df5db827f8dc29f660bf613bfa2939e/test/instance_diamonds.lean#L124-L138 is the proof of the non-equal diamond

[Eric Wieser]

But it amounts to saying that the action of $K^\times$ on $K[K^\times]$ is ambiguous, as is the action of $K$ on $K[K]$

[Eric Wieser]

(I bring up the $K[K^\times]$ example to avoid the "well we only care about $K[G]$ where $G$ is a group" counterargument)

[Eric Wieser]

Eric Rodriguez said:

more type synonyms? :/ seems to be how mathcomp deal with it

I think this would solve the problem, but I suspect it will be very annoying for what Kevin wants to do.

[Kevin Buzzard]

-- If this were an instance, it would conflict with the natural
-- action of `k[k]` on itself given by multiplication.

The thing is that k[k] doesn't happen except in pathological computer science land (edit: just seen your comment on k[k^*]). In fact if R is a nontrivial ring (which it always is) and G is a group (which it always is, except when you're making polynomials) then R can never be G because nontrivial rings can never be groups. However they can certainly be additive groups.

So there is something interesting going on here with monoid_algebra v add_monoid_algebra. I claim that they are in some sense different beasts, because monoid_algebra eats a ring and a monoid, and add_monoid_algebra eats a ring and an add_monoid. Problems with scalar actions might occur with one if the ring is the monoid and with the other if the ring is the add_monoid. In particular the two problems are not "reflected" by to_additive.

[Eric Wieser]

I don't think we need to worry about add_monoid_algebra k A much here, since it's just monoid_algebra k (multiplicative A) so the same arguments apply

[Kevin Buzzard]

OK so it really is true that there are two distinct actions of $K^\times$ on $K[K^\times]$.

[Kevin Buzzard]

So we just make the important one (the action of $G$ on $K[G]$) the instance

[Kevin Buzzard]

and then just use of k * x for the other one

[Eric Wieser]

The other action is the one that says $K[G]$ is a $K$-algebra though, which is also important

[Kevin Buzzard]

Sure, but that's the K-action not the K^*-action. Or does every R-action on a thing induce an R^*-action?

[Kevin Buzzard]

When this sort of thing happens in lectures, mathematicians just introduce two different notations for the two actions

[Eric Wieser]

Or does every R-action on a thing induce an R^*-action?

Yes (docs#units.mul_action). This turns out to be useful, because it means we can turn every monoid action into a group action if we know we're working with the units

[Kevin Buzzard]

It can absolutely happen that X can act on Y in more than one way.

[Kevin Buzzard]

We can fix it in this case by defining G to be a group defeq to K^*. Then we have the G-action and the K^*-action and that's a nice fix. You can even make G irreducible the moment you did it, for safety.

[Eric Wieser]

One way out of the problem is to just use f : X →* perm Y and f x y instead of x • y

[Eric Wieser]

Or even f x • y if you like your •s, since we have docs#equiv.perm.apply_mul_action

[Eric Wieser]

Kevin Buzzard said:

We can fix it in this case by defining G to be a group defeq to K^*. Then we have the G-action and the K^*-action and that's a nice fix. You can even make G irreducible the moment you did it, for safety.

This would be more appealing if we could tell lean to emit an error if someone tries to work with $K[K^\times]$ rather than giving them rope to hang themselves with

[Eric Wieser]

That is, a means of blacklisting instances

[Kevin Buzzard]

I am not convinced that this problem is any more real than the following situation. A user finds themselves in a situation where they really do want two group structures on a type. They go ahead with [inst1 : group G] [inst2 : group G] and then nothing works, and then we explain to them that they have to do def H := G and [inst2 : group H].

[Adam Topaz]

Do people ever actually think about $K[K]$ and/or $K[K^\times]$ in real life?

[Kevin Buzzard]

I once wrote a paper in a scenario where this on this sort of thing, and I did use a type synonym. I had a Lie group G and was doing representation theory over the complex numbers. An example of the Lie group could have been $\mathbb{C}^\times$ but I called it $\overline{\R}^\times$ because the mathematics was telling me that it was a "different $\mathbb{C}$" to the one in the coefficient field.

[Kevin Buzzard]

Adam -- yes. Representation theory of real reductive groups.

[Adam Topaz]

Ah right

[Kevin Buzzard]

But as I say, they're in some sense "two different copies of the complex numbers"; one of them is just an abstract algebraic closure of the reals (or at least it was in the paper of Langlands I was using).

[Kevin Buzzard]

I should say that Langlands didn't explicitly say this, it came out of me trying to make what was happening in the paper more functorial.

[Adam Topaz]

But anyway I agree with you Kevin, the $K$ inside of $K[K]$ should really be thought of as different from the scalars

[Adam Topaz]

The correct spelling of $K[K^\times]$ should be $K[\mathbb{G}_m(K)]$ anyway.

[Eric Wieser]

Kevin Buzzard said:

Adam -- yes. Representation theory of real reductive groups.

I'm surprised that the case I constructed to prove a point actually turns out to be a thing people care about

[Eric Wieser]

Kevin Buzzard said:

I am not convinced that this problem is any more real than the following situation. A user finds themselves in a situation where they really do want two group structures on a type. They go ahead with [inst1 : group G] [inst2 : group G] and then nothing works, and then we explain to them that they have to do def H := G and [inst2 : group H].

This seems like a reasonable argument to me as long as we're only talking about K[G] on groups and not monoids (which is why we probably need separate group_algebra and monoid_algebra

[Kevin Buzzard]

I know that in Iwasawa theory people talk about the completion of the group ring $$\Z_p{\Z_p^\times]$$ too. I would like to argue that this diamond is there independent of this whole group ring business. If we just have a group G and a field k acting on an object (which can happen independent of whether one has made the group ring) then the units of the field act on the object so if the units of the field happen to be the group then you have two actions and already this is a diamond in some sense. The fix here should be a type synonym eg $GL_1(R)$ instead of units R. What I'm saying is that the monoid algebra definition is not creating any new diamonds, it's just bringing to the fore an issue which was already there because if we use typeclasses then we're only allowed one action of X on Y, just like we're only allowed one monoid structure on X (which is an action of X on X). So I propose we ignore this issue as I don't believe it will impede progress. With this in mind do we still need this type synonym in the group algebra PR?

[Kevin Buzzard]

An easier way of seeing the problem might be that if we have the statement "if G \times H acts on X then we get induced actions of G and H on X" then we have what you would call a diamond in the case where G=H and what I would call nothing to worry about

[Johan Commelin]

I agree that this is probably just a diamond that we have to live with.

[Johan Commelin]

But it would be good to record it somewhere, so that we don't forget when it exists.

[Kevin Buzzard]

It's because it's there in reality! The complex representation theory of real reductive groups really does give you two different actions of C^* on a vector space

[Johan Commelin]

Sure, but the question is how to deal with it later on. This could be via a type synonym for the group, or via specialized notation to distinguish the two actions. But we can figure that out when we get there.

[Eric Wieser]

An easier way of seeing the problem might be that if we have the statement "if G \times H acts on X then we get induced actions of G and H on X" then we have what you would call a diamond in the case where G=H and what I would call nothing to worry about

This situation doesn't arise in mathlib though: we don't have instances that go in this direction, precisely because they would create diamonds. Instances build data for "big" types (like G × H) out of instances on the pieces, not vice versa.

[Johan Commelin]

Does G act on G \times H? I can imagine we would have an instance for that in mathlib.

[Kevin Buzzard]

Well then I claim we shouldn't have an induced action of units K on V given an action of K on V for the same reason

[Kevin Buzzard]

Because units K is obviously smaller than K (although the type theorists are going to argue that it's bigger)

[Eric Wieser]

Yes, I mean "big" in the type theory sense

[Johan Commelin]

@Eric Wieser But if we have an action of G on G \times H, and also an action of H on G \times H, then we have a diamond. That's the same problem as we have with monoid_algebra.

[Kevin Buzzard]

And the fix is not yet another type ascription, it's to just leave it alone and let people fix it if they run into it. Mathematicians will know if they're running into it, their Spidey senses go off if they have two actions of X on Y

[Eric Wieser]

We have no global instance for has_scalar G (G × H) though (unless G acts on H too, then it's docs#prod.has_scalar), nor would it be safe to add one

[Kevin Buzzard]

Oh boo

[Kevin Buzzard]

How about bimodules? Do we have these yet?

[Eric Wieser]

Over two different rings? Yes, [module R M] [module Sᵐᵒᵖ M] [smul_comm_class R Sᵐᵒᵖ M]

[Kevin Buzzard]

Modules for group rings are a situation in real mathematics where two (generically) distinct objects act on the same side on an object. We have to support this and worry about "what if the objects are the same" later

[Johan Commelin]

Why don't we add an action of G^mop on monoid_algebra K G? Does that solve all our problems?

[Kevin Buzzard]

Well what about bimodules where the the two rings are the same? We can't use Eric's suggestion there. But that doesn't mean that we can't develop a theory of bimodules. It just means we ignore the issue

[Eric Wieser]

Does that solve all our problems

Not after #10716 it doesn't, which adds the kᵐᵒᵖ action

[Eric Wieser]

Well what about bimodules where the the two rings are the same? We can't use Eric's suggestion there.

Why can't we use the spelling above for bimodules over the same ring?

[Johan Commelin]

Fair enough. But it will certainly make the problems very tiny.

[Eric Wieser]

If we're going to use this with a type synonym like mul_opposite, we could also solve it with a dedicated synonym

[Johan Commelin]

mul_opposite would be natural: On k[G] there is an action of k on the left, and an action of G on the right.

[Johan Commelin]

Lean forces us to accept an action of k on the right. But maybe that shouldn't be a global instance.

[Johan Commelin]

I agree that algebras are bimodules, but should that be a def or an instance?

[Eric Wieser]

It could certainly maybe be an instance only in a locale

[Eric Wieser]

Although if algebras must be bimodules (and therefore carry a right action), then the algebra R (A →ₗ [R] A) instance requires lean to find the right action on A

[Eric Wieser]

I could still be persuaded that #10716 is a bad idea, but am like 80% sure we probably want it

[Johan Commelin]

So how do you suggest we deal with the G-action on k[G]?

[Johan Commelin]

Just multiply with of g, where of : G -> k[G]?

[Kevin Buzzard]

In representation theory you absolutely want that action because it's the regular representation. Already you have this pathological "what if G is syntactically k^*" question

[Eric Wieser]

What's the downside of the of g * x approach? (Other than being less appealing visually)

[Eric Wieser]

Presumably there are bits of the action API you want access to; do you know which bits?

[Kevin Buzzard]

We want all of it I suspect, because one of the big theorems in representation theory of finite groups is how the action of $G$ on $k[G]$ decomposes as a sum of irreducibles.

[Kevin Buzzard]

For me, you saying "well perhaps we have to completely avoid making the action because of the extremely unlikely event that G is syntactically k^*" is like you saying "well I think we should stop using typeclasses for groups because of the extremely unlikely event that we want two distinct groups structures on a type"

[Eric Wieser]

To be clear, I'm begrudgingly ok with the action as long as it's on the group_algebra where it's less likely to cause harm than the (add_) monoid_algebra

[Eric Wieser]

But I'd also like to understand what actually changes in practice if we say "let's not use • syntax for this action, let's just use a suitably bundled function"

[Johan Commelin]

Kevin Buzzard said:

We want all of it I suspect, because one of the big theorems in representation theory of finite groups is how the action of $G$ on $k[G]$ decomposes as a sum of irreducibles.

This can be phrased as how the k[G]-module k[G] over itself decomposes as sum of irreducibles.

[Sebastien Gouezel]

Often, the action is also written as $L_g a$ or $R_g a$ if you want to act on the left or on the right. This could be easily mimicked by using a type synonym foo G for G, acting on whatever you want, and calling the identity map from G to foo G as L, and then writing L g \bu a is totally non-ambiguous, diamond free, and close enough to common mathematical practice.

[Eric Wieser]

Kevin Buzzard said:

one of the big theorems in representation theory of finite groups is how the action of $G$ on $k[G]$ decomposes as a sum of irreducibles.

What would a lean statement of that look like under your preferred spelling, so that we can compare other spellings?

[Johan Commelin]

Another solution would be a pretty way of writing "g viewed as element of k[G]". I'm not sure a coercion will do. In maths, it is common to write [g].

[Eric Wieser]

We discussed having the quotient brackets work for free constructions like that in another thread

[Eric Wieser]

I think there was general agreement but no one volunteered to do the work

[Kevin Buzzard]

Eric Wieser said:

Kevin Buzzard said:

one of the big theorems in representation theory of finite groups is how the action of $G$ on $k[G]$ decomposes as a sum of irreducibles.

What would a lean statement of that look like under your preferred spelling, so that we can compare other spellings?

As Johan says, it should probably be a statement of the form "The R-module R is R-isomorphic to a certain exterior direct sum"

[Eric Wieser]

Where did R come from?

[Kevin Buzzard]

It's k[G]

[Eric Wieser]

It doesn't sound like the lean statement even mentions a G action then?

[Kevin Buzzard]

The thing is that a k-linear G-action on a k-vector space is the same thing as a k[G]-action. We already have a good theory of module actions, so if we could get the group algebra merged somehow (and right now I'm really confused about whether it needs to be different from the module algebra) then the theory of G-modules could just be developed as a theory of k[G]-modules.

[Kevin Buzzard]

@Eric Wieser how about making monoid_algebra and add_monoid_algebra irreducible and not making group_algebra at all, and disregarding the issue that G could in theory syntactically be units k because mathematicians are only too well aware when they have two distinct actions of A on B and will know to take evasive action via a type synonym (which can be described to them in some docstring). Does this solve the problems which started this thread and the problems with #11574?

[Kevin Buzzard]

The examples which have been flagged before have had G definitionally k^* but not syntactically.

[Antoine Labelle]

The main problem I had that started this thread was monoid_algebra.of simplifying to finsupp.single even though that's not really wanted. I suppose this wouldn't be the case anymore if monoid_algebra was made irreducible?

[Eric Wieser]

Making monoid_algebra irreducible is orthogonal to your issue

[Eric Wieser]

Removing the simp lemma is enough, but right now that creates more problems that it solves

[Eric Wieser]

Because we can't choose of as the canonical spelling (right now) because it doesn't work on magma algebras

[Eric Wieser]

So until we introduce something better, the only suitable spelling right now is finsupp.single, even though that had the wrong type.

[Antoine Labelle]

I see, so for now I guess I'll just make my problematic lemma use of but not make it a simp lemma

[Antoine Labelle]

Hi! I want to define the tensor product of two representations of a monoid G by g • (v ⊗ₜ w) = (g • v) ⊗ₜ (g • w), but I noticed that there is already docs#tensor_product.left_has_scalar which defines the action by letting G act only on the left factor. What are the reasons for this definition of an action on the left only, and is it possible to define the action I want on V ⊗ W without ambiguity with the other definition? Do I need to use a type synonym?

[Adam Topaz]

I suspect the action on the left is useful when you want to consider the base-change of an $A$-module $M$ to some $A$-algebra $B$, which is defined as the tensor product $B \otimes_A M$.

[Eric Wieser]

The action on the left is the obvious one when the action is by the field of the two vector spaces (and equal to the equivalent action on the right), which is why it's the default

[Antoine Labelle]

So I have to use a type synonym?

[Eric Wieser]

If you want to use • notation and not something like docs#tensor_product.map, yes

[Eric Wieser]

I don't know whether it makes more sense to put the type synonym on the tensor type or the action type

[Eric Wieser]

You might be able to get away without the synonym... What would the typeclass requirements for such an action be?

[Antoine Labelle]

Eric Wieser said:

You might be able to get away without the synonym... What would the requirements for such an action be?

Something like that

variables (k G V W : Type*) [comm_semiring k] [monoid G] [add_comm_monoid V] [add_comm_monoid W]
variables [module k V] [distrib_mul_action G V] [smul_comm_class G k V]
variables [module k W] [distrib_mul_action G W] [smul_comm_class G k W]

[Eric Wieser]

Is that enough for distrib_mul_action G (V ⊗[R] W)?

[Antoine Labelle]

I think it is, yes

[Eric Wieser]

Yeah, you definitely need a type synonym then

[Eric Wieser]

I would guess putting the type synonym on G works out better

[Antoine Labelle]

Eric Wieser said:

I would guess putting the type synonym on G works out better

Why is that? Putting the type synonym on the tensor product seems more natural to me since otherwise we can't compare the tensor representation to other representations of G.

[Kevin Buzzard]

Youch. Yes both the diagonal action for a tensor product group rep and the left action for base extension are pretty important :-/

[Robert Maxton]

shame our subscript options are so limited, or we could use •_D and •_L

[Robert Maxton]

or the like

[Yaël Dillies]

It's not really a matter of notation but a matter of API. If you start using •_D and •_L, then all the lemmas about • don't apply anymore.

[Kevin Buzzard]

Is this evidence that we should not define a G-representation over a field k as being definitionally a k[G]-module?

[Eric Wieser]

I thought we already decided that [module (monoid_algebra k G) X] was definitely the wrong way to go anyway (and instead to go via the separate actions of k and G)

[Eric Wieser]

Perhaps a type alias representation used as representation G solves most of the issues

[Oliver Nash]

Antoine Labelle said:

So I have to use a type synonym?

Yes.

I thought about this in some detail a while back and shared some details here: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.234773.20base.20change/near/240929318 which may or may not be useful.

[Antoine Labelle]

I am trying to implement the type synonym following @Oliver Nash's suggestions, as follows:

open_locale tensor_product

variables (k G V W : Type*) [comm_semiring k] [monoid G] [add_comm_monoid V] [add_comm_monoid W]
variables [module k V] [distrib_mul_action G V] [smul_comm_class G k V]
variables [module k W] [distrib_mul_action G W] [smul_comm_class G k W]
variables (v : V) (w : W)

@[derive [add_comm_monoid, module k]]
def tensor_rep : Type* := (V ⊗[k] W)

notation V ` ⊗[` k `,` G `] ` W := tensor_rep k V W
notation v ` ⊗ₜ[` k `,` G `] ` w := (tensor_product.tmul k v w : V ⊗[k,G] W)

The last line is problematic because I reference V and W. This shouldn't be a problem since I think there should be a way to infer V and W as the types of v and w. Is there a way to do that?

[Eric Wieser]

You should define a to_rep function that changes a tensor product to your type

[Eric Wieser]

Like docs#to_lex, docs#order_dual.to_dual, docs#conj_act.to_conj_act, etc

[Eric Wieser]

Then use that definition in your notation

[Antoine Labelle]

Thanks!

[Antoine Labelle]

Hi! After working for a bit on representation theory, I noticed that the approach I took to define k-linear representations of G on a vector space V as distrib_mul_action G V + smul_comm_class G k Vcauses a lot of issues due to ambiguity between different actions and potential diamonds. After some discussion with @Eric Wieser , we came to the conclusion that it might be better to avoid entirely scalar multiplication when doing representation theory and stick with the definition G →* (V →ₗ [k] V), writing φ g v everywhere we previously wrote g • v, where φ is the name of the representation (which is slightly less convenient, especially when φ is actually a long name, but seems like the least worst solution).
Before I start refactoring all I did so far, I was wondering what were the opinions of other people interested in representation theory in mathlib on this matter. Does anyone see downsides of this approach that we might have missed?

[Oliver Nash]

I think we should be able to obtain a situation similar to informal mathematics: when there is a single (or distinguished) action on a space then we can use the scalar multiplication notation. However when we are considering several actions simultaneously, and do not wish to distinguish any of them, (as happens quite a bit in representation theory) then we will be explicit and give the action a name.

[Oliver Nash]

If you've been talking with Eric about this then it's very likely the approach you have in mind is sound.

[Eric Wieser]

To elaborate on that idea, the outline was something like

abbreviation representation := G →* (V →ₗ[k] V)

def representation.trivial : representation G k V := 1

def representation.tprod (rV : representation G k V) (rW : representation G k W) :
  representation G k (V ⊗[K] W) :=
{ to_fun := λ g, tensor_product.map (rV g) (rW g), ..sorry}

-- I have no idea what a good name is
def representation.on_monoid_algebra (R : representation G k V) :
  monoid_algebra k G →+* (V →ₗ[k] V) := sorry

/-- notation something like `rV →R rW` -/
structure representation_map (rV : representation G k V) (rW : representation G k W) extends V →ₗ[k] W :=
(map_repr : \forall g x, to_fun (rV g x) = rW g (to_fun x))

[Eric Wieser]

My feeling generally was that this would generate less boilerplate than the equivalent approach with type synonyms

[Oliver Nash]

I think we'll probably want both approaches eventually but I am certain that we'll want something similar to the above whatever we do.

[Frédéric Dupuis]

For what it's worth, I also much prefer this approach over using has_scalar, there are just too many scalar actions around in this context.

[Antoine Labelle]

#13573

[Scott Morrison]

I've defined Rep k G, the category of (bundled) representations of G over k. It seems to be nicely compatible with the new design.

[Scott Morrison]

#13683

[Scott Morrison]

I was pleased to find that verifying it has (co)limits and a natural monoidal structure was very smooth!

[Scott Morrison]

The PR doesn't include preparing the preadditive and abelian instances, but this shouldn't be too hard now.

[Johan Commelin]

Cool! Unfortunately you're hitting a timeout here: https://github.com/leanprover-community/mathlib/pull/13683/files

[Johan Commelin]

I'm still a bit sad that it looks like we can't use scalar multiplication in rep'n theory. But I guess that's life in lean, for now.

[Scott Morrison]

Fixed the timeouts.

[Antoine Labelle]

Nice, that's definitely gonna be very useful! If we prove enough properties of this category we're gonna be able to use category_theory.preadditive.schur, which is great since I'll need Schur's lemma to get to the orthogonality of characters.

[Scott Morrison]

I've added PRs

• #13685: Rep k G is symmetric monoidal
• #13689: Rep k G is abelian

[Scott Morrison]

I guess showing that it is a k-linear category should be done as well (easy?), and also that it is monoidal closed (not sure).

[Antoine Labelle]

For monoidal closed, I think the internal hom should be what I called lin_hom in #13573, and I don't think it should be too hard to prove that it's adjoint to the tensor product.

[Johan Commelin]

Another TODO:

• Equivalence with Module k[G].

[Kevin Buzzard]

Another to-do: Tannakian?

[Johan Commelin]

I've never really dared to say it. But Tannaka duality would be a wonderful milestone.

[Scott Morrison]

I did the equivalence with Module k[G] in #13713. (Still needs some linting, and one declaration is mysteriously incredibly slow; if anyone wants to have a look at counit_iso in src/representation_theory/Rep.lean?)

[Scott Morrison]

This is a bit painful as we have to grapple with all the different actions and fight the typeclass system as we convert between them. But it seems to work out okay.

[Scott Morrison]

I think tannakian (just the fact that Rep G is tannakian, not tannakian duality itself) is probably pretty easy! We'll have the rigid structure soon, and I think we already know that the forgetful functor is monoidal and exact.

[Scott Morrison]

More immediately important is to hook up the existing work on schur's lemma and maschke's theorem, and show Rep k G is semisimple when it is.

[Scott Morrison]

I've added fdRep k G in #13740, which acquires cheaply a rigid structure when G is a group.

[Johan Commelin]

Scott Morrison said:

I think tannakian (just the fact that Rep G is tannakian, not tannakian duality itself) is probably pretty easy! We'll have the rigid structure soon, and I think we already know that the forgetful functor is monoidal and exact.

Maybe we can actually get Tannaka reconstruction fairly quickly in the case of finite groups. After all, the general case requires algebraic groups, and I don't think we are anywhere near those.

[Scott Morrison]

Here's a summary of the current stack of PR's on representation theory.

• Rep k G in #13683
• Rep k G is symmetric monoidal in #13685, depending on a PR about braidings in #13684
• Rep k G is abelian in #13689
• fdRep k G in #13740, depending on #13738 which in turn depends on two PRs about rigid structures in #13736 and #13707.
• Rep k G ≌ Module (monoid_algebra k G) in #13713, depending on refactoring PRs in #13760 and #13759.

[Scott Morrison]

In particular currently needing review are #13683, #13684, #13736, #13707, and #13760. (#13759 is back to me after a helpful review from Eric.)

[Johan Commelin]

@Scott Morrison Thanks for all those PRs. I finally had some time to look at them. They're great.

[Scott Morrison]

Added:

• Rep k G is k-linear and k-linear monoidal, waiting on #13689.

[Scott Morrison]

and

• FinVect k has all finite limits, #13793 depending on #13792

[Scott Morrison]

I'm very satisfied by the last one. We've had Schur's lemma in mathlib for over a year, but stated in maximal generality: it holds for any linear category over an algebraically closed field, with finite dimensional hom spaces, and kernels.

Finally, fdRep k G satisfies those hypotheses, so we can write:

-- Verify that Schur's lemma applies out of the box.
lemma finrank_hom_simple_simple [is_alg_closed k] (V W : fdRep k G) [simple V] [simple W] :
  finrank k (V ⟶ W) = if nonempty (V ≅ W) then 1 else 0 :=
category_theory.finrank_hom_simple_simple k V W

[Antoine Labelle]

That's wonderful! I think we're not very far from the orthogonality of characters, though there's still some linear algebra missing.

[Scott Morrison]

Sometime over the weekend I'll hook up Maschke's theorem with the new setup.

[Scott Morrison]

After that, I think if I keep working on representation theory I might take an excursion into semisimple categories, and decompositions into simple objects.

[Kyle Miller]

For Schur's lemma applied to endomorphisms, there's a generalization due to Dixmier (and generalized further by Quillen) that if you have a simple $A$-module $M$ where $A$ is an algebra over an algebraically closed field $k$, if $|k|>\dim_k(M)$ then $\operatorname{End}_A(M)\cong k$. (If you drop "algebraically closed" then instead the conclusion is that endomorphisms are all algebraic over $k$). For example, the space of endomorphisms of a countable-dimensional simple representation of a group over $\mathbb{C}$ is one-dimensional.

If somebody were to try to formalize this, where would be a good place for it? (still src/category_theory/preadditive/schur.lean?) Potentially it would pull in things about transcendence degree.

[Kevin Buzzard]

For example, the space of endomorphisms of a countable-dimensional simple representation of a group over \mathbb{C}C is one-dimensional.

This result is used in the basic theory of smooth admissible representations of p-adic groups, which we will have all the ingredients for when we've figured out how to do continuous representations of topological groups.

[Scott Morrison]

This would be great to have. If it pulls in transcendence degrees then just make a new file for it.

[Scott Morrison]

Does the proof really use that it is an A-module? I've never looked at these generalisations. Schur's lemma is usually stated for modules, but in fact this is irrelevant for the version in mathlib.

[Kyle Miller]

It seems like it's important that $M$ is an $A$-module, but maybe there's some $k$-linear category trick. There's a step where you give $M$ the structure of a vector space over $k(t)$ using the $A$-module structure. You also need that $M$ is a vector space over $k$ to get its dimension.

Here's the proof I know: Let $f:M\to M$ be an $A$-linear endomorphism. Suppose for sake of contradiction that $f$ is not algebraic over $k$. Then by Schur's lemma, $f$ is an isomorphism since it's not zero. We have that $M$ is a vector space over the field $k(t)$ of rational functions, with $t$ acting by $f$. Since $M$ is nonzero we have $\dim_{k(t)}M\geq 1$, so $\dim_k M \geq \dim_k k(t)$. Since $\{ (t-c)^{-1} \mid c\in k\}\subset k(t)$ is a linearly independent set over $k$ (since, clearing denominators, a linear dependence would be that $t$ is algebraic over $k$), we also have $\dim_k k(t) \geq |k|$. But, we assumed that $|k|>\dim_k(M)$, so we have a contradiction, hence $f$ is algebraic over $k$.

If $k$ is algebraically closed, then you use the minimal polynomial to get an eigenvalue for $f$ and do the usual algebraically closed Schur's lemma proof.

[Scott Morrison]

That proof doesn't actually use the $A$ module structure, I think, just the fact that there is a faithful k-linear functor to k-Vect?

[Kevin Buzzard]

This this is the proof Taylor taught me :-) I thought the 1/(t-c) trick was brilliant.

[Damiano Testa]

That same trick is also used for what I've seen referred to as a "quick and dirty" proof of the Nullstellensatz. You can see the trick in the highest scoring answer here.

[Kyle Miller]

Scott Morrison said:

That proof doesn't actually use the $A$ module structure, I think, just the fact that there is a faithful k-linear functor to k-Vect?

Oh, yeah, that's all you need. I got confused and forgot $f$ was just an endomorphism, so the $A$-module structure is not used. (If $A$ acts on the right, then I like to think of the morphisms as acting on the left since then $fxa$ suggests the usual $af(x)=f(ax)$. The proof only uses the left action by the category and some things about dimension.)

It's interesting how this is true no matter the faithful k-linear functor. Over an algebracially closed field, is it true that there's always one that sends simple modules to 1D vector spaces? I know that's true for semisimple algebras over an algebraically closed field.

[Antoine Labelle]

Hi! I need to talk about equivalence of representations, and I was wondering if I should use for that the isomorphisms provided by the category Rep k G defined by @Scott Morrison or if I should define independently types rep_hom and rep_equiv which would extend linear_map and linear_equiv. I'm not very familiar with how category theory is used in mathlib, so I'd appreciate some advice on this.

[Scott Morrison]

We're potentially on new ground here... I'm tempted to suggest we try and proceed "within" the category theory API for now, and only bail out and define everything "unbundled" as necessary. But we will have to be careful trip interpret "necessary" liberally: the first sign of your theoretic troubles caused by using the category theory library should cause us to retreat.

[Scott Morrison]

But this is only one opinion, and a biased one.

[Scott Morrison]

But I do like the idea of finally being able to stop defining the same basic ideas (isomorphism, etc), and using the polymorphic model provide by category theory. Worth a try, as an experiment?

[Scott Morrison]

This all said, I think most of the future work on representation theory for a while should be developing the representation theory of (finite dimensional) algebras.

[Scott Morrison]

The main representations-of-groups specific fact is already there in maschke.lean, and most of what is needed to hook that up to decomposition into irreducibles and character theory is true more generally.

[Scott Morrison]

I was thinking that perhaps we should just plough through Etingof's notes on representation theory. They are a bit nonlinear, but if we just do whatever subset is on the minimal path to his treatment of representations of finite groups I think we'd get a very pretty, and appropriately generalized, treatment.

[Scott Morrison]

This is actually why I wrote my "simple implies indecomposable" PR last night: it was the first statement I could find in his notes that we didn't have.

[Antoine Labelle]

So far I focused on group representations because my goal was to get orthogonality of characters. I'm not really aware of how character theory generalizes to finite-dimensional algebras, is there a more general version of orthogonality of characters for finite groups?

[Kyle Miller]

Something that comes to mind is finite-dimensional Hopf algebras. These have a one-dimensional space of "integrals" that you can use to generalize averaging-over-the-group arguments. (Group algebras are Hopf algebras, and $\sum_{g\in G}g$ is an integral.) I'm pretty sure these are all you need to get that characters of non-isomorphic simple representations are orthogonal, where you define something like $\langle V, W\rangle = \operatorname{tr}_{V\otimes W^*}(\Delta(\int))$ (the trace of the action of the comultiplication of the integral on $V\otimes W^*$). That can be rewritten in terms of characters for V and W.

The way that formula expands for groups using the un-scaled integral is $\langle V,W\rangle = \sum_{g\in G} \operatorname{tr}_V(g)\operatorname{tr}_W(g^{-1})$, using the fact that $\operatorname{tr}_{W^*}(g)=\operatorname{tr}_{W}(g^{-1})$ (for Hopf algebras in general, the antipode can be used to put things in terms of $\operatorname{tr}_W$)

[Scott Morrison]

even if we don't go via hopf algebras, while orthogonality of characters doesn't hold generally, there are interesting statements. e.g. Theorem 3.6.2 of https://klein.mit.edu/~etingof/repb.pdf

(i) Characters of (distinct) irreducible finite dimensional representations of A are linearly independent.
(ii) If A is a finite dimensional semisimple algebra, then these characters form a basis of (A/[A, A])^∗

[Scott Morrison]

But I guess for just checking orthogonality there's no point knowing anything about the relationship with characters of algebras.

[Scott Morrison]

But the facts the characters span, and determine the representation, come from more general facts, and ideally we would deduce these facts in the Rep G setting from the more general statements.

[Scott Morrison]

but don't hesitate to do whatever work on orthogonality you like

[Scott Morrison]

if we want to relate the characters you define for G and the characters for k[G], we can retrofit that later

[Antoine Labelle]

Anyway for now I've been mostly doing linear algebra and proving stuff about traces of linear maps, which will be useful both for algebras and for groups

[Kyle Miller]

I forget -- do you need anything beyond semisimplicity to get that A/[A,A] is isomorphic to the center Z(A) as a vector space?

[Antoine Labelle]

But I'll try to get more familiar with the category theory API soon

[Junyan Xu]

@Antoine Labelle has open PRs defining several natural maps involving dual modules, contractions and traces (for example), and I am wondering whether all this stuff (including definition of trace) should be rewritten in terms of docs#category_theory.exact_pairing. I'm not suggesting to simply adopt the categorical formalism, but at least we would like to easily convert between both formalisms. And the current definition of trace (which landed in mathlib two years ago #3125) only works for finite free modules, but I think we eventually want it for finite projective modules as well, for K-theory or whatever, and exact_pairing probably offers us greatest generality. I'd appreciate comments from @Scott Morrison on this.

[Scott Morrison]

Yes, I hope this can be aligned as closely as possible, so that "bundling" statements up as statements about rigid categories is as trivial as possible.

[Antoine Labelle]

Is it true that dual_tensor_hom R M N is an equivalence whenever M is a finite projective module?

[Junyan Xu]

I believe so. (Here is a "reference": https://mathoverflow.net/a/156274/3332)

[Junyan Xu]

It seems in the module case, you can derive all isomorphisms involving duals from (module.dual R M) ⊗[R] M →ₗ[R] module.End R M being an isomorphism, which seems a simpler statement than exact_pairing. Is there some advanced theory that I can look into?

[Antoine Labelle]

Can you derive the more general (module.dual R M) ⊗[R] N →ₗ[R] (M →ₗ[R] N) from this?

[Junyan Xu]

It's pretty easy to define Mᵛ → M → (M → N) → Mᵛ ⊗ N which lift to Mᵛ ⊗ M → (M → N) → Mᵛ ⊗ N, and if you have the canonical element in Mᵛ ⊗ M that corresponds to 1 : End M then you get (M → N) → Mᵛ ⊗ N. (I'm using ᵛ to denote the dual; I think this is a common notation but forget where I saw it; Wikipedia uses *.)

[Antoine Labelle]

I see, that's nice!

[Scott Morrison]

The check notation is particularly nice for duals once you reach dagger categories and start interacting with operator algebras. At that point * is so massively overloaded that no one is allowed to use it. :-)

[Junyan Xu]

It seems that the following are all equivalent:
(1) The identity is in the image of the natural map Mᵛ ⊗ M → End M.
(2) M is a rigid object in the category of R-modules, with M and Mᵛ forming an exact_pairing ((1) is basically one of the "triangle" identities saying M → M is id, and the other one follows (the proof invokes extensionality, showing that two linear functionals agree on every element of M, and doesn't seem to follow from axioms of symmetric closed monoidal categories)).
(3) The natural map Mᵛ ⊗ M → End M is an isomorphism (with inverse given by the construction (M → N) → Mᵛ ⊗ N above (also on the Wikipedia page)).
(4) M is a finite projective module (finiteness is trivial; projectivity follows from https://en.wikipedia.org/wiki/Projective_module#Dual_basis, proof).

So we can just work with finite projective modules for maximal generality.
Notice that M → Mᵛᵛ being an isomorphism (M reflexive) is strictly weaker, as M doesn't have to be finite or projective (e.g. the direct sum of countably many Z).

One may be tempted to construct all natural maps involving tensor and Hom and prove identities between them using the axioms of symmetric closed monoidal categories and rigid objects, but that's likely cumbersome (though a ramped up coherence tactic might help); simply using extensionality would be easier: if the identity doesn't involve the inverse of Mᵛ ⊗ M → End M it's probably rfl, but I think we need to figure out a better (and uniform) way to do proofs like this where the inverse is involved.

[Antoine Labelle]

In the categorical language, when the inverse is involved can't we just use docs#category_theory.is_iso.inv_comp_eq to get rid of the inverse, just as I used linear_map.cancel_right when doing these kinds of proofs in the linear algebra language?

[Scott Morrison]

Could I just ping on a few PRs on the #queue: #13713 #13870 #13908 #13967 #13933 (and hopefully #13740, it's just linting now after a merge conflict)?

[Antoine Labelle]

I started trying to work with @Scott Morrison 's Rep k G category, and one issue I noticed is that it assumes that k is a ring (due to Module k assuming a ring), while so far I've tried to only assume semiring when possible. Is there any reason why Module k isn't defined for semirings?

[Antoine Labelle]

I don't know if there's really any interesting case in which we have a semiring which is not a ring, but if there are some things that we can state in this generality I guess that it's better to do so?

[Scott Morrison]

Probably this can be generalized. I suspect that at the time Module was defined the library was less generalized than it is now. If you'd like to have a go at this please do, otherwise I can try soon.

[Scott Morrison]

And yes, I think it's good if results are stated as generally as possible. It seems to pay off later in a mathlib style library. :-) Also often it's helpful for understanding proofs when the hypotheses are as weak as possible --- fewer misleading clues about wrong directions you might take!

[Antoine Labelle]

I tried quickly to check what happens what happens if I replace ring by semiring in Module, and the problem is that we also need to replace add_comm_group by add_comm_monoid for the underlying abelian group of the module, which causes some problems for example in has_forget_to_AddCommGroup since M doesn't have an add_comm_group instance anymore.

[Antoine Labelle]

There's docs#module.add_comm_monoid_to_add_comm_group but it's a def and not an instance so I'm not sure how to use it.

[Scott Morrison]

Okay, I spent a while on this, and I think it is sadly impossible.

[Scott Morrison]

I can get Module/basic.lean to compile, but only be constructing dubious instances, which later break everything.

[Antoine Labelle]

Hm, that's unfortunate...

[Scott Morrison]

I'd been worried that we would need a different Module to handle modules over k-algebras, but so far I can get away with just the one.

[Scott Morrison]

But this seems worse.

[Scott Morrison]

What did you want to do over semirings? Maybe looking at a concrete statement will lead to inspiration. :-)

[Antoine Labelle]

As an example, I was thinking of restating docs#representation.lin_hom in the category theory language using Rep k G. Currently this definition works for semirings, but Rep k G requires a ring.

[Scott Morrison]

I see. It would be nice to construct the closed monoidal instance on Rep k G.

[Scott Morrison]

I propose that for now we just proceed with the restriction that k is a ring in Rep k G...

[Scott Morrison]

I don't think I've ever met someone who does representation theory over semirings.

[Antoine Labelle]

Fair enough

[Scott Morrison]

#13789, #13845, #13933 would like some review, and are on the "representation theory queue", if anyone reading here would like to take a look. :-)

[Scott Morrison]

I'm hoping that soon I will have the equivalence of "is a sum of simple objects" and "every subobject is complemented" in any preadditive category (with a few bits and pieces), and after that the density theorem (the map A ⟶ End V is surjective for any irreducible f.d. representation V of a k-algebra A).

[Antoine Labelle]

I see that we have a right_rigid_category instance for fdRep k G, but we don't have left_rigid_category. This is very annoying since we need the left version in order to get the monoidal_closed structure (docs#monoidal_closed_of_left_rigid_category).
I looked at FinVect and noticed that here also we weirdly only have the right rigid structure but not the left one. Is there any reason for that? If I want to access the monoidal structure of fdRep k G, should I go back to FinVect and add the left rigid structure there, or is it available in another way that I am missing?

[Antoine Labelle]

@Scott Morrison

[Scott Morrison]

I think no good reason this is missing. Maybe it would be nice to show that if you're braided one implies the other?

[Scott Morrison]

Or just do it directly for FinVect.

[Scott Morrison]

The PR that did this was just plugging together immediately available pieces.

[Antoine Labelle]

I don't think we even have that FinVect is braided so for now I think the second option is simpler.

[Antoine Labelle]

Though proving braiding for FinVect shouldn't be too hard. The natural way to do it would be to prove it more generally for docs#category_theory.monoidal_category.full_monoidal_subcategory. By the way, is there a reason why this is not an instance?

[Antoine Labelle]

Ok, so trying to prove that FinVect is symmetric, I figured I should probably use docs#category_theory.braided_category_of_fully_faithful, but for that I need a monoidal version of docs#category_theory.full_subcategory_inclusion. How do I get lean to figure out the monoidal structure on {X : C // P X} here?

def full_monoidal_subcategory_inclusion
  (P : C → Prop) (h_id : P (𝟙_ C)) (h_tensor : ∀ {X Y}, P X → P Y → P (X ⊗ Y)) :
  monoidal_functor {X : C // P X} C := sorry

[Scott Morrison]

I think the best approach here will be to introduce monoidal_subcategory P h_id h_tensor as a synonym for {X : C // P X} and put a monoidal_category instance on that.

[Scott Morrison]

Perhaps even add monoidal_predicate which bundles together P, h_id and h_tensor.

[Scott Morrison]

Does that make sense / seem plausible?

[Antoine Labelle]

Sounds good, done in #14311. Let me know what you think.

[Scott Morrison]

Left a few comments. Mostly looks promising, thanks for doing this!

[Antoine Labelle]

@Scott Morrison What are your thoughts on that comment?

[Scott Morrison]

Yes, this looks good.

[Antoine Labelle]

#13794 (depending on #13789) is all I'm missing to PR a proof of the orthogonality of characters for finite groups. It has been open for a while, so it would be great if it could get merged soonish! If left some comment on #13789.

[Remy van Dobben de Bruyn]

Are there any status updates on this? I had started to work on similar things (Schur orthogonality etc), but I don't want to duplicate efforts, and it seems like most of it has been done already.

[Remy van Dobben de Bruyn]

(deleted)

[Remy van Dobben de Bruyn]

Antoine Labelle said:

#13794 (depending on #13789) is all I'm missing to PR a proof of the orthogonality of characters for finite groups. It has been open for a while, so it would be great if it could get merged soonish! If left some comment on #13789.

(I am also a new user, so maybe I'm doing something wrong, but I think this commit is not in my local copy yet...)

[Alex J. Best]

All those commits are on a branch (branch#orthogonality) which is not yet merged into master so your local version of master won't have them yet.

[Alex J. Best]

It looks like the first thing that needs to happen to get the ball rolling on these again is to fix the merge conflicts in #13789 with master

[Alex J. Best]

I just tried to fix #13789 lets see if the other branches also work now

[Alex J. Best]

Ok and I've merged branch 'semorrison/fdRep-linear' into semorrison/fdRep-schur and it looks like it builds ok, so #13794 will hopefully turn green after a while and be ready for review when the first PR is merged

[Antoine Labelle]

Are there any status updates on this? I had started to work on similar things (Schur orthogonality etc), but I don't want to duplicate efforts, and it seems like most of it has been done already.

Yes, we basically have orthgonality of characters modulo the merging of these old PRs. We don't have yet that the characters span the class functions though, that would be a next natural step.

[Antoine Labelle]

Or incorporating this in a more general setting of representations of algebras.

[Scott Morrison]

Thanks @Alex J. Best for fixing #13789. It's merged now, and I've just updated #13794 (Schur's lemma applies to fdRep) and it looks good. Hopefully someone can approve it shortly.

[Remy van Dobben de Bruyn]

@Antoine Labelle Oh great! Should I pick it up somewhere, or are you rolling with these representations?

[Remy van Dobben de Bruyn]

(Our local Lean workshop is working towards Burnside's p^aq^b theorem, so there are many other parts that I could start working on.)

[Remy van Dobben de Bruyn]

But I love thinking about general finite dimensional representation theory too, so I'm more than happy to dive in here as well.

[Antoine Labelle]

I haven't worked on that for a few months, so feel free to start working on any result that we don't currently have.

[Antoine Labelle]

Let me know if you have any questions on the current API.

[Antoine Labelle]

I've updated #16043, it's now ready to be reviewed.