Primitive actions from blocks and chains of blocks

For a transitive group action, the blocks containing a chosen point are order-isomorphic to the subgroups containing its stabilizer. This file applies that correspondence at the two ends of the block lattice, and then along a chain of blocks.

A minimal non-singleton block gives a primitive action of its setwise stabilizer on the block. A maximal proper block gives a maximal subgroup of the original group, and hence a primitive action of the original group on the translates of the block. These are different actions: the first resolves the action inside one block, while the second passes to the induced block system.

Both are ends of one statement. Covering relations among blocks containing a are exactly the covering relations among their stabilizers, so the maximal chains of blocks {a} = B₀ ⋖ ⋯ ⋖ Bₖ = X correspond to the maximal chains of subgroups from the stabilizer of a to G (as flags, this is Flag.map (MulAction.block_stabilizerOrderIso G a)). At a step Bᵢ ⋖ Bᵢ₊₁ the stabilizer of Bᵢ₊₁ acts primitively on the translates of Bᵢ contained in Bᵢ₊₁, and the cardinality of X is the product of the degrees of these primitive actions. This is the chain of imprimitivity along which a transitive group is built from primitive pieces.

Main results

• MulAction.IsBlock.isAtom_iff_stabilizer_covBy: atomicity of a block is equivalent to its stabilizer covering the point stabilizer.
• MulAction.IsBlock.isPreprimitive_stabilizer_of_isAtom: the stabilizer of an atomic block acts primitively on that block.
• MulAction.IsBlock.isCoatom_iff_isCoatom_stabilizer: a block is coatomic exactly when its stabilizer is a maximal subgroup.
• MulAction.IsBlock.isPreprimitive_orbit_of_isCoatom: the action on the translates of a coatomic block is primitive.
• MulAction.BlockMem.covBy_iff_stabilizer_covBy: a block covers another exactly when its stabilizer covers the other's.
• MulAction.IsBlock.mem_orbit_stabilizer_iff: the translates of B by the stabilizer of a block C ⊇ B are the translates of B contained in C.
• MulAction.BlockMem.isPreprimitive_stabilizer_orbit_of_covBy: for blocks B₁ ⋖ B₂, the stabilizer of B₂ acts primitively on the translates of B₁ that it contains.
• MulAction.BlockMem.natCard_eq_prod_ncard_orbit_stabilizer: along a chain of blocks from {a} to X, the cardinality of X is the product of the numbers of translates at each step.

References

• H. Wielandt, Finite Permutation Groups, Theorem 7.5.
• J. D. Dixon and B. Mortimer, Permutation Groups, Theorem 1.5A.

