inv_ext

Mathlib.CategoryTheory.Iso

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

← MathLib Explorer

English

If f : X ≅ Y is an isomorphism and g : Y ⟶ X with f.hom ≫ g = 𝟙 X, then f.inv = g.

Русский

Если f: X ≅ Y, и g: Y ⟶ X удовлетворяет f.hom ≫ g = 𝟙 X, тогда f.inv = g.

LaTeX

$$$f.hom\gg g = 𝟙 X\to f.inv = g$$$

Lean4

@[aesop apply safe (rule_sets := [CategoryTheory])]
theorem inv_ext {f : X ≅ Y} {g : Y ⟶ X} (hom_inv_id : f.hom ≫ g = 𝟙 X) : f.inv = g :=
  ((hom_comp_eq_id f).1 hom_inv_id).symm

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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