whiskerRight_comp_unit_app — Mathlib

English

Naturality of the unit when whiskering on the right, showing compatibility of the unit with right action by a fixed object y.

Русский

Натуральность единицы при правом взведении (whisker right), показывающая совместимость единицы с правым действием фиксированного объекта y.

LaTeX

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

Lean4

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

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