isColimitBiproductToPushout

Mathlib.CategoryTheory.Abelian.Basic

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

Lean4

/-- The cofork induced by the canonical map `Y ⊞ Z ⟶ pushout f g` is in fact a colimit cokernel
    cofork. -/
def isColimitBiproductToPushout : IsColimit (biproductToPushoutCofork f g) :=
  Cofork.IsColimit.mk _
    (fun s =>
      pushout.desc (biprod.inl ≫ Cofork.π s) (biprod.inr ≫ Cofork.π s) <|
        sub_eq_zero.1 <| by
          rw [← Category.assoc, ← Category.assoc, ← sub_comp, sub_eq_add_neg, ← neg_comp, ← biprod.lift_eq,
            Cofork.condition s, zero_comp])
    (fun s => by apply biprod.hom_ext' <;> simp) fun s m h => by apply pushout.hom_ext <;> simp [← h]

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

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

Разделы

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

Аффилиация

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