Transporting permutation groups along an equivalence

An equivalence e : α ≃ β induces the group isomorphism Equiv.permCongrHom e from Equiv.Perm α to Equiv.Perm β, and so carries a subgroup G ≤ Equiv.Perm α to the subgroup G.map e.permCongrHom.toMonoidHom ≤ Equiv.Perm β. The two subgroups are the same permutation group written in two numberings of the points. This file records that the invariants of a permutation group which do not depend on the numbering are unchanged: containment in the alternating group, transitivity, and primitivity. (The order is Subgroup.card_map_of_injective.)

The same invariants may also be read off the image of a permutation representation instead of the acting group: an action of G on α and the action of the subgroup (MulAction.toPermHom G α).range of Equiv.Perm α have the same orbits and the same blocks.

Main results

• Equiv.map_permCongrHom_le_alternatingGroup_iff: transport preserves evenness.
• Equiv.conj_eq_permCongrHom: conjugation by a permutation is transport along that permutation.
• Equiv.isPretransitive_map_permCongrHom_iff: transport preserves transitivity.
• Equiv.map_inf_alternatingGroup_permCongrHom: transport preserves the even part of a subgroup.
• Equiv.isPretransitive_inf_alternatingGroup_map_permCongrHom_iff: transport preserves transitivity of the even part of a subgroup.
• Equiv.isPreprimitive_map_permCongrHom_iff: transport preserves primitivity.
• MulAction.isPretransitive_range_toPermHom_iff, MulAction.isPreprimitive_range_toPermHom_iff: a group action and its image in the permutations are transitive, respectively primitive, together.

theorem Equiv.conj_eq_permCongrHom {α : Type u_1} (τ : Perm α) : MulAut.conj τ = permCongrHom τ

Conjugation by a permutation is the transport automorphism induced by that permutation.

theorem Equiv.isPretransitive_map_permCongrHom_iff {α : Type u_1} {β : Type u_2} (e : α ≃ β) (G : Subgroup (Perm α)) : MulAction.IsPretransitive (↥(Subgroup.map e.permCongrHom.toMonoidHom G)) β ↔ MulAction.IsPretransitive (↥G) α

Transport along an equivalence preserves transitivity.

theorem Equiv.isPreprimitive_map_permCongrHom_iff {α : Type u_1} {β : Type u_2} (e : α ≃ β) (G : Subgroup (Perm α)) : MulAction.IsPreprimitive (↥(Subgroup.map e.permCongrHom.toMonoidHom G)) β ↔ MulAction.IsPreprimitive (↥G) α

Transport along an equivalence preserves primitivity.

theorem Equiv.map_permCongrHom_eq_map_conj {α : Type u_1} {β : Type u_2} (e e' : α ≃ β) (G : Subgroup (Perm α)) : Subgroup.map e'.permCongrHom.toMonoidHom G = Subgroup.map (↑(MulAut.conj (e.symm.trans e'))) (Subgroup.map e.permCongrHom.toMonoidHom G)

Reading a permutation group through two equivalences differs by exactly one conjugation, by the re-indexing permutation e.symm.trans e'. So the transported subgroup is well defined only up to conjugacy, while the group itself is canonical.

@[simp]

theorem Equiv.map_inf_alternatingGroup_permCongrHom {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (e : α ≃ β) (G : Subgroup (Perm α)) : Subgroup.map (↑e.permCongrHom) (G ⊓ alternatingGroup α) = Subgroup.map (↑e.permCongrHom) G ⊓ alternatingGroup β

Transport along an equivalence carries the even part of a permutation subgroup to the even part of its transport.

@[simp]

theorem Equiv.isPretransitive_inf_alternatingGroup_map_permCongrHom_iff {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (e : α ≃ β) (G : Subgroup (Perm α)) : MulAction.IsPretransitive (↥(Subgroup.map (↑e.permCongrHom) G ⊓ alternatingGroup β)) β ↔ MulAction.IsPretransitive (↥(G ⊓ alternatingGroup α)) α

Transport along an equivalence preserves transitivity of the intersection of a permutation subgroup with the alternating group.

theorem Equiv.map_permCongrHom_le_alternatingGroup_iff {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (e : α ≃ β) (G : Subgroup (Perm α)) : Subgroup.map e.permCongrHom.toMonoidHom G ≤ alternatingGroup β ↔ G ≤ alternatingGroup α

Transport along an equivalence preserves containment in the alternating group, since it preserves the sign of every permutation.

@[simp]

theorem MulAction.isPretransitive_range_toPermHom_iff (G : Type u_1) (α : Type u_2) [Group G] [MulAction G α] : IsPretransitive (↥(toPermHom G α).range) α ↔ IsPretransitive G α

A group action is transitive exactly when its image in the permutations is.

@[simp]

theorem MulAction.isPreprimitive_range_toPermHom_iff (G : Type u_1) (α : Type u_2) [Group G] [MulAction G α] : IsPreprimitive (↥(toPermHom G α).range) α ↔ IsPreprimitive G α

A group action is primitive exactly when its image in the permutations is.