of_isLimit_cone — Mathlib

English

Variant: from any cone D: WalkingCospan ⥤ C, and IsLimit c, the corresponding cospan-cone yields an IsPullback.

Русский

Вариант: из любого конуса D: WalkingCospan ⥤ C, если c — предел, то соответствующий конус-коспан образует IsPullback.

LaTeX

$$IsPullback (c.π.app left) (c.π.app right) (D.map inl) (D.map inr)$$

Lean4

/-- Variant of `of_isLimit` for an arbitrary cone on a diagram `WalkingCospan ⥤ C`. -/
theorem of_isLimit_cone {D : WalkingCospan ⥤ C} {c : Cone D} (hc : IsLimit c) :
    IsPullback (c.π.app .left) (c.π.app .right) (D.map WalkingCospan.Hom.inl) (D.map WalkingCospan.Hom.inr)
    where
  w := by simp_rw [Cone.w]
  isLimit' := ⟨IsLimit.equivOfNatIsoOfIso _ _ _ (PullbackCone.isoMk c) hc⟩

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