toPermHom — Mathlib

English

For a group G acting on a set α, each g ∈ G defines a permutation of α, giving a monoid hom toPermHom: G →* Perm(α).

Русский

Для группы G, действующей на множество α, каждый элемент g порождает перестановку α, задавая моноид-гомоморфизм toPermHom: G →* Perm(α).

LaTeX

$$$\text{toPermHom} : G \to_* \mathrm{Perm}(\alpha), \quad \text{toPermHom}(g) = \text{MulAction.toPerm}(g).$$$

Lean4

/-- Given an action of a group `G` on a set `α`, each `g : G` defines a permutation of `α`. -/
@[simps]
def toPermHom : G →* Equiv.Perm α where
  toFun := MulAction.toPerm
  map_one' := Equiv.ext <| one_smul G
  map_mul' u₁ u₂ := Equiv.ext <| mul_smul (u₁ : G) u₂

Похожие утверждения