English
For any M, N bimodules, whiskering with the identity on N yields the identity bimodule on M ⊗ N.
Русский
Для любых би-модуля M, N whiskerLeft от идентичности на N даёт тождественный би-модуль на M ⊗ N.
LaTeX
$$$$ M.whiskerLeft (\mathrm{id} N) = \mathrm{id}(M.tensorBimod N). $$$$
Lean4
theorem id_whiskerLeft_bimod {X Y : Mon C} {M N : Bimod X Y} (f : M ⟶ N) :
whiskerLeft (regular X) f = (leftUnitorBimod M).hom ≫ f ≫ (leftUnitorBimod N).inv :=
by
dsimp [tensorHom, regular, leftUnitorBimod]
ext
apply coequalizer.hom_ext
dsimp
slice_lhs 1 2 => rw [ι_colimMap, parallelPairHom_app_one]
dsimp [LeftUnitorBimod.hom]
slice_rhs 1 2 => rw [coequalizer.π_desc]
dsimp [LeftUnitorBimod.inv]
slice_rhs 1 2 => rw [Hom.left_act_hom]
slice_rhs 2 3 => rw [leftUnitor_inv_naturality]
slice_rhs 3 4 => rw [whisker_exchange]
slice_rhs 4 4 => rw [← Iso.inv_hom_id_assoc (α_ X.X X.X N.X) (X.X ◁ N.actLeft)]
slice_rhs 5 7 => rw [← Category.assoc, ← coequalizer.condition]
slice_rhs 3 4 => rw [associator_inv_naturality_left]
slice_rhs 4 5 => rw [← comp_whiskerRight, MonObj.one_mul]
have : (λ_ (X.X ⊗ N.X)).inv ≫ (α_ (𝟙_ C) X.X N.X).inv ≫ ((λ_ X.X).hom ▷ N.X) = 𝟙 _ := by monoidal
grind
