associator_inv_apply — Mathlib

English

The hom part of the associator applied to x produces the triple ⟨x.1, x.2, x.3⟩, reflecting the nested tensor product.

Русский

Гом-часть ассоциатора, применённая к x, выдаёт тройку ⟨x.1, x.2, x.3⟩.

LaTeX

$$$\alpha_{((K.functorHom L) \otimes (L.functorHom M))}.hom x = \langle x.1, x.2, x.3 \rangle$$$

Lean4

@[simp]
theorem associator_inv_apply (K L M N : C ⥤ D) {X : C}
    (x : ((K.functorHom L) ⊗ (L.functorHom M) ⊗ (M.functorHom N)).obj X) :
    (α_ ((K.functorHom L).obj X) ((L.functorHom M).obj X) ((M.functorHom N).obj X)).inv x = ⟨⟨x.1, x.2.1⟩, x.2.2⟩ :=
  rfl

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