inv_δᵣ

Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor

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

English

inv(δᵣ F d c) = μᵣ F d c; i.e., the inverse of δᵣ is μᵣ.

Русский

inv(δᵣ F d c) = μᵣ F d c; то есть обратный δᵣ равен μᵣ.

LaTeX

$$$\mathrm{inv}(\delta^{\mathrm{r}} F d c) = \mu^{\mathrm{r}} F d c$$$

Lean4

@[simp]
theorem inv_δᵣ : CategoryTheory.inv (δᵣ F d c) = μᵣ F d c :=
  Eq.symm <| IsIso.eq_inv_of_hom_inv_id <| δᵣ_comp_μᵣ F d c

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

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

Разделы

Аффилиация

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