primitive actions

Stream: maths

[Antoine Chambert-Loir]

In the ongoing branch#acl-Wielandt, I formalize results about primitive actions of groups on sets. This is fundamental material for the moment, it might go up to a theorem of Jordan that a primitive subgroup of the symmetric/alternating group that contains a transposition/a 3-cycle is the full symmetric group/the full alternating group.
Adding to this the Iwasawa criterion for simplicity, we will get a nice and complicated proof of simplicity for the alternating group.

In this field, with(G X : Type*) [group G] [mul_action G X], a B : set Xis called a block if ∀ (g : G), g • B = B ∨ disjoint (g • B) B, and the action is primitive if it is transitive and if all blocks are the trivial ones, which means : B = ∅ ∨ (∃ (x : X), B = {x}) ∨ B = ⊤)

I wonder about the interest of formulating the first two parts of the disjunction using either docs#set.subsingleton`, or docs#nontrivial (which means having at least 2 elements). What would you recommend ?

[Yaël Dillies]

Just noticing that you can replace ∀ (g : G), g • B = B ∨ disjoint (g • B) B by (range $ λ g : G, g • B).pairwise_disjoint id

[Kevin Buzzard]

You don't want to use nontrivial because that's about types not terms

[Kevin Buzzard]

We have empty and singleton and subsingleton for sets, perhaps subsingleton is the shortest way to do it

[Antoine Chambert-Loir]

@Yaël Dillies , at first, I was frightened by your reformulation, but it has a nice geometric content which is fundamental : the g • B form a partition of G, see line 91, definition of is_block' , and line 374, lemma is_block_system.of_block` in branch#acl-Wielandt.

[Antoine Chambert-Loir]

So maybe it is better to have a strong hypothesis, and in any case, we have is_block_mk to create instances of is_block.

[Yaël Dillies]

Yes, exactly. My biggest concern is API-writing and I feel like an homogeneous definition like the one I proposed is much easier to write an API for.

[Yaël Dillies]

This reminds me of the condition you need to make a quotient of a manifold under an action.

[Yaël Dillies]

I forgot the name but with your stuff it would be written ∀ s, is_open s → is_block action s.

[Antoine Chambert-Loir]

Can you explain in a few words why writing an API would be much easier this way? (The same tension exists in unformalized math, you can switch the strength of a hypothesis from a definition and the theorem. In one case, it is hard to prove that the property holds, but it directly has many implications ; in the other case, it is easy to prove that the property holds, but you need to apply a theorem to get implications. I am tempted to prefer the first solution.)