English
Proof that preserving equalizers and products yields preservation of limits.
Русский
Доказательство того, что сохранение равноселителей и произведений влечет сохранение пределов.
LaTeX
$$Proof of preservesLimit_of_preservesEqualizers_and_product$$
Lean4
/-- If a functor creates equalizers and finite products, it creates finite 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 createsFiniteLimitsOfCreatesEqualizersAndFiniteProducts [HasEqualizers D] [HasFiniteProducts D]
(G : C ⥤ D) [G.ReflectsIsomorphisms] [CreatesLimitsOfShape WalkingParallelPair G] [CreatesFiniteProducts G] :
CreatesFiniteLimits G where createsFiniteLimits _ _ _ := createsLimitsOfShapeOfCreatesEqualizersAndProducts G
