English
There is an isomorphism of G-sets diagonal G(n+1) ≅ leftRegular G ⊗ trivial G (Fin n → G) for each n, built recursively by the given construction.
Русский
Для каждого n существует изоморфизм диагонального действия diagonal G(n+1) ≅ leftRegular G ⊗ trivial G (Fin n → G), конструируемый по заданному рекурсивному процессу.
LaTeX
$$$\text{diagonalSuccIsoTensorTrivial}(n) : \ diagonal G (n+1) \cong \text{leftRegular} G \otimes \text{trivial } G (\text{Fin } n \to G)$$$
Lean4
/-- An isomorphism of `G`-sets `Gⁿ⁺¹ ≅ G × Gⁿ`, where `G` acts by left multiplication on `Gⁿ⁺¹` and
`G` but trivially on `Gⁿ`. The map sends `(g₀, ..., gₙ) ↦ (g₀, (g₀⁻¹g₁, g₁⁻¹g₂, ..., gₙ₋₁⁻¹gₙ))`,
and the inverse is `(g₀, (g₁, ..., gₙ)) ↦ (g₀, g₀g₁, g₀g₁g₂, ..., g₀g₁...gₙ).` -/
noncomputable def diagonalSuccIsoTensorTrivial : ∀ n : ℕ, diagonal G (n + 1) ≅ leftRegular G ⊗ trivial G (Fin n → G)
| 0 =>
diagonalOneIsoLeftRegular G ≪≫ (ρ_ _).symm ≪≫ tensorIso (Iso.refl _) (tensorUnitIso (Equiv.ofUnique PUnit _).toIso)
| n + 1 =>
diagonalSuccIsoTensorDiagonal _ _ ≪≫
tensorIso (Iso.refl _) (diagonalSuccIsoTensorTrivial n) ≪≫
leftRegularTensorIso _ _ ≪≫
tensorIso (Iso.refl _) (mkIso (Fin.insertNthEquiv (fun _ => G) 0).toIso fun _ => rfl)
