Subrepresentations

Stream: maths

[Winston Yin]

Seeing as the representation theory of groups is being built, would it be worth defining subrepresentations and representation homomorphisms, copying a lot of lemmas over from submodules and linear maps?

[Winston Yin]

They would be defined as:

structure subrepresentation
  {k G V : Type*} [comm_semiring k] [monoid G] [add_comm_monoid V] [module k V]
  (ρ : representation k G V) extends submodule k V :=
(smulG_mem' : ∀ (g : G) {x : V}, x ∈ carrier → ρ g x ∈ carrier)

structure rep_hom
  {k G V V' : Type*} [comm_semiring k] [monoid G]
  [add_comm_monoid V] [module k V] [add_comm_monoid V'] [module k V']
  (ρ : representation k G V) (ρ' : representation k G V') extends V →ₗ[k] V' :=
(smul_comm : ∀ (g : G) (x : V), ρ' g (to_fun x) = to_fun (ρ g x))

[Kevin Buzzard]

My immediate instinct is "yes"! But perhaps others should weigh in. Is there some trick where you deduce everything from submodule and the fact that it's a k[G]-module?

[Winston Yin]

I actually did most of the work for this about a year ago but that was before Rep and representation were defined the way they are now. I essentially copy-pasted the lemmas from submodule and linear_map (before the semilinear map rewrite) with minimal modification

[Winston Yin]

I also made a branch containing some other lemmas for the direct sum of fdReps. Would very much welcome suggestions towards a PR.

[Oliver Nash]

@Winston Yin I would also say, yes we want these definitions. Indeed they are exactly analogous to docs#lie_submodule and docs#lie_module_hom which we have had for some time and which seem to work well.

[Oliver Nash]

I would add that at some point we should probably start leaning on our powerful category theory library for things like this though. For example I note that we have an open PR (which I hope to see merged soon) #14308 in which certain maps are shown to be morphisms of G-modules using our category theory library.

[Oliver Nash]

This latter approach is less well explored though. In the case of #14308 it is likely a win because I believe our category theory is likely to be very valuable when working with cohomology.

[Antoine Labelle]

So far I've been doing a little experiment to try to work as much as possible with the category theory library while developping representation theory, which is why we don't have things like rep_hom or rep_equiv. I still think it's good eventually to have both, so feel free to add these things!

[Antoine Labelle]

Also I noticed on your branch that you go through matrices to prove the formula for the trace of a direct sum. It's ok but you can probably get a much neater proof by using docs#linear_map.trace_eq_contract (see the proof of docs#linear_map.trace_prod_map for an example).

[Antoine Labelle]

@Kevin Buzzard With the current approach this seems complicated to do because representations don't come with an instance of module (monoid_algebra k G), due to possibke diamonds in the case of different representations on the same vector space.

[Winston Yin]

What I did last year was to define representation to extent the module class together with a smul commutation condition. I realised that this makes it tricky to compare different representations of the same vector space.

I'll look into simplifying the direct sum proofs with your suggestions @Antoine Labelle, thank you. I find that I am not so good at writing concise proofs but rely much on Lean's automation magic.

I especially find that direct_sum, dfinsupp, etc are quite tricky to use in proofs. Lean frequently has trouble inferring type classes. Variable declarations are generally verbose. rw and subst often don't work because expressions are tucked behind a λ i : ι. Maybe there's some trick I'm missing.

As for proofs generalised by category theory, I wish I knew enough category theory to help.

[Antoine Labelle]

If rw doesn't work for this kind of reason I think simp only often work

[Winston Yin]

In this branch are the following things: homomorphisms and equivalences between representations, subrepresentation, lattice of subreps, irreducibility and Schur’s Lemma, direct sum representation

[Winston Yin]

A lot of these are directly copied and modified from linear_map, linear_equiv, submodule, submodule.lattice. Not sure if all of the duplication is necessary

[Winston Yin]

Need some advice on which parts could be turned into a PR

[Antoine Labelle]

Wow that all looks really cool! You should probably break this down into a bunch of separate PRs by themes.
I'll try to look more closely later, for now just a quick comment, the average map you defined already exists, see the representation_theory/invariants file.

[Winston Yin]

Oh that’s cool! I’ll look at it. Who is developing representation theory currently? I should talk to them and try not to step on their toes

[Winston Yin]

Specifically, it would be nice to discuss when to use the category theory definitions Rep and fdRep and when to use the explicit representation

[Winston Yin]

For example, currently to specify the character of a representation ρ, one needs to say (fdRep.of ρ).character, when it would be more straightforward to define ρ.character directly

[Antoine Labelle]

Yes, so far representation theory has been develloped mostly by me and @Scott Morrison. I would be happy to discuss any questions you have regarding the approach to take.

[Antoine Labelle]

About the representation v.s. Rep/fdRep question, as I mentioned somewhere above I am doing a kind of experiment to see if most of the theory can be developed using the category theory library, which is why character is only defined for fdRep. The idea is that when talking about characters the variables should always be of type fdRep and the construction of new representations should occur as much as possible within fdRep, so that you don't have to do things like (fdRep.of ρ).character. You can look at this thread for some discussion about that.

[Antoine Labelle]

Now, what I've observed is that this works fairly well as long as we can indeed do everything internal to fdRep, but since the API for Rep/fdRepis still something in progress and not fully developed, it's not always possible and sometimes annoying back-and-forth between the categorical and non-categorical libraries is needed. For example docs#representation.lin_hom in categorical language should be docs#category_theory.ihom, but since we don't have yet that Rep and fdRep are closed categories (i.e. ihom is always defined) the statement of docs#fdRep.char_lin_hom requires fdRep.of (I do plan on adding the closed structure and fixing that in the future though).

[Antoine Labelle]

But this is really an experiment, so if you want to develop the API for representations in a more classical way, replicating all the linear_map API you're also welcome to do it.

[Antoine Labelle]

Let me know if you have any other questions.

[Winston Yin]

Replicating the linear_map API is not ideal but it’s the most straightforward thing I could do. However, I would also like to understand the benefits of the categorical approach. Is the main idea that the restrictions on V are now contained as a field in the fdRep structure rather than using type class in the hypotheses? How would one express additional conditions on V, say, smul_comm_class k’ k V for some other k’?

[Antoine Labelle]

I think the main benefit of the categorical approach is precisely to avoid replicating all the API for morphisms, equivalences, subobjects, products, etc. whenever we want to define a new kind of structure. Instead of repeatedly proving the same things in different contexts, it's nice to prove them once and for all for general categories (with suitable extra structure; monoidal, braided, closed, etc.) and then to apply them in various contexts.

[Antoine Labelle]

If we want to look at representations with additional structure or conditions, we can simply define a new category for these and possibly some forgetful functor that relate it to fdRep.

[Winston Yin]

Made a PR #15196 for rep_hom and rep_equiv. I figured I should push these while I try to understand how it works in category theory

[Antoine Labelle]

I left a few comments. You have a weird linting error that you should try to fix by the way, you can ask for help in another thread if you can't fix it.

[Winston Yin]

Thanks, Antoine!

[Winston Yin]

I also finally spent some time learning category theory, with the hope that I'll start to understand some of your and Scott's work

[Winston Yin]

For example docs#representation.lin_hom in categorical language should be docs#category_theory.ihom, but since we don't have yet that Rep and fdRep are closed categories

It seems to me that lin_hom is not exactly ihom on Rep k G, but rather ihom on Module k that has a G-action. If lin_hom is restricted to linear maps that commute with the G-action, it becomes trivial. Am I missing something?

[Antoine Labelle]

You're confusing the internal hom ihom with the hom-sets. A priori the internal hom does not need to have anything to do with the hom-sets, and you can check that for the category Rep k G the internal hom is indeed linhom using the definition of ihom as the adjoint of tensor product.

[Winston Yin]

Ah this make sense after I read the definition again. Thanks!

[Scott Morrison]

I would be excited to see if we can avoid all this. It's a lot of boilerplate, and perhaps we can just use the category theoretic interface.