SubMulAction

Stream: PR reviews

[Antoine Chambert-Loir]

PR #23962 (and the ongoing #23970) introduces docs#SubMulAction s of various subgroups on various subsets of an action of a group G on a type A.

• for a : A, of stabilizer G aon the complement of {a}
• for s : Set A, of fixingSubgroup G s on the complement of s

and develops their relations. This is useful (and classical) in group theory to establish multiple transitivity properties.

[Antoine Chambert-Loir]

A lot of these relations are essentially trivial, for example, comparing fixingSubgroup (stabilizer G a) s to fixingSubgroup G (insert a s) (except that this doesn't type!).
Maybe, it could be possible and more practical to introduce a notion of SubSubMulAction which depends on a subgroup and on a subset.

[Antoine Chambert-Loir]

This is reminiscent of the type-theoretical nuisances that @Peter Nelson had to fight against in his development of matroid theory.