Type of subrepresentation

Stream: Is there code for X?

[Gareth Ma]

I am playing around with RepresentationTheory.FdRep, which defines (finite dimensional) representations as a (bundled) action of $G$ on a finitely generated module $V/k$, so in Lean code

{k G : Type u} [Field k] [Group G] (V : FdRep k G)

How should I construct/define the type of a subrepresentation, i.e. a submodule of $V/k$ compatible with the $G$-action? I was guessing to do something like

(W : FdRep k G) (hW : IsSubmodule W V)

But there is no mix-in (I think that's what it's called) for IsSubmodule. \subset doesn't work since I also need to preserve the module structure right, and defining W as a : Submodule k V plus it's G-stable means well I can't use the FdRep API I think.

[Gareth Ma]

I can't find any "sub-action" either, unless it's some abstract nonsense hidden in CategoryTheory.<10 folders deep>.<5 namespace deep>

[Gareth Ma]

I tried W : Action (Subobject V.V) (MonCat.of G) (just guessing), and while Subobject V.V is a Category, it's not a LargeCategory.

[Gareth Ma]

I should have Zulip'ed harder, but there was this thread which defined subrepresentation (Lean 3) but was never pushed upstream.

[Gareth Ma]

https://github.com/leanprover-community/mathlib/compare/master...representation_theory_winstonyin There are 3000 lines of un-upstreamed code here

@Kim Morrison @Antoine Labelle pinging because you two are the main author of the RepresentationTheory library.

[Gareth Ma]

I just looked at the proof of Maschke's Theorem, and I realised that (if I understand correctly) a subrepresentation is written as Submodule (MonoidAlgebra k G) V, i.e. a $k[G]$-submodule. Is that correct?

[Gareth Ma]

Okay I kind of understand, so this "works" because [Module (MonoidAlgebra k G) V], and there is equivalenceModuleMonoidAlgebra to convert between this hypothesis and ... V : Rep k G

[Kevin Buzzard]

The issue with representation theory is that there are two ways to set it up -- either as the theory of kG-modules via [Module kG V] or using the language of category theory via Rep and fdRep, and we went with category theory and now every undergraduate who comes along is confused by it. In set theory there's such a thing as a subset. In type theory we emulate this via Set and make second-class citizens (terms not types) which we then coerce to types if we want to think of them as modules and not submodules. In category theory an exact translation of the concept doesn't exist because objects of categories don't have elements as far as the theory is concerned so the literal concept of subset makes no sense. However if you're thinking categorically, which many undergraduates aren't, you realise that you can just get away with a monic morphism because up to isomorphism (which is all you can talk about in category theory anyway) a submodule is the same thing as a monic morphism in this category.

[Kevin Buzzard]

Basically category theory is dropping enough structure to make the theory the same as far as an expert is concerned but making the basics impenetrable for undergraduates. I've seen this with my own eyes before (representation theory projects in my class usually end up being given up on)

[Gareth Ma]

Thanks for the explanation about the set ups for rep theory, it's kind of inevitable due to Mathlib's philosophy I guess. But I think the issue about undergraduates finding it confusing can be (hopefully) resolved by writing better API to translate between the two set ups, plus having a tutorial on how to translate statements, e.g. a chapter on MIL. I can try to help with that once (1) I understand the math theory a bit better and (2) I understand the Mathlib setup a lot better

[Gareth Ma]

Integrals are set up as Borel integrals (I think?) but IntervalIntegral makes them usable for say number theory lol