whiskerRight_ε_η — Mathlib

English

For any object T in D, the right whiskering of the unit and counit by T composes to the identity on the tensor unit tensored with T.

Русский

Для любого объекта T в D правая усечка единицы и куд-одинца по T образуют тождественный гомомор в I_D ⊗ T.

LaTeX

$$$$ \\varepsilon_F \\;\\triangleright\\; T \\;\\circ\\; \\eta_F \\;\\triangleright\\; T = \\mathrm{id}_{I_D \\otimes T} $$$$

Lean4

@[reassoc (attr := simp)]
theorem whiskerRight_ε_η (T : D) : ε F ▷ T ≫ η F ▷ T = 𝟙 _ := by
  rw [← MonoidalCategory.comp_whiskerRight, ε_η, id_whiskerRight]

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