whiskerLeft_app_apply — Mathlib

English

The inverse of the associator applied to x decomposes x into nested pairs, reflecting the tensor associativity in the enriched setting.

Русский

Обратный ассоциатор применяется к x и разлагает x на вложенные пары, отражая ассоциативность тензорной операции во внутреннем обогащении.

LaTeX

$$$\alpha_{(K.functorHom L).obj X, (L.functorHom M).obj X, (M.functorHom N).obj X}^{-1} x = \langle \langle x.1, x.2.1 \rangle, x.2.2 \rangle$$$

Lean4

@[simp]
theorem whiskerLeft_app_apply (K L M N : C ⥤ D) (g : L.functorHom M ⊗ M.functorHom N ⟶ L.functorHom N) {X : C}
    (a : (K.functorHom L ⊗ L.functorHom M ⊗ M.functorHom N).obj X) :
    (K.functorHom L ◁ g).app X a = ⟨a.1, g.app X a.2⟩ :=
  rfl

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