Developing irreducible representations for mathlib

Stream: mathlib4

[Stepan Nesterov]

I am a math PhD student interested in developing the basic properties of irreducible and absolutely irreducible representations for mathlib, motivated by potential applications in the FLT project.

Do I need to get preliminary approval for content/exact statements that I would like to add to mathlib? For example, let's say that I would like to make a PR which makes a definition of an (absolutely) irreducible representation and culminates with a proof that every absolutely irreducible representation of an abelian group is one-dimensional.

Do I have to discuss beforehand in which generality should the theorem be stated? For example, instead of developing the theory of absolutely irreducible representations of a group, I could define absolutely simple modules over algebras over a field, and prove that an absolutely simple module over a commutative algebra over a field is one-dimensional. Maybe the results should be proven in an even broader context, which I cannot think of right now.

Do I have to discuss beforehand which definitions to use? I couldn't help but notice that in ##Mathlib.RepresentationTheory.Character orthogonality relations are proved using CategoryTheory.Simple as a definition for an irreducible representation. Does this mean that mathlib prefers not to have a separate definition of an irreducible representation? In comparison, in the FLT project the irreducibility is defined separately as

universe u

variable {G : Type*} [Group G]

variable {k : Type u} [Field k]

variable {W : Type*} [AddCommMonoid W] [Module k W]

class IsIrreducible (ρ : Representation k G W) : Prop where
  irreducible : IsSimpleOrder (Subrepresentation ρ)

Thank you in advance,
Stepan

[Kim Morrison]

It's generally good to discuss ahead of time if you're up for it!

[Kim Morrison]

The fact that Mathlib's representation theory currently uses CategoryTheory.Simple is a mistake (mine). While we should certain make the connections with category theory, and use it, and make it easier to use, we also need to make progress on representation theory and it is clear that the way forward is to make non-categorical definitions.

[Stepan Nesterov]

I see by looking at https://github.com/leanprover-community/mathlib4/commits/master/ that most commits to mathlib are generally pretty small (rarely exceeding a 100 lines of code). If that is the typical length of a mathlib PR, I could start, for example, by creating a file Mathlib.RepresentationTheory.Irreducible, and prove an equivalence between three definitions:

• The FLT project definition IsSimpleOrder (Subrepresentation ρ)
• IsSimpleModule ρ.asModule
• CategoryTheory.Simple Rep.of ρ
  Is this a good idea for a first mathlib PR and if so, are there any other equivalent definitions that should be included?

[Kim Morrison]

This sounds very good to me!

[Ruben Van de Velde]

And yes, please try to make fairly small PRs, especially when you're starting out. It makes review a lot smoother

[Stepan Nesterov]

I have a question about homomorphisms of representations.
As far as I can tell, currently the way to talk about a homomorphism from ρ to σ is to writeρ.asModule →ₗ[k[G]] σ.asModule. Is this intentional according to the Mathlib style, or would it be beneficial to set up separate notation for homomorphisms of representations?

[Stepan Nesterov]

