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.

[Junyan Xu]

It seems that the last thing about representations of finite groups merged into mathlib was this PR #16043 which adds orthonormality of characters, but mathlib still doesn't know that the characters span the space of class functions, and the consequence that there are as many characters as conjugacy classes. Has anyone proved the p^a q^b theorem, no matter in Lean 3 or Lean 4? Maybe progress stalled due to the port.

Has anyone attempted to compute some character tables? Many tables require some induced characters to fill; the concrete definition of induced representations with explicit basis from coset representatives is probably good for computation, while the definition via tensor product is good for proving Frobenius reciprocity (but mathlib's TensorProduct needs a noncommutative generalization). Has anyone worked towards Brauer's theorem on induced characters?

I'm asking because I'm trying to find possible projects in this area for a bachelor student's thesis. I've also found another topic #general > Leiden representation theory project @ 💬 which is also from the Lean 3 era. Is there any activity in the Zulip stream mentioned there?

[Kevin Buzzard]

For me the difficulty with undergraduate representation theory projects is that half of the results we have are about vector spaces with group actions and the other half are shrouded in category theory and are about docs#FDRep . Moving between the two setups is not at all easy because typeclass instances don't round-trip very well

[Yaël Dillies]

Javier's FLT subproject is seemingly plagued with this issue as well

[Andrew Yang]

Is there a reason why representation theory in mathlib is based on category theory and not unbundled like the other algebraic library?
Is it to connect to the homology library better?

[Kim Morrison]

Hmm, I think it is just because I did the early work, and was over-eager to use the category theory library.

[Kim Morrison]

I was quite keen to e.g. use a general theory of semisimple objects, without having separate-but-close definitions for representations of groups and of rings, etc.

[Kim Morrison]

I'm happy to call it a historical mistake? :-)

[Winston Yin (尹維晨)]

How do you propose that mathlib should proceed with developing representation theory? Would you oppose a parallel, more concrete approach? Coming from physics, I’m always excited to see more representation theory, but I have not been able to help develop or make effective use of the current library.

[Winston Yin (尹維晨)]

Once upon a time I asked this and got the response from somebody that category theory is “the right way” to do things. I couldn’t tell if that was said partly in humour or based on valid design considerations, so I’d like to ask again.

[Dean Young]

I would like to lobby for the representation theory of 𝔰𝔲(2) to be studied, maybe culminating in the theorem that demonstrates self-duality for SU(2)-representations. It could be a good foot in the door.

There is also a mysterious and deep analogy with Pontrjagin duality in its relation with S¹, the unit ball in ℂ; SU(2) is the unit ball in the quaternions and is simply connected so determined by the Lie-algebra structure via the Lie-algebra functor using precomposition with the exponential map of a Lie group.

[Kevin Buzzard]

Right now here is the car crash that is representation theory in mathlib:

import Mathlib

-- How do we do "a representation of the group G on a k-vector space"?
variable (k G : Type) [Field k] [Group G]

-- non-category method via typeclasses
variable (V : Type) [AddCommGroup V] [Module k V] [DistribMulAction G V]
  [SMulCommClass k G V]

-- non-category method via Representation
variable (V' : Type) [AddCommGroup V'] [Module k V'] (ρ : Representation k G V')

-- non-category method via k[G]-modules
variable (V'' : Type) [AddCommGroup V''] [Module (MonoidAlgebra k G) V'']
  [Module k V''] [IsScalarTower k (MonoidAlgebra k G) V'']

-- category method via Rep
variable (𝓥 : Rep k G)

-- category method via FDRep
variable (𝓥' : FDRep k G)

Perhaps the community needs to make a decision on which of the five choices we have should be built upon in order to prove something like the $p^aq^b$ theorem (or, more ambitiously, to get AI to formalise the classification of finite simple groups).

The reason that FDRep is a thing is that bare representation theory of a group is not really a thing beyond the case of finite groups. This is not entirely true, there some countable groups which people study bare representations of (although I don't know if people study infinite-dimensional representations of them). The moment one goes to infinite groups one typically has a topology (Galois groups, Weil groups, Lie groups, locally profinite groups are four examples which spring to mind immediately) and one only studies representations which are continuous in some appropriate sense. And there's a rich theory of representations of Lie algebras (as Elliot mentions above), but Lie algebras aren't groups so the axioms are a bit different.

[Johan Commelin]

/poll Which of Kevin's approaches do you like best?

• non-category method via typeclasses
• non-category method via Representation
• non-category method via k[G]-modules
• category method via Rep
• category method via FDRep

[Oliver Nash]

Maybe worth a bit commentary. Off the top of my head I'd probably say:

• Use "non-category method via typeclasses" when you want to develop theory wrt a single fixed rep (this should be the default)
• Use "non-category method via Representation" when you need to make statements that involve several representations (e.g., the number of irreps of a finite group is number of conjugacy classes)
• Have instances to use "non-category method via k[G]-modules" internally in a proof (e.g., if want to use some theory of simple modules) but never make statements in this language
• Use "category method"(s) when you actually want to apply it as a tool and / or study this category as a thing in its own right

[Jan Grabowski]

I feel like my instinctual answer (an option 6, using the category of k[G]-modules) is being quite strongly influenced by both personal preferences and it being unclear whether we expect developments after this point to be applicable outside the realm of group representation theory. If/when we want to build tools that we can use for representation theory of algebras, I would argue for a categorical approach. But (a) it seems from a glance at the thread (but not a careful read of it all) that there is a specific group-theoretic aim to this project and (b) it reminds me slightly of Oliver's talk on root systems (as in "we'll know the right definition when several other versions have failed to work").

[Kim Morrison]

I agree very much that one should develop the basic theory of representations of (finite-dimensional) algebras, and then leverage that as much as possible via k[G].

[Kim Morrison]

When I was doing rep theory years ago in Lean I was intending to follow Etingof's book along these lines.

[Johan Commelin]

Oliver Nash said:

• Use "non-category method via Representation" when you need to make statements that involve several representations (e.g., the number of irreps of a finite group is number of conjugacy classes)

I don't understand this one. Would you mind elaborating please?
I would expect your example statement to go via isomorphism classes, and hence categorical language.

[Kevin Buzzard]

I feel like my instinctual answer (an option 6, using the category of k[G]-modules)

Darn it, I thought I had them all!

-- category method via k[G]-modules
variable (𝓥'' : ModuleCat (MonoidAlgebra k G))

Thanks @Jan Grabowski ! I added it to the list of options.

[Jan Grabowski]

Also, as a side note, my experience of teaching rep theory of finite groups - including up to Burnside's $p^a q^b$ theorem - was that at some point it felt like there was a branching off. One direction was about categories, modules, extensions etc. (what I would somewhat loosely call "representation theory") and the other was characters ("character theory" :smile: ). The notes I have, based on James--Liebeck, suggest that you need very little representation theory in this sense for Burnside's theorem - algebraic integers, orthogonality of characters, a smidge of Sylow theory. Despite voting for #6 (obvs), I am not at all certain this is going to be the most helpful way of getting to that particular result and may indeed get in the way.

[Kevin Buzzard]

Oh here's a 7th option:

variable (V : Type) [AddCommGroup V] [Module k V] [DistribMulAction G V]
  [SMulCommClass G k V]

(the SMulCommClass input got permuted). Turns out that docs#SMulCommClass.symm isn't an instance so this is a genuinely different set-up.

In representation theory people usually put a $G$-action on $Hom_k(V,W)$ via $(gf)(v)=g(f(g^{-1}v))$ but this is not the default action of G on V →ₗ[k] W.

[Anatole Dedecker]

I will read this whole discussion more carefully later, but please keep in mind that whatever method is chosen needs to be able to be enriched with topology at some point (both for the group and the vector space). I’m naturally leaning towards the smul definition precisely for that reason: we already have the corresponding continuity assumption as docs#ContinuousSMul

[Kevin Buzzard]

Another issue with the SMulCommClass approach is that it's probably difficult to do things like work with two 1-dimensional representations where we would probably have V = k but two different actions of G. The Representation approach avoids this.

[Joël Riou]

I would like to point out that there is an issue with the "category method with ModuleCat". The category of representations can be thought as the category of k[G]-modules, but this is not compatible with the tensor product, because the tensor product of representations is given by the tensor product of the underlying k-modules, not by the tensor product of k[G]-modules (which is not defined anyway unless G is commutative). Then, categorywise, we need to use a different name.

[Johan Commelin]

Kevin Buzzard said:

Another issue with the SMulCommClass approach is that it's probably difficult to do things like work with two 1-dimensional representations where we would probably have V = k but two different actions of G. The Representation approach avoids this.

This is a good observation. But I feel like as soon as we migrate to V = k, then we are in pretty special territory and we might want special API for that case anyway. So it might as well get a separate name.
For example, there will be quite some overlap with MulChar. (And maybe we can even reuse it?)

[Jan Grabowski]

@Joël Riou I'm confused by something in your comments - quite possibly it's flagged a mathematical subtlety I've not thought about carefully enough.

The group algebra is a Hopf algebra, with the diagonal coproduct, and this makes its module category a monoidal category (whether G is Abelian or not). Are you saying this is somehow not compatible with a tensor product of representations?

[Jan Grabowski]

Responding to the 1-dimensional case, surely we'll want to be able to handle e.g. the regular representation of a finite Abelian group, wherein several different 1-dim reps will be needed, at the same time?

Edit: what I was thinking but probably didn't manage to say clearly was that I didn't quite understand the rationale for a special API, since having multiple 1D reps around is not exactly rare.

(Do we have an emoji for "treat my posts as essentially uninformed speculation as to what might be a better choice for formalization, and thank you for your patience"? :face_with_spiral_eyes:, maybe?)

[Jan Grabowski]

(Noting indeed that MulChar is relevant! And with apologies for lack of formatting, due to incompetence...)

[Kevin Buzzard]

I would imagine that the Hopf algebra tensor product is exactly the representation tensor product (but I didn't check). What Joel is saying is that if G is abelian then we may already have a tensor product on ModuleCat k[G] and it will be the wrong one.

[Edward van de Meent]

I'm a bit late to this conversation, but I'd like to point out that for the non-cat type class Vs Representation discussion, a similar (I think?) decision was made for docs#Algebra (as evidenced by the module doc string)

[Dean Young]

Do these plans intend to incorporate Lie groups or the Peter-Weyl theorem? Representations for those are continuous.

[Kevin Buzzard]

I think that right now we're figuring out how to do representations, and we're hoping that we'll be able to add continuous representations later (e.g. with ContinuousSMul).

[Antoine Chambert-Loir]

Juste a note that continuous representations of a topological group on a topological vector space will fit ContinuousSMul but won't coincide with continuous morphisms from the group to the group of continuous automorphisms of the topological vector space.

[Dean Young]

@Antoine Chambert-Loir did you mean 'to ...' (emphasis added) (ellipsis added)

[David Michael Roberts]

Dean Young said:

S¹, the unit ball in ℂ; SU(2) is the unit ball in the quaternions

Did you mean 'unit sphere's?

[Johan Commelin]

The poll from Feb 10 over [here, broken link check below] was quite strongly in favour of a "maximally unbundled" approach. I'm going to attempt a refactor of the library in that style.

[Yaël Dillies]

(the link is broken)

[Johan Commelin]

#maths > Representation Theory @ 💬

[Johan Commelin]

I am proposing the following definition

/-- A representation of `G` on the `k`-module `V` is TODO. -/
class Representation (R G V : Type*)
    [CommSemiring R] [Monoid G] [AddCommMonoid V] [Module R V] [DistribMulAction G V]
    extends Module (MonoidAlgebra R G) V,
      SMulCommClass R G V, IsScalarTower R (MonoidAlgebra R G) V where
  single_one_smul (R) : ∀ g : G, ∀ v : V, single g (1:R) • v = g • v

namespace Representation

variable (R G V : Type*)
variable [CommSemiring R] [Monoid G] [AddCommMonoid V] [Module R V]
variable [DistribMulAction G V] [Representation R G V]

instance : SMulCommClass G R V := SMulCommClass.symm R G V

@[simp]
protected lemma single_smul (g : G) (r : R) (v : V) :
    single g r • v = g • r • v := by
  rw [smul_comm g, ← single_one_smul R g v, ← smul_assoc, MonoidAlgebra.smul_single', mul_one]

instance : SMulCommClass R (MonoidAlgebra R G) V where
  smul_comm x y v := by apply y.induction_on <;> simp [smul_comm x]

instance : SMulCommClass (MonoidAlgebra R G) R V := SMulCommClass.symm R (MonoidAlgebra R G) V

noncomputable
def mk_of_action (k G V : Type*) [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V]
    [DistribMulAction G V] [SMulCommClass k G V] [SMulCommClass G k V] :
    Representation k G V where
  smul x := lift k G (Module.End k V) (DistribMulAction.toModuleEnd k V) x
  one_smul v := by simp [(· • ·)]
  mul_smul := by simp [(· • ·)]
  smul_zero := by simp [(· • ·)]
  smul_add := by simp [(· • ·)]
  add_smul := by simp [(· • ·)]
  zero_smul := by simp [(· • ·)]
  smul_assoc x y v := by
    have := map_smul (lift k G (Module.End k V) (DistribMulAction.toModuleEnd k V)) x y
    apply_fun (· v) at this
    rwa [LinearMap.smul_apply] at this
  single_one_smul g v := by
    have := MonoidAlgebra.lift_single (DistribMulAction.toModuleEnd k V) g (1:k)
    apply_fun (· v) at this
    rwa [one_smul, DistribMulAction.toModuleEnd_apply, DistribMulAction.toLinearMap_apply] at this

open MonoidAlgebra (of) in
noncomputable
def mk_mulAction_of_module (R G V : Type*) [CommSemiring R] [Monoid G] [AddCommMonoid V]
    [Module R V] [Module (MonoidAlgebra R G) V] [IsScalarTower R (MonoidAlgebra R G) V] :
    DistribMulAction G V where
  smul g v := of R G g • v
  one_smul v := show of R G 1 • v = v by simp only [map_one, one_smul]
  mul_smul g h v := show of R G (g * h) • v = of R G g • (of R G h • v) by
    simp only [map_mul, mul_smul]
  smul_zero g := show of R G g • (0 : V) = 0 by simp only [smul_zero]
  smul_add g v₁ v₂ := show of R G g • (v₁ + v₂) = of R G g • v₁ + of R G g • v₂ by
    simp only [smul_add]

open MonoidAlgebra (of) in
def mk_of_module (R G V : Type*) [CommSemiring R] [Monoid G] [AddCommMonoid V] [Module R V]
    [Module (MonoidAlgebra R G) V] [IsScalarTower R (MonoidAlgebra R G) V] :
    letI : DistribMulAction G V := mk_mulAction_of_module R G V
    Representation R G V :=
  letI : DistribMulAction G V := mk_mulAction_of_module R G V
  { smul_comm r g v := by
      show r • of R G g • v = of R G g • (r • v)
      rw [← algebraMap_smul (MonoidAlgebra R G) r v, ← smul_assoc, ← smul_assoc,
        smul_eq_mul, ← Algebra.commutes, ← smul_eq_mul, algebraMap_smul]
    single_one_smul g v := rfl }

end Representation

[Johan Commelin]

If this design isn't torn apart, then I will start building instances for $\otimes$, internal Hom, and add the notion of morphisms and subrepresentations.

[Johan Commelin]

And then there are a few results on characters that can be carried over.
Finally, we should connect this unbundled approach to the category theory files, of which there are a few.

[Kevin Buzzard]

I could imagine informally that there are examples where $G$ acts on $R$ both trivially and nontrivially (for example a finite group can act on $\mathbb{C}$ in more than one way). That's my reservation about making Representation a class.

[Johan Commelin]

Fair enough. But I wonder if those non-trivial actions should use a type synonym.

[Kevin Buzzard]

So you would make an instance of Representation R G R with the trivial action?

[Johan Commelin]

Yes

[Kevin Buzzard]

So then every group would act trivially on every ring in mathlib?

[Johan Commelin]

Ouch, I hadn't thought about that yet :oops:

[Johan Commelin]

Even worse: every monoid on every comm-semiring...

[Adam Topaz]

I haven’t been following this discussion too closely. What’s the issue with just using Module (MonoidAlgebra ..) ..?

[Johan Commelin]

And derive things like [SMul G V] from that?

[Johan Commelin]

I was worried that would lead to diamonds... I think we want to be able to write g \bu v, and not only of R G g \bu v.

[Adam Topaz]

Or just make up some new notation for conveniently talking about elements of G acting on V.

[Johan Commelin]

But you want to rw [mul_smul] and things like that... I guess.

[Adam Topaz]

docs#mul_smul

[Adam Topaz]

Ok, yeah such things would only work after breaking up the mul in the monoid algebra.

[Kevin Buzzard]

[Module (MonoidAlgebra...] will also not allow you have to two actions of G on k

[Adam Topaz]

Yeah I agree. I think we should just bundle and call it a day.

[Anatole Dedecker]

Here’s a wild suggestion which has been on my mind for a while, and that I want to at least mention.

It seems to me that, in informal maths, people really like naming their actions. This is already the case for some group actions (e.g the one by conjugation), but for representations I would say this is even more common (or at least in the areas I’ve been in contact with). Is there a way that we can turn docs#SMul into a « there is a canonical action denoted in the usual way », but develop the whole theory for named actions ?

To be clear I know this is quite far from anything we've done, and I expect their are some insurmountable issues. But I would really like to be able to talk about both the left and right regular representation of a (discrete) group $\Gamma$ on the same type $\ell^2\Gamma$…

[Yaël Dillies]

Anatole, I had the suggestion to make notation for the case of action by a type synonym. For example, docs#translate could (almost) be defined by translate a f := DomMulAct.mk a • f (it's instead equal to DomMulAct.mk (-a) • f, but I still believe we could change it)

[Yaël Dillies]

So my idea would be:

• Stick to SMul as it is today
• If you want a different action than the canonical SMul G Xone, define a type synonym Foo G and provide SMul (Foo G) X
• If you want nice •-like notation, define it by doing something like g •Foo x := Foo.mk g • x

[Yaël Dillies]

Eg this is what the RightActions scope does for you in the case of Foo := MulOpposite

[Anatole Dedecker]

But in the context of representation theory the type alias would be on the acted on side right ?

[Yaël Dillies]

What's the reasoning that brings you to this conclusion?

[Anatole Dedecker]

I don’t have a complete argument (and I have to leave the discussion for now), but it feels weird to me to change the group when you are studying the representations of a fixed group.

[Antoine Chambert-Loir]

If a monoid has a left and a right action on a type X, it will be painful to have to write everytime g • x for the left one, and toRight g • x for the other one, but one could imagine that some notation makes this simpler, such as g •ₗ x and g •ᵣ x, and why not x •ᵣ g.
Especially when X can be G itself.

[Antoine Chambert-Loir]

It could be an interesting test of what notation works if one tries to formalize the statement and the main steps of the proof of the Skolem-Noether theorem.

[Yaël Dillies]

Antoine Chambert-Loir said:

If a monoid has a left and a right action on a type X, it will be painful to have to write everytime g • x for the left one, and toRight g • x for the other one, but one could imagine that some notation makes this simpler, such as g •ₗ x and g •ᵣ x, and why not x •ᵣ g.
Especially when X can be G itself.

import Mathlib

open scoped RightActions

variable {M : Type*} [Monoid M]

example (a b : M) : a •> b = a * b := rfl
example (a b : M) : a <• b = a * b := rfl

[Jester Cabading]

Hi there.
I am currently working on a project of formalizing math to add to mathlib and my supervisor wants me to add Artin's theorem.
I just wanted to ask: has that already been done or is someone already working on it?

[Kevin Buzzard]

Can you state the theorem? The Artins have proved lots of theorems.

[Artie Khovanov]

I am working on formalising a theorem of Artin (and Schreier) but I doubt it's the same one :upside_down:

[Jester Cabading]

It states that a character on a finite group is a rational linear combination of characters induced from all cyclic subgroups of the group

[Jester Cabading]

This one:
https://en.wikipedia.org/wiki/Artin%27s_theorem_on_induced_characters

[Kevin Buzzard]

I'd rather see Brauer's theorem (the integral version) formalised as I need this for FLT!

[Raghuram]

Johan Commelin said:

I am proposing the following definition
...

Has this gone any further than here?

[Raghuram]

Anatole Dedecker said:

Is there a way that we can turn docs#SMul into a « there is a canonical action denoted in the usual way », but develop the whole theory for named actions ?

BTW regarding this, how about adding notation a •[rho] b (and similarly for the "sided" notations in the RightActions namespace scope) where rho is simply the instance of SMul? Then the difference between defining a canonical and a named action is just instance vs def, and similarly while specifying it (this does require a coercion from any class for which one uses names instead of instances to SMul). If this (or allowing that coercion) is too "invasive", it could be scoped to a namespace (say NamedActions) and only for a more special class such as Representation.

[Johan Commelin]

@Raghuram Thanks for asking! I've been convinced by Kevin Buzzard and Amelia Livingston that the current setup is the best option we currently have/know.
And the whole pipeline of PRs that Amelia has lined up is a proof that the current setup can be made to work quite well!

[Raghuram]

Thanks for your reply. I have a couple of questions:

• Which interface does "current setup" refer to? Representation (as a non-typeclasse?), Module-DistribMulAction-SMulCommClass, Rep, FDRep or ModuleCat (MonoidAlgebra ..)?
• Is this the sequence of PRs you're referring to?

[Johan Commelin]

Indeed, that's the list of PRs. And they're mostly in terms of Rep.

[Jester Cabading]

I know that mathlib already has charcters of a group representation defined, but is there a way to take all the irreducible characters of a group? I'm trying to define virtual characters and need to take the free abelian group generated by all such characters.

[Kevin Buzzard]

There are several ways to write down the character of a group representation. When you say you know mathlib has them, what exactly did you have in mind? Can you write some fully working code?

There are several ways to do representation theory in mathlib. Have you thought about which way is best suited for your application?

[Jester Cabading]

I guess what I mean is I want to be able to take the set of all irreducible representations of a group, not just define a particular representation/character

[Kenny Lau]

Jester Cabading said:

I guess what I mean is I want to be able to take the set of all irreducible representations of a group, not just define a particular representation/character

is it a set?

(this is not just some off-hand comment, it's a really nasty fact that it isn't a set, and you have to do some arbitrary constructions here; it will either live one universe higher, or you'll end up with something that is horrible in some way)

[Kenny Lau]

I looked at the library and it doesn't seem like they defined what it means to be irreducible

[Raghuram]

Kenny Lau said:

is it a set?

One could consider the set of irreducible quotients of the regular representation, maybe.

[Junyan Xu]

If you work with k-representation of a finite group G with (|G|, char k) = 1 then you can take all docs#isotypicComponent of the k[G]-module k[G] and choose a simple submodule from each of them ...

[Junyan Xu]

One could consider the set of irreducible quotients of the regular representation, maybe.

Yeah this is more general, and mathlib knows docs#isSimpleModule_iff_quot_maximal
It's still possible that different maximal (left) ideals give rise to isomorphic simple modules, so you need to take a quotient of the type of maximal ideals.

[Kenny Lau]

@Jester Cabading here's a mathematically correct definition that you shouldn't use:

import Mathlib.RepresentationTheory.Rep

universe u

variable (k G : Type u) [CommRing k] [Monoid G]

open CategoryTheory

def irreps : Type (u + 1) :=
  { x : Skeleton (Rep k G) // ∀ W : Submodule k ((fromSkeleton _).obj x).V,
      (∀ g : G, W ≤ Submodule.comap (((fromSkeleton _).obj x).ρ g) W) →
      W = ⊥ ∨ W = ⊤ }

[Kenny Lau]

but you would essentially want to do something like that, possibly with modification as suggested by the other helpful users above

[Kenny Lau]

here's one implementation decision that you'll have to make @Jester Cabading: We currently have Rep.equivalenceModuleMonoidAlgebra saying Rep k G ≌ ModuleCat (MonoidAlgebra k G), so from this point onwards you need to decide whether you want to use Rep k G or whether you want to use ModuleCat (MonoidAlgebra k G). The two definitions Junyan linked to above are for modules, not reps, and afaik they haven't been translated to the language of reps

[Jester Cabading]

I still have to figure out the stuff about universes because I don't understand why the irreducibles have to live in a higher universe, but thank you for the help

[Kevin Buzzard]

Kenny is just pointing out an analogue of the observation that the collection of all groups of order 1 isn't a set because it's "too big to be a set".

[Jester Cabading]

I see.
However, if I'm talking about a particular finite group, all its irreducible k-linear representations would be finite right?

[Kenny Lau]

@Jester Cabading the set of all finite dimensional R-vector spaces is still not a set

[Kenny Lau]

you've confused yourself by taking equivalence classes

[Kenny Lau]

when you use i-forgot-the-name's theorem to make a neat square of irreps and conjugacy classes, you're looking at equivalence classes of irreps

[Kenny Lau]

hmm, gpt says there's no name for that theorem

[Kevin Buzzard]

Jester Cabading said:

I see.
However, if I'm talking about a particular finite group, all its irreducible k-linear representations would be finite right?

It looks like Lean's definition of "equal" is different to yours, probably that's where the problem lies. If I have a vector space V with an action of G, and then I make a new vector space by choosing an element v, removing that element from V, and adding a completely different element v' instead, giving a (different?) vector space V', and then I let G act on this new vector space V' by saying that it acts on all the other elements of V in the same way, and it acts on v' the way the old representation acted on v, would you say that V and V' were equal? Or would you say that they were isomorphic? And when you talk about "all" the irreducible reps of a group, do you mean that two representations are different if they are not equal or if they are not isomorphic? Welcome to formalization :-)

[Jester Cabading]

From what I've interpreted so far: in my head I'm thinking about isomorphism classes of representations, but when I work with lean I have to treat it differently?

[Kenny Lau]

what you said right now is correct, when you work with lean you have to always remember that they are isomorphism classes, and two reps that are isomorphic are not "equal"

[Kenny Lau]

what went wrong earlier was when you assumed that they were "equal" instead of "isomorphic"

[Kevin Buzzard]

Right, there's certainly a finite set of isomorphism classes, but Lean has two different symbols for isomorphism and for equality, that's all, they're different things. This is completely irrelevant to what you want to talk about, it's just that formalization forces you to be very precise.

[Kenny Lau]

i gave you the code above which is one translation that is mathematically correct, but that's definitely not the only translation, and definitely not the best translation

[Kenny Lau]

so when you're formalising, you also have to always bear in mind that there is more than one way to translate something

[Antoine Chambert-Loir]

This is not a problem in formalization, but a problem in mathematics. Here is a copy of the a page in Bourbaki's Algebra 8 volume, showing how this question can be taken care of in “standard” math.
image.png

[Jester Cabading]

So in defining the representation ring of a finte group G (I don't think it's in mathlib yet), I think I would have to state it as the free abelian group generated by the set of isomorphism classes of irreducible representations

[Antoine Chambert-Loir]

More or less, depending on what you mean with “set of isomorphism classes of irreducible representations”, which, itself depends on what you mean with “isomorphism classes”. If you mean that an isomorphism class is the set of all representations isomorphic to a given one, then there is no such set. But it is true (and a theorem, not a too difficult one) that there exists a set, all of whose elements are irreducible representations, such that any irreducible representation is isomorphic to exactly one of them.

[Kenny Lau]

Jester Cabading said:

So in defining the representation ring of a finte group G (I don't think it's in mathlib yet), I think I would have to state it as the free abelian group generated by the set of isomorphism classes of irreducible representations

What I've been trying to say to you is that you first need a good definition for "set of isomorphism classes of irreducible representations"

[Kenny Lau]

there are at least 5 ways to do it (don't quote me on this)

[Jester Cabading]

good I understand what to do now or at least start working on

[Kenny Lau]

the first decision that you need to make, which I've mentioned above (and you seem to have ignored), is this: you need to choose between Rep k G and k[G]-Module

[Kevin Buzzard]

And Representation k G V

[Jester Cabading]

I understood that part

[Kevin Buzzard]

docs#Representation

[Antoine Chambert-Loir]

this latter type is not very useful in this context because it takes an additional argument (the space on which it acts).

[Kenny Lau]

Rep k G and ModuleCat k[G] are bundled versions of Representation k G V and Module k[G] V respectively

[Kenny Lau]

"bundle" here meaning that V has been hidden away under it

[Antoine Chambert-Loir]

You can take the subtype of Rep k G consisting of irreducible representations, quotient by isomorphism, and you will get a type on which you can construct your representation ring. However, if k G : Type u, this will be Type (u+1) (probably bad design here, we need k to live in its universe, and to be Small.{u}) and your representation ring will be too. However, you can show that it is small and then define IrredRep k G : Type u to be its docs#Shrink.

[Antoine Chambert-Loir]

(Terminology: why naming it docs#Rep and not RepCat?)

[Antoine Chambert-Loir]

The other option (at least as soon as one does not discuss continuous representations of topological groups) to define the type of irreducible representations would be to note (as done above) that they have a model as a quotient of the group algebra, leading to a type IrredRep which naturally belongs to the same universe as G. Then, a theorem will prove that any irreducible representation, wherever universe it lives in, will be isomorphic to exactly one of those of that type IrredType.

[Kenny Lau]

Here's a terrible idea:

1. Let S be the set of maximal submodules of k[G] (it is really a set!).
2. Form the k[G]-module that is the direct product of k[G]/M across M in S.
3. Take the equivalence class of irreducible submodules of that big module.

Now given M irreducible:

4. For each x in M non-zero, let Ann(x) be { r : k[G] | r x = 0 }, then it is a maximal submodule.
5. Define the following map from M to that big module:
6. uh actually idk how to make this work maybe other people will have worse ideas, i give up lol

[Jester Cabading]

For some group/monoid G, I was told to try taking the disjoint union of all Hom(G, GL_n(k)) or Hom(G, End(k^n)) ranging over all natural n then modding by isomorphism to define the "set of all isomorphism classes of finite dimensional k-linear representations".
I wanted to ask if this makes sense since it's different from all the suggestions above.

[Kenny Lau]

sounds good to me

[Kevin Buzzard]

Yes that's a great idea because it avoids all the foundational difficulties.

[Anatole Dedecker]

Really any construction is fine as long as you have the proper API. What I would expect is:

• the type should live in the same universe as the group (okay maybe the field has to come into play, but no +1). Otherwise we’re losing some (admittedly rarely useful) mathematical content.
• I really don’t think any of this is specific to finite groups, right?
• there should be a function building an element given an arbitrary irreducible representation, and a lemma that two representations give equal elements iff they are isomorphic.
• there should be a way to get back a representation from an element. This is not generally how we use quotients, but in this case mathematicians really pick representatives all the time (a bit like for L^p spaces, see docs#MeasureTheory.AEEqFun.instCoeFun) so it makes sense to have it.

[Antoine Chambert-Loir]

What is definitely specific to finite groups is that irreductible representations are finite dimensional.

[Anatole Dedecker]

Sure, but the construction of the irreducible dual can be done just once for all groups (and indeed, even for all algebras instead of the ones associated with groups), so I claim we should work in this generality from the beginning.

[Jester Cabading]

I'm not entirely sure how to do finite direct sums on lean; I'm trying to take k^n for some field k

[Kenny Lau]

Jester Cabading said:

I'm not entirely sure how to do finite direct sums on lean; I'm trying to take k^n for some field k

either Fin n -> k or Fin n \->\0 k

[Kenny Lau]

personally i prefer the former

[Jester Cabading]

does this have the structure of a vector space?

[Jester Cabading]

in Lean

[Kenny Lau]

Jester Cabading said:

does this have the structure of a vector space?

of course

[Kevin Buzzard]

Jester Cabading said:

does this have the structure of a vector space?

You don't need to ask -- you can just check yourself:

import Mathlib

variable (k : Type) [Field k] (n : ℕ)

#synth Module k (Fin n → k) -- succeeds

[Jester Cabading]

thank you; I wasn't aware of #synth

[Jester Cabading]

How can we take infinite sum types? I wanted to take the disjoint union stuff indexed by all the natural numbers

[Aaron Liu]

What do you want to union?

[Aaron Liu]

The dependent sum type is docs#Sigma

[Jester Cabading]

I wanted to take the union of all Hom(G, End(k^n)) for all natural N

[Jester Cabading]

I mean all natural n

[Aaron Liu]

that would be done with docs#Sigma (disjoint union of sets types)

[Jester Cabading]

I don't understand how to do disjoint unions with Sigma types

[Kenny Lau]

Jester Cabading said:

I don't understand how to do disjoint unions with Sigma types

import Mathlib.Algebra.Module.Equiv.Defs
import Mathlib.Algebra.Module.LinearMap.End
import Mathlib.Algebra.Module.Pi

universe u v

variable (G : Type u) [Monoid G] (k : Type v) [CommSemiring k]

def Rep.Bound : Type (max u v) :=
  Σ n : ℕ, G →* ((Fin n → k) →ₗ[k] (Fin n → k))

[Kenny Lau]

@Jester Cabading Sigma types are explained in 7.1 in MiL. I would highly recommend reading the book.

[Jester Cabading]

thank you; I may also have sort of skipped that part in chapter 7

[Jester Cabading]

definitely looking into it more now

[Jester Cabading]

I don't know where I can find in mathlib that linear equivalences of modules form a group under composition which I'm pretty sure is true

[Kenny Lau]

Jester Cabading said:

I don't know where I can find in mathlib that linear equivalences of modules form a group under composition which I'm pretty sure is true

import Mathlib

#synth Group ((Fin 3 → ℝ) ≃ₗ[ℝ] (Fin 3 → ℝ))

[Jester Cabading]

Are there specific steps necessary to define a structure on a quotient type? I want to show that the representation ring is a semiring but I was told that I have to be careful because its elements are equivalence classes and not actually representations.

[Kenny Lau]

@Jester Cabading yes, please use Quotient.lift instead of Quotient.out to define the functions

[Jester Cabading]

Do we have a notion of a direct sum of 2 representations? I know we have the tensor product but I cannot seem to find a direct sum.

[Kevin Buzzard]

We have many ways of talking about representations, your question would be easier to answer with a #mwe . Perhaps the answer is V × W and if it isn't then could you ask your question in code rather than in informal language?

[Jester Cabading]

How do we say in lean that 2 k-modules M and N are isomorphic?

[Aaron Liu]

You give the k-linear equivalence between them

[Aaron Liu]

a #mwe would be very helpful

[Aaron Liu]

but without any other context I would say M ≃ₗ[k] N

[Jester Cabading]

Is that not a type?
Also I'm not sure what to even type so I can't really show a #mwe

[Jester Cabading]

Aaron Liu said:

You give the k-linear equivalence between them

I want to say there exists a k-linear equivalence but don't really necessarily know what it is.

[Aaron Liu]

Jester Cabading said:

Aaron Liu said:

You give the k-linear equivalence between them

I want to say there exists a k-linear equivalence but don't really necessarily know what it is.

What's the context for this? Usually you want to know which k-linear equivalence you have.

[Jester Cabading]

I want to prove the following:
Given representations (x1 x2 y1 y2 : Rep k G), (x1 isomorphic to x2), (y1 isomorphic to y2),
then (x1 + y1) is isomorphic to (x2 + y2)

[Jester Cabading]

Where by + I mean direct sum

[Aaron Liu]

So clearly you do want to know the specific isomorphism here

[Aaron Liu]

there are a lot of ways you can state this one

[Aaron Liu]

you would not need to use Rep if it was a theorem about k-modules so why are you using Rep here?

[Jester Cabading]

I wanted to restate representations as k[G]-modules because I think it would be easier to deal with, but also prove things for rep theory

[Aaron Liu]

so it depends on what you're using it for but given no additional information I would state this using the category theory

[Jester Cabading]

Some extra information: I ultimately want to define the representation ring which consists of equivalence classes of representations. To define the sum as the direct sum, I believe I have to show that it's independent on choice of representative.

[Aaron Liu]

which direct sum are you using?

[Jester Cabading]

For k[G]-modules V and W, V \times W

[Aaron Liu]

docs#LinearEquiv.prodCongr

[Jester Cabading]

thank you

[Weiyi Wang]

(sorry if this is off-topic. I just started learning a little bit of representation theory and this thread happens to be named the same)
Does anyone know what this comment in 1000.lean is referring to? https://github.com/leanprover-community/mathlib4/blob/master/docs/1000.yaml#L639

title: Maschke's theorem
# RepresentationTheory/Maschke comes very close, but doesn't prove the standard form yet...

To my untrained eyes, https://leanprover-community.github.io/mathlib4_docs/Mathlib/RepresentationTheory/Maschke.html seems to be already a full formalization to Maschke's theorem comparing to other material I am reading about the theorem. What is the "standard form" referring to here?

[Jester Cabading]

I have the following definition in terms of functions, but I want to make them into morphisms of their respective objects (first is monoid homomorphism then the second is linear maps). How would I go about doing this?

import Mathlib
open Rep
universe u
variable (k G : Type u) [CommSemiring k] [Monoid G] (x y : Rep k G)

/- Direct sum of representations -/
noncomputable def Rep.dsum :
    G → (x.ρ.asModule × y.ρ.asModule) → (x.ρ.asModule × y.ρ.asModule) :=
    fun g ↦ (fun (v, w) ↦ (x.ρ g v, y.ρ g w))

[Aaron Liu]

Your code has errors

[Aaron Liu]

failed to synthesize
  Ring k

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.

[Kevin Buzzard]

@Jester Cabading the "w" in #mwe stands for "no errors". I would really like to encourage you to ask questions with #mwe's as it makes them ambiguity-free. But regardless of errors, I am confused about your question because you start with terms of type Rep k G (i.e. objects in the category of k-linear G-reps) and then immediately turn them into k[G]-modules with .ρ.asModule. You and I both know that these things are "the same" but Lean would be the first to point out that as far as it's concerned they are not the same (they are the same mathematical information packaged up in two completely different ways). You would be better off choosing exactly one way of thinking about representations and building on that. My instinct is that docs#Representation is the way which is easiest for beginners.

[Kevin Buzzard]

I am surprised that I can find tensor product of representations, representations on hom sets and dual representations all in Mathlib.RepresentationTheory.Basic but no direct sum of two representations?

[Jester Cabading]

import Mathlib

open Representation
universe u

variable (k G V W : Type u) [CommSemiring k] [Monoid G] [AddCommMonoid V] [AddCommMonoid W] [Module k V] [Module k W]

def Representation.dsum (x : Representation k G V) (y : Representation k G W) : G → V × W → V × W :=
fun g ↦ fun (v, w) ↦ (x g v, y g w)

How do I turn all the functions into morphisms?

[Aaron Liu]

What kind of morphisms do you want?

[Aaron Liu]

Right now you have morphisms in the category of types

[Kenny Lau]

@Jester Cabading let me stress that there are a lot of ways to translate a given mathematical sentence into Lean, and most often when you're just starting out, the first one you pick will not be the most conventional one.

So for example here, you might view "is isomorphic" as a proposition, but as you've pointed out, conventionally we regard it as a type. (If you really want the proposition and have a very good reason for it, use Nonempty (M ≃ₗ[k] N).)

[Kenny Lau]

and for the latest question since you want to construct a term of type Representation k G (V \x W), you should follow Representation and look at its constructor.

[Kim Morrison]

Do we not already have the split Grothendieck groups of an additive category? (And Grothendieck ring when it is monoidal?)

[Kevin Buzzard]

Aaron Liu said:

What kind of morphisms do you want?

Surely the question is clear here -- they just want the direct sum as a Representation

[Kevin Buzzard]

And I couldn't find it

[Bryan Wang]

Kevin Buzzard said:

I am surprised that I can find tensor product of representations, representations on hom sets and dual representations all in Mathlib.RepresentationTheory.Basic but no direct sum of two representations?

#27755 maybe makes a start at addressing this..

[Jester Cabading]

Kenny Lau said:

Jester Cabading let me stress that there are a lot of ways to translate a given mathematical sentence into Lean, and most often when you're just starting out, the first one you pick will not be the most conventional one.

So for example here, you might view "is isomorphic" as a proposition, but as you've pointed out, conventionally we regard it as a type. (If you really want the proposition and have a very good reason for it, use Nonempty (M ≃ₗ[k] N).)

I made a proposition on if 2 representations are isomorphic and used it as an equivalence relation to make a quotient type. Though I'm not too sure if this is the right approach.

[Jester Cabading]

Kim Morrison said:

Do we not already have the split Grothendieck groups of an additive category? (And Grothendieck ring when it is monoidal?)

If we do, I have heard that the representation ring is just the Grothendieck ring in the category Rep. I'm not sure how to deal with it though so I have just been working explicitly with Representation.

[Kenny Lau]

@Jester Cabading yes, that is the right approach, but you should also have the versions without Nonempty, and only include the Nonempty in the last step

[Jester Cabading]

What I did was make the following definition:

import Mathlib

open Representation
universe u
variable (k G V W : Type u) [CommSemiring k] [Monoid G] [AddCommMonoid V] [AddCommMonoid W]
[Module k V] [Module k W]
(x : Representation k G V) (y : Representation k G W)

def Representation.isom : Prop :=
∃ f : V ≃ₗ[k] W, ∀ g : G, f ∘ x g = y g ∘ f

[Kevin Buzzard]

You don't want to do that, you want to give the data. It's much easier to work with in a theorem prover. It's surprising how often a mathematician says "theorem: there exists an isomorphism" when what they mean is "definition: we're only ever talking about this isomorphism". An example is the first isomorphism"theorem" which doesn't say "G/ker is iso to image", it says "...and we always use this specific isomorphism so we can do diagram chases". You can't get that data out of an abstract Prop

[Kevin Buzzard]

I'm sorry it's taken so long for me to get back to your questions Jester. Here is a more idiomatic way to define direct sum of two representations and equivalence of representations in the Representation world:

import Mathlib

universe u

variable {k G V W : Type u} [CommRing k] [Group G]
    [AddCommGroup V] [Module k V] (ρ : Representation k G V)
    [AddCommGroup W] [Module k W] (ψ : Representation k G W)

def Representation.prod : Representation k G (V × W) where
  toFun g := (ρ g).prodMap (ψ g)
  map_one' := by simp
  map_mul' g h := by simp; rfl

structure RepresentationEquiv extends V ≃ₗ[k] W where
  smul: ∀ g : G, toFun ∘ ρ g = ψ g ∘ toFun

On top of that you could define

def Representation.isom : Prop := Nonempty (RepresentationEquiv ρ ψ)

but even though this is how mathematicians are trained to think, this concept is less fundamental in the formalisation of mathematics and probably doesn't need its own definition.

[Jester Cabading]

So if a proposition isn't the best way to get an equivalence relation to define a setoid, what should I do to mod out the representations by isomorphism?

[Yaël Dillies]

Is it useful to mod out representations by isomorphisms?

[Kenny Lau]

only when you're dealing with size issues

[Kenny Lau]

this thread has been going on so long that i forgot what the original moivationi was, but there are certainly some situations where you would need to deal with size issues

[Kenny Lau]

e.g. it's a famous theorem that the character table is a square

[Jester Cabading]

I'm trying to define the representation ring which is a quotient of representations by isomorphism

[Jester Cabading]

Kenny Lau said:

Jester Cabading said:

I don't understand how to do disjoint unions with Sigma types

import Mathlib.Algebra.Module.Equiv.Defs
import Mathlib.Algebra.Module.LinearMap.End
import Mathlib.Algebra.Module.Pi

universe u v

variable (G : Type u) [Monoid G] (k : Type v) [CommSemiring k]

def Rep.Bound : Type (max u v) :=
  Σ n : ℕ, G →* ((Fin n → k) →ₗ[k] (Fin n → k))

So I was gonna use this and then mod out by the equivalence relation of isomorphism

[Kenny Lau]

@Jester Cabading yes, that is good, but i'm saying that the "main" stuffs should not be propositions

[Kenny Lau]

e.g. taking the direct sum of two representations shouldn't be a proposition

[Kenny Lau]

(the thing that we discovered was missing)

[Jester Cabading]

yes that part I understand at least

[Kenny Lau]

@Jester Cabading I suspect you might not ever need to mod Rep.Bound out by isomorphism

[Jester Cabading]

how should I define the representation ring?

[Kenny Lau]

maybe something similar to Pic?

[Kenny Lau]

i.e. Shrink the Rep category and hope that you get a semiring...

[Kenny Lau]

btw how do you make the ring after modding out Rep.Bound in your original proposal?

[Jester Cabading]

I was told to prove that sums and products are invariant under choice of representative; i.e. if M = M' and N = N' then M+N = M' + N'

[Kenny Lau]

import Mathlib

universe u

open CategoryTheory

variable (R : CommRingCat.{u})

#synth Monoid (Skeleton (ModuleCat.{u} R)) -- succeeds
#synth AddMonoid (Skeleton (ModuleCat.{u} R)) -- fails

[Kenny Lau]

I think we need more infrastructure to make this one work...?

[Jester Cabading]

Jester Cabading said:

I was told to prove that sums and products are invariant under choice of representative; i.e. if M = M' and N = N' then M+N = M' + N'

Then I think this allows me to use direct sum and tensor product as semiring operations on the quotient type

[Kenny Lau]

and then how do you get the ring?

[Kenny Lau]

you probably do the Grothendieck construction?

[Kenny Lau]

(deleted)

[Jester Cabading]

Kenny Lau said:

and then how do you get the ring?

I forgot but my supervisor told me how it's constructed; I was planning to ask him once I finished the semiring step

[Kenny Lau]

@loogle AddCommMonoid (CategoryTheory.Skeleton _)
@loogle AddMonoid (CategoryTheory.Skeleton _)
@loogle Add (CategoryTheory.Skeleton _)
@loogle Zero (CategoryTheory.Skeleton _)

[loogle]

:shrug: nothing found

[Kenny Lau]

yeah I think we're missing infrastructure

[Kenny Lau]

@Jester Cabading I advise you to provide the infrastructure as stated above, and then just Shrink the whole thing in the end; it will be mathematically isomorphic to the semiring you construct in the other proposal

[Kenny Lau]

(and much more easier to work with)

[Kenny Lau]

@Jester Cabading Could you remind me the use of the rep ring?

[Jester Cabading]

I believe actually the importance is virtual characters, because that's what is used in Artin's theorem on induced characters

[Jester Cabading]

so I think we can map each representation to its character in the ring of class functions of a finite group G

[Kevin Buzzard]

But you don't need to do anything complicated like you're doing to prove Artin's theorem, this is just messing around with functions from G to $\mathbb{C}.$ We need Artin's theorem for FLT by the way!

[Jester Cabading]

Serre's linear representations of finite groups proof of Artin's theorem relies on it does it not?

[Kevin Buzzard]

I don't know, I'm in a field for the week. Why not sketch the proof here?

[Jester Cabading]

I apologize for the late response, but I think Serre basically states Artin’s theorem as a corollary to this

[Jester Cabading]

Let X be a family of subgroups of a finite group G. Let Ind: \oplus_{H in X} R(H) \to R(G) be defined by the family of Ind H. Then the following are equivalent:

(i) G is the union of the conjugates of subgroups in X

(ii) The cokernel of Ind is finite

[Jester Cabading]

Here R(H)/R(G) is the virtual characters which I think is isomorphic to their respective representation rings

[Jester Cabading]

Kenny Lau said:

Jester Cabading I advise you to provide the infrastructure as stated above, and then just Shrink the whole thing in the end; it will be mathematically isomorphic to the semiring you construct in the other proposal

I don't fully understand what you're suggesting and the stuff about skeletons and shrinking in Lean, so I have decided to continue the painstaking process of constructing the representation ring. This is also because I understand this more and already have some work done on it and I don't have much time left to work.

[Jester Cabading]

How do we construct a specific element of a sigma type? I want to define a function (specifically addition) for the following:
Kenny Lau said:

Jester Cabading said:

I don't understand how to do disjoint unions with Sigma types

import Mathlib.Algebra.Module.Equiv.Defs
import Mathlib.Algebra.Module.LinearMap.End
import Mathlib.Algebra.Module.Pi

universe u v

variable (G : Type u) [Monoid G] (k : Type v) [CommSemiring k]

def Rep.Bound : Type (max u v) :=
  Σ n : ℕ, G →* ((Fin n → k) →ₗ[k] (Fin n → k))

[Kenny Lau]

Jester Cabading said:

How do we construct a specific element of a sigma type?

\<a, b\>

[Jester Cabading]

Is there an k-linear isomorphism of vector spaces between k^n*k^m and k^(n+m) in mathlib?
I want to write the product representation as a representation of k^(n+m) rather than the former.

[Kenny Lau]

Jester Cabading said:

Is there an k-linear isomorphism of vector spaces between k^n*k^m and k^(n+m) in mathlib?
I want to write the product representation as a representation of k^(n+m) rather than the former.

1. LinearEquiv.sumArrowLequivProdArrow
2. LinearEquiv.funCongrLeft
3. finSumFinEquiv

[Jester Cabading]

thank you

[Jester Cabading]

Kevin Buzzard said:

I'm sorry it's taken so long for me to get back to your questions Jester. Here is a more idiomatic way to define direct sum of two representations and equivalence of representations in the Representation world:

import Mathlib

universe u

variable {k G V W : Type u} [CommRing k] [Group G]
    [AddCommGroup V] [Module k V] (ρ : Representation k G V)
    [AddCommGroup W] [Module k W] (ψ : Representation k G W)

def Representation.prod : Representation k G (V × W) where
  toFun g := (ρ g).prodMap (ψ g)
  map_one' := by simp
  map_mul' g h := by simp; rfl

structure RepresentationEquiv extends V ≃ₗ[k] W where
  smul: ∀ g : G, toFun ∘ ρ g = ψ g ∘ toFun

On top of that you could define

def Representation.isom : Prop := Nonempty (RepresentationEquiv ρ ψ)

but even though this is how mathematicians are trained to think, this concept is less fundamental in the formalisation of mathematics and probably doesn't need its own definition.

For this definition of Equivalence, is there a way to extend the definition so that given some (x : RepresentationEquiv ...) I can use (x.trans, x.symm) including the structure of smul?

[Jester Cabading]

Hopefully that question makes sense

[Kevin Buzzard]

Yeah you would have to build API for RepresentationEquiv just like any other definition needs API. Take a look at the mathlib definitions of eg docs#LinearEquiv , they no doubt come with hundreds of lines of boilerplate code directly after.

The specific problem with representation theory is that the community seems confused about whether to develop the API for Representation or Rep/FDRep, so statements of the form "why don't morphisms/isomorphisms of Representation exist?" might be met with answers of the form "well morphisms and isomorphisms of objects in categories exist so use those instead". Historically for most branches of basic algebra (eg groups, rings, modules) the elementary approach existed before category theory in mathlib was even viable, so the structure was built up in the non-category way. But for representation theory this didn't occur and now we have this kind of mess.

[Jester Cabading]

I'm trying to prove a fact about a quotient type with the following tactic:
"induction q using Quotient.ind" where q is a variable in the type, but when I do this it removes the variable name and replaces it with "a✝".
How do I add a label to this variable so that I can refer to it in my proof?

[Ruben Van de Velde]

induction q using Quotient.ind with | _ q =>

[Jester Cabading]

thank you very much

[Jester Cabading]

does mathlib have a notion of a zero-dimensional vector space and thus a zero representation?

[Oliver Nash]

I think you probably want docs#Subsingleton

[Oliver Nash]

For example, here is how you prove that every vector is zero in this setting:

import Mathlib.Algebra.Field.Defs
import Mathlib.Algebra.Module.Defs

example (k V : Type) [Field k] [AddCommGroup V] [Module k V] [Subsingleton V] (v : V) :
    v = 0 :=
  Subsingleton.elim v 0

[Oliver Nash]

Lastly see docs#Module.finrank_zero_of_subsingleton

[Jester Cabading]

thank you

[Jester Cabading]

Is there also a defined linear equivalence between finite dimensional V and k^n or should I definite it myself?

[Kevin Buzzard]

You'll need to choose a basis but then it's there

[Oliver Nash]

And if you don't have a basis to hand then you can obtain one via docs#Module.Free.chooseBasis

[Jester Cabading]

Kenny Lau said:

Jester Cabading said:

Is there an k-linear isomorphism of vector spaces between k^n*k^m and k^(n+m) in mathlib?
I want to write the product representation as a representation of k^(n+m) rather than the former.

1. LinearEquiv.sumArrowLequivProdArrow
2. LinearEquiv.funCongrLeft
3. finSumFinEquiv

Are there analogous theorems to construct a k-linear equivalence between (k^n \otimes k^m) and (k^(n*m))?

[Jester Cabading]

also, is there a way to refer to a component of a pure tensor
v⊗ₜ[k] w

[Jester Cabading]

nvm about that last question actually I think I need to figure out first how to take a variable (u : V ⊗[k] W) and decompose it using the basis of pure tensors

[Kenny Lau]

Jester Cabading said:

Are there analogous theorems to construct a k-linear equivalence between (k^n \otimes k^m) and (k^(n*m))?

We seem to be missing this, the closest one is docs#finsuppTensorFinsupp' with finsupp

[Kenny Lau]

Jester Cabading said:

also, is there a way to refer to a component of a pure tensor
v⊗ₜ[k] w

you first need to show that it forms a basis, which is some more work built upon the my previous comment

[Jester Cabading]

Is it a mathematical fact that we can take any u in the vector space V ⊗ₜ[k] W and express it as v ⊗ₜ[k] w for some (v : V) (w : W)

[Aaron Liu]

no I'm pretty sure that's false

[Kenny Lau]

Jester Cabading said:

Is it a mathematical fact that we can take any u in the vector space V ⊗ₜ[k] W and express it as v ⊗ₜ[k] w for some (v : V) (w : W)

what is true is that you can express it as the sum of finitely many of those, and that is in mathlib

[Kenny Lau]

TensorProduct.exists_finset

[Kenny Lau]

(x : TensorProduct R M N) :
∃ (S : Finset (M × N)), x = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2

[Jester Cabading]

Kenny Lau said:

Jester Cabading said:

Is it a mathematical fact that we can take any u in the vector space V ⊗ₜ[k] W and express it as v ⊗ₜ[k] w for some (v : V) (w : W)

what is true is that you can express it as the sum of finitely many of those, and that is in mathlib

Oh yes that is what I need; thank you

[Kevin Buzzard]

Jester Cabading said:

Is it a mathematical fact that we can take any u in the vector space V ⊗ₜ[k] W and express it as v ⊗ₜ[k] w for some (v : V) (w : W)

The way to see that this is false is to look at the following model: $V$ is length 2 row vectors, $W$ is length 2 column vectors, and then a model for $V\otimes W$ is 2 by 2 matrices, with $v\otimes w$ being modelled as the product $vw$ (product of a 2x1 and 1x2 matrix is a 2x2 matrix). It's not hard to see that 2x2 matrices of the form $vw$ are very special -- they all have rank at most 1. So a special case of your question is "does every 2x2 matrix have rank at most 1?" and the identity matrix is a counterexample.

[Kevin Buzzard]

It's nice to have toy models for lots of things in mathematics. Tensor products are very abstract objects and they're only defined by this funny universal property, which means they're only defined up to unique isomorphism as opposed to being defined on the nose. Mathlib has TensorProduct (a concrete model, defined as a quotient of a hugely infinite object which is totally hopeless to compute with) but it also has IsTensorProduct (where you can use far more concrete models). The concrete model of matrices as tensor products of vector spaces was super-helpful for me when getting oriented with tensor products.

[Kevin Buzzard]

It's also very disconcerting to discover that a general element of $V\otimes W$ cannot be written as $v\otimes w$. For many other constructions in mathematics, for example direct sums, products, quotients etc it's very easy to write down a general formula for an element of this exotic new object and get a clear understanding as to what extent the formula uniquely defines the element (for example an element of a product $X\times Y$ is just a pair $(x,y)$, and an element of a quotient group $G/H$ is a coset $gH$ or you can think of it as an equivalence class $[g]$ where $[g_1]=[g_2]$ iff $g_1^{-1}g_2\in H$). But for tensor products this sort of concrete way of modelling elements is completely hopeless. We know that elements of the form $v\otimes w$ give you elements of $V\otimes W$ and it's a theorem that every element of $V\otimes W$ can be written as a finite sum of things of the form $v\otimes w$, but trying to figure out e.g. if two finite sums represent the same element of $V\otimes W$, or (equivalently) trying to work out if a finite sum of explicit elements of the form $v\otimes w$ is zero or not, can be an extremely hard problem. So it's far more difficult to do concrete calculations with tensor products than it is to do calculations with other objects like direct products, and you often have to resort to the universal property, or earlier-proved theorems, if you want to reason about it.

[Kevin Buzzard]

In mathlib we have some very nice universal properties for tensor products, such as "if you're trying to prove things about all elements of $V\otimes W$, and if you can prove it for elements of the form $v\otimes w$ and if you can also show that if your property is true for $a$ and for $b$ then it's true for $a+b$, then your property is true for all elements of the form $V\otimes W$. This is another (rather nice) way of saying that every element is a finite linear combination of things of the form $v\otimes w$.

[Jester Cabading]

Is there a difference between (Fin n to k) and the Finsupp version?
I understand Lean treats them as different types but is there a difference mathematically?

[Kevin Buzzard]

Finitely-supported functions from a type to k will embed into all functions from that type to k, and the embedding will be a bijection if the source type is finite yes.

[Kenny Lau]

@Jester Cabading Finsupp.linearEquivFunOnFinite

[Jester Cabading]

I want to define a function on an element v of a tensor product, but I want to define it in terms of a finite sum of pure tensors. I know using TensorProduct.exists_finset that I can rewrite v, but I do not understand how to use this rewrite in a function definition.

[Aaron Liu]

can you do it inductively or use the universal property?

[Kenny Lau]

Jester Cabading said:

using TensorProduct.exists_finset

this is already a bad idea mathematically, because there are different ways to represent the same tensor, so you'll need to prove that your definition is independent of the way to express it.

for example going back to 2x2-matrix, where v1⊗v2 is the matrix v1 v2^T where v1 and v2 are column vectors, then (1 0; 0 1) is e1⊗e1 + e2⊗e2, but it's also (e1+e2)⊗(e1-e2) - e2⊗e1 + e1⊗e2 + 2e2⊗e2

mathematically, the correct way to define a function on V⊗W is to use the universal property, which says that a linear map V⊗W -> M corresponds to a bilinear map V x W -> M

[Jester Cabading]

right that makes sense

[Jester Cabading]

I'm really struggling with proving that the tensor product of representations distributes over direct sum of representations. I know what the map is or should be between the spaces, but I can't figure out how to define it in Lean.

[Jester Cabading]

I'm trying to define the isomorphism using this answer in stack exchange:
https://math.stackexchange.com/questions/805019/distributivity-of-tensor-products-over-direct-sums-for-group-representations

[Kenny Lau]

@Jester Cabading you shouldn't need to prove it yourself, every standard fact would be in mathlib already

[Jester Cabading]

The product/sum of representations was not even defined before; I don't think the actual isomorphism has been defined in Mathlib

[Kim Morrison]

It's just M \times N. It's certainly there.

[Thomas Waring]

Note that the "product" of representations in your ring will be Representation.tprod, and M \times N = Representation.prod M N is the product of the types M and N, which is algebraically the direct sum — you can see this if you look at the definition of DirectSum, which is a pi-type:

def DirectSum [∀ i, AddCommMonoid (β i)] : Type _ :=
  Π₀ i, β i

(ignoring what changes when the sum is infinite)

[Edward van de Meent]

ah, that reminds me, Representation.tprod really shoud be renamed (since it clashes with docs#tprod)

[Jester Cabading]

Using TensorProduct.exists_finset I know that anything in (V \otimes W) is a finite sum of pure tensors, but is there a way I can use this to prove that anything in (V \otimes W) \otimes U is a finite sum of pure tensors of 3 vectors?

[Kenny Lau]

@Jester Cabading yes, tensor distributes over addition, and you can choose a finset for each one again

[Kenny Lau]

i.e.given x in (V ⊗ W) ⊗ U, write it as ∑ vw_i ⊗ₜ u_i, then for each i write vw_i as ∑ v_ij ⊗ₜ w_ij, then x = ∑∑ v_ij ⊗ₜ w_ij ⊗ₜ u_i

[Kenny Lau]

the "for each i" part is the choose tactic

[Jester Cabading]

What would that look like in lean?

[Jester Cabading]

nevermind I think I can figure it out myself

[Jester Cabading]

is there a way to turn a semiring into a ring similar to how we can turn a commutative monoid into a commutative group using the grothendieck group?

[Aaron Liu]

grothendieck ring?

[Aaron Liu]

it's the "ring of differences"

[Aaron Liu]

the left adjoint to the forgetful functor from rings to semirings

[Aaron Liu]

(I'm assuming you're talking about unital rings but I don't see why it shouldn't work with nonunital rings too)

[Jester Cabading]

where can I find that in mathlib?

[Jester Cabading]

Kenny Lau said:

i.e.given x in (V ⊗ W) ⊗ U, write it as ∑ vw_i ⊗ₜ u_i, then for each i write vw_i as ∑ v_ij ⊗ₜ w_ij, then x = ∑∑ v_ij ⊗ₜ w_ij ⊗ₜ u_i

So I've used the choose tactic and gotten a hypothesis of the form "For all w in (V ⊗ W), w = ∑ ...".
How can I rewrite x in terms of this? I can't seem to get rw to work with it.

[Jester Cabading]

I don't understand how to use rw to rewrite the elements "vw_i" in the summation

[Christian Merten]

Could you post an #mwe? It is very unlikely that writing a general element as a sum over pure tensors is the right approach. Instead, it is often easier to use so called "induction principles". These are statements of the form: "If the claim holds for the zero element, is stable under addition and holds for all pure tensors, then it is true for every element of the tensor product" (docs#TensorProduct.induction_on).

[Jester Cabading]

There's a few representation isomorphisms I was defining using tensor product module isomorphisms (distributivity over direct sum, tensor product with 0 is still zero) so I had to show they commute with the g-action. In every case except associativity, simply just using "exists_finset" for any vector in the tensor product sufficed.
I think these induction principles could work so I'll try it.

Christian Merten said:

Could you post an #mwe? It is very unlikely that writing a general element as a sum over pure tensors is the right approach. Instead, it is often easier to use so called "induction principles". These are statements of the form: "If the claim holds for the zero element, is stable under addition and holds for all pure tensors, then it is true for every element of the tensor product" (docs#TensorProduct.induction_on).

[Kevin Buzzard]

Yes the induction principles should be perfect for checking G-actions.

[Aaron Liu]

Jester Cabading said:

where can I find that in mathlib?

Probably not exactly this is in mathlib but maybe if you're lucky you'll find something like "all algebraic theories are monadic"

[Kenny Lau]

Jester Cabading said:

these induction principles could work

these new ways are more unfamiliar but in my experience better, that's just a fact of life that you'll have to go through

[Jester Cabading]

So I need to show this

((↑(TensorProduct.assoc k V W U)).toFun ∘ ⇑(((ρ.tprod ψ).tprod φ) g)) v =
  (⇑((ρ.tprod (ψ.tprod φ)) g) ∘ (↑(TensorProduct.assoc k V W U)).toFun) v

where v is an element of (V \otimes W) \otimes U, but when I try to apply the theorem "TensorProduct.induction_on" it doesn't seem to work properly. Am I just doing it wrong?

[Kenny Lau]

@Jester Cabading induction v using TensorProduct.induction_on

[Jester Cabading]

Kenny Lau said:

Jester Cabading induction v using TensorProduct.induction_on

When I do this, I get an implicit variable in (V \otimes W). How can I use this variable as an explicit term?

[Kenny Lau]

Jester Cabading said:

Kenny Lau said:

Jester Cabading induction v using TensorProduct.induction_on

When I do this, I get an implicit variable in (V \otimes W). How can I use this variable as an explicit term?

when you hover over induction you get the instruction manual

[Kenny Lau]

see the part with with

[Jester Cabading]

it keeps saying unknown tactic when I try to use with

induction v using TensorProduct.induction_on with | zero => _ | tmul => x y | add => x y

[Kenny Lau]

did you import Mathlib?

[Jester Cabading]

yes

[Kenny Lau]

can you post #mwe?

[Jester Cabading]

well it doesn't work so I don't think it counts as a mwe

[Jester Cabading]

but I can post what I have written so far

[Yaël Dillies]

A MWE needs to work not in the sense that it builds fully, but in the sense that it shows the error/problem you are encountering

[Kenny Lau]

otherwise there would be no point in posting an mwe

[Jester Cabading]

that makes sense

[Jester Cabading]

import Mathlib
open Representation
open LinearEquiv
open TensorProduct

universe u
variable {k G V W U : Type u} [Field k] [Monoid G]
[AddCommMonoid V] [Module k V] [AddCommMonoid W] [Module k W] [AddCommMonoid U] [Module k U]
(ρ : Representation k G V) (ψ : Representation k G W) (φ : Representation k G U)

structure RepEquiv extends V ≃ₗ[k] W where
smul : ∀ g : G, toFun ∘ ρ g = ψ g ∘ toFun

noncomputable def tprod_assoc : RepEquiv ((ρ.tprod ψ).tprod φ) (ρ.tprod (ψ.tprod φ)) where
toLinearEquiv := TensorProduct.assoc k V W U
smul := by
    intro g
    ext v
    induction v using TensorProduct.induction_on with | zero => _ | tmul => x y | add => _

[Jester Cabading]

from what I understand, "with" for induction allows you to add names for the variables

[Yaël Dillies]

You are writing | tmul => x y but the syntax is | tmul x y => _

[Jester Cabading]

ah ok thank you

[Jester Cabading]

So characters have been defined and developed in FDRep; I want to be able to use characters and those properties, but everything I've been working with is in Representation k G. I imagine I'd have to do some functorial stuff to show that RepEquiv (which is defined in the code above) is the same as an isomorphism in Rep. Is this the way go about it?

[Kenny Lau]

@Jester Cabading yes, see RingEquiv.toCommRingCatIso for example

[Jester Cabading]

So I have instantiated the Representation Ring as a semiring; is there a way to use the Grothendieck construction to turn a semiring into a ring?

[Kenny Lau]

Algebra.GrothendieckAddGroup but you might need to first turn it to a ring

[Jester Cabading]

my goal is to get a ring, but I can only know how to define it as a semiring

[Kenny Lau]

@Jester Cabading i'm saying my linked thing gives you an abelian group which is the correct ring except that the ring structure hasn't been defined

[Jester Cabading]

oh I see what you mean