English
If limits exist for all finite J in a suitable sense, then HasFiniteLimits C holds.
Русский
Если пределы существуют для всех конечных J в подходящем смысле, то выполняется HasFiniteLimits C.
LaTeX
$$$\forall J\, (\operatorname{Fin}(J) \Rightarrow \operatorname{HasLimitsOfShape}(J, C)) \Rightarrow \operatorname{HasFiniteLimits}(C)$$$
Lean4
/-- We can always derive `HasFiniteLimits C` by providing limits at an
arbitrary universe. -/
theorem hasFiniteLimits_of_hasFiniteLimits_of_size
(h : ∀ (J : Type w) {𝒥 : SmallCategory J} (_ : @FinCategory J 𝒥), HasLimitsOfShape J C) : HasFiniteLimits C where
out := fun J hJ hhJ =>
by
haveI := h (ULiftHom.{w} (ULift.{w} J)) <| @CategoryTheory.finCategoryUlift J hJ hhJ
have l : @Equivalence J (ULiftHom (ULift J)) hJ (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) :=
@ULiftHomULiftCategory.equiv J hJ
apply
@hasLimitsOfShape_of_equivalence (ULiftHom (ULift J)) (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) C _ J
hJ l.symm _
