isIso_actionHomRight

Mathlib.CategoryTheory.Monoidal.Action.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MonoidalCategory.MonoidalLeftAction.isIso_actionHomRight

English

For any x in C and any morphism f: y ⟶ z in D, the morphism x ⊙ₗ f is an isomorphism in D.

Русский

Для любого x в C и любого морфизма f: y ⟶ z в D, морфизм x ⊙ₗ f является изоморфизмом в D.

LaTeX

$$$\\forall x:\\, C,\\; f:\\, y \\to z:\\; IsIso (x ⊴ₗ f)$$$

Lean4

instance isIso_actionHomRight (x : C) {y z : D} (f : y ⟶ z) [IsIso f] : IsIso (x ⊴ₗ f) :=
  ⟨x ⊴ₗ inv f, by simp⟩

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

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

Разделы

Аффилиация

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