whiskerLeft_comp_unit_app — Mathlib

English

Naturality of the unit when whiskering on the left; compatibility of the unit with left action by x.

Русский

Натуральность единицы при левом взведении; совместимость единицы с левым действием по x.

LaTeX

$$$ F.obj x \\; \\triangleleft\\; G.map g \\; \\circ \\; (\\text{unit } F G)_{(x,y')} = (\\text{unit } F G)_{(x,y)} \\circ (F \\⊛ G)_{(x \\triangleleft g)} $$$

Lean4

@[reassoc (attr := simp)]
theorem whiskerLeft_comp_unit_app (g : y ⟶ y') :
    F.obj x ◁ G.map g ≫ (unit F G).app (x, y') = (unit F G).app (x, y) ≫ (F ⊛ G).map (x ◁ g) := by
  simpa [tensorHom_def] using (unit F G).naturality (𝟙 _ ×ₘ g)

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