whisker_exchange — Mathlib

English

Compatibility of whiskering on both sides with tensoring under localization.

Русский

Совместимость whisker слева и справа с тензорированием в локализации.

LaTeX

$$$\\text{whisker exchange compatibility}$$$

Lean4

@[reassoc]
theorem whisker_exchange {Q X Y Z : LocalizedMonoidal L W ε} (f : Q ⟶ X) (g : Y ⟶ Z) : Q ◁ g ≫ f ▷ Z = f ▷ Y ≫ X ◁ g :=
  by simp only [← id_tensorHom, ← tensorHom_id, ← tensor_comp, id_comp, comp_id]

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