iteratedWreathToPermHom — Mathlib

English

There is a canonical homomorphism from IteratedWreathProduct G n to Perm(Fin n → G).

Русский

Существует канонический гомоморфизм из IteratedWreathProduct G n в Perm(Fin n → G).

LaTeX

$$$\text{iteratedWreathToPermHom}(G,n) : \mathrm{IteratedWreathProduct}(G,n) \to^* \mathrm{Perm}(\mathrm{Fin}(n) \to G) $$$

Lean4

/-- The homomorphism from `IteratedWreathProduct G n` to `Perm (Fin n → G)`. -/
def iteratedWreathToPermHom (G : Type*) [Group G] : (n : ℕ) → (IteratedWreathProduct G n →* Equiv.Perm (Fin n → G))
  | 0 => 1
  | n + 1 => by
    let _ := MulAction.compHom (Fin n → G) (iteratedWreathToPermHom G n)
    exact
      (Fin.succFunEquiv G n).symm.permCongrHom.toMonoidHom.comp
        (RegularWreathProduct.toPerm (IteratedWreathProduct G n) G (Fin n → G))

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