of_isIso_fac_left

Mathlib.CategoryTheory.Iso

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

← MathLib Explorer

English

If f is an isomorphism and h is an isomorphism with f ≫ g = h, then g is an isomorphism.

Русский

Если f изоморфизм и h изоморфизм и f ≫ g = h, то g изоморфизм.

LaTeX

$$$IsIso f\to IsIso h\to f\gg g = h\to IsIso g$$$

Lean4

theorem of_isIso_fac_left {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {h : X ⟶ Z} [IsIso f] [hh : IsIso h] (w : f ≫ g = h) :
    IsIso g := by
  rw [← w] at hh
  exact of_isIso_comp_left f g

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

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

Разделы

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

Аффилиация

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