English
For P : Bimod R S, the right unitor morphism and its inverse compose to the identity on P.X, mirroring the unit coherence on the right.
Русский
Для P : Bimod R S правый унитор и его обратное композиции образуют тождественный отображение на P.X.
LaTeX
$$$$ \operatorname{hom} P \circ \operatorname{inv} P = \mathrm{id}_{P.X}. $$$$
Lean4
theorem hom_inv_id : hom P ≫ inv P = 𝟙 _ :=
by
dsimp only [hom, inv, TensorBimod.X]
ext; dsimp
slice_lhs 1 2 => rw [coequalizer.π_desc]
slice_lhs 1 2 => rw [rightUnitor_inv_naturality]
slice_lhs 2 3 => rw [← whisker_exchange]
slice_lhs 3 4 => rw [coequalizer.condition]
slice_lhs 2 3 => rw [associator_naturality_right]
slice_lhs 3 4 => rw [← whiskerLeft_comp, MonObj.mul_one]
slice_rhs 1 2 => rw [Category.comp_id]
monoidal
