Group actions

Stream: maths

[Antoine Chambert-Loir]

I am in the course of formalizing a substantial part of the book of Wielandt on Finite group actions. One of the goals will be to have a “natural” proof for simplicity of many groups, using Iwasawa's criterion and the notion of primitivity. Meanwhile, there should be a theorem of Jordan that a primitive subgroup of the alternating group that contains one 3-cycle is the full alternating group. Later goals could be a proof of the O'Nan-Scott theorem, but we'll see.
There are three branches in progress,

• branch#iwasawa-lemma proves the Iwasawa lemma but does not go far enough for having the desired properties of primitive actions
• branch#acl-Wielandt is a more systematic way of studying primitivity
• branch#an-very-simple proves the simplicity of the alternating group in a simple way, independent of the other two branches.

A few questions now :

• Recall that a group action on a set X is $n$-transitive if it acts transitively on $n$-tuples of pairwise distinct elements. There are at least two ways to encode this : either l : list X with l.length = n /\ l.nodup, or using injective maps fin n -> X, and possibly other. Which one seems preferable to you? (branch#Wielandt uses lists).
• A boring part of what I wrote during the last 2 days consists in rewriting lists (using cons), coercing them to subtypes, etc. If some people (@Yaël Dillies , @Eric Wieser …) could have a look and tell me whether this is ridiculously complicated, or kind of the way to do it, it would be cool.
• The way mathematicians do the theory involves a lot of other group actions. For example, if a group $G$ acts on a set $X$, it acts on list X, on set X, on invariant subsets, on nodup_lists, on lists of given size, etc. Also, the subgroup of $G$ fixing pointwise a subset s : set X acts on s.compl. All these coercions require instances, and a lot of rewriting lemmas. I already wrote some of them. Maybe this is not the good way to do it. You can have a look in the file ad_sub_mul_actions.lean .

Thank y'all for your help and comments.

[Adam Topaz]

Concerning question 1, I think using injective maps is the best approach, at least because it will be easier to define the group action on this type using this approach.

[Yaël Dillies]

namely fin n ↪ X, which can probably be generalized to ι ↪ X in most places.

[Adam Topaz]

The file data/fin (I think?) should have a lot of the list-like API (cons, etc.) for tuples defined as functions from fin n.

[Yaël Dillies]

The one thing you will have a hard time doing with that approach is adding/removing elements.

[Adam Topaz]

Yeah, to remove elements you can compose with docs#fin.succ_above and similar lemmas

[Yaël Dillies]

If you want to add/remove elements a lot, then I'd suggest using (a subtype) of list or (a subtype of) docs#array.

[Adam Topaz]

I disagree with @Yaël Dillies here. If some construction is missing that would be useful for the fin n approach, then it is almost surely something that would be useful for simplicial sets, so it should be added anyway.

[Eric Wieser]

Regarding your last question, I think instance : mul_action G (list X) is a natural thing to have alongside the corresponding actions on set and finset, it's just that no one has needed it

[Yaël Dillies]

Yes, and similarly for docs#sym2, docs#sym and all this little corner of data structures.

[Eric Wieser]

Recall that a group action on a set X is n-transitive if it acts transitively on n-tuples of pairwise distinct elements.

I wasn't able to find the statement of this in branch#acl-Wielandt - is it in one of the other branches?

[Antoine Chambert-Loir]

@Eric Wieser Indeed, and I wrote some of them. The question is how much does one need ?

[Antoine Chambert-Loir]

Eric Wieser said:

Recall that a group action on a set X is n-transitive if it acts transitively on n-tuples of pairwise distinct elements.

I wasn't able to find the statement of this in branch#acl-Wielandt - is it in one of the other branches?

https://github.com/leanprover-community/mathlib/blob/acl-Wielandt/acl-sandbox/group_theory/wielandt.lean#L1267

(I have the strange habit of storing the new files that I'm working on in a bizarre directory.)

[Eric Wieser]

I'm really struggling to understand why $n$-transitive is interesting - is it any different to "transitive and cardinality at least $n$"?

[Eric Wieser]

Nevermind, I get it now - You're using the same action for every point in the list

[Eric Wieser]

Is is_multiply_pretransitive M α m equivalent to is_pretransitive M (fin m → α) and m ≤ #α ?

[Antoine Chambert-Loir]

Essentially yes, but to is_pretransitive M (fin m ↪ X α).
(The cardinal inequality would be added to get is_multiply_transitive.)

[Antoine Chambert-Loir]

(Can one write something like m ≤ #α when α is not a fintype? I had to define card_ge α m to mean that there is a nodup listof melements of type α.

[Eric Wieser]

# is docs#cardinal.mk not docs#fintype.card

[Eric Wieser]

I'm not sure I understand why you need fin m ↪ X and not just fin m → X. The latter is much more appealing because it already has the pointwise action defined on it

[Sebastien Gouezel]

If you want to say that an action acts transitively on m-tuples of points, you can not use fin m → X, right?

[Kevin Buzzard]

Eric the issue is that a constant function fin 2 -> X can never be mapped to a non-constant function. 2-transitivity means "given random a != b and c != d, there exists g such that g bub a = c and g bub b = d". If you allow a=b this breaks.

[Eric Wieser]

Thanks, I knew I'd missed something; in this case the constant function example

[Eric Wieser]

I created #12798 to makef : fin m ↪ X have an codomain-wide action by g : G, such that ⇑(g • f) = g • ⇑f

[Antoine Chambert-Loir]

To go on with maths, the issue of primitivity is similar, in so that primitive actions are sometimes called one-and-a-half-transitive : a primitive action is transitive, and a 2-transitive action is primitive. To give examples:

• The 2-Sylow subgroups of the symmetric group $\mathfrak S_4$ acts transitively on $\{1,2,3,4\}$ but not primitively (they preserve a partition such as $\{\{1,2\},\{3,4\}\}$ ).

• The action of the orthogonal group $\mathrm{SO}(3,\mathbf R)$ on the 3-dimensional projective space, it is not 2-transitive (because it respects the angle between two lines), but it is primitive.)

[Antoine Chambert-Loir]

Eric Wieser said:

# is docs#cardinal.mk not docs#fintype.card

I feel I will need docs#enat.card because of infinite sets. ;-)

[Kevin Buzzard]

We wrote nat.card when doing Sylow's theorems and here it works very well, because all finite groups have cardinality >= 1 and all infinite groups have cardinality 0. But I appreciate that this trick doesn't work in general :-)

[Thomas Browning]

Using 1,2,3,...,0 for 1,2,3,...,infinity is pretty nice. I've also been using this same trick for index, and so far it's worked pretty smoothly. (But as Kevin mentioned, this works best when 0 doesn't appear already)

[Eric Rodriguez]

this also works well for exponents

[Eric Rodriguez]

(as in docs#monoid.exponent)

[Damiano Testa]

It's a similar trick to the characteristic of a field, as well

[Kevin Buzzard]

Yes, that's a situation where for some reason we went for the 0 convention and not the infinity convention. You either look at the size of the image of Z in the field or the nonnegative generator of the kernel.

[Antoine Chambert-Loir]

However, this useful lemma is false with docs#nat.card and works with docs#enat.card :

import set_theory.fincard

lemma nat_le_enat_card_iff_exists_embedding (α : Type*) (n : ℕ) :
  (n : enat) ≤ enat.card α ↔ nonempty (fin n ↪ α) :=
begin
  split,
  { intro hα,
    cases fintype_or_infinite α with hfα hfα'; resetI,
    { refine function.embedding.nonempty_of_card_le _,
      rw [fintype.card_fin n, ← enat.coe_le_coe, ← enat.card_eq_coe_fintype_card],
      exact hα },
    { use (infinite.nat_embedding α) ∘ (function.embedding.subtype _),
      apply function.injective.comp; exact embedding_like.injective _ } },
  { rintro ⟨h : fin n ↪ α⟩,
    cases fintype_or_infinite α; resetI,
    -- case finite
    simp only [enat.card_eq_coe_fintype_card, enat.coe_le_coe],
    rw ← fintype.card_fin n,
    exact fintype.card_le_of_embedding h,
    -- case infinite
    simp only [enat.card_eq_top_of_infinite, le_top] }
end

@Eric Wieser , should I PR this in set_theory.fincard.lean ?

[Eric Wieser]

Is there a reason you prefer docs#enat.card to docs#cardinal.mk here?

[Eric Wieser]

I suspect your lemma is almost true by definition for cardinals

[Antoine Chambert-Loir]

Maybe that's only because I couldn't find the function I needed…

[Antoine Chambert-Loir]

You're right, that's docs#cardinal.le_def !