instIsIsoCommaHom

Mathlib.CategoryTheory.MorphismProperty.Comma

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MorphismProperty.Comma.instIsIsoCommaHom

English

In a comma setting, the equality of homomorphisms with inverses is preserved: (inv f).hom = inv(f.hom).

Русский

В комме сохраняется равенство гомоморфизмов и их обратных: (inv f).hom = inv(f.hom).

LaTeX

$$$\\text{inv\_hom}: (inv f).\\mathrm{hom} = \\mathrm{inv}(f.\\mathrm{hom})$$$

Lean4

instance {X Y : P.Comma L R Q W} (f : X ⟶ Y) [IsIso f] : IsIso f.hom :=
  (forget L R P Q W).map_isIso f

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

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

Разделы

Аффилиация

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