instIsIsoHom

Mathlib.CategoryTheory.Monoidal.CommMon_

URI: https://scilib.ai/kg/mathlib#CommMon.instIsIsoHom

English

Given a morphism f with IsIso in the forgetful category, the underlying morphism f.hom is an isomorphism.

Русский

При наличии изоморфизма f в забывающем контексте базовая карта f.hom является изоморфизмом.

LaTeX

$$$\\text{If } [IsIso f] \\Rightarrow IsIso f.hom$$$

Lean4

instance {M N : CommMon C} {f : M ⟶ N} [IsIso f] : IsIso f.hom :=
  inferInstanceAs <| IsIso <| (forget C).map f

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

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

Разделы

Аффилиация

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