whiskerRight_tensor — Mathlib

English

Let X, X' : C and f: X → X' with Y, Z objects. The right whiskering of f on Y ⊗ Z relates to whiskering by Y and Z via the associator: f ▷ (Y ⊗ Z) = (α_{X Y Z})^{-1} ≫ (f ▷ Y) ▷ Z ≫ (α_{X' Y Z}).hom.

Русский

Пусть X, X' : C и f: X → X' и Y, Z объекты. Правое обёртывание f над Y ⊗ Z связано с оберткой над Y и над Z через ассоциатор: f ▷ (Y ⊗ Z) = (α_{X Y Z})^{-1} ≫ (f ▷ Y) ▷ Z ≫ (α_{X' Y Z}).hom.

LaTeX

$$$ f \\triangleleft (Y \\otimes Z) = (\\alpha_{X Y Z})^{-1} \\circ (f \\triangleleft Y) \\triangleleft Z \\circ (\\alpha_{X' Y Z}).hom $$$

Lean4

@[reassoc, simp]
theorem whiskerRight_tensor {X X' : C} (f : X ⟶ X') (Y Z : C) :
    f ▷ (Y ⊗ Z) = (α_ X Y Z).inv ≫ f ▷ Y ▷ Z ≫ (α_ X' Y Z).hom :=
  by
  simp only [← tensorHom_id]
  rw [associator_naturality]
  simp

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