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