e_isoExt_inv

Mathlib.CategoryTheory.Limits.Shapes.Images

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.IsImage.e_isoExt_inv

English

For IsImage F and F' of f, the hom map of isoExt matches F'.m after precomposition with F.m, i.e. (same as 72008).

Русский

Для изобразимого f факторизации F и F' сохраняется соответствие: g ∘ F'.m = F.m, где g — гомоморфизм из isoExt.

LaTeX

$$$\operatorname{comp}(\mathrm{isoExt}(hF,hF').hom, F'.m) = F.m.$$$

Lean4

theorem e_isoExt_inv : F'.e ≫ (isoExt hF hF').inv = F.e := by simp

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

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

Разделы

Аффилиация

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