inv_δ

Mathlib.CategoryTheory.Monoidal.Functor

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.Monoidal.inv_δ

English

The inverse of the tensorator μ for F at X and Y equals the corresponding δ morphism.

Русский

Обратный тензоратор μ на F для X и Y равен соответствующему δ-морфизму.

LaTeX

$$$$ \\mathrm{inv}(\\mu_F X Y) = \\delta_F X Y $$$$

Lean4

@[simp]
theorem inv_δ (X Y : C) : CategoryTheory.inv (δ F X Y) = μ F X Y := by simp [← inv_μ]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru