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 g = f.inv.

Русский

Если f: X ≅ Y и g: Y ⟶ X с f.hom ≫ g = 𝟙 X, то g = f.inv.

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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