Zulip Chat Archive

Stream: maths

Topic: Semisimple modules


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Aaron Anderson (Dec 31 2020 at 18:42):

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

view this post on Zulip Aaron Anderson (Dec 31 2020 at 18:43):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Dec 31 2020 at 18:59):

Is there something like this done in mathcomp or Isabelle?

view this post on Zulip 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.

view this post on Zulip 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".

view this post on Zulip Kenny Lau (Dec 31 2020 at 19:11):

you mean the sup

view this post on Zulip 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".

view this post on Zulip 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: May 14 2021 at 20:13 UTC