English
In the graded tensor setting, the i-th component of the inverse of the right unitor on K is given by the composition of the right unitor at K.X_i, whiskering with a unit object, and the unit insertion map, mirroring the left-unitor case.
Русский
В градуированном тензорном контексте i-я компонента обратного правого унитора на K задаётся композитом правого унитора на K.X_i, оборачивания с единичным объектом и вставкой единицы, аналогично случаю левого унитора.
LaTeX
$$$(\\mathrm{rightUnitor}' K)^{-1}_i = (\\rho_{K.X_i})^{-1} \\; \\circ\\; (K.X_i) \\!\\triangleleft\\; (\\mathrm{singleObjXSelf} c 0 (\\mathrm{Id}_C))^{-1} \\; \\circ\\; \\iota_{\\otimes} K (tensorUnit) i 0 i (\\mathrm{add\_zero}\, i)$$$
Lean4
theorem rightUnitor'_inv (i : I) :
(rightUnitor' K).inv i =
(ρ_ (K.X i)).inv ≫
((K.X i) ◁ (singleObjXSelf c 0 (𝟙_ C)).inv) ≫ ιTensorObj K (tensorUnit C c) i 0 i (add_zero i) :=
by
dsimp [rightUnitor']
rw [GradedObject.Monoidal.rightUnitor_inv_apply, assoc, assoc, Iso.cancel_iso_inv_left,
GradedObject.Monoidal.ι_tensorHom]
dsimp
rw [id_tensorHom, ← whiskerLeft_comp_assoc]
congr 2
rw [← cancel_epi (GradedObject.Monoidal.tensorUnit₀ (I := I)).hom, Iso.hom_inv_id_assoc]
dsimp [tensorUnitIso]
rw [dif_pos rfl]
rfl