Ok I guess I underestimated how long the proof of IsSimpleOrder (Subrepresentation ρ) ↔ * IsSimpleModule ρ.asModule would be. I proved it by constructing an order isomorphism Subrepresentation ρ ≃o Submodule A[G] ρ.asModule` and that's already about a 100 lines.

[Stepan Nesterov]

https://github.com/leanprover-community/mathlib4/pull/32856
Currently my PR fails "check the PR title format":
feat: definition of an irreducible representation

https://github.com/leanprover-community/mathlib4/actions/runs/20198356387/job/57985595813?pr=32856#step:4:40

https://github.com/leanprover-community/mathlib4/actions/runs/20198356387/job/57985595813?pr=32856#step:4:41error: failed to parse latest release tag

https://github.com/leanprover-community/mathlib4/actions/runs/20198356387/job/57985595813?pr=32856#step:4:42Error: Process completed with exit code 1.

What did I do wrong?

[Ruben Van de Velde]

I think you can ignore that error; the other one is valid, though

[Stepan Nesterov]

Ok I added docstrings

[Stepan Nesterov]

Now it says
Run if [[ "failure" != "success" ]]; then

https://github.com/leanprover-community/mathlib4/actions/runs/20198356387/job/57985595813?pr=32856#step:32:14+ [[ failure != \s\u\c\c\e\s\s ]]

https://github.com/leanprover-community/mathlib4/actions/runs/20198356387/job/57985595813?pr=32856#step:32:15Please run 'lake exe mk_all' to regenerate the import all files

https://github.com/leanprover-community/mathlib4/actions/runs/20198356387/job/57985595813?pr=32856#step:32:16+ echo 'Please run '\''lake exe mk_all'\'' to regenerate the import all files'

https://github.com/leanprover-community/mathlib4/actions/runs/20198356387/job/57985595813?pr=32856#step:32:17+ exit 1

https://github.com/leanprover-community/mathlib4/actions/runs/20198356387/job/57985595813?pr=32856#step:32:18Error: Process completed with exit code 1.

[Ruben Van de Velde]

Yes, please also run lake exe mk_all - new files need to be added to Mathlib.lean, and that tool will do it for you

[Stepan Nesterov]

Alright all checks have passed!
Thank you for the help :)

[Stepan Nesterov]

I have extended the theory of irreducible representations and managed to prove the following result:

theorem one_dimensional_of_irreducible_of_abelian [IsIrreducible ρ] [FiniteDimensional k V]
    [Nontrivial V] [IsAlgClosed k] [IsMulCommutative G] : Module.finrank k V = 1

I see that sometimes there are PRs in mathlib that depend on other PRs. Is this considered good practice to create chains of PRs like that or is it better to wait until my first PR is reviewed?

[Kevin Buzzard]

It's fine to have PRs which depend on other PRs. Thanks for working on this!

[Kim Morrison]

It does make me sad when we prove things about representations of groups that are true of representations of algebras...

[Stepan Nesterov]

I am considering whether I should first PR this:

variable {k : Type*} (A V : Type*) [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [AddCommGroup V]
    [Module k V] [Module A V] [IsScalarTower k A V]

theorem one_dimensional_of_simple_of_commutative [IsMulCommutative A] [IsSimpleModule A V]
    [FiniteDimensional k V] : Module.rank k V = 1 := by
  sorry

If I do, which directory does it go to? I think RepresentationTheory is specifically about representation of groups right now. In a new file in RingTheory/SimpleModule maybe?

[Kim Morrison]

I think we shouldn't be shy about treating the representation theory of commutative algebras as part of RepresentationTheory/. Just make a new directory there?

[Stepan Nesterov]

Ok I've just PRed the general algebra fact: https://github.com/leanprover-community/mathlib4/pull/33216

It does give a mysterious error though:

Run cd pr-branch

https://github.com/leanprover-community/mathlib4/actions/runs/20450645550/job/58762751810?pr=33216#step:14:10+ cd pr-branch

https://github.com/leanprover-community/mathlib4/actions/runs/20450645550/job/58762751810?pr=33216#step:14:11+ lake env

https://github.com/leanprover-community/mathlib4/actions/runs/20450645550/job/58762751810?pr=33216#step:14:12info: plausible: cloning https://github.com/leanprover-community/plausible

https://github.com/leanprover-community/mathlib4/actions/runs/20450645550/job/58762751810?pr=33216#step:14:13error: external command 'git' exited with code 128

https://github.com/leanprover-community/mathlib4/actions/runs/20450645550/job/58762751810?pr=33216#step:14:14Error: Process completed with exit code 1.

[Ruben Van de Velde]

Doesn't sound like your fault, I restarted the job

[Andrew Yang]

Kim Morrison said:

I think we shouldn't be shy about treating the representation theory of commutative algebras as part of RepresentationTheory/. Just make a new directory there?

I am slightly hesitant about this. I think having a more clear cut line between top level folders is better and I wonder if we could come up with one here first?

[Stepan Nesterov]

Is this PR https://github.com/leanprover-community/mathlib4/pull/33802 set up correctly as a PR which depends on my two previous PRs?
I see that it includes (copies of) commits from both of them, but you can't tell at a glance that these are commits from different PRs, so it makes me worried

[Ruben Van de Velde]

No, you should edit the PR summary to follow the instructions in the comment:

If this PR depends on other PRs, please list them below this comment,
using the following format:
- [ ] depends on: #abc [optional extra text]
- [ ] depends on: #xyz [optional extra text]

[Stepan Nesterov]

Ok fixed it

[Stepan Nesterov]

In https://github.com/leanprover-community/mathlib4/pull/33221 I was asked to discuss on Zulip the naming of "homomorphism between two representations", which can either be called "intertwining map", or "equivariant linear map". How does this usually work, do people vote on this?

[Stepan Nesterov]

On a related note, is it worth creating a special syntax for intertwining/equivariant maps, such as (ρ →i[G] σ) or (ρ →e[G] σ) ?

[Kevin Buzzard]

I'm not objecting to IntertwiningMap, people mat complain that it's long but we have ContinuousLinearMap which is longer, and you only really type it in theorem names because we have notation.

For notation, probably the notation needs to mention the ring as well as the group? Wait -- I guess both the ring and the group can be read off from the types of rho and sigma? So you could just have ρ →ᵣ σ for "map of representations"?

[Artie Khovanov]

Are there subgroup restriction coercions on representations? If so, and if that operation is common in practice, we might want to keep the group in the notation.

[Stepan Nesterov]

Artie Khovanov said:

Are there subgroup restriction coercions on representations? If so, and if that operation is common in practice, we might want to keep the group in the notation.

I don't think there are, might it be a good idea to add them?

[Artie Khovanov]

I don't know this part of the library sorry
I also don't know much rep theory, I only have a first course in it, so I don't know what sorts of constructions are common

[Stepan Nesterov]

In #33802, the following question was brought up: mathlib already has an older spelling of Schur's lemma, FDRep.simple_iff_end_is_rank_one, which defines an irreducible representation as a simple object in the category of representations. I have developed a few PRs using an alternative definition of an irreducible representation, which I copied from the FLT project.
In a subsequent PR, I could prove the equivalence of two definitions, and make the earlier API for irreducible representations available for FLT. However, it is a bit inelegant to have to juggle two definitions like that. It is worthwhile to attempt to refactor some parts of the library to use the FLT definition?

[Oliver Nash]

I think we should proceed with #33802, that the link to the category theory should be an equivalence between docs#Representation.IsIrreducible and docs#CategoryTheory.Simple, and that the results outside the category theory library should be stated using docs#Representation.IsIrreducible and not docs#CategoryTheory.Simple.

As to proofs of statements which do not use the language of category theory, I think we should use category theory results (porting their proofs on the fly via equivalences) only if it saves substantial work. This does mean that for easy results like Schur we'll have some proof duplication but I think this will make for a more maintainable library.

[Oliver Nash]

We have followed this pattern elsewhere in the library. E.g., a recent case where I encountered it is demonstrated in docs#CommRingCat.epi_iff_epi

[Stepan Nesterov]

Should the references to docs#FDRep in file#Mathlib/RepresentationTheory/Character be replaced by an unbundled version then?

variable {G k V : Type*} [Monoid G] [Field k] [AddCommGroup V] [Module k V] [FiniteDimensional k V] (ρ : Representation k G V)

[Kevin Buzzard]

My instinct is that we should be developing representation theory using docs#Representation for now, because we've decided on this as a definition and now we need to do the experiment of figuring out if it works.

[Stepan Nesterov]

Another issue that came up in #34584 is the need to refactor file#Mathlib/RepresentationTheory/Maschke to use Finite instead of Fintype. As I'm refactoring it anyway, I could also change all the category-theoretic spellings of representation-theoretic notions to the ones I've been developing: Rep to Representation, CategoryTheory.Simple to IsIrreducible etc. Obviously I have to worry about some projects relying on these old theorems breaking because I changed assumptions. Do people think this refactor is worth doing? Do I need to mark old theorems as deprecated? (I see that label in mathlib from time to time)

[Kevin Buzzard]

Can we just reprove the theorems for Representation and leave the Rep ones?

[Stepan Nesterov]

What would the naming convention be for such cases? For example, if we have

def character (V : FDRep k G) (g : G) :=
  LinearMap.trace k V (V.ρ g)

do I define

def character' (ρ : Representation k G V) (g : G) :=
  LinearMap.trace k V (ρ g)

[Bryan Wang]

Probably Representation.character

[Stepan Nesterov]

Ah right, different namespaces

[Stepan Nesterov]

Ok I've created locally a carbon copy of the file Character.lean with all the spellings changed from Rep to Representation. What would be a good way to PR it to mathlib? As a separate file or a new section of the old file?

[Stepan Nesterov]

Well I need just a small PR #34888 to define a respelling of 'isomorphism of representations', and then my refactor will work

[Stepan Nesterov]

In the PR #35100, I complete the proof of orthogonality of characters for Representation's.