associator_inv_snd — Mathlib

English

Let C be a monoidal category with finite products. For all objects X, Y, Z in C, the inverse of the associator α_{X,Y,Z} composes with the second projection to the expected result: (α_{X,Y,Z})^{-1} ∘ pr_2 = pr_2 ∘ pr_2. In other words, the inverse associator is compatible with the second projection.

Русский

Пусть C — моноидальная категория с конечными произведениями. Для любых объектов X, Y, Z в C обратимый ассоциатор α_{X,Y,Z} совместим с второй проекцией: (α_{X,Y,Z})^{-1} ∘ pr_2 = pr_2 ∘ pr_2.

LaTeX

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

Lean4

@[reassoc]
theorem associator_inv_snd (X Y Z : C) : (α_ X Y Z).inv ≫ prod.snd = prod.snd ≫ prod.snd := by simp [associator_inv]

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