Primitive actions

Definitions

• MulAction.IsPreprimitive G X A structure that says that the action of a type G on a type X (defined by an instance SMul G X) is preprimitive, namely, it is pretransitive and the only blocks are ⊤ and subsingletons. (The pretransitivity assumption is essentially trivial, because orbits are blocks, unless the action itself is trivial.)

  The notion which is introduced in classical books on group theory is restricted to group actions. In fact, it may be irrelevant if the action is degenerate, when “trivial blocks” might not be blocks. Moreover, the classical notion is primitive, which further assumes that X is not empty.

• MulAction.IsQuasiPreprimitive G X A structure that says that the action of the group G on the type X is quasipreprimitive, namely, normal subgroups of G which act nontrivially act pretransitively.

• We prove some straightforward theorems that relate preprimitivity under equivariant maps, for images and preimages.

Relation with stabilizers

• MulAction.isSimpleOrderBlockMem_iff_isPreprimitive relates primitivity and the fact that the inclusion order on blocks containing is simple.

• MulAction.isCoatom_stabilizer_iff_preprimitive An action is preprimitive iff the stabilizers of points are maximal subgroups.

• MulAction.IsPreprimitive.isCoatom_stabilizer_of_isPreprimitive Stabilizers of points under a preprimitive action are maximal subgroups.

Relation with normal subgroups

• MulAction.IsPreprimitive.isQuasipreprimitive Preprimitive actions are quasipreprimitive.

Particular results for actions on finite types

• MulAction.IsPreprimitive.of_prime_card : A pretransitive action on a finite type of prime cardinal is preprimitive.

• MulAction.IsPreprimitive.of_card_lt Given an equivariant map from a preprimitive action, if the image is at least twice the codomain, then the codomain is preprimitive.

• MulAction.IsPreprimitive.exists_mem_smul_and_not_mem_smul : Theorem of Rudio. For a preprimitive action, a subset which is neither empty nor full has a translate which contains a given point and avoids another one.

class AddAction.IsPreprimitive (G : Type u_1) (X : Type u_2) [VAdd G X] extends AddAction.IsPretransitive G X : Prop

An additive action is preprimitive if it is pretransitive and the only blocks are the trivial ones

• exists_vadd_eq (x y : X) : ∃ (g : G), g +ᵥ x = y
• isTrivialBlock_of_isBlock {B : Set X} : IsBlock G B → IsTrivialBlock B

  An action is preprimitive if it is pretransitive and the only blocks are the trivial ones

class MulAction.IsPreprimitive (G : Type u_1) (X : Type u_2) [SMul G X] extends MulAction.IsPretransitive G X : Prop

An action is preprimitive if it is pretransitive and the only blocks are the trivial ones

• exists_smul_eq (x y : X) : ∃ (g : G), g • x = y
• isTrivialBlock_of_isBlock {B : Set X} : IsBlock G B → IsTrivialBlock B

  An action is preprimitive if it is pretransitive and the only blocks are the trivial ones

class AddAction.IsQuasiPreprimitive (G : Type u_1) (X : Type u_2) [AddGroup G] [AddAction G X] extends AddAction.IsPretransitive G X : Prop

An additive action of an additive group is quasipreprimitive if any normal subgroup that has no fixed point acts pretransitively

• exists_vadd_eq (x y : X) : ∃ (g : G), g +ᵥ x = y
• isPretransitive_of_normal {N : AddSubgroup G} [N.Normal] : fixedPoints (↥N) X ≠ Set.univ → IsPretransitive (↥N) X

class MulAction.IsQuasiPreprimitive (G : Type u_1) (X : Type u_2) [Group G] [MulAction G X] extends MulAction.IsPretransitive G X : Prop

An action of a group is quasipreprimitive if any normal subgroup that has no fixed point acts pretransitively

• exists_smul_eq (x y : X) : ∃ (g : G), g • x = y
• isPretransitive_of_normal {N : Subgroup G} [N.Normal] : fixedPoints (↥N) X ≠ Set.univ → IsPretransitive (↥N) X

theorem MulAction.IsBlock.subsingleton_or_eq_univ {G : Type u_1} {X : Type u_2} [SMul G X] [IsPreprimitive G X] {B : Set X} (hB : IsBlock G B) : B.Subsingleton ∨ B = Set.univ

theorem AddAction.IsBlock.subsingleton_or_eq_univ {G : Type u_1} {X : Type u_2} [VAdd G X] [IsPreprimitive G X] {B : Set X} (hB : IsBlock G B) : B.Subsingleton ∨ B = Set.univ

theorem MulAction.IsPreprimitive.of_subsingleton {G : Type u_1} {X : Type u_2} [SMul G X] [Nonempty G] [Subsingleton X] : IsPreprimitive G X

theorem AddAction.IsPreprimitive.of_subsingleton {G : Type u_1} {X : Type u_2} [VAdd G X] [Nonempty G] [Subsingleton X] : IsPreprimitive G X

