id_whiskerRight_bimod — Mathlib

English

Compatibility of whiskerLeft with composition in bimodules via associator moves.

Русский

Совместимость whiskerLeft с композициями в биомодулях через перестановки ассоциатора.

LaTeX

$$$$ \{ M : Bimod W X \, N : Bimod X Y \} \; (M.tensorBimod N).whiskerLeft f = \cdots $$$$

Lean4

theorem id_whiskerRight_bimod {X Y Z : Mon C} {M : Bimod X Y} {N : Bimod Y Z} :
    whiskerRight (𝟙 M) N = 𝟙 (M.tensorBimod N) := by
  ext
  apply Limits.coequalizer.hom_ext
  dsimp only [tensorBimod_X, whiskerRight_hom, id_hom']
  simp only [id_whiskerRight, ι_colimMap, parallelPair_obj_one, parallelPairHom_app_one, Category.id_comp]
  erw [Category.comp_id]

Похожие утверждения