hasLimits — Mathlib

English

Let C be a Grothendieck abelian category; then C has all small limits of size w; equivalently, HasLimitsOfSize w C.

Русский

Пусть C — абелева категория Гротендьек; тогда C имеет все малые пределы размерности w; эквивалентно HasLimitsOfSize w C.

LaTeX

$$$\mathrm{HasLimitsOfSize}_{\,w, w}\; C$$$

Lean4

instance hasLimits : HasLimitsOfSize.{w, w} C :=
  have : HasLimits.{w, u} (ShrinkHoms C) := hasLimits_of_hasColimits_of_hasSeparator
  Adjunction.has_limits_of_equivalence (ShrinkHoms.equivalence C |>.functor)

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