whiskerLeft_η_ε — Mathlib

English

For any X, Y in C and T in D, whiskering δ F X Y by T on the left with μ F X Y on the right yields the identity on T ⊗ F(X) ⊗ F(Y).

Русский

Для любых X, Y ∈ C и T ∈ D, левая усечка δ F X Y по T совместно с μ F X Y даёт тождественный морфизм на T ⊗ F X ⊗ F Y.

LaTeX

$$$$ T \\triangleleft \\delta_F X Y \\;\\circ\\; T \\triangleleft \\mu_F X Y = \\mathrm{id}_{T \\otimes F X \\otimes F Y} $$$$

Lean4

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

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