English
There is a simple expression for the diagonal-free homomorphism: it maps single f a to a simple form involving successive products of f, namely the expression of a single h.
Русский
Существуют явные формулы для гомоморфизма диагонального свободного типа: он переводит одиночный элемент в простую форму через последовательно произведения.
LaTeX
$$$$ (\\text{diagonalSuccIsoFree } k\, G\, n).hom.hom(\\mathrm{single} f a) = \\mathrm{single} (\\lambda i => (f i.castSucc)^{-1} * f i.succ) \\\\; (\\mathrm{single}(f 0) a). $$$$
Lean4
@[simp]
theorem diagonalSuccIsoFree_hom_hom_single (f : Fin (n + 1) → G) (a : k) :
(diagonalSuccIsoFree k G n).hom.hom (single f a) = single (fun i => (f i.castSucc)⁻¹ * f i.succ) (single (f 0) a) :=
by simp [diagonalSuccIsoFree, leftRegularTensorTrivialIsoFree_hom_hom_single_tmul_single (k := k)]
