Documentation

TauCeti.Algebra.GroupAction.PermutationRepresentation

The permutation representation of a group action on an enumerated set #

A group G acting on a set α with n elements permutes them, and choosing an enumeration e : α ≃ Fin n turns that into a homomorphism G →* Equiv.Perm (Fin n). This file is that transport and the price of the choice.

The action on α is the intrinsic object and needs no choices. A symmetric group does not appear until e is chosen, and the point is that the choice costs exactly one conjugation and no more:

So the action is canonical, while the resulting subgroup of a particular symmetric group is canonical only up to conjugacy. This is the same phenomenon as Mathlib's Polynomial.Gal.galActionHom, which acts on p.rootSet E rather than on Fin p.natDegree for the same reason.

permutationRepresentation needs no hypothesis. When the action is faithful it is injective, and permutationEmbedding bundles that as the injection G ↪ S_n into the ambient symmetric group; the isomorphism onto the image is MonoidHom.ofInjective (permutationRepresentation_injective e), which needs no wrapper here.

The motivating case is a Galois group permuting the embeddings of a field: G = M ≃ₐ[F] M acting on L →ₐ[F] M by postcomposition (TauCeti/Algebra/GroupAction/AlgHom.lean), where TauCeti/FieldTheory/Normal/Embeddings.lean supplies faithfulness from the generation hypothesis as faithfulSMul_of_normalClosure_eq_top.

Main results #

source
def Equiv.permutationRepresentation {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {n : ℕ} (e : α ≃ Fin n) :
G →* Perm (Fin n)

The permutation representation of a group action, read through an enumeration e. The action on α is canonical; e only names the points.

Equations
Instances For
    source
    @[simp]
    theorem Equiv.permutationRepresentation_apply {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {n : ℕ} (e : α ≃ Fin n) (g : G) (i : Fin n) :
    (e.permutationRepresentation g) i = e (g • e.symm i)

    The transported permutation sends an index to the index of its translate: i names the point e.symm i, and its image names g • e.symm i.

    source
    theorem Equiv.permutationRepresentation_injective {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {n : ℕ} [FaithfulSMul G α] (e : α ≃ Fin n) :
    Function.Injective ⇑e.permutationRepresentation

    G embeds in S_n when the action is faithful: an element acting trivially on the enumerated points fixes every point, hence is the identity.

    source
    def Equiv.permutationEmbedding {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {n : ℕ} [FaithfulSMul G α] (e : α ≃ Fin n) :
    G ↪ Perm (Fin n)

    G injects into S_n, for an enumeration e of the points and a faithful action on them. A consumer wanting the isomorphism onto the image instead writes MonoidHom.ofInjective (permutationRepresentation_injective e).

    Equations
    Instances For
      source
      @[simp]
      theorem Equiv.permutationEmbedding_apply {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {n : ℕ} [FaithfulSMul G α] (e : α ≃ Fin n) (g : G) :
      e.permutationEmbedding g = e.permutationRepresentation g

      The embedding acts as the representation.

      source
      theorem Equiv.permutationRepresentation_eq_conj {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {n : ℕ} (e e' : α ≃ Fin n) (g : G) :
      e'.permutationRepresentation g = e.symm.trans e' * e.permutationRepresentation g * (e.symm.trans e')⁻¹

      Replacing the enumeration conjugates the representation inside S_n, by the re-indexing permutation e.symm.trans e'. The subgroup of Equiv.Perm (Fin n) is therefore well defined only up to conjugacy, while the action on α itself is canonical.

      source
      theorem Equiv.map_permutationRepresentation_range_conj {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {n : ℕ} (e e' : α ≃ Fin n) :
      Subgroup.map (↑(MulAut.conj (e.symm.trans e'))) e.permutationRepresentation.range = e'.permutationRepresentation.range

      The represented subgroups of S_n are conjugate, by the same re-indexing permutation. This is the subgroup-level form of permutationRepresentation_eq_conj, and it is what makes "canonical up to conjugacy" a statement about the image rather than about individual elements.

      source
      theorem Equiv.permutationRepresentation_eq_of_map_smul {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {n : ℕ} (e : α ≃ Fin n) {ρ : G →* Perm (Fin n)} (he : ∀ (g : G) (x : α), e (g • x) = (ρ g) (e x)) :
      e.permutationRepresentation = ρ

      An equivariant enumeration recovers the representation. If e carries the action of G on α to the action of G on Fin n through ρ, then ρ is the permutation representation read through e.

      source
      @[simp]
      theorem Equiv.ker_permutationRepresentation {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {n : ℕ} (e : α ≃ Fin n) :
      e.permutationRepresentation.ker = (MulAction.toPermHom G α).ker

      The kernel does not depend on the enumeration: it is the kernel of the action.

      source
      @[simp]
      theorem Equiv.comap_stabilizer_permutationRepresentation {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {n : ℕ} (e : α ≃ Fin n) (x : α) :
      Subgroup.comap e.permutationRepresentation (MulAction.stabilizer (Perm (Fin n)) (e x)) = MulAction.stabilizer G x

      The point stabilisers of the representation are those of the action: the stabiliser of the index e x pulls back to the stabiliser of x.

      source
      @[simp]
      theorem Equiv.isPretransitive_range_permutationRepresentation_iff {G : Type u_1} {α : Type u_2} [Group G] [MulAction G α] {n : ℕ} (e : α ≃ Fin n) :
      MulAction.IsPretransitive (↥e.permutationRepresentation.range) (Fin n) ↔ MulAction.IsPretransitive G α

      The representation is transitive exactly when the action is.