epi_shortComplex_g

Mathlib.Algebra.Homology.CommSq

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

← MathLib Explorer

English

In a pushout square, the right-hand map g is an epimorphism.

Русский

В пуш-аут-квадрате правая стрелка g является эпиморфизмом.

LaTeX

$$$ \text{Epi } h.shortComplex.g $$$

Lean4

theorem epi_shortComplex_g (h : IsPushout f g inl inr) : Epi h.shortComplex.g :=
  by
  rw [Preadditive.epi_iff_cancel_zero]
  intro _ b hb
  exact Cofork.IsColimit.hom_ext h.isColimitCokernelCofork (by simpa using hb)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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