English
For all indices i, j, the inverse left unitor intertwines with the i→j differential of the tensor with the tensor unit: (leftUnitor' K)^{-1}_i ; (tensorObj (tensorUnit C c) K).d_{i j} = K.d_{i j} ; (leftUnitor' K)^{-1}_j. This expresses the naturality of the left unitor with respect to the differential in the graded tensor context.
Русский
Для всех пар индексов i, j обратный левый унитор взаимно приводят дифференциал в градуированной тензорной конструкции: (leftUnitor' K)^{-1}_i ; (tensorObj (tensorUnit C c) K).d_{i j} = K.d_{i j} ; (leftUnitor' K)^{-1}_j. Это выражает естественность левового унитора по отношению к дифференциалу в градационной тензорной структуре.
LaTeX
$$$(\\mathrm{leftUnitor}' K)^{-1}_i \\; \\circ\\; (\\mathrm{tensorObj}(\\mathrm{tensorUnit}\\, C\\, c)\\, K)^{\\!d}_{i j} = K^{d}_{i j} \\; \\circ\\; (\\mathrm{leftUnitor}' K)^{-1}_j$$$
Lean4
@[reassoc]
theorem leftUnitor'_inv_comm (i j : I) :
(leftUnitor' K).inv i ≫ (tensorObj (tensorUnit C c) K).d i j = K.d i j ≫ (leftUnitor' K).inv j :=
by
by_cases hij : c.Rel i j
· simp only [leftUnitor'_inv, assoc, mapBifunctor.d_eq, Preadditive.comp_add, mapBifunctor.ι_D₁, mapBifunctor.ι_D₂,
unit_tensor_d₁, comp_zero, zero_add]
rw [mapBifunctor.d₂_eq _ _ _ _ _ hij _ (by simp)]
dsimp
simp only [ComplexShape.ε_zero, one_smul, ← whisker_exchange_assoc, id_whiskerLeft, assoc, Iso.inv_hom_id_assoc]
· simp only [shape _ _ _ hij, comp_zero, zero_comp]
