Group action refactor

Stream: maths

[Chris Hughes]

Currently we use the has_scalar typeclass for group actions. This seems to me slightly inappropriate for a lot of finite group theory because the actions considered aren't necessarily canonical and there are several on the same type (for example a group acts on itself by both multiplication and conjugation). You often only define an action to prove by orbit-stabilizer that it has a fixed point of something, and then never mention it again. You don't really need the • notation either.

@Eric Wieser suggested the definition of a new class in #8592. It would be an action satisfying `a • (x * y) = a • x * a • y. I could in principle have used such a class to define semidirect products, but I deliberately did not because I thought that the morphism G →* mul_aut H might not be canonical.

My question is whether we should refactor some of the finite group theory and use G →* perm α in the statement of the orbit stabilizer theorem and the finite group theory lemmas that depend on it?

This problem seems somewhat analogous to the algebra type class; although we need this class, we definitely need ring_hom as well so we're not defining type aliases every time we have a non-identity ring hom R -> R. The same sort of problem might come up if we ever want to define $\mathbb{R}^n$ as an $\mathbb{R}[X]$ module - there are many structures that we want to consider.

[Eric Wieser]

It's worth noting that the new typeclass I'm suggesting is just a weaker version of the (almost entirely unused) docs#mul_semiring_action typeclass that already exists

[Patrick Massot]

I don't have an answer to your question, I can only agree very strongly with the observation that we often have several actions of a group on the same space.

[Eric Wieser]

Perhaps @Kenny Lau should chime in, since they created mul_semiring_action

[Oliver Nash]

I also agree that we'll need to deal with this one day and I'm glad to see it getting talked about again. I have occasionally worried about the way we use typeclasses to store data (such as an action) though I'm impressed how far we've got without any real issues.

[Oliver Nash]

Having said all that, if we did want to work with the conjugation action and just ignore this elephant we could consider something like:

import data.bracket
import algebra.group

variables (G : Type*) [group G]

instance group.conjugation : has_bracket G G := ⟨λ g h, g*h*g⁻¹⟩

variables (g h h' : G)

lemma group_bracket_def : ⁅g, h⁆ = g*h*g⁻¹ := rfl

example : ⁅g, h*h'⁆ = ⁅g, h⁆ * ⁅g, h'⁆ := by simp [group_bracket_def]

-- etc.

Mind you we would have to make sure not to do this for additive groups:

-- Breaks `lie_ring`:
instance very_bad (G : Type*) [add_group G] : has_bracket G G := ⟨λ g h, g + h - g⟩

[Eric Wieser]

Presumably if we're talking about the conjugation action then #8627 is the relevant PR and #8592 is only really a downstream consequence.

[Johan Commelin]

I'm not really up to speed with the measure theory library, but I have the impression that a similar problem was solved there.

[Johan Commelin]

One can talk about "the" measure on a space, but otoh one can also integrate against "a" specific measure by providing it explicitly.

[Johan Commelin]

@Yury G. Kudryashov didn't you set up something like that?

[Anatole Dedecker]

Indeed. The way it works is that defs take an explicit μ : measure α argument which can be built automatically using the docs#volume_tac tactic which just fills the "canonical" measure (if there is one)

[Anatole Dedecker]

See for example docs#measure_theory.integrable

[Eric Rodriguez]

Whenever I'm working with different actions (on paper anyways) I always feel like I have different notations for each. So maybe the "right" solution is just encourage more use of `local notation x •ₜ y := action_t x y for when actions differ, and if there really is a canonical action just use •

[Eric Wieser]

I noticed that we already have docs#mul_action.perm and docs#mul_action.function_End and #intermediate_field.subgroup_action. Generalizing these in #8724 gives us another spelling of conjugation, mul_aut.conj g • h.

[Chris Hughes]

The trouble with this is that it's an action of a different group so I won't be able to apply the theorem https://leanprover-community.github.io/mathlib_docs/group_theory/p_group.html#mul_action.card_modeq_card_fixed_points . The mul_action notation isn't that desirable for conjugation, I just want the group action lemmas.

[Eric Wieser]

Can you elaborate what you mean by that? Is the problem that you end up obtaining card (G ≃* G) and not card G when you apply that lemma, in the situation I describe?

[Chris Hughes]

Yes

[Eric Wieser]

I think using mul_aut.conj.restrict_range g • h would work.

[Chris Hughes]

That would work for this particular problem, but I don't think it's a great long term solution. It doesn't help if I want to apply the orbit stabilizer theorem for example, or at least it's very awkward.

[Eric Wieser]

Chris Hughes said:

Eric Wieser suggested the definition of a new class in #8592. It would be an action satisfying `a • (x * y) = a • x * a • y

I have added this class in #8918, which at this point in time already has four quite a few instances.

[Yury G. Kudryashov]

I should have an unfinished draft of this kind of refactor.

[Yury G. Kudryashov]

But I think that it's easier to redo it than to revive the old code.

[Yury G. Kudryashov]

I suggest the following notation: c •[a] x for a.smul c x.

[Yury G. Kudryashov]

I think that we should have lemmas in the mul_action about non-canonical actions. Most of them should have a version in the root namespace taking [mul_action M α] instead of (a : mul_action M α).

[Yury G. Kudryashov]

(btw, I suggest notation M ` ↷ ` α := mul_action M α)

[Johan Commelin]

you need moar ``` back ` ticks ```

[Yury G. Kudryashov]

I hope that we can use some tactic to transfer lemmas from (a : mul_action M α) to [mul_action M α].

[Yury G. Kudryashov]

I tried to make this refactor a couple of times, and failed because I failed to stop myself from touching too many things.

[Thomas Browning]

I'm a bit late to the party, but this sort of refactor sounds good to me. I like the idea of being able to pass in a : M ↷ α. The tactic idea sounds nice, if it's feasible.

[Eric Wieser]

How does this notation extend to distrib_mul_action etc?

[Eric Wieser]

Also, you could argue we already have a : M →* function.End α as an existing notation to that proposed arrow