English
For f: Fin(n+1) → G, the map on the hom components of the diagonal-trivial isot is given by a pair (f0, i ↦ f(castSucc i)^{-1} f(i.succ)).
Русский
Для отображения f: Fin(n+1) → G отображение на компоненты гомоморфизма диагонального тривиального изоморфизма задаётся парой (f0, i ↦ f(castSucc i)^{-1} f(i+1)).
LaTeX
$${ hom := (f 0, \lambda i => f(\mathrm{castSucc}\u0000 i)^{-1} f(i.succ)) }$$
Lean4
@[simp]
theorem diagonalSuccIsoTensorTrivial_hom_hom_apply {n : ℕ} (f : Fin (n + 1) → G) :
(diagonalSuccIsoTensorTrivial G n).hom.hom f = (f 0, fun i => (f (Fin.castSucc i))⁻¹ * f i.succ) := by
induction n with
| zero => exact Prod.ext rfl (funext fun x => Fin.elim0 x)
| succ n hn =>
refine Prod.ext rfl (funext fun x => ?_)
induction x using Fin.cases <;>
simp_all only [tensorObj_V, diagonalSuccIsoTensorTrivial, Iso.trans_hom, tensorIso_hom, Iso.refl_hom,
id_tensorHom, comp_hom, whiskerLeft_hom, types_comp_apply, whiskerLeft_apply, leftRegularTensorIso_hom_hom,
tensor_ρ, tensor_apply, ofMulAction_apply] <;>
simp [ofMulAction_V, types_tensorObj_def, Fin.tail]
