inv_μₗ

Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.LeftLinear.inv_μₗ

English

For any x in D and any isomorphism f in C, inv (x ⊴ᵣ f) = x ⊴ᵣ inv f.

Русский

Для любого x в D и изоморфизма f в C, обратное к x ⊴ᵣ f равно x ⊴ᵣ f^{-1}.

LaTeX

$$$inv(x \triangleleft_r f) = x \triangleleft_r inv(f).$$$

Lean4

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

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

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

Разделы

Аффилиация

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