tensorHom_app_fst — Mathlib

English

The fst projection interacts with tensorHom in a canonical way: the fst component of the tensor of f and g, applied at j, equals the composition with f.app j.

Русский

Проекция fst взаимодействует с tensorHom канонически: fst-компонента тензора f и g, применённого на j, равна композиции с f.app j.

LaTeX

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

Lean4

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

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