isIso_factorThruCoimage

Mathlib.CategoryTheory.Abelian.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Abelian.isIso_factorThruCoimage

English

In an Abelian category, the coimage–image comparison is always an isomorphism for any morphism.

Русский

В абелевой категории сопоставление кообраза и образа всегда изоморфизм для любого морфизма.

LaTeX

$$$$ \\operatorname{coimageImageComparison} f \\in \\mathrm{Iso} $$$$

Lean4

instance isIso_factorThruCoimage [Epi f] : IsIso (Abelian.factorThruCoimage f) := by infer_instance

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

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

Разделы

Аффилиация

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