isIso_actionHomLeft

Mathlib.CategoryTheory.Monoidal.Action.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MonoidalCategory.MonoidalRightAction.isIso_actionHomLeft

English

δᵣ is an isomorphism in the right-linear setting; i.e., δᵣ F d c is an isomorphism.

Русский

δᵣ в праволинейном окружении является изоморфизмом; то есть δᵣ F d c — изоморфизм.

LaTeX

$$$\operatorname{IsIso}(\delta^{\mathrm{r}} F d c)$$$

Lean4

instance isIso_actionHomLeft {x y : D} (f : x ⟶ y) [IsIso f] (z : C) : IsIso (f ⊵ᵣ z) :=
  ⟨inv f ⊵ᵣ z, by simp⟩

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

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

Разделы

Аффилиация

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