English
For all i, j, the right unitor inverse intertwines with the i→j differential in the tensor with the tensor unit: (rightUnitor' K)^{-1}_i ; (tensorObj K (tensorUnit C c)).d_{i j} = K.d_{i j} ; (rightUnitor' K)^{-1}_j.
Русский
Для всех i, j обратный правый унитор компонуется с дифференциалом в тензорном произведении с тензорной единицей так же, как и слева.
LaTeX
$$$(\\mathrm{rightUnitor}' K)^{-1}_i \\; \\circ\\; (\\mathrm{tensorObj} K (\\mathrm{tensorUnit}\\, C\\, c))^{d}_{i j} = K^{d}_{i j} \\; \\circ\\; (\\mathrm{rightUnitor}' K)^{-1}_j$$$
Lean4
theorem rightUnitor'_inv_comm (i j : I) :
(rightUnitor' K).inv i ≫ (tensorObj K (tensorUnit C c)).d i j = K.d i j ≫ (rightUnitor' K).inv j :=
by
by_cases hij : c.Rel i j
· simp only [rightUnitor'_inv, assoc, mapBifunctor.d_eq, Preadditive.comp_add, mapBifunctor.ι_D₁, mapBifunctor.ι_D₂,
tensor_unit_d₂, comp_zero, add_zero]
rw [mapBifunctor.d₁_eq _ _ _ _ hij _ _ (by simp)]
dsimp
simp only [one_smul, whisker_exchange_assoc, whiskerRight_id, assoc, Iso.inv_hom_id_assoc]
· simp only [shape _ _ _ hij, comp_zero, zero_comp]
