has_limits_of_hasEqualizers_and_products

English

If a category has finite products and equalizers, it has all finite limits.

Русский

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

LaTeX

$$$HasFiniteProducts\,C \land HasEqualizers\,C \Rightarrow HasFiniteLimits\,C$$$

Lean4

/-- Any category with products and equalizers has all limits. -/
@[stacks 002N]
theorem has_limits_of_hasEqualizers_and_products [HasProducts.{w} C] [HasEqualizers C] : HasLimitsOfSize.{w, w} C :=
  { has_limits_of_shape := fun _ _ => { has_limit := fun F => hasLimit_of_equalizer_and_product F } }

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