whiskerLeft_app_snd — Mathlib

English

The snd component after whiskerLeft with g matches the snd component after applying g.

Русский

snd-компонента после whiskerLeft с g совпадает со snd после применения g.

LaTeX

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

Lean4

@[reassoc (attr := simp)]
theorem whiskerLeft_app_snd (F₁ : J ⥤ C) {F₂ F₂' : J ⥤ C} (g : F₂ ⟶ F₂') (j : J) :
    (F₁ ◁ g).app j ≫ snd _ _ = snd _ _ ≫ g.app j :=
  (tensorHom_app_snd (𝟙 F₁) g j)

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