hasLimits — Mathlib

English

The over category Over X has all limits provided the base category C has the needed limits and X is fixed; more precisely, if C has the specified limits, then Over X has them as well.

Русский

Категория Over X имеет все пределы, если исходная категория C имеет необходимые пределы; конкретно, наличие пределов в C переносится в Over X.

LaTeX

$$$$ \text{HasLimitsOfShape } J(\mathrm{Over}\; X) $$$$

Lean4

instance hasLimits {B : C} [HasWidePullbacks.{w} C] : HasLimitsOfSize.{w, w} (Over B) :=
  by
  have := ConstructProducts.over_binaryProduct_of_pullback (B := B)
  have := hasEqualizers_of_hasPullbacks_and_binary_products (C := Over B)
  have := ConstructProducts.over_products_of_widePullbacks (B := B)
  apply has_limits_of_hasEqualizers_and_products

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