tensorHom_app_snd — Mathlib

English

Similarly for the snd projection: the snd component after tensorHom aligns with g.app j.

Русский

Аналогично для snd: snd-компонента после tensorHom согласуется с g.app j.

LaTeX

$$$$ (f \otimes g)_{\text{app}}^j \circ \mathrm{snd}_{F_1',F_2'} = \mathrm{snd}_{F_1,F_2} \circ g^{\,app}_j. $$$$

Lean4

@[reassoc (attr := simp)]
theorem tensorHom_app_snd {F₁ F₁' F₂ F₂' : J ⥤ C} (f : F₁ ⟶ F₁') (g : F₂ ⟶ F₂') (j : J) :
    (f ⊗ₘ g).app j ≫ snd _ _ = snd _ _ ≫ g.app j :=
  by
  change (f ⊗ₘ g).app j ≫ (snd F₁' F₂').app j = _
  rw [← NatTrans.comp_app, tensorHom_snd, NatTrans.comp_app]
  rfl

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