whiskerLeft_app_fst — Mathlib

English

The app at j of F₁ whisks left by g has its fst component equal to the fst component of F₁ evaluated at j.

Русский

На точке j F₁ ◁ g имеет fst-компонент равный fst-компоненте F₁(j).

LaTeX

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

Lean4

@[reassoc (attr := simp)]
theorem whiskerLeft_app_fst (F₁ : J ⥤ C) {F₂ F₂' : J ⥤ C} (g : F₂ ⟶ F₂') (j : J) : (F₁ ◁ g).app j ≫ fst _ _ = fst _ _ :=
  (tensorHom_app_fst (𝟙 F₁) g j).trans (by simp)

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