instIsIsoEqToHom

Mathlib.CategoryTheory.EqToHom

URI: https://scilib.ai/kg/mathlib#CategoryTheory.instIsIsoEqToHom

English

For any equality h: X = Y in a category, the morphism eqToHom h is an isomorphism.

Русский

Для любого равенства h: X = Y в категории морфизм eqToHom h является изоморфизмом.

LaTeX

$$$ \\operatorname{IsIso}(\\mathrm{eqToHom}(h)) $$$

Lean4

instance {X Y : C} (h : X = Y) : IsIso (eqToHom h) :=
  (eqToIso h).isIso_hom

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

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

Разделы

Аффилиация

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