isIso_inl_iso_of_epi

Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq

URI: https://scilib.ai/kg/mathlib#CategoryTheory.IsPushout.isIso_inl_iso_of_epi

English

If h is a pushout of f,g with inl,inr and HasPushout f g, then inl composed with isoPushout.hom equals the pushout's left injector.

Русский

Если есть пушаут f,g с inl,inr и HasPushout, то inl ∘ isoPushout.hom = pushout.inl.

LaTeX

$$$inl \circ h.isoPushout.hom = pushout.inl\ f\ g$$$

Lean4

theorem isIso_inl_iso_of_epi (h : IsPushout f f inl inr) : IsIso inl :=
  h.cocone.isIso_inl_of_epi_of_isColimit h.isColimit

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

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

Разделы

Аффилиация

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