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 \\mu_F X Y \\;\\circ\\; T \\triangleleft \\delta_F X Y = \\mathrm{id}_{T \\otimes F X \\otimes F Y} $$$$

Lean4

@[reassoc (attr := simp)]
theorem whiskerLeft_μ_δ (X Y : C) (T : D) : T ◁ μ F X Y ≫ T ◁ δ F X Y = 𝟙 _ := by
  rw [← MonoidalCategory.whiskerLeft_comp, μ_δ, MonoidalCategory.whiskerLeft_id]

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