English
The map iteratedWreathToPermHom G n is injective for all n.
Русский
Каждое отображение iteratedWreathToPermHom G n инъективно.
LaTeX
$$$ (n : Nat) \to\; Function.Injective (iteratedWreathToPermHom G n) $$$
Lean4
theorem iteratedWreathToPermHomInj (G : Type*) [Group G] : (n : ℕ) → Function.Injective (iteratedWreathToPermHom G n)
| 0 => by
simp only [IteratedWreathProduct_zero]
apply Function.injective_of_subsingleton
| n + 1 => by
let _ := MulAction.compHom (Fin n → G) (iteratedWreathToPermHom G n)
have : FaithfulSMul (IteratedWreathProduct G n) (Fin n → G) :=
⟨fun h ↦ iteratedWreathToPermHomInj G n (Equiv.ext h)⟩
exact
((Fin.succFunEquiv G n).symm.permCongrHom.toEquiv.comp_injective _).mpr
(RegularWreathProduct.toPermInj (IteratedWreathProduct G n) G (Fin n → G))
