eq_inv_of_inv_hom_id

Mathlib.CategoryTheory.Iso

URI: https://scilib.ai/kg/mathlib#CategoryTheory.IsIso.eq_inv_of_inv_hom_id

English

If inv f ≫ f = id_Y for an isomorphism f, then inv f = g implies g = inv f.

Русский

Если inv f ≫ f = id_Y для изоморфизма f, тогда inv f = g подразумевает g = inv f.

LaTeX

$$ {f : X ⟶ Y} [IsIso f] {g : Y ⟶ X} (inv_hom_id : g ≫ f = id_Y) : g = inv f$$

Lean4

theorem eq_inv_of_inv_hom_id {f : X ⟶ Y} [IsIso f] {g : Y ⟶ X} (inv_hom_id : g ≫ f = 𝟙 Y) : g = inv f :=
  (inv_eq_of_inv_hom_id inv_hom_id).symm

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

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

Разделы

Аффилиация

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