associator_inv_app — Mathlib

English

In the functor category with a cartesian monoidal structure, the inverse associator is computed componentwise: for every object j in J, the j-th component of the inverse associator equals the inverse associator of the evaluated objects.

Русский

В категорийной теории Функторов с декартовым монодическим тождеством обратный ассоциатор вычисляется по компонентам: для каждого j ∈ J j-й компонент инверсии ассоциатора равен инверсии α(F1(j), F2(j), F3(j)).

LaTeX

$$$(\alpha_{F_1,F_2,F_3})^{-1}_j = \alpha^{-1}_{F_1(j),F_2(j),F_3(j)}$$$

Lean4

@[simp]
theorem associator_inv_app (F₁ F₂ F₃ : J ⥤ C) (j : J) : (α_ F₁ F₂ F₃).inv.app j = (α_ _ _ _).inv := by
  rw [← cancel_mono ((α_ _ _ _).hom), Iso.inv_hom_id, ← associator_hom_app, Iso.inv_hom_id_app]

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