hasPullbacks_of_hasBinaryProducts_of_hasEqualizers

English

If a category has all binary products and all equalizers, then it has all pullbacks.

Русский

Если категория имеет все двоичные произведения и все равнозначители, то она имеет все пуллбэки.

LaTeX

$$$$\text{HasPullbacks } C\quad\text{(i.e. pullbacks exist for all pairs of morphisms).}$$$$

Lean4

/-- If a category has all binary products and all equalizers, then it also has all pullbacks.
As usual, this is not an instance, since there may be a more direct way to construct
pullbacks. -/
theorem hasPullbacks_of_hasBinaryProducts_of_hasEqualizers (C : Type u) [Category.{v} C] [HasBinaryProducts C]
    [HasEqualizers C] : HasPullbacks C :=
  { has_limit := fun F => hasLimit_of_iso (diagramIsoCospan F).symm }

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