hasEqualizers_of_hasLimit_parallelPair

English

If every diagram parallelPair f g has a limit in C, then C has all equalizers.

Русский

Если для каждой пары стрел f,g из X в Y в C существует предел диаграммы parallelPair f g, то C имеет все эквалайзеры.

LaTeX

$$$ [\\forall X,Y,f,g, \\ HasLimit( parallelPair f g )] \\Rightarrow HasEqualizers C $$$

Lean4

/-- If `C` has all limits of diagrams `parallelPair f g`, then it has all equalizers -/
theorem hasEqualizers_of_hasLimit_parallelPair [∀ {X Y : C} {f g : X ⟶ Y}, HasLimit (parallelPair f g)] :
    HasEqualizers C :=
  { has_limit := fun F => hasLimit_of_iso (diagramIsoParallelPair F).symm }

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