natTransEquiv_symm_whiskerRight_functorHom_app

English

Naturality of the symmetry under whiskering: the symmetrized action on K.functorHom L by natTransEquiv.symm f matches the expected application on the component level.

Русский

Натуральность симметрии при взвешивании: симметризированное действие natTransEquiv.symm f на K.functorHom L совпадает с ожидаемым применением на уровне компонентов.

LaTeX

$$$((natTransEquiv.symm f) \ ▷ K.functorHom L).app X a = (HomObj.ofNatTrans f, a.2)$$$

Lean4

@[simp]
theorem natTransEquiv_symm_whiskerRight_functorHom_app (K L : C ⥤ D) (X : C) (f : K ⟶ K)
    (x : 𝟙_ _ ⊗ (K.functorHom L).obj X) :
    ((natTransEquiv.symm f ▷ K.functorHom L).app X x) = (HomObj.ofNatTrans f, x.2) :=
  rfl

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