isIso_of_comp_hom_eq_id

Mathlib.CategoryTheory.Iso

URI: https://scilib.ai/kg/mathlib#CategoryTheory.isIso_of_comp_hom_eq_id

English

If g is an isomorphism and f ≫ g = 𝟙 Y, then f is an isomorphism.

Русский

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

LaTeX

$$$(IsIso g)\to (f\gg g = 𝟙 Y) \to IsIso f$$$

Lean4

theorem isIso_of_comp_hom_eq_id (g : X ⟶ Y) [IsIso g] {f : Y ⟶ X} (h : f ≫ g = 𝟙 Y) : IsIso f :=
  by
  rw [(comp_hom_eq_id _).mp h]
  infer_instance

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

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

Разделы

Аффилиация

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