English
Formulas describing how limits are computed via products and equalizers.
Русский
Формулы вычисления пределов через произведения и равноселители.
LaTeX
$$Limit formulas via products and equalizers$$
Lean4
/-- If a functor creates equalizers and products, it creates limits.
We additionally require the rather strong condition that the functor reflects isomorphisms. It is
unclear whether the statement remains true without this condition. There are various definitions of
"creating limits" in the literature, and whether or not the condition can be dropped seems to depend
on the specific definition that is used. -/
noncomputable def createsLimitsOfSizeOfCreatesEqualizersAndProducts [HasEqualizers D] [HasProducts.{w} D] (G : C ⥤ D)
[G.ReflectsIsomorphisms] [CreatesLimitsOfShape WalkingParallelPair G]
[∀ J, CreatesLimitsOfShape (Discrete.{w} J) G] : CreatesLimitsOfSize.{w, w} G where
CreatesLimitsOfShape := createsLimitsOfShapeOfCreatesEqualizersAndProducts G