theorem MulAction.IsBlock.existsUnique_mem_orbit {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [IsPretransitive G X] {B : Set X} (hB : IsBlock G B) (hBne : B.Nonempty) (x : X) : ∃! C : ↑(orbit G B), x ∈ ↑C

For a transitive action, every point lies in exactly one translate of a nonempty block.

theorem MulAction.IsBlock.isAtom_iff_stabilizer_covBy {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [IsPretransitive G X] {B : Set X} {a : X} (hB : IsBlock G B) (ha : a ∈ B) : IsAtom ⟨B, ⋯⟩ ↔ stabilizer G a ⋖ stabilizer G B

A block B containing a is an atom in the block lattice exactly when its setwise stabilizer covers the point stabilizer of a.

theorem MulAction.IsBlock.isPreprimitive_stabilizer_of_isAtom {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [IsPretransitive G X] {B : Set X} {a : X} (hB : IsBlock G B) (ha : a ∈ B) (hmin : IsAtom ⟨B, ⋯⟩) : IsPreprimitive ↥(stabilizer G B) ↑B

If B is a minimal non-singleton block containing a, then the setwise stabilizer of B acts primitively on B.

Minimality is expressed by saying that B is an atom of MulAction.BlockMem G a. The bottom element of this order is the singleton {a}, so atomicity also supplies the nontriviality of the type B required by the point-stabilizer criterion for primitivity.

theorem MulAction.IsBlock.isCoatom_iff_isCoatom_stabilizer {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [IsPretransitive G X] {B : Set X} {a : X} (hB : IsBlock G B) (ha : a ∈ B) : IsCoatom ⟨B, ⋯⟩ ↔ IsCoatom (stabilizer G B)

A block B containing a is a coatom in the block lattice exactly when its setwise stabilizer is a maximal subgroup of G.

theorem MulAction.IsBlock.isPreprimitive_orbit_of_isCoatom {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [IsPretransitive G X] {B : Set X} {a : X} (hB : IsBlock G B) (ha : a ∈ B) (hmax : IsCoatom ⟨B, ⋯⟩) : IsPreprimitive G ↑(orbit G B)

If B is a maximal proper block containing a, then G acts primitively on the block system formed by the translates of B.

The carrier of this action is the orbit of B for the pointwise action of G on Set X; its elements are exactly the sets g • B.

Chains of blocks

Between the two extremal cases sits the general step. If B ⋖ C in the lattice of blocks containing a, the setwise stabilizer of C permutes the translates of B contained in C, and this action is primitive. Iterating along a chain {a} = B 0 ⋖ B 1 ⋖ ⋯ ⋖ B k = X of blocks resolves the action into a tower of primitive actions, and the degree of the action is the product of their degrees.

theorem MulAction.BlockMem.covBy_iff_stabilizer_covBy {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [IsPretransitive G X] {a : X} {B₁ B₂ : BlockMem G a} : B₁ ⋖ B₂ ↔ stabilizer G ↑B₁ ⋖ stabilizer G ↑B₂

A block covers another in the lattice of blocks containing a exactly when the setwise stabilizer of the first covers that of the second in the subgroup lattice.

theorem MulAction.IsBlock.mem_orbit_stabilizer_iff {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] {B C D : Set X} (hC : IsBlock G C) (hBC : B ⊆ C) : D ∈ orbit (↥(stabilizer G C)) B ↔ D ∈ orbit G B ∧ D ⊆ C

Let B be a subset of a block C. A set is a translate of B by the setwise stabilizer of C exactly when it is a translate of B contained in C.

theorem MulAction.BlockMem.ncard_mul_ncard_orbit_stabilizer_eq {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [IsPretransitive G X] {a : X} {B₁ B₂ : BlockMem G a} (h : B₁ ≤ B₂) : (↑B₁).ncard * (orbit ↥(stabilizer G ↑B₂) ↑B₁).ncard = (↑B₂).ncard

If B₁ ≤ B₂ are blocks containing a, then B₂ is the disjoint union of the translates of B₁ by its setwise stabilizer, so its cardinality is that of B₁ times their number.

theorem MulAction.BlockMem.isPreprimitive_stabilizer_orbit_of_covBy {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [IsPretransitive G X] {a : X} {B₁ B₂ : BlockMem G a} (h : B₁ ⋖ B₂) : IsPreprimitive ↥(stabilizer G ↑B₂) ↑(orbit ↥(stabilizer G ↑B₂) ↑B₁)

The step of a chain of imprimitivity. If B₁ ⋖ B₂ in the lattice of blocks containing a, then the setwise stabilizer of B₂ acts primitively on the translates of B₁ by its elements, which are the translates of B₁ contained in B₂ (MulAction.IsBlock.mem_orbit_stabilizer_iff).

For B₁ = {a} this is the primitive action of the stabilizer of an atomic block on that block, MulAction.IsBlock.isPreprimitive_stabilizer_of_isAtom, read on singletons; for B₂ = Set.univ it is the primitive action on the block system of a coatomic block, MulAction.IsBlock.isPreprimitive_orbit_of_isCoatom.

theorem MulAction.BlockMem.ncard_last_eq_mul_prod_ncard_orbit_stabilizer {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [IsPretransitive G X] {a : X} {k : ℕ} (B : Fin (k + 1) → BlockMem G a) (hB : Monotone B) : (↑(B (Fin.last k))).ncard = (↑(B 0)).ncard * ∏ i : Fin k, (orbit ↥(stabilizer G ↑(B i.succ)) ↑(B i.castSucc)).ncard

Along a chain B 0 ≤ B 1 ≤ ⋯ ≤ B k of blocks containing a, the cardinality of the last block is that of the first times the number of translates of B i by the stabilizer of B (i + 1), taken over all steps.

theorem MulAction.BlockMem.natCard_eq_prod_ncard_orbit_stabilizer {G : Type u_1} {X : Type u_2} [Group G] [MulAction G X] [IsPretransitive G X] {a : X} {k : ℕ} (B : Fin (k + 1) → BlockMem G a) (hB : Monotone B) (h0 : B 0 = ⊥) (hk : B (Fin.last k) = ⊤) : Nat.card X = ∏ i : Fin k, (orbit ↥(stabilizer G ↑(B i.succ)) ↑(B i.castSucc)).ncard

The degree along a chain of imprimitivity. For a chain {a} = B 0 ≤ B 1 ≤ ⋯ ≤ B k = X of blocks containing a, the cardinality of X is the product over the steps of the number of translates of B i by the stabilizer of B (i + 1). When every step is a cover these are the degrees of the primitive actions of MulAction.BlockMem.isPreprimitive_stabilizer_orbit_of_covBy.