associator_inv_snd — Mathlib

English

Let X, Y, Z be objects in a cartesian monoidal category. Then the inverse of the associator α_{X,Y,Z} composed with the projection snd_{X⊗Y,Z} equals the projection snd_{X,Y⊗Z}; i.e. (α_{X,Y,Z})^{-1} ∘ snd(X⊗Y, Z) = snd(X, Y⊗Z).

Русский

Пусть X, Y, Z — объекты в картинианальной моноидальной категории. Тогда обратный ассоциатор α_{X,Y,Z}^{-1} после проекции snd_{X⊗Y,Z} даёт проекцию snd_{X,Y⊗Z}; то есть (α_{X,Y,Z})^{-1} ∘ snd(X⊗Y, Z) = snd(X, Y⊗Z).

LaTeX

$$$(\alpha_{X,Y,Z})^{-1} \circ \mathrm{snd}(X\otimes Y, Z) = \mathrm{snd}(X, Y\otimes Z)$$$

Lean4

@[reassoc (attr := simp)]
theorem associator_inv_snd (X Y Z : C) : (α_ X Y Z).inv ≫ snd _ _ = snd _ _ ≫ snd _ _ := by
  simp [snd_def, ← leftUnitor_whiskerRight_assoc, -leftUnitor_whiskerRight, ← comp_whiskerRight_assoc]

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