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_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))

source

theorem AddAction.isPreprimitive_ofFixingAddSubgroup_conj_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))

source

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)

source

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)

source

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

Prop

An additive action is n-multiply preprimitive if is is n-multiply transitive and if, when n ≥ 1, for every set s of cardinality n - 1, the action of fixingAddSubgroup 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

Instances

source

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)

source

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

Prop

A group action is n-multiply preprimitive if is is n-multiply transitive 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

Instances

source

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)

source

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

IsMultiplyPretransitive M α n

source

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

IsMultiplyPretransitive M α n

source

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

IsMultiplyPreprimitive M α 0

Any action is 0-preprimitive

source

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

IsMultiplyPreprimitive M α 0

source

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

source

theorem AddAction.is_zero_preprimitive_iff (M : Type u_1) (α : Type u_2) [AddGroup M] [AddAction M α] :

IsMultiplyPreprimitive M α 1 ↔ IsPreprimitive M α

source

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

source

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

source

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.

source

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

source

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)

source

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

source

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.

source

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.

source

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.

source

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.

source

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

source

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

source

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

source

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

Documentation

Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Multiply preprimitive actions #