Commit 2025-05-18 18:58 6c6d0c0d

View on Github →

feat(GroupTheory/GroupAction/MultiplePretransitivity): define multiply transitive actions (#23386) This PR defines multiply transitive actions and proves the first basic lemmas about them.

  • MulAction.IsMultiplyPretransitive: An multiplicative action of a group G on a type α is n-transitive if the action of G on Fin n ↪ α is pretransitive.
  • Any action is 0-pretransitive
  • MulAction.is_one_pretransitive_iff : An action is 1-pretransitive iff it is pretransitive
  • MulAction.is_two_pretransitive_iff : An action is 2-pretransitive if for any a, b, c, d, such that a ≠ b and c ≠ d, there exist g : G such that g • a = b and g • c = d.
  • MulAction.isMultiplyPretransitive_of_le : If an action is n-pretransitive, then it is m-pretransitive for all m ≤ n.

Remarks on implementation

These results are results about actions on types n ↪ α induced by an action on α, and some results are developed in this context.

Estimated changes

modified def Fin.Embedding.append
modified theorem Fin.Embedding.coe_append
modified def Fin.Embedding.snoc
modified theorem Fin.Embedding.snoc_castSucc
modified theorem Fin.Embedding.snoc_last