associator_hom_app — Mathlib

English

The associator hom app at j matches the canonical associator hom at F₁(j), F₂(j), F₃(j).

Русский

Гомоморфия ассоциатора на точке j совпадает с канонической гомоморфией ассоциатора на F₁(j), F₂(j), F₃(j).

LaTeX

$$$$ (\mathrm{associator} F_1 F_2 F_3).\mathrm{hom}.app j = (\mathrm{associator}_{F_1(j),F_2(j),F_3(j)}).\mathrm{hom}. $$$$

Lean4

@[simp]
theorem associator_hom_app (F₁ F₂ F₃ : J ⥤ C) (j : J) : (α_ F₁ F₂ F₃).hom.app j = (α_ _ _ _).hom :=
  by
  apply hom_ext
  · rw [← fst_app, ← NatTrans.comp_app, associator_hom_fst]
    simp
  · apply hom_ext
    · rw [← snd_app, ← NatTrans.comp_app, ← fst_app, ← NatTrans.comp_app, Category.assoc, associator_hom_snd_fst]
      simp
    · rw [← snd_app, ← NatTrans.comp_app, ← snd_app, ← NatTrans.comp_app, Category.assoc, associator_hom_snd_snd]
      simp

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