Free actions

Stream: Is there code for X?

[Anatole Dedecker]

Am I going completely mad or are we really missing the definition of freeness of a group action ?!?

[Yaël Dillies]

Looks like we got away with faithful actions all this time :flushed:

[Aaron Liu]

isn't that just docs#MulAction + docs#IsCancelSMul

[Anatole Dedecker]

Aha, that works indeed. I’m a bit surprised by the name though, "free action" seems much more standard.

[Anatole Dedecker]

Also this doesn’t work to represent free monoid actions because of the extra cancellability assumption, but I guess that’s not a big deal

[Yury G. Kudryashov]

I'm not sure which definition is better for minor monoid actions. Could you please open a PR song the words "free action" to the docstring?

[Anatole Dedecker]

A bit too late for me right now, will do tomorrow if no one beats me to it

[Aaron Liu]

what's a free monoid action?

[Aaron Liu]

Anatole Dedecker said:

Aha, that works indeed. I’m a bit surprised by the name though, "free action" seems much more standard.

You have to think about the modules over a given ring

[Aaron Liu]

they're also smul

[Yury G. Kudryashov]

You can't have a free action / IsCancelSMul for modules because of smul_zero/zero_smul.

[Yury G. Kudryashov]

Aaron Liu said:

what's a free monoid action?

There are (at least) two ways to generalize free group actions to monoids. One way is to say that a • x = x → a = 1, another one is to say something like docs#IsCancelSMul.

[Anatole Dedecker]

My (probably naïve) guess is that a • x = x → a = 1 is not a good thing in this context. It would be like defining injectivity of a monoid hom by its kernel being trivial, which is just not an interesting notion. See also the choice that was made for docs#FaithfulSMul

[Yaël Dillies]

... or docs#Module.IsTorsionFree, although the "not interesting notion" is unfortunately used by the left ℝ≥0∞-action over itself in docs#MeasureTheory.Measure.ae_smul_measure_iff, since the more interesting one doesn't hold :half_frown:

[Anatole Dedecker]

#31009 (sorry for the delay)