inv_ε

Mathlib.CategoryTheory.Monoidal.Functor

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

English

Alternative expression for the inverse of the left unitor image under F in terms of δ and μ and η.

Русский

Альтернативное выражение для обратного образа левого унитора через δ, μ и η.

LaTeX

$$$$ F(\\lambda_X)^{-1} = (\\lambda_{F X})^{-1} \\circ (ε F \\triangleright F X) \\circ μ F (I, X) $$$$

Lean4

@[simp]
theorem inv_ε : CategoryTheory.inv (ε F) = η F := by simp [← inv_η]

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

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

Разделы

Аффилиация

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