0PDV Proof. We have σ=(Rξ1−∘mult)∘(Rξ1−⊗Rξ2−⊗εLξ1+,Rξ1−)∘(Rξ1−⊗λ⊗Rξ1−)∘(ηLξ1+,Rξ1−⊗id).\sigma=(R_{\xi_{1}^{-}}\circ\textrm{mult})\circ(R_{\xi_{1}^{-}}\otimes R_{\xi_{2}^{-}}\otimes\varepsilon_{L_{\xi_{1}^{+}},R_{\xi_{1}^{-}}})\circ(R_{\xi_{1}^{-}}\otimes\lambda\otimes R_{\xi_{1}^{-}})\circ(\eta_{L_{\xi_{1}^{+}},R_{\xi_{1}^{-}}}\otimes\operatorname{id}\nolimits). We have α=(id⊠αξ2−(−1))⋅(α|U⊠id)\alpha=(\operatorname{id}\nolimits\boxtimes\alpha_{\xi_{2}^{-}(-1)})\cdot(\alpha_{|U}\boxtimes\operatorname{id}\nolimits), hence α⊗β=(id⊠αξ2−(−1))⊗(α|U⋅β)\alpha\otimes\beta=(\operatorname{id}\nolimits\boxtimes\alpha_{\xi_{2}^{-}(-1)})\otimes(\alpha_{|U}\cdot\beta). As a consequence, it is enough to prove the first statement of the lemma assuming that α|U=idU\alpha_{|U}=\operatorname{id}\nolimits_{U}. In that case, the composition above is given by α⊗β\displaystyle\alpha\otimes\beta ↦∑x∈ξ~1−1(T)(idT∖{ξ~1(x)}⊠ξ~1([−1→x]))⊗(idT∖{ξ~1(x)}⊠ξ~1([x→1]))⊗α⊗β\displaystyle\mapsto\sum_{x\in\tilde{\xi}_{1}^{-1}(T)}(\operatorname{id}\nolimits_{T\setminus\{\tilde{\xi}_{1}(x)\}}\boxtimes\tilde{\xi}_{1}([-1\to x]))\otimes(\operatorname{id}\nolimits_{T\setminus\{\tilde{\xi}_{1}(x)\}}\boxtimes\tilde{\xi}_{1}([x\to 1]))\otimes\alpha\otimes\beta ↦∑x∈ξ~1−1(T)(idT∖{ξ~1(x)}⊠ξ~1([−1→x]))⊗(αξ2−(−1)⊠id)⊗(id⊠ξ~1([x→1]))⊗β\displaystyle\mapsto\sum_{x\in\tilde{\xi}_{1}^{-1}(T)}(\operatorname{id}\nolimits_{T\setminus\{\tilde{\xi}_{1}(x)\}}\boxtimes\tilde{\xi}_{1}([-1\to x]))\otimes(\alpha_{\xi_{2}^{-}(-1)}\boxtimes\operatorname{id}\nolimits)\otimes(\operatorname{id}\nolimits\boxtimes\tilde{\xi}_{1}([x\to 1]))\otimes\beta ↦(id⊠βξ1−(−1))⊗(αξ2−(−1)⊠id)⊗β|S\displaystyle\mapsto(\operatorname{id}\nolimits\boxtimes\beta_{\xi_{1}^{-}(-1)})\otimes(\alpha_{\xi_{2}^{-}(-1)}\boxtimes\operatorname{id}\nolimits)\otimes\beta_{|S} ↦(id⊠βξ1−(−1))⊗(αξ2−(−1)⊠β|S).\displaystyle\mapsto(\operatorname{id}\nolimits\boxtimes\beta_{\xi_{1}^{-}(-1)})\otimes(\alpha_{\xi_{2}^{-}(-1)}\boxtimes\beta_{|S}). It is immediate to check that the formula for σ−1\sigma^{-1} does produce an inverse. ∎