English
If G preserves equalizers and products, then it preserves limits.
Русский
Если G сохраняет равноселители и произведения, то он сохраняет пределы.
LaTeX
$$$PreservesLimits G$$
Lean4
/-- If a functor creates terminal objects and pullbacks, 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 createsFiniteLimitsOfCreatesTerminalAndPullbacks [HasTerminal D] [HasPullbacks D] (G : C ⥤ D)
[G.ReflectsIsomorphisms] [CreatesLimitsOfShape (Discrete.{0} PEmpty) G] [CreatesLimitsOfShape WalkingCospan G] :
CreatesFiniteLimits G where
createsFiniteLimits _ _
_ :=
{
CreatesLimit :=
have : HasTerminal C := hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape G
have : HasPullbacks C := hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape G
have : HasFiniteLimits C := hasFiniteLimits_of_hasTerminal_and_pullbacks
createsLimitOfReflectsIsomorphismsOfPreserves }
