English
For any bimodule P : Bimod R S, the left unitor morphism and its inverse compose to the identity on P.X, i.e., the left unitor is a two–sided inverse in this bimodule context.
Русский
Пусть P : Bimod R S. Левый униторный морфизм и его обратный образ образуют тождественный отображение на P.X; левый унитор является bi–модулярной обратной связью.
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 [leftUnitor_inv_naturality]
slice_lhs 2 3 => rw [whisker_exchange]
slice_lhs 3 3 => rw [← Iso.inv_hom_id_assoc (α_ R.X R.X P.X) (R.X ◁ P.actLeft)]
slice_lhs 4 6 => rw [← Category.assoc, ← coequalizer.condition]
slice_lhs 2 3 => rw [associator_inv_naturality_left]
slice_lhs 3 4 => rw [← comp_whiskerRight, MonObj.one_mul]
slice_rhs 1 2 => rw [Category.comp_id]
monoidal
