English
For any monoid G and natural n, there is a natural isomorphism between the diagonal action on G^{n+1} and the tensor of the left-regular action with the diagonal on G^n, i.e., diagonal G(n+1) ≅ leftRegular G ⊗ diagonal G n.
Русский
Для моноида G и натурального n существует естественное изоморождение между диагональным действием на G^{n+1} и тензором левого регулярного действия на диагональ на G^n: diagonal G(n+1) ≅ leftRegular G ⊗ diagonal G n.
LaTeX
$$$\text{diagonal}(G, n+1) \cong \text{leftRegular}(G) \otimes \text{diagonal}(G, n),$$$
Lean4
/-- The natural isomorphism of `G`-sets `Gⁿ⁺¹ ≅ G × Gⁿ`, where `G` acts by left multiplication on
each factor. -/
@[simps!]
noncomputable def diagonalSuccIsoTensorDiagonal [Monoid G] (n : ℕ) :
diagonal G (n + 1) ≅ leftRegular G ⊗ diagonal G n :=
mkIso (Fin.consEquiv _).symm.toIso fun _ => rfl
