whiskerLeft_app_tensor_app — Mathlib

English

Naturality of whiskering left with respect to tensoring on the right in a natural transformation setting: the appropriate tensor-naturality identity holds.

Русский

Натуральность по отношению к отбивке слева в отношении тензорного правого действия в ситуации естественной трансформации.

LaTeX

$$$\\text{whiskerLeft_app_tensor_app}$ expresses the naturality of tensor with whiskering on the left and right.$$

Lean4

@[reassoc]
theorem whiskerLeft_app_tensor_app {X' Y' : J} (f : X' ⟶ Y') (X : J) :
    F.obj X ◁ G.map f ≫ (α.app X ⊗ₘ β.app Y') = (α.app X ⊗ₘ β.app X') ≫ F'.obj X ◁ G'.map f := by
  simpa using tensor_naturality α β (𝟙 X) f

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