Library mathcomp.fingroup.action

Group action: orbits, stabilisers, transitivity. is_action D to == the function to : T -> aT -> T defines an action of D : {set aT} on T. action D T == structure for a function defining an action of D. act_dom to == the domain D of to : action D rT. {action: aT &-> T} == structure for a total action. := action [set: aT] T TotalAction to1 toM == the constructor for total actions; to1 and toM are the proofs of the action identities for 1 and a * b, respectively. is_groupAction R to == to is a group action on range R: for all a in D, the permutation induced by to a is in Aut R. Thus the action of D must be trivial outside R. groupAction D R == the structure for group actions of D on R. This is a telescope on action D rT. gact_range to == the range R of to : groupAction D R. GroupAction toAut == constructs a groupAction for action to from toAut : actm to @* D \subset Aut R (actm to is the morphism to {perm rT} associated to 'to'). orbit to A x == the orbit of x under the action of A via to. orbit_transversal to A S == a transversal of the partition orbit to A @: S of S, provided A acts on S via to. amove to A x y == the set of a in A whose action sends x to y. 'C_A[x | to] == the stabiliser of x : rT in A :&: D. 'C_A(S | to) == the pointwise stabiliser of S : {set rT} in D :&: A. 'N_A(S | to) == the global stabiliser of S : {set rT} in D :&: A. 'Fix(S | to) [a] == the set of fixpoints of a in S. 'Fix(S | to)(A) == the set of fixpoints of A in S. In the first three A can be omitted and defaults to the domain D of to; in the last two S can be omitted and defaults to [set: T], so 'Fix_to[a] is the set of all fixpoints of a. The domain restriction ensures that stabilisers have a canonical group structure, but note that 'Fix sets are generally not groups. Indeed, we provide alternative definitions when to is a group action on R: 'C(G | to)(A) == the centraliser in R :&: G of the group action of D :&: A via to 'C(G | to) [a] == the centraliser in R :&: G of a \in D, via to. These sets are groups when G is; G can be omitted: 'C(|to)(A) is the centraliser in R of the action of D :&: A via to. [acts A, on S | to] == A \subset D acts on the set S via to. {acts A, on S | to} == A acts on the set S (Prop statement). {acts A, on group G | to} == [acts A, on S | to] /\ G \subset R, i.e., A \subset D acts on G \subset R, via to : groupAction D R. [transitive A, on S | to] == A acts transitively on S. [faithful A, on S | to] == A acts faithfully on S. acts_irreducibly to A G == A acts irreducibly via the groupAction to on the nontrivial group G, i.e., A does not act on any nontrivial subgroup of G. Important caveat: the definitions of orbit, amove, 'Fix(S | to)(A), transitive and faithful assume that A is a subset of the domain D. As most of the permutation actions we consider are total this is usually harmless. (Note that the theory of partial actions is only partially developed.) In all of the above, to is expected to be the actual action structure, not merely the function. There is a special scope %act for actions, and constructions and notations for many classical actions: 'P == natural action of a permutation group via aperm. 'J == internal group action (conjugation) via conjg (_ ^ _). 'R == regular group action (right translation) via mulg (_ * _). (However, to limit ambiguity, _ * _ is NOT a canonical action.) to^* == the action induced by to on {set rT} via to^* (== setact to). 'Js == the internal action on subsets via _ :^ _, equivalent to 'J^*. 'Rs == the regular action on subsets via rcoset, equivalent to 'R^*. 'JG == the conjugation action on {group rT} via (_ :^ _)%G. to / H == the action induced by to on coset_of H via qact to H, and restricted to (qact_dom to H) == 'N(rcosets H 'N(H) | to^* ). 'Q == the action induced to cosets by conjugation; the domain is qact_dom 'J H, which is provably equal to 'N(H). to %% A == the action of coset_of A via modact to A, with domain D / A and support restricted to 'C(D :&: A | to). to \ sAD == the action of A via ract to sAD == to, if sAD : A \subset D. [Aut G] == the permutation action restricted to Aut G, via autact G. < [nRA]> == the action of A on R via actby nRA == to in A and on R, and the trivial action elsewhere; here nRA : [acts A, on R | to] or nRA : {acts A, on group R | to}. to^? == the action induced by to on sT : @subType rT P, via subact to with domain subact_dom P to == 'N( [set x | P x] | to). phi == the action of phi : D >-> {perm rT}, via mact phi. to \o f == the composite action (with domain f @*^-1 D) of the action to with f : {morphism G >-> aT}, via comp_act to f. Here f must be the actual morphism object (e.g., coset_morphism H), not the underlying function (e.g., coset H). The explicit application of an action to is usually written (to%act x a), but %act can be omitted if to is an abstract action or a set action to0^*. Note that this form will simplify and expose the acting function. There is a %gact scope for group actions; the notations above are recognised in %gact when they denote canonical group actions. Actions can be used to define morphisms: actperm to == the morphism D >-> {perm rT} induced by to. actm to a == if a \in D the function on D induced by the action to, else the identity function. If to is a group action with range R then actm to a is canonically a morphism on R. We also define here the restriction operation on permutations (the domain of this operations is a stabiliser), and local automorphism groups: restr_perm S p == if p acts on S, the permutation with support in S that coincides with p on S; else the identity. Note that restr_perm is a permutation group morphism that maps Aut G to Aut S when S is a subgroup of G. Aut_in A G == the local permutation group 'N_A(G | 'P) / 'C_A(G | 'P) Usually A is an automorphism group, and then Aut_in A G is isomorphic to a subgroup of Aut G, specifically restr_perm @* A. Finally, gproduct.v will provide a semi-direct group construction that maps an external group action to an internal one; the theory of morphisms between such products makes use of the following definition: morph_act to to' f fA <=> the action of to' on the images of f and fA is the image of the action of to, i.e., for all x and a we have f (to x a) = to' (f x) (fA a). Note that there is no mention of the domains of to and to'; if needed, this predicate should be restricted via the {in ...} notation and domain conditions should be added.

Need to close the Section here to avoid re-declaring all Argument Scopes

camlp4 grammar factoring

Lemmas that do not require the group structure on the action domain. Some lemmas like actMin would be actually be valid for arbitrary rT, e.g., for actions on a function type, but would be difficult to use as a view due to the confusion between parameters and assumptions.

Warning: this directive depends on names of bound variables in the definition of injective, in ssrfun.v.

Lemmas that require a (partial) group domain.

These lemmas are only established for total actions (domain = [set: rT])

This is Aschbacher (5.2)