whiskerRight_μ_δ — Mathlib

English

For any X, Y in C and T in D, whiskering the associativity-like morphism μ with δ on the right yields the identity on the tensor of F X and F Y tensored with T.

Русский

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

LaTeX

$$$$ \\mu_F X Y \\;\\triangleright\\; T \\;\\circ\\; \\delta_F X Y \\;\\triangleright\\; T = \\mathrm{id}_{\\bigl(F X \\otimes F Y\\bigr) \\triangleright T} $$$$

Lean4

@[reassoc (attr := simp)]
theorem whiskerRight_μ_δ (X Y : C) (T : D) : μ F X Y ▷ T ≫ δ F X Y ▷ T = 𝟙 _ := by
  rw [← MonoidalCategory.comp_whiskerRight, μ_δ, id_whiskerRight]

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