hasPullbacks_of_hasLimit_cospan — Mathlib

English

If the left leg f is an isomorphism, then the pullback of f and g exists.

Русский

Если левая дуга f является изоморфизмом, то существует прообраз pullback для f и g.

LaTeX

$$$$ \text{If } f \text{ is an isomorphism, then } \text{HasPullback}(f,g). $$$$

Lean4

/-- If `C` has all limits of diagrams `cospan f g`, then it has all pullbacks -/
theorem hasPullbacks_of_hasLimit_cospan [∀ {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}, HasLimit (cospan f g)] :
    HasPullbacks C :=
  { has_limit := fun F => hasLimit_of_iso (diagramIsoCospan F).symm }

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