hasPushouts_of_hasColimit_span — Mathlib

English

If a category D has wide pushouts, then it has binary pushouts.

Русский

Если в категории D существуют широкие пушауты, то существуют бинарные пушауты.

LaTeX

$$$$ \text{HasWidePushouts}(D) \Rightarrow \text{HasPushouts}(D). $$$$

Lean4

/-- If `C` has all colimits of diagrams `span f g`, then it has all pushouts -/
theorem hasPushouts_of_hasColimit_span [∀ {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}, HasColimit (span f g)] : HasPushouts C :=
  { has_colimit := fun F => hasColimit_of_iso (diagramIsoSpan F) }

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