Imprimitivity gives a wreath product embedding

Let G act transitively on α, and let B be a nonempty block. The translates g • B form the block system MulAction.orbit G B, a partition of α on which G acts. Choosing, for each translate C, an element of G carrying B onto C identifies α with the grid orbit G B × B: a point is sent to the translate containing it, together with its position inside that translate transported back to B.

Under this identification every element of G permutes the rows {C} × B of the grid, so it acts through the imprimitive action of the wreath product Sym(B) ≀ Sym(orbit G B). This gives a group homomorphism G →* WreathProduct (Equiv.Perm B) (orbit G B) whose top component is the action of G on the block system. Its kernel is the kernel of the action on α, so it is injective exactly when that action is faithful. The elements it sends into the base group orbit G B → Equiv.Perm B are exactly those acting trivially on the block system. So when the action on α is faithful, the kernel of the action on the block system embeds in the base group.

The identification of α with the grid depends on the chosen elements of G. The lemmas below describe it only through properties that hold for every such choice.

Main definitions

• MulAction.IsBlock.imprimitivityEquiv: the identification α ≃ orbit G B × B.
• MulAction.IsBlock.toWreathProduct: the homomorphism G →* WreathProduct (Equiv.Perm B) (orbit G B).

Main results

• MulAction.IsBlock.imprimitivityEquiv_smul: the identification is equivariant, from the action on α to the imprimitive wreath-product action on orbit G B × B.
• MulAction.IsBlock.toWreathProduct_right: the top component is the action on the block system.
• MulAction.IsBlock.toWreathProduct_eq_iff: two elements have the same image exactly when they act identically on α.
• MulAction.IsBlock.ker_toWreathProduct: the kernel is the kernel of the action on α.
• MulAction.IsBlock.toWreathProduct_injective_iff: the homomorphism is injective exactly when the action on α is faithful.
• MulAction.IsBlock.comap_toWreathProduct_range_inl: the preimage of the base group is the kernel of the action on the block system.

References

• J. D. Dixon and B. Mortimer, Permutation Groups, Theorem 2.6A.

noncomputable def MulAction.IsBlock.imprimitivityEquiv {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {B : Set α} [IsPretransitive G α] (hB : IsBlock G B) (hBne : B.Nonempty) : α ≃ ↑(orbit G B) × ↑B

For a transitive action and a nonempty block B, the identification of α with the grid orbit G B × B. A point x is sent to the translate C of B containing it, together with the point of B obtained by moving x back along a chosen element of G carrying B onto C.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MulAction.IsBlock.imprimitivityEquiv_fst_eq_iff {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {B : Set α} [IsPretransitive G α] (hB : IsBlock G B) (hBne : B.Nonempty) {x : α} {C : ↑(orbit G B)} : ((hB.imprimitivityEquiv hBne) x).1 = C ↔ x ∈ ↑C

The first coordinate of hB.imprimitivityEquiv hBne x is the translate of B containing x.

theorem MulAction.IsBlock.imprimitivityEquiv_symm_apply_mem {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {B : Set α} [IsPretransitive G α] (hB : IsBlock G B) (hBne : B.Nonempty) (y : ↑(orbit G B) × ↑B) : (hB.imprimitivityEquiv hBne).symm y ∈ ↑y.1

The point of α corresponding to a grid position (C, b) lies in the translate C.

theorem MulAction.IsBlock.imprimitivityEquiv_smul_fst {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {B : Set α} [IsPretransitive G α] (hB : IsBlock G B) (hBne : B.Nonempty) (g : G) (x : α) : ((hB.imprimitivityEquiv hBne) (g • x)).1 = g • ((hB.imprimitivityEquiv hBne) x).1

Moving a point by g moves the translate containing it by g.

noncomputable def MulAction.IsBlock.toWreathProduct {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {B : Set α} [IsPretransitive G α] (hB : IsBlock G B) (hBne : B.Nonempty) : G →* TauCeti.WreathProduct (Equiv.Perm ↑B) ↑(orbit G B)

For a transitive action and a nonempty block B, the homomorphism from G to the wreath product Sym(B) ≀ Sym(orbit G B) through which G acts on the grid hB.imprimitivityEquiv hBne : α ≃ orbit G B × B.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MulAction.IsBlock.imprimitiveToPerm_toWreathProduct {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {B : Set α} [IsPretransitive G α] (hB : IsBlock G B) (hBne : B.Nonempty) (g : G) : (TauCeti.WreathProduct.imprimitiveToPerm (Equiv.Perm ↑B) ↑(orbit G B) ↑B) ((hB.toWreathProduct hBne) g) = (hB.imprimitivityEquiv hBne).permCongrHom (toPerm g)

The imprimitive permutation of the grid given by hB.toWreathProduct hBne g is the action of g transported along hB.imprimitivityEquiv hBne.

@[simp]

theorem MulAction.IsBlock.imprimitivityEquiv_smul {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {B : Set α} [IsPretransitive G α] (hB : IsBlock G B) (hBne : B.Nonempty) (g : G) (x : α) : (hB.imprimitivityEquiv hBne) (g • x) = (hB.toWreathProduct hBne) g • (hB.imprimitivityEquiv hBne) x

The identification α ≃ orbit G B × B is equivariant for the action of G on α and the imprimitive wreath-product action through hB.toWreathProduct hBne.

@[simp]

theorem MulAction.IsBlock.toWreathProduct_right {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {B : Set α} [IsPretransitive G α] (hB : IsBlock G B) (hBne : B.Nonempty) (g : G) : ((hB.toWreathProduct hBne) g).right = toPerm g

The top component of hB.toWreathProduct hBne g is the action of g on the block system.

theorem MulAction.IsBlock.toWreathProduct_left_apply {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {B : Set α} [IsPretransitive G α] (hB : IsBlock G B) (hBne : B.Nonempty) (g : G) (C : ↑(orbit G B)) (b : ↑B) : (((hB.toWreathProduct hBne) g).left C) b = ((hB.imprimitivityEquiv hBne) (g • (hB.imprimitivityEquiv hBne).symm (g⁻¹ • C, b))).2

The base component of hB.toWreathProduct hBne g at the translate C moves a grid position b to the position of g applied to the point at (g⁻¹ • C, b).

@[simp]

theorem MulAction.IsBlock.toWreathProduct_eq_iff {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {B : Set α} [IsPretransitive G α] (hB : IsBlock G B) (hBne : B.Nonempty) {g₁ g₂ : G} : (hB.toWreathProduct hBne) g₁ = (hB.toWreathProduct hBne) g₂ ↔ ∀ (x : α), g₁ • x = g₂ • x

Two elements have the same wreath-product image exactly when they act identically on α. This holds without a faithfulness assumption.

@[simp]

theorem MulAction.IsBlock.ker_toWreathProduct {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {B : Set α} [IsPretransitive G α] (hB : IsBlock G B) (hBne : B.Nonempty) : (hB.toWreathProduct hBne).ker = (toPermHom G α).ker

The wreath-product homomorphism has exactly the kernel of the action on α.

theorem MulAction.IsBlock.toWreathProduct_injective_iff {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {B : Set α} [IsPretransitive G α] (hB : IsBlock G B) (hBne : B.Nonempty) : Function.Injective ⇑(hB.toWreathProduct hBne) ↔ FaithfulSMul G α

The homomorphism hB.toWreathProduct hBne is injective exactly when G acts faithfully on α. In that case it embeds G in Sym(B) ≀ Sym(orbit G B).

theorem MulAction.IsBlock.comap_toWreathProduct_range_inl {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {B : Set α} [IsPretransitive G α] (hB : IsBlock G B) (hBne : B.Nonempty) : Subgroup.comap (hB.toWreathProduct hBne) SemidirectProduct.inl.range = (toPermHom G ↑(orbit G B)).ker

The elements of G that hB.toWreathProduct hBne sends into the base group orbit G B → Equiv.Perm B are exactly those acting trivially on the block system.