whiskerLeft_ε_η — Mathlib

English

For any D, the left whiskering of ε F and η F by T composes to the identity on T ⊗ F(I) where I is the tensor unit.

Русский

Для любого D левой усечкой ε F и η F по T образуется тождественный морфизм на T ⊗ F(I).

LaTeX

$$$$ T \\triangleleft \\varepsilon_F \\;\\circ\\; T \\triangleleft \\eta_F = \\mathrm{id}_{T \\otimes F(I)} $$$$

Lean4

@[reassoc (attr := simp)]
theorem whiskerLeft_ε_η (T : D) : T ◁ ε F ≫ T ◁ η F = 𝟙 _ := by
  rw [← MonoidalCategory.whiskerLeft_comp, ε_η, MonoidalCategory.whiskerLeft_id]

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