English
The action of the alternating group has trivial blocks: any block is trivial.
Русский
Действие чередующей группы имеет тривиальные блоки: любой блок тривиален.
LaTeX
$$IsTrivialBlock B$$
Lean4
/-- The action of the alternating group has trivial blocks.
This holds for any `α`, even when `Nat.card α ≤ 2` and the action
is not preprimitive, because it is not pretransitive. -/
theorem isTrivialBlock_of_isBlock {B : Set α} (hB : IsBlock (alternatingGroup α) B) : IsTrivialBlock B :=
by
rcases le_or_gt (Nat.card α) 2 with h2 | h2
· exact isTrivialBlock_of_card_le_two h2 B
rcases le_or_gt (Nat.card α) 3 with h3 | h4
· replace h3 : Nat.card α = 3 := le_antisymm h3 h2
have : IsPretransitive (alternatingGroup α) α := isPretransitive_of_three_le_card α h3.ge
have : IsPreprimitive (alternatingGroup α) α := IsPreprimitive.of_prime_card (h3 ▸ prime_three)
exact this.isTrivialBlock_of_isBlock hB
suffices IsPreprimitive (alternatingGroup α) α by apply IsPreprimitive.isTrivialBlock_of_isBlock hB
apply isPreprimitive_of_is_two_pretransitive
letI := isMultiplyPretransitive α
apply isMultiplyPretransitive_of_le (n := Nat.card α - 2) _ (sub_le _ _)
rwa [← add_le_add_iff_right 2, Nat.sub_add_cancel (le_of_lt h2)]
