comp_inv_eq_id

Mathlib.CategoryTheory.Iso

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Iso.comp_inv_eq_id

English

Let α: X ≅ Y, f: Z → Y, g: Z → X. Then g = f ≫ α.inv iff g ≫ α.hom = f.

Русский

Пусть α: X ≅ Y, f: Z → Y, g: Z → X. Тогда g = f ≫ α.inv эквивиано g ≫ α.hom = f.

LaTeX

$$$g = f \gg α.inv \;\Leftrightarrow\; g \gg α.hom = f$$$

Lean4

theorem comp_inv_eq_id (α : X ≅ Y) {f : X ⟶ Y} : f ≫ α.inv = 𝟙 X ↔ f = α.hom :=
  comp_hom_eq_id α.symm

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

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

Разделы

Аффилиация

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