instIsIsoHomOfMapForget

Mathlib.CategoryTheory.Monoidal.Mon_

URI: https://scilib.ai/kg/mathlib#Mon.instIsIsoHomOfMapForget

English

If f is an isomorphism in Mon C, then its underlying hom is an isomorphism in C.

Русский

Если f является изоморфизмом в Mon C, то его базовый гомоморфизм является изоморфизмом в C.

LaTeX

$$$\\text{If } f:\\,M\\to N\\text{ isIso in Mon C, then } f.hom \\text{ isIso in } C$$$

Lean4

instance {A B : Mon C} (f : A ⟶ B) [e : IsIso ((forget C).map f)] : IsIso f.hom :=
  e

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

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

Разделы

Аффилиация

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