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.

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.IsPretransitive.of_embedding {G : Type u_3} {H : Type u_4} {α : Type u_5} {β : Type u_6} [Group G] [MulAction G α] [Group H] [MulAction H β] {σ : G → H} {f : α →ₑ[σ] β} {n : Type u_7} (hf : Function.Surjective ⇑f) [IsPretransitive G (n ↪ α)] : IsPretransitive H (n ↪ β)

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

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

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

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

Any action is 0-pretransitive.

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

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

Any action is 0-pretransitive.

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

def MulActionHom.oneEmbeddingMap {G : Type u_3} {α : Type u_5} [Group G] [MulAction G α] {one : Type u_7} [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_3} {α : Type u_5} [AddGroup G] [AddAction G α] {one : Type u_7} [Unique one] : (one ↪ α) →ₑ[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_3} {α : Type u_5} [Group G] [MulAction G α] {one : Type u_7} [Unique one] : Function.Bijective ⇑oneEmbeddingMap

theorem AddActionHom.zeroEmbeddingMap_bijective {G : Type u_3} {α : Type u_5} [AddGroup G] [AddAction G α] {one : Type u_7} [Unique one] : Function.Bijective ⇑zeroEmbeddingMap

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

An action is 1-pretransitive iff it is pretransitive.

theorem AddAction.zeroEmbedding_isPretransitive_iff {G : Type u_3} {α : Type u_5} [AddGroup G] [AddAction G α] {one : Type u_7} [Unique one] : IsPretransitive G (one ↪ α) ↔ IsPretransitive G α

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

theorem MulAction.is_one_pretransitive_iff {G : Type u_3} {α : Type u_5} [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_3} {α : Type u_5} [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_3} {α : Type u_5} [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_3} {α : Type u_5} [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_3} {α : Type u_5} [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_3} {α : Type u_5} [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_3} {α : Type u_5} [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_3} {α : Type u_5} [AddGroup G] [AddAction G α] (h2 : IsMultiplyPretransitive G α 2) : IsPreprimitive G α

A 2-transitive additive action is primitive.

def MulActionHom.embMap (G : Type u_3) (α : Type u_5) [Group G] [MulAction G α] {m : Type u_7} {n : Type u_8} (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_3) (α : Type u_5) [AddGroup G] [AddAction G α] {m : Type u_7} {n : Type u_8} (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_3} {α : Type u_5} [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_3} {α : Type u_5} [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_3} {α : Type u_5} [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_3} {α : Type u_5} [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][Wielandt-1964].

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][Wielandt-1964].

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 fixator 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 fixator 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.