isColimitBinaryCofanSum — Mathlib

English

The binary cofan binaryCofanSum is a colimit for the pair of cofans c1 and c2.

Русский

Двойной кофан binaryCofanSum является колимитом пары кофанов c1 и c2.

LaTeX

$$$IsColimit( binaryCofanSum\\ c\\ c_1\\ c_2\\ hc_1\\ hc_2 )$$$

Lean4

/-- The binary cofan `binaryCofanSum c c₁ c₂ hc₁ hc₂` is colimit. -/
def isColimitBinaryCofanSum : IsColimit (binaryCofanSum c c₁ c₂ hc₁ hc₂) :=
  BinaryCofan.IsColimit.mk _
    (fun f₁ f₂ =>
      Cofan.IsColimit.desc hc
        (fun i =>
          match i with
          | Sum.inl i₁ => c₁.inj i₁ ≫ f₁
          | Sum.inr i₂ => c₂.inj i₂ ≫ f₂))
    (fun f₁ f₂ => Cofan.IsColimit.hom_ext hc₁ _ _ (by simp)) (fun f₁ f₂ => Cofan.IsColimit.hom_ext hc₂ _ _ (by simp))
    (fun f₁ f₂ m hm₁ hm₂ => by
      apply Cofan.IsColimit.hom_ext hc
      rintro (i₁ | i₂) <;> cat_disch)

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