Multiple transitivity

• MulAction.IsMultiplyPretransitive: A multiplicative action of a group G on a type α is n-transitive if the action of G on Fin n ↪ α is pretransitive.

• MulAction.is_zero_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.isPreprimitive_of_is_two_pretransitive : A 2-transitive action is preprimitive

• MulAction.isMultiplyPretransitive_of_le : If an action is n-pretransitive, then it is m-pretransitive for all m ≤ n, provided α has at least n elements.

Results for permutation groups

• The permutation group is pretransitive, is multiply pretransitive, and is preprimitive (for its natural action)

• Equiv.Perm.eq_top_if_isMultiplyPretransitive: a subgroup of Equiv.Perm α which is Nat.card α - 1 pretransitive is equal to ⊤.

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.

def Function.Injective.mulActionHom_embedding {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {H : Type u_3} {β : Type u_4} [Group H] [MulAction H β] {σ : G → H} {f : α →ₑ[σ] β} (ι : Type u_5) (hf : Injective ⇑f) : (ι ↪ α) →ₑ[σ] ι ↪ β

An injective equivariant map α →ₑ[σ] β induces an equivariant map on embedding types (ι ↪ α) → (ι ↪ β).

Equations

• Function.Injective.mulActionHom_embedding ι hf = { toFun := fun (x : ι ↪ α) => { toFun := f.toFun ∘ x.toFun, inj' := ⋯ }, map_smul' := ⋯ }

def Function.Injective.addActionHom_embedding {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {H : Type u_3} {β : Type u_4} [AddGroup H] [AddAction H β] {σ : G → H} {f : α →ₑ[σ] β} (ι : Type u_5) (hf : Injective ⇑f) : (ι ↪ α) →ₑ[σ] ι ↪ β

An injective equivariant map α →ₑ[σ] β induces an equivariant map on embedding types (ι ↪ α) → (ι ↪ β).

Equations

• Function.Injective.addActionHom_embedding ι hf = { toFun := fun (x : ι ↪ α) => { toFun := f.toFun ∘ x.toFun, inj' := ⋯ }, map_vadd' := ⋯ }

@[simp]

theorem Function.Injective.mulActionHom_embedding_apply {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {H : Type u_3} {β : Type u_4} [Group H] [MulAction H β] {σ : G → H} {f : α →ₑ[σ] β} {ι : Type u_5} (hf : Injective ⇑f) {x : ι ↪ α} {i : ι} : ((mulActionHom_embedding ι hf) x) i = f (x i)

@[simp]

theorem Function.Injective.addActionHom_embedding_apply {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {H : Type u_3} {β : Type u_4} [AddGroup H] [AddAction H β] {σ : G → H} {f : α →ₑ[σ] β} {ι : Type u_5} (hf : Injective ⇑f) {x : ι ↪ α} {i : ι} : ((addActionHom_embedding ι hf) x) i = f (x i)

theorem Function.Injective.mulActionHom_embedding_isInjective {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {H : Type u_3} {β : Type u_4} [Group H] [MulAction H β] {σ : G → H} {f : α →ₑ[σ] β} {ι : Type u_5} (hf : Injective ⇑f) : Injective ⇑(mulActionHom_embedding ι hf)

theorem Function.Injective.addActionHom_embedding_isInjective {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {H : Type u_3} {β : Type u_4} [AddGroup H] [AddAction H β] {σ : G → H} {f : α →ₑ[σ] β} {ι : Type u_5} (hf : Injective ⇑f) : Injective ⇑(addActionHom_embedding ι hf)

theorem Function.Bijective.mulActionHom_embedding_isBijective {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {H : Type u_3} {β : Type u_4} [Group H] [MulAction H β] {σ : G → H} {f : α →ₑ[σ] β} {ι : Type u_5} (hf : Bijective ⇑f) : Bijective ⇑(Injective.mulActionHom_embedding ι ⋯)

theorem Function.Bijective.addActionHom_embedding_isBijective {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {H : Type u_3} {β : Type u_4} [AddGroup H] [AddAction H β] {σ : G → H} {f : α →ₑ[σ] β} {ι : Type u_5} (hf : Bijective ⇑f) : Bijective ⇑(Injective.addActionHom_embedding ι ⋯)

@[reducible, inline]

abbrev MulAction.IsMultiplyPretransitive (G : Type u_1) (α : Type u_2) [Group G] [MulAction G α] (n : ℕ) : Prop

An action of a group on a type α is n-pretransitive if the associated action on Fin n ↪ α is pretransitive.

Equations

• MulAction.IsMultiplyPretransitive G α n = MulAction.IsPretransitive G (Fin n ↪ α)

@[reducible, inline]

abbrev AddAction.IsMultiplyPretransitive (G : Type u_1) (α : Type u_2) [AddGroup G] [AddAction G α] (n : ℕ) : Prop

An additive action of an additive group on a type α is n-pretransitive if the associated action on Fin n ↪ α is pretransitive.

Equations

• AddAction.IsMultiplyPretransitive G α n = AddAction.IsPretransitive G (Fin n ↪ α)

theorem MulAction.isMultiplyPretransitive_iff {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {n : ℕ} : IsMultiplyPretransitive G α n ↔ ∀ (x y : Fin n ↪ α), ∃ (g : G), g • x = y

theorem AddAction.isMultiplyPretransitive_iff {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {n : ℕ} : IsMultiplyPretransitive G α n ↔ ∀ (x y : Fin n ↪ α), ∃ (g : G), g +ᵥ x = y

theorem MulAction.IsPretransitive.of_embedding {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {H : Type u_3} {β : Type u_4} [Group H] [MulAction H β] {σ : G → H} {f : α →ₑ[σ] β} {n : Type u_5} (hf : Function.Surjective ⇑f) [IsPretransitive G (n ↪ α)] : IsPretransitive H (n ↪ β)

theorem AddAction.IsPretransitive.of_embedding {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {H : Type u_3} {β : Type u_4} [AddGroup H] [AddAction H β] {σ : G → H} {f : α →ₑ[σ] β} {n : Type u_5} (hf : Function.Surjective ⇑f) [IsPretransitive G (n ↪ α)] : IsPretransitive H (n ↪ β)

theorem MulAction.IsPretransitive.of_embedding_congr {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {H : Type u_3} {β : Type u_4} [Group H] [MulAction H β] {σ : G → H} {f : α →ₑ[σ] β} {n : Type u_5} (hσ : Function.Surjective σ) (hf : Function.Bijective ⇑f) : IsPretransitive G (n ↪ α) ↔ IsPretransitive H (n ↪ β)

theorem AddAction.IsPretransitive.of_embedding_congr {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {H : Type u_3} {β : Type u_4} [AddGroup H] [AddAction H β] {σ : G → H} {f : α →ₑ[σ] β} {n : Type u_5} (hσ : Function.Surjective σ) (hf : Function.Bijective ⇑f) : IsPretransitive G (n ↪ α) ↔ IsPretransitive H (n ↪ β)

theorem MulAction.is_zero_pretransitive {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {n : Type u_5} [IsEmpty n] : IsPretransitive G (n ↪ α)

Any action is 0-pretransitive.

theorem AddAction.is_zero_pretransitive {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {n : Type u_5} [IsEmpty n] : IsPretransitive G (n ↪ α)

theorem MulAction.is_zero_pretransitive' {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] : IsMultiplyPretransitive G α 0

Any action is 0-pretransitive.

theorem AddAction.is_zero_pretransitive' {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] : IsMultiplyPretransitive G α 0

def MulActionHom.oneEmbeddingMap {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {one : Type u_5} [Unique one] : (one ↪ α) →ₑ[id] α

For Unique one, the equivariant map from one ↪ α to α.

Equations

• MulActionHom.oneEmbeddingMap = { toFun := Function.Embedding.oneEmbeddingEquiv.toFun, map_smul' := ⋯ }

def AddActionHom.zeroEmbeddingMap {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {zero : Type u_5} [Unique zero] : (zero ↪ α) →ₑ[id] α

For Unique one, the equivariant map from one ↪ α to α

Equations

• AddActionHom.zeroEmbeddingMap = { toFun := Function.Embedding.oneEmbeddingEquiv.toFun, map_vadd' := ⋯ }

theorem MulActionHom.oneEmbeddingMap_bijective {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {one : Type u_5} [Unique one] : Function.Bijective ⇑oneEmbeddingMap

theorem AddActionHom.zeroEmbeddingMap_bijective {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {zero : Type u_5} [Unique zero] : Function.Bijective ⇑zeroEmbeddingMap

theorem MulAction.oneEmbedding_isPretransitive_iff {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {one : Type u_5} [Unique one] : IsPretransitive G (one ↪ α) ↔ IsPretransitive G α

An action is 1-pretransitive iff it is pretransitive.

theorem AddAction.zeroEmbedding_isPretransitive_iff {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {zero : Type u_5} [Unique zero] : IsPretransitive G (zero ↪ α) ↔ IsPretransitive G α

An additive action is 1-pretransitive iff it is pretransitive.

theorem MulAction.is_one_pretransitive_iff {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] : IsMultiplyPretransitive G α 1 ↔ IsPretransitive G α

An action is 1-pretransitive iff it is pretransitive.

theorem AddAction.is_zero_pretransitive_iff {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] : IsMultiplyPretransitive G α 1 ↔ IsPretransitive G α

An additive action is 1-pretransitive iff it is pretransitive.

theorem MulAction.is_two_pretransitive_iff {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] : IsMultiplyPretransitive G α 2 ↔ ∀ {a b c d : α}, a ≠ b → c ≠ d → ∃ (g : G), g • a = c ∧ g • b = d

An action is 2-pretransitive iff it can move any two distinct elements to any two distinct elements.

theorem AddAction.is_two_pretransitive_iff {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] : IsMultiplyPretransitive G α 2 ↔ ∀ {a b c d : α}, a ≠ b → c ≠ d → ∃ (g : G), g +ᵥ a = c ∧ g +ᵥ b = d

An additive action is 2-pretransitive iff it can move any two distinct elements to any two distinct elements.

theorem MulAction.isPretransitive_of_is_two_pretransitive {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] [h2 : IsMultiplyPretransitive G α 2] : IsPretransitive G α

A 2-pretransitive action is pretransitive.

theorem AddAction.isPretransitive_of_is_two_pretransitive {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] [h2 : IsMultiplyPretransitive G α 2] : IsPretransitive G α

A 2-pretransitive additive action is pretransitive.

theorem MulAction.isPreprimitive_of_is_two_pretransitive {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] (h2 : IsMultiplyPretransitive G α 2) : IsPreprimitive G α

A 2-transitive action is primitive.

theorem AddAction.isPreprimitive_of_is_two_pretransitive {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] (h2 : IsMultiplyPretransitive G α 2) : IsPreprimitive G α

A 2-transitive additive action is primitive.

def MulActionHom.embMap (G : Type u_1) (α : Type u_2) [Group G] [MulAction G α] {m : Type u_5} {n : Type u_6} (e : m ↪ n) : (n ↪ α) →ₑ[id] m ↪ α

The natural equivariant map from n ↪ α to m ↪ α given by an embedding e : m ↪ n.

Equations

• MulActionHom.embMap G α e = { toFun := fun (i : n ↪ α) => e.trans i, map_smul' := ⋯ }

def AddActionHom.embMap (G : Type u_1) (α : Type u_2) [AddGroup G] [AddAction G α] {m : Type u_5} {n : Type u_6} (e : m ↪ n) : (n ↪ α) →ₑ[id] m ↪ α

The natural equivariant map from n ↪ α to m ↪ α given by an embedding e : m ↪ n.

Equations

• AddActionHom.embMap G α e = { toFun := fun (i : n ↪ α) => e.trans i, map_vadd' := ⋯ }

theorem MulAction.isMultiplyPretransitive_of_le' {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {m n : ℕ} [IsMultiplyPretransitive G α n] (hmn : m ≤ n) (hα : ↑n ≤ ENat.card α) : IsMultiplyPretransitive G α m

If α has at least n elements, then any n-pretransitive action on α is m-pretransitive for any m ≤ n.

This version allows α to be infinite and uses ENat.card. For Finite α, use MulAction.isMultiplyPretransitive_of_le

theorem AddAction.isMultiplyPretransitive_of_le' {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {m n : ℕ} [IsMultiplyPretransitive G α n] (hmn : m ≤ n) (hα : ↑n ≤ ENat.card α) : IsMultiplyPretransitive G α m

If α has at least n elements, then any n-pretransitive action on α is n-pretransitive for any m ≤ n.

This version allows α to be infinite and uses ENat.card. For Finite α, use AddAction.isMultiplyPretransitive_of_le.

theorem MulAction.isMultiplyPretransitive_of_le {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {m n : ℕ} [IsMultiplyPretransitive G α n] (hmn : m ≤ n) (hα : n ≤ Nat.card α) [Finite α] : IsMultiplyPretransitive G α m

If α has at least n elements, then an n-pretransitive action is m-pretransitive for any m ≤ n.

For an infinite α, use MulAction.isMultiplyPretransitive_of_le'.

theorem AddAction.isMultiplyPretransitive_of_le {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {m n : ℕ} [IsMultiplyPretransitive G α n] (hmn : m ≤ n) (hα : n ≤ Nat.card α) [Finite α] : IsMultiplyPretransitive G α m

If α has at least n elements, then an n-pretransitive action is m-pretransitive for any m ≤ n.

For an infinite α, use MulAction.isMultiplyPretransitive_of_le'.

theorem SubMulAction.ofStabilizer.isMultiplyPretransitive_iff_of_conj {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {n : ℕ} {a b : α} {g : G} (hg : b = g • a) : MulAction.IsMultiplyPretransitive (↥(MulAction.stabilizer G a)) (↥(ofStabilizer G a)) n ↔ MulAction.IsMultiplyPretransitive (↥(MulAction.stabilizer G b)) (↥(ofStabilizer G b)) n

theorem SubAddAction.ofStabilizer.isMultiplyPretransitive_iff_of_conj {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {n : ℕ} {a b : α} {g : G} (hg : b = g +ᵥ a) : AddAction.IsMultiplyPretransitive (↥(AddAction.stabilizer G a)) (↥(ofStabilizer G a)) n ↔ AddAction.IsMultiplyPretransitive (↥(AddAction.stabilizer G b)) (↥(ofStabilizer G b)) n

theorem SubMulAction.ofStabilizer.isMultiplyPretransitive_iff {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] [MulAction.IsPretransitive G α] {n : ℕ} {a b : α} : MulAction.IsMultiplyPretransitive (↥(MulAction.stabilizer G a)) (↥(ofStabilizer G a)) n ↔ MulAction.IsMultiplyPretransitive (↥(MulAction.stabilizer G b)) (↥(ofStabilizer G b)) n

theorem SubAddAction.ofStabilizer.isMultiplyPretransitive_iff {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] [AddAction.IsPretransitive G α] {n : ℕ} {a b : α} : AddAction.IsMultiplyPretransitive (↥(AddAction.stabilizer G a)) (↥(ofStabilizer G a)) n ↔ AddAction.IsMultiplyPretransitive (↥(AddAction.stabilizer G b)) (↥(ofStabilizer G b)) n

theorem SubMulAction.ofStabilizer.isMultiplyPretransitive {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] [MulAction.IsPretransitive G α] {n : ℕ} {a : α} : MulAction.IsMultiplyPretransitive G α n.succ ↔ MulAction.IsMultiplyPretransitive (↥(MulAction.stabilizer G a)) (↥(ofStabilizer G a)) n

Multiple transitivity of a pretransitive action is equivalent to one less transitivity of stabilizer of a point (Wielandt, th. 9.1, 1st part)

theorem SubAddAction.ofStabilizer.isMultiplyPretransitive {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] [AddAction.IsPretransitive G α] {n : ℕ} {a : α} : AddAction.IsMultiplyPretransitive G α n.succ ↔ AddAction.IsMultiplyPretransitive (↥(AddAction.stabilizer G a)) (↥(ofStabilizer G a)) n

Multiple transitivity of a pretransitive action is equivalent to one less transitivity of stabilizer of a point Wielandt, th. 9.1, 1st part.

theorem SubMulAction.ofFixingSubgroup.isMultiplyPretransitive (G : Type u_1) {α : Type u_2} [Group G] [MulAction G α] {m n : ℕ} [Hn : MulAction.IsMultiplyPretransitive G α n] (s : Set α) [Finite ↑s] (hmn : s.ncard + m = n) : MulAction.IsMultiplyPretransitive (↥(fixingSubgroup G s)) (↥(ofFixingSubgroup G s)) m

The fixingSubgroup of a finite subset of cardinal d in an n-transitive action acts n-d-transitively on the complement.

theorem SubAddAction.ofFixingAddSubgroup.isMultiplyPretransitive (G : Type u_1) {α : Type u_2} [AddGroup G] [AddAction G α] {m n : ℕ} [Hn : AddAction.IsMultiplyPretransitive G α n] (s : Set α) [Finite ↑s] (hmn : s.ncard + m = n) : AddAction.IsMultiplyPretransitive (↥(fixingAddSubgroup G s)) (↥(ofFixingAddSubgroup G s)) m

The fixingSubgroup of a finite subset of cardinal d in an n-transitive additive action acts n-d-transitively on the complement.

theorem SubMulAction.ofFixingSubgroup.isMultiplyPretransitive' {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {m n : ℕ} [MulAction.IsMultiplyPretransitive G α n] (s : Set α) [Finite ↑s] (hmn : s.ncard + m ≤ n) (hn : ↑n ≤ ENat.card α) : MulAction.IsMultiplyPretransitive (↥(fixingSubgroup G s)) (↥(ofFixingSubgroup G s)) m

The fixator of a finite subset of cardinal d in an n-transitive action acts m transitively on the complement if d + m ≤ n.

theorem SubAddAction.ofFixingAddSubgroup.isMultiplyPretransitive' {G : Type u_1} {α : Type u_2} [AddGroup G] [AddAction G α] {m n : ℕ} [AddAction.IsMultiplyPretransitive G α n] (s : Set α) [Finite ↑s] (hmn : s.ncard + m ≤ n) (hn : ↑n ≤ ENat.card α) : AddAction.IsMultiplyPretransitive (↥(fixingAddSubgroup G s)) (↥(ofFixingAddSubgroup G s)) m

The fixator of a finite subset of cardinal d in an n-transitive additive action acts m transitively on the complement if d + m ≤ n.

theorem MulAction.IsMultiplyPretransitive.index_of_fixingSubgroup_mul {G : Type u_1} [Group G] {α : Type u_2} [MulAction G α] [Finite α] {k : ℕ} (Hk : IsMultiplyPretransitive G α k) {s : Set α} (hs : s.ncard = k) : (fixingSubgroup G s).index * (Nat.card α - k).factorial = (Nat.card α).factorial

For a multiply pretransitive action, computes the index of the fixing_subgroup of a subset of adequate cardinality

theorem MulAction.IsMultiplyPretransitive.index_of_fixingSubgroup_eq {G : Type u_1} [Group G] {α : Type u_2} [MulAction G α] [Finite α] (s : Set α) (hMk : IsMultiplyPretransitive G α s.ncard) : (fixingSubgroup G s).index = (Nat.card α).choose s.ncard * s.ncard.factorial

For a multiply pretransitive action, computes the index of the fixingSubgroup of a subset of adequate cardinality.

theorem Equiv.Perm.isMultiplyPretransitive (α : Type u_1) (n : ℕ) : MulAction.IsMultiplyPretransitive (Perm α) α n

The permutation group Equiv.Perm α acts n-pretransitively on α for all n.

instance Equiv.Perm.instIsPreprimitive {α : Type u_1} : MulAction.IsPreprimitive (Perm α) α

The action of the permutation group of α on α is preprimitive

theorem Equiv.Perm.eq_top_of_isMultiplyPretransitive {α : Type u_1} [Finite α] {G : Subgroup (Perm α)} (hmt : MulAction.IsMultiplyPretransitive (↥G) α (Nat.card α - 1)) : G = ⊤

A subgroup of Perm α is ⊤ if(f) it is (Nat.card α - 1)-pretransitive.

@[deprecated Equiv.Perm.eq_top_of_isMultiplyPretransitive (since := "2025-10-03")]

theorem Equiv.Perm.eq_top_if_isMultiplyPretransitive {α : Type u_1} [Finite α] {G : Subgroup (Perm α)} (hmt : MulAction.IsMultiplyPretransitive (↥G) α (Nat.card α - 1)) : G = ⊤

Alias of Equiv.Perm.eq_top_of_isMultiplyPretransitive.

---

A subgroup of Perm α is ⊤ if(f) it is (Nat.card α - 1)-pretransitive.

theorem AlternatingGroup.isMultiplyPretransitive (α : Type u_1) [Fintype α] [DecidableEq α] : MulAction.IsMultiplyPretransitive (↥(alternatingGroup α)) α (Nat.card α - 2)

The alternatingGroup on α is (card α - 2)-pretransitive.

theorem IsMultiplyPretransitive.alternatingGroup_le (α : Type u_1) [Fintype α] [DecidableEq α] (G : Subgroup (Equiv.Perm α)) (hmt : MulAction.IsMultiplyPretransitive (↥G) α (Nat.card α - 2)) : alternatingGroup α ≤ G

A subgroup of Equiv.Perm α which is (card α - 2)-pretransitive contains alternatingGroup α.

theorem AlternatingGroup.isPretransitive_of_three_le_card (α : Type u_1) [Fintype α] [DecidableEq α] (h : 3 ≤ Nat.card α) : MulAction.IsPretransitive (↥(alternatingGroup α)) α

The alternating group on 3 letters or more acts transitively.

theorem AlternatingGroup.isTrivialBlock_of_isBlock (α : Type u_1) [Fintype α] [DecidableEq α] {B : Set α} (hB : MulAction.IsBlock (↥(alternatingGroup α)) B) : MulAction.IsTrivialBlock B

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 AlternatingGroup.isPreprimitive_of_three_le_card (α : Type u_1) [Fintype α] [DecidableEq α] (h : 3 ≤ Nat.card α) : MulAction.IsPreprimitive (↥(alternatingGroup α)) α

The alternating group on 3 letters or more acts primitively