isIso_of_hom_comp_eq_id

Mathlib.CategoryTheory.Iso

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

English

If g ≫ f = 𝟙 X for some f and g with g invertible, then f is an isomorphism.

Русский

Если g ∘ f = id X и g является изоморфизмом, то f — изоморфизм.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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