Zulip Chat Archive

Stream: new members

Topic: Annihilator of modules over noncommutative ring


Haruhisa Enomoto (May 04 2022 at 11:07):

Sorry again for my noncomutative question.
I encountered the problem (for me) that an annihilator of a module over a ring is only defined for commutative rings in submodule.annihilator.
I want it to work for noncommutative rings, but some problem arises.
In mathlib, annihilator of M is defined to be the kernel of left action, which is R-hom, so it automatically becomes an left ideal. But the same definition doesn't work for noncommutative case.
I think the solution of this is to

  1. change the definition of submodule.annihilator to include the noncommutative case, and
  2. rewrite all the proof which use submodule.annihilator.

Is this a correct way? Or maybe is there any simple solution?
(And I also wonder how to define submodule.annihilator so that part 2 becomes easier.)

Johan Commelin (May 04 2022 at 11:09):

I think you could do (1), and then add a lemma submodule.annihilator_def_cr which proves that it is the same as the old def in the commutative case. After that (2) should be easy (just rw with that new lemma, when needed).

Johan Commelin (May 04 2022 at 11:10):

Once that is done, you can generalize the rest of the API to the nc case in bits and pieces as needed.

Eric Wieser (May 04 2022 at 11:26):

I would guess we want a version of linear_map.lsmul with a right action by R somewhere?


Last updated: Dec 20 2023 at 11:08 UTC