of_isColimit_cocone — Mathlib

English

The inverse part of the pullback iso composed with fst equals the canonical pullback fst.

Русский

Обратная часть исоморфизма pullback, умноженная на fst, даёт каноническую стрелку pullback.fst.

LaTeX

$$$ h.isoPullback.inv \circ fst = pullback.fst f g $$$

Lean4

/-- Variant of `of_isColimit` for an arbitrary cocone on a diagram `WalkingSpan ⥤ C`. -/
theorem of_isColimit_cocone {D : WalkingSpan ⥤ C} {c : Cocone D} (hc : IsColimit c) :
    IsPushout (D.map WalkingSpan.Hom.fst) (D.map WalkingSpan.Hom.snd) (c.ι.app .left) (c.ι.app .right)
    where
  w := by simp_rw [Cocone.w]
  isColimit' := ⟨IsColimit.equivOfNatIsoOfIso _ _ _ (PushoutCocone.isoMk c) hc⟩

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