English
If a category has terminal objects and pullbacks, it has finite limits.
Русский
Если в категории существуют терминальные объекты и вытянутые пределы, то существуют конечные пределы.
LaTeX
$$$HasTerminal C \land HasPullbacks C \Rightarrow HasFiniteLimits C$$$
Lean4
/-- If G preserves terminal objects and pullbacks, it preserves all finite limits. -/
theorem preservesFiniteLimits_of_preservesTerminal_and_pullbacks [HasTerminal C] [HasPullbacks C] (G : C ⥤ D)
[PreservesLimitsOfShape (Discrete.{0} PEmpty) G] [PreservesLimitsOfShape WalkingCospan G] :
PreservesFiniteLimits G :=
by
have : HasFiniteLimits C := hasFiniteLimits_of_hasTerminal_and_pullbacks
have : PreservesLimitsOfShape (Discrete WalkingPair) G := preservesBinaryProducts_of_preservesTerminal_and_pullbacks G
have : PreservesLimitsOfShape WalkingParallelPair G := preservesEqualizers_of_preservesPullbacks_and_binaryProducts G
have : PreservesFiniteProducts G := .of_preserves_binary_and_terminal _
exact preservesFiniteLimits_of_preservesEqualizers_and_finiteProducts G