theorem MulAction.IsPreprimitive.of_isTrivialBlock_base {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [IsPretransitive G X] (a : X) (H : ∀ {B : Set X}, a ∈ B → IsBlock G B → IsTrivialBlock B) : IsPreprimitive G X

If the action is pretransitive, then the trivial blocks condition implies preprimitivity (based condition)

theorem AddAction.IsPreprimitive.of_isTrivialBlock_base {G : Type u_1} {X : Type u_2} [AddGroup G] [AddAction G X] [IsPretransitive G X] (a : X) (H : ∀ {B : Set X}, a ∈ B → IsBlock G B → IsTrivialBlock B) : IsPreprimitive G X

If the action is pretransitive, then the trivial blocks condition implies preprimitivity (based condition)

theorem MulAction.IsPreprimitive.of_isTrivialBlock_of_not_mem_fixedPoints {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {a : X} (ha : a ∉ fixedPoints G X) (H : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B) : IsPreprimitive G X

If the action is not trivial, then the trivial blocks condition implies preprimitivity (pretransitivity is automatic) (based condition)

theorem AddAction.IsPreprimitive.of_isTrivialBlock_of_not_mem_fixedPoints {G : Type u_1} {X : Type u_2} [AddGroup G] [AddAction G X] {a : X} (ha : a ∉ fixedPoints G X) (H : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B) : IsPreprimitive G X

If the action is not trivial, then the trivial blocks condition implies preprimitivity (pretransitivity is automatic) (based condition)

theorem MulAction.mk' {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] (Hnt : fixedPoints G X ≠ ⊤) (H : ∀ {B : Set X}, IsBlock G B → IsTrivialBlock B) : IsPreprimitive G X

If the action is not trivial, then the trivial blocks condition implies preprimitivity (pretransitivity is automatic)

theorem AddAction.mk' {G : Type u_1} {X : Type u_2} [AddGroup G] [AddAction G X] (Hnt : fixedPoints G X ≠ ⊤) (H : ∀ {B : Set X}, IsBlock G B → IsTrivialBlock B) : IsPreprimitive G X

If the action is not trivial, then the trivial blocks condition implies preprimitivity (pretransitivity is automatic)

theorem MulAction.IsPreprimitive.of_surjective {M : Type u_3} [Group M] {α : Type u_4} [MulAction M α] {N : Type u_5} {β : Type u_6} [Group N] [MulAction N β] {φ : M →* N} {f : α →ₑ[⇑φ] β} [IsPreprimitive M α] (hf : Function.Surjective ⇑f) : IsPreprimitive N β

theorem AddAction.IsPreprimitive.of_surjective {M : Type u_3} [AddGroup M] {α : Type u_4} [AddAction M α] {N : Type u_5} {β : Type u_6} [AddGroup N] [AddAction N β] {φ : M →+ N} {f : α →ₑ[⇑φ] β} [IsPreprimitive M α] (hf : Function.Surjective ⇑f) : IsPreprimitive N β

theorem MulAction.isPreprimitive_congr {M : Type u_3} [Group M] {α : Type u_4} [MulAction M α] {N : Type u_5} {β : Type u_6} [Group N] [MulAction N β] {φ : M →* N} {f : α →ₑ[⇑φ] β} (hφ : Function.Surjective ⇑φ) (hf : Function.Bijective ⇑f) : IsPreprimitive M α ↔ IsPreprimitive N β

theorem AddAction.isPreprimitive_congr {M : Type u_3} [AddGroup M] {α : Type u_4} [AddAction M α] {N : Type u_5} {β : Type u_6} [AddGroup N] [AddAction N β] {φ : M →+ N} {f : α →ₑ[⇑φ] β} (hφ : Function.Surjective ⇑φ) (hf : Function.Bijective ⇑f) : IsPreprimitive M α ↔ IsPreprimitive N β

@[simp]

theorem MulAction.isSimpleOrder_blockMem_iff_isPreprimitive (G : Type u_3) [Group G] {X : Type u_4} [MulAction G X] [IsPretransitive G X] [Nontrivial X] (a : X) : IsSimpleOrder (BlockMem G a) ↔ IsPreprimitive G X

A pretransitive action on a nontrivial type is preprimitive iff the set of blocks containing a given element is a simple order

@[simp]

theorem AddAction.isSimpleOrder_blockMem_iff_isPreprimitive (G : Type u_3) [AddGroup G] {X : Type u_4} [AddAction G X] [IsPretransitive G X] [Nontrivial X] (a : X) : IsSimpleOrder (BlockMem G a) ↔ IsPreprimitive G X

A pretransitive action on a nontrivial type is preprimitive iff the set of blocks containing a given element is a simple order

theorem MulAction.isCoatom_stabilizer_iff_preprimitive (G : Type u_3) [Group G] {X : Type u_4} [MulAction G X] [IsPretransitive G X] [Nontrivial X] (a : X) : IsCoatom (stabilizer G a) ↔ IsPreprimitive G X

A pretransitive action is preprimitive iff the stabilizer of any point is a maximal subgroup (Wielandt, th. 7.5)

theorem AddAction.isCoatom_stabilizer_iff_preprimitive (G : Type u_3) [AddGroup G] {X : Type u_4} [AddAction G X] [IsPretransitive G X] [Nontrivial X] (a : X) : IsCoatom (stabilizer G a) ↔ IsPreprimitive G X

A pretransitive action is preprimitive iff the stabilizer of any point is a maximal subgroup (Wielandt, th. 7.5)

theorem MulAction.IsPreprimitive.isCoatom_stabilizer_of_isPreprimitive (G : Type u_3) [Group G] {X : Type u_4} [MulAction G X] [Nontrivial X] [IsPreprimitive G X] (a : X) : IsCoatom (stabilizer G a)

In a preprimitive action, stabilizers are maximal subgroups

theorem AddAction.IsPreprimitive.isCoatom_stabilizer_of_isPreprimitive (G : Type u_3) [AddGroup G] {X : Type u_4} [AddAction G X] [Nontrivial X] [IsPreprimitive G X] (a : X) : IsCoatom (stabilizer G a)

In a preprimitive action, stabilizers are maximal subgroups.

@[instance 100]

instance MulAction.IsPreprimitive.isQuasiPreprimitive {M : Type u_3} [Group M] {α : Type u_4} [MulAction M α] [IsPreprimitive M α] : IsQuasiPreprimitive M α

In a preprimitive action, any normal subgroup that acts nontrivially is pretransitive (Wielandt, th. 7.1).

@[instance 100]

instance AddAction.IsPreprimitive.isQuasiPreprimitive {M : Type u_3} [AddGroup M] {α : Type u_4} [AddAction M α] [IsPreprimitive M α] : IsQuasiPreprimitive M α

In a preprimitive additive action, any normal subgroup that acts nontrivially is pretransitive (Wielandt, th. 7.1).

theorem MulAction.IsPreprimitive.of_prime_card {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [hGX : IsPretransitive G X] (hp : Nat.Prime (Nat.card X)) : IsPreprimitive G X

A pretransitive action on a set of prime order is preprimitive

theorem AddAction.IsPreprimitive.of_prime_card {G : Type u_1} {X : Type u_2} [AddGroup G] [AddAction G X] [hGX : IsPretransitive G X] (hp : Nat.Prime (Nat.card X)) : IsPreprimitive G X

A pretransitive action on a set of prime order is preprimitive

theorem MulAction.IsPreprimitive.of_card_lt {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {H : Type u_3} {Y : Type u_4} [Group H] [MulAction H Y] {φ : G → H} {f : X →ₑ[φ] Y} [Finite Y] [IsPretransitive H Y] [IsPreprimitive G X] (hf' : Nat.card Y < 2 * (Set.range ⇑f).ncard) : IsPreprimitive H Y

The codomain of an equivariant map of large image is preprimitive if the domain is

theorem AddAction.IsPreprimitive.of_card_lt {G : Type u_1} {X : Type u_2} [AddGroup G] [AddAction G X] {H : Type u_3} {Y : Type u_4} [AddGroup H] [AddAction H Y] {φ : G → H} {f : X →ₑ[φ] Y} [Finite Y] [IsPretransitive H Y] [IsPreprimitive G X] (hf' : Nat.card Y < 2 * (Set.range ⇑f).ncard) : IsPreprimitive H Y

The codomain of an equivariant map of large image is preprimitive if the domain is

theorem MulAction.IsPreprimitive.exists_mem_smul_and_not_mem_smul {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [IsPreprimitive G X] {A : Set X} (hfA : A.Finite) (hA : A.Nonempty) (hA' : A ≠ Set.univ) {a b : X} (h : a ≠ b) : ∃ (g : G), a ∈ g • A ∧ b ∉ g • A

Theorem of Rudio (Wielandt, 1964, Th. 8.1)

For a preprimitive action, a subset which is neither empty nor full has a translate which contains a given point and avoids another one.

theorem AddAction.IsPreprimitive.exists_mem_vadd_and_not_mem_vadd {G : Type u_1} {X : Type u_2} [AddGroup G] [AddAction G X] [IsPreprimitive G X] {A : Set X} (hfA : A.Finite) (hA : A.Nonempty) (hA' : A ≠ Set.univ) {a b : X} (h : a ≠ b) : ∃ (g : G), a ∈ g +ᵥ A ∧ b ∉ g +ᵥ A

Theorem of Rudio (Wielandt, 1964, Th. 8.1)

For a preprimitive additive action, a subset which is neither empty nor full has a translate which contains a given point and avoids another one.