Multiply preprimitive actions

Let G be a group acting on a type α.

• MulAction.IsMultiplyPreprimitive : The action is said to be n-primitive if, for every subset s : Set α with n elements, the actions f stabilizer G s on the complement of s is primitive.

• MulAction.is_zero_preprimitive : any action is 0-primitive

• MulAction.is_one_preprimitive_iff : an action is 1-primitive if and only if it is primitive

• MulAction.isMultiplyPreprimitive_ofStabilizer: if an action is n + 1-primitive, then the action of stabilizer G a on the complement of {a} is n-primitive.

• MulAction.isMultiplyPreprimitive_succ_iff_ofStabilizer : for 1 ≤ n, an action is n + 1-primitive, then the action of stabilizer G a on the complement of {a} is n-primitive. ofFixingSubgroup.isMultiplyPreprimitive

• MulAction.ofFixingSubgroup.isMultiplyPreprimitive: If an action is s.ncard + m-primitive, then the action of FixingSubgroup G s on the complement of s is m-primitive.

theorem MulAction.isPreprimitive_of_fixingSubgroup_empty_iff {G : Type u_1} [Group G] {α : Type u_2} [MulAction G α] : IsPreprimitive ↥(fixingSubgroup G ∅) ↥(SubMulAction.ofFixingSubgroup G ∅) ↔ IsPreprimitive G α

theorem AddAction.isPreprimitive_of_fixingAddSubgroup_empty_iff {G : Type u_1} [AddGroup G] {α : Type u_2} [AddAction G α] : IsPreprimitive ↥(fixingAddSubgroup G ∅) ↥(SubAddAction.ofFixingAddSubgroup G ∅) ↔ IsPreprimitive G α

theorem MulAction.isPreprimitive_ofFixingSubgroup_conj_iff {G : Type u_1} [Group G] {α : Type u_2} [MulAction G α] {s : Set α} {g : G} : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) ↔ IsPreprimitive ↥(fixingSubgroup G (g • s)) ↥(SubMulAction.ofFixingSubgroup G (g • s))

theorem AddAction.isPreprimitive_ofFixingAddSubgroup_addConj_iff {G : Type u_1} [AddGroup G] {α : Type u_2} [AddAction G α] {s : Set α} {g : G} : IsPreprimitive ↥(fixingAddSubgroup G s) ↥(SubAddAction.ofFixingAddSubgroup G s) ↔ IsPreprimitive ↥(fixingAddSubgroup G (g +ᵥ s)) ↥(SubAddAction.ofFixingAddSubgroup G (g +ᵥ s))

theorem MulAction.isPreprimitive_fixingSubgroup_insert_iff {G : Type u_1} [Group G] {α : Type u_2} [MulAction G α] {a : α} {t : Set ↥(SubMulAction.ofStabilizer G a)} : IsPreprimitive ↥(fixingSubgroup G (insert a (Subtype.val '' t))) ↥(SubMulAction.ofFixingSubgroup G (insert a (Subtype.val '' t))) ↔ IsPreprimitive ↥(fixingSubgroup (↥(stabilizer G a)) t) ↥(SubMulAction.ofFixingSubgroup (↥(stabilizer G a)) t)

theorem AddAction.isPreprimitive_fixingAddSubgroup_insert_iff {G : Type u_1} [AddGroup G] {α : Type u_2} [AddAction G α] {a : α} {t : Set ↥(SubAddAction.ofStabilizer G a)} : IsPreprimitive ↥(fixingAddSubgroup G (insert a (Subtype.val '' t))) ↥(SubAddAction.ofFixingAddSubgroup G (insert a (Subtype.val '' t))) ↔ IsPreprimitive ↥(fixingAddSubgroup (↥(stabilizer G a)) t) ↥(SubAddAction.ofFixingAddSubgroup (↥(stabilizer G a)) t)

class AddAction.IsMultiplyPreprimitive (M : Type u_1) (α : Type u_2) [AddGroup M] [AddAction M α] (n : ℕ) : Prop

A group action is n-multiply preprimitive if it is n-multiply pretransitive and if, when n ≥ 1, for every set s of cardinality n - 1, the action of fixingSubgroup M s on the complement of s is preprimitive.

• isMultiplyPretransitive : IsMultiplyPretransitive M α n

  An n-preprimitive action is n-pretransitive.

• isPreprimitive_ofFixingAddSubgroup {s : Set α} (hs : s.encard + 1 = ↑n) : IsPreprimitive ↥(fixingAddSubgroup M s) ↥(SubAddAction.ofFixingAddSubgroup M s)

  In an n-preprimitive action, the action of fixingAddSubgroup M s on ofFixingAddSubgroup M s is preprimitive, for all sets s such that s.encard + 1 = n.

theorem AddAction.isMultiplyPreprimitive_iff (M : Type u_1) (α : Type u_2) [AddGroup M] [AddAction M α] (n : ℕ) : IsMultiplyPreprimitive M α n ↔ IsMultiplyPretransitive M α n ∧ ∀ {s : Set α}, s.encard + 1 = ↑n → IsPreprimitive ↥(fixingAddSubgroup M s) ↥(SubAddAction.ofFixingAddSubgroup M s)

class MulAction.IsMultiplyPreprimitive (M : Type u_1) (α : Type u_2) [Group M] [MulAction M α] (n : ℕ) : Prop

A group action is n-multiply preprimitive if it is n-multiply pretransitive and if, when n ≥ 1, for every set s of cardinality n - 1, the action of fixingSubgroup M s on the complement of s is preprimitive.

• isMultiplyPretransitive : IsMultiplyPretransitive M α n

  An n-preprimitive action is n-pretransitive.

• isPreprimitive_ofFixingSubgroup {s : Set α} (hs : s.encard + 1 = ↑n) : IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)

  In an n-preprimitive action, the action of fixingSubgroup M s on ofFixingSubgroup M s is preprimitive, for all sets s such that s.encard + 1 = n.

theorem MulAction.isMultiplyPreprimitive_iff (M : Type u_1) (α : Type u_2) [Group M] [MulAction M α] (n : ℕ) : IsMultiplyPreprimitive M α n ↔ IsMultiplyPretransitive M α n ∧ ∀ {s : Set α}, s.encard + 1 = ↑n → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)

instance MulAction.instIsMultiplyPretransitiveOfIsMultiplyPreprimitive (M : Type u_1) (α : Type u_2) [Group M] [MulAction M α] (n : ℕ) [IsMultiplyPreprimitive M α n] : IsMultiplyPretransitive M α n

instance AddAction.instIsMultiplyPretransitiveOfIsMultiplyPreprimitive (M : Type u_1) (α : Type u_2) [AddGroup M] [AddAction M α] (n : ℕ) [IsMultiplyPreprimitive M α n] : IsMultiplyPretransitive M α n

theorem MulAction.is_zero_preprimitive (M : Type u_1) (α : Type u_2) [Group M] [MulAction M α] : IsMultiplyPreprimitive M α 0

Any action is 0-preprimitive.

theorem AddAction.is_zero_preprimitive (M : Type u_1) (α : Type u_2) [AddGroup M] [AddAction M α] : IsMultiplyPreprimitive M α 0

Any action is 0-preprimitive.

theorem MulAction.is_one_preprimitive_iff (M : Type u_1) (α : Type u_2) [Group M] [MulAction M α] : IsMultiplyPreprimitive M α 1 ↔ IsPreprimitive M α

An action is preprimitive iff it is 1-preprimitive.

theorem AddAction.is_zero_preprimitive_iff (M : Type u_1) (α : Type u_2) [AddGroup M] [AddAction M α] : IsMultiplyPreprimitive M α 1 ↔ IsPreprimitive M α

An action is preprimitive iff it is 1-preprimitive.

theorem MulAction.isMultiplyPreprimitive_ofStabilizer (M : Type u_1) (α : Type u_2) [Group M] [MulAction M α] [IsPretransitive M α] {n : ℕ} {a : α} [IsMultiplyPreprimitive M α n.succ] : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n

The action of stabilizer M a is one-less preprimitive.

theorem AddAction.isMultiplyPreprimitive_ofStabilizer (M : Type u_1) (α : Type u_2) [AddGroup M] [AddAction M α] [IsPretransitive M α] {n : ℕ} {a : α} [IsMultiplyPreprimitive M α n.succ] : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubAddAction.ofStabilizer M a)) n

The action of stabilizer M a is one-less preprimitive.

theorem MulAction.isMultiplyPreprimitive_succ_iff_ofStabilizer (M : Type u_1) (α : Type u_2) [Group M] [MulAction M α] [IsPretransitive M α] {n : ℕ} (hn : 1 ≤ n) {a : α} : IsMultiplyPreprimitive M α n.succ ↔ IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n

A pretransitive action is n.succ-preprimitive iff the action of stabilizers is n-preprimitive.

theorem AddAction.isMultiplyPreprimitive_succ_iff_ofStabilizer (M : Type u_1) (α : Type u_2) [AddGroup M] [AddAction M α] [IsPretransitive M α] {n : ℕ} (hn : 1 ≤ n) {a : α} : IsMultiplyPreprimitive M α n.succ ↔ IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(SubAddAction.ofStabilizer M a)) n

A pretransitive action is n.succ-preprimitive iff the action of stabilizers is n-preprimitive.

theorem MulAction.ofFixingSubgroup.isMultiplyPreprimitive (M : Type u_1) (α : Type u_2) [Group M] [MulAction M α] {m n : ℕ} [IsMultiplyPreprimitive M α n] {s : Set α} [Finite ↑s] (hs : s.ncard + m = n) : IsMultiplyPreprimitive (↥(fixingSubgroup M s)) (↥(SubMulAction.ofFixingSubgroup M s)) m

The fixator of a subset of cardinal d in an n-primitive action acts n-d-primitively on the remaining (d ≤ n).

theorem AddAction.ofFixingSubgroup.isMultiplyPreprimitive (M : Type u_1) (α : Type u_2) [AddGroup M] [AddAction M α] {m n : ℕ} [IsMultiplyPreprimitive M α n] {s : Set α} [Finite ↑s] (hs : s.ncard + m = n) : IsMultiplyPreprimitive (↥(fixingAddSubgroup M s)) (↥(SubAddAction.ofFixingAddSubgroup M s)) m

The fixator of a subset of cardinal d in an n-primitive action acts n-d-primitively on the remaining (d ≤ n).

theorem MulAction.isMultiplyPreprimitive_of_isMultiplyPretransitive_succ (M : Type u_1) (α : Type u_2) [Group M] [MulAction M α] {n : ℕ} (hα : ↑n.succ ≤ ENat.card α) [IsMultiplyPretransitive M α n.succ] : IsMultiplyPreprimitive M α n

n.succ-pretransitivity implies n-preprimitivity.

theorem AddAction.isMultiplyPreprimitive_of_isMultiplyPretransitive_succ (M : Type u_1) (α : Type u_2) [AddGroup M] [AddAction M α] {n : ℕ} (hα : ↑n.succ ≤ ENat.card α) [IsMultiplyPretransitive M α n.succ] : IsMultiplyPreprimitive M α n

n.succ-pretransitivity implies n-preprimitivity.

theorem MulAction.isMultiplyPreprimitive_of_le (M : Type u_1) (α : Type u_2) [Group M] [MulAction M α] {n : ℕ} (hn : IsMultiplyPreprimitive M α n) {m : ℕ} (hmn : m ≤ n) (hα : ↑n ≤ ENat.card α) : IsMultiplyPreprimitive M α m

An n-preprimitive action is m-preprimitive for m ≤ n.

theorem AddAction.isMultiplyPreprimitive_of_le (M : Type u_1) (α : Type u_2) [AddGroup M] [AddAction M α] {n : ℕ} (hn : IsMultiplyPreprimitive M α n) {m : ℕ} (hmn : m ≤ n) (hα : ↑n ≤ ENat.card α) : IsMultiplyPreprimitive M α m

An n-preprimitive action is m-preprimitive for m ≤ n.

theorem MulAction.IsMultiplyPreprimitive.of_bijective_map {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] {N : Type u_3} {β : Type u_4} [Group N] [MulAction N β] {φ : M → N} {f : α →ₑ[φ] β} (hf : Function.Bijective ⇑f) {n : ℕ} (h : IsMultiplyPreprimitive M α n) : IsMultiplyPreprimitive N β n

theorem AddAction.IsMultiplyPreprimitive.of_bijective_map {M : Type u_1} {α : Type u_2} [AddGroup M] [AddAction M α] {N : Type u_3} {β : Type u_4} [AddGroup N] [AddAction N β] {φ : M → N} {f : α →ₑ[φ] β} (hf : Function.Bijective ⇑f) {n : ℕ} (h : IsMultiplyPreprimitive M α n) : IsMultiplyPreprimitive N β n

theorem MulAction.isMultiplyPreprimitive_congr {M : Type u_1} {α : Type u_2} [Group M] [MulAction M α] {N : Type u_3} {β : Type u_4} [Group N] [MulAction N β] {φ : M → N} (hφ : Function.Surjective φ) {f : α →ₑ[φ] β} (hf : Function.Bijective ⇑f) {n : ℕ} : IsMultiplyPreprimitive M α n ↔ IsMultiplyPreprimitive N β n

theorem AddAction.isMultiplyPreprimitive_congr {M : Type u_1} {α : Type u_2} [AddGroup M] [AddAction M α] {N : Type u_3} {β : Type u_4} [AddGroup N] [AddAction N β] {φ : M → N} (hφ : Function.Surjective φ) {f : α →ₑ[φ] β} (hf : Function.Bijective ⇑f) {n : ℕ} : IsMultiplyPreprimitive M α n ↔ IsMultiplyPreprimitive N β n