Zulip Chat Archive

Stream: maths

Topic: Semisimple modules

Aaron Anderson (Dec 31 2020 at 18:38):

I'm looking to define semisimple modules, but there are a few equivalent definitions, and I'm not sure how to express all of them in mathlib at the moment.

Aaron Anderson (Dec 31 2020 at 18:42):

In Lang's Algebra, there are the following three conditions for when M is semisimple:

  1. M is the sum of a family of simple submodules
  2. M is the direct sum of a family of simple submodules
  3. Any submodule of M is a direct summand

Aaron Anderson (Dec 31 2020 at 18:42):

Of these, 1. and 2. require #5473 defining simple modules

Aaron Anderson (Dec 31 2020 at 18:43):

and 2. and 3. at face value require defining internal direct sums

Aaron Anderson (Dec 31 2020 at 18:44):

Currently, the closest thing to semisimplicity in mathlib is Maschke's Theorem, which shows that every submodule has a complement in the sense of is_compl.

Aaron Anderson (Dec 31 2020 at 18:45):

Ideally, I'd pick one of these definitions, state all of them, prove them all equivalent, and make that a PR.

Aaron Anderson (Dec 31 2020 at 18:46):

However, I think there's a lot to work out with internal direct sums that I'm not sure how to do, and I'm not sure it's necessary at the moment to profit from semisimple modules (and move towards representation theory).

Aaron Anderson (Dec 31 2020 at 18:50):

Would the following be a reasonable approach?

  • Develop the internal direct sum for 2 submodules (show that if they are disjoint, then their sup is isomorphic to their direct product)
  • Show that if two submodules satisfy is_compl, then the whole module is isomorphic to their direct product
  • Define is_semisimple_module using the exists_is_compl definition in our version of Maschke's Theorem
  • Show that this is equivalent to 1., where by "sum" I mean Sup.

Aaron Anderson (Dec 31 2020 at 18:54):

That last definition is equivalent to saying that the complete_lattice is atomistic, once I show that simple submodules are the same as minimal submodules, which are atoms in the order. Much of the machinery for that is in #5493

Johan Commelin (Dec 31 2020 at 18:58):

I think we'll need an API for internal direct sum anyway. But I agree that it doesn't sound very appealing to work on.

Johan Commelin (Dec 31 2020 at 18:59):

I haven't thought hard about it yet. If anybody knows of other libraries that have worked on this, that would be good to know.

Johan Commelin (Dec 31 2020 at 18:59):

Is there something like this done in mathcomp or Isabelle?

Kevin Buzzard (Dec 31 2020 at 19:09):

If it's any help, for vector spaces over a field 1. says "there exists a spanning set", 2. says "there exists a basis" and 3. says "this module is projective". They're all true for vector spaces over a field. They're equivalent but not always all true for modules over a commutative local ring.

Kevin Buzzard (Dec 31 2020 at 19:10):

I think that in our setting, 1. just says "the inf of the simple submodules is top".

Kenny Lau (Dec 31 2020 at 19:11):

you mean the sup

Kevin Buzzard (Dec 31 2020 at 19:11):

and 3. can be just written as "for any S in M, there's a map from M to S which is a one-sided inverse".

Kevin Buzzard (Dec 31 2020 at 19:12):

Being a direct summand is the same as having a compl, but compls are in general not unique.

Last updated: Dec 20 2023 at 11:08 UTC