hasFiniteLimits — Mathlib

English

If C has finite wide pullbacks, then for every object B, the over category Over B has finite limits.

Русский

Если в C существуют конечные широкие вытягивания, то для любого объекта B категория Over B имеет конечные пределы.

LaTeX

$$$\text{HasFiniteLimits}(\mathrm{Over}(B)) \quad\text{for all } B, \text{ provided } \text{HasFiniteWidePullbacks}(C).$$$

Lean4

instance hasFiniteLimits {B : C} [HasFiniteWidePullbacks C] : HasFiniteLimits (Over B) :=
  by
  have := ConstructProducts.over_finiteProducts_of_finiteWidePullbacks (B := B)
  have := hasEqualizers_of_hasPullbacks_and_binary_products (C := Over B)
  apply hasFiniteLimits_of_hasEqualizers_and_finite_products

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