associator_hom_apply — Mathlib

English

The hom component of the associator in the enriched setting sends the nested structure to a triple of components.

Русский

Гом-компонента ассоциатора во внутреннем обогащении переводит вложенную структуру в тройку компонент.

LaTeX

$$$\big(\alpha_{((K.functorHom L) (L.functorHom M))} \big).hom x = \langle x.1.1, x.1.2, x.2 \rangle$$$

Lean4

@[simp]
theorem associator_hom_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)).hom x = ⟨x.1.1, x.1.2, x.2⟩ :=
  rfl

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