English
If for every finite J there exist limits of shape J in C, then HasFiniteLimits C.
Русский
Если для каждого конечного J существуют пределы формы J в C, то HasFiniteLimits C.
LaTeX
$$$\forall J\; [\operatorname{Fin}(J) \Rightarrow \operatorname{HasLimitsOfShape}(J, C)] \Rightarrow \operatorname{HasFiniteLimits}(C)$$$
Lean4
/-- We can always derive `HasFiniteColimits C` by providing colimits at an
arbitrary universe. -/
theorem hasFiniteColimits_of_hasFiniteColimits_of_size
(h : ∀ (J : Type w) {𝒥 : SmallCategory J} (_ : @FinCategory J 𝒥), HasColimitsOfShape J C) : HasFiniteColimits 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
@hasColimitsOfShape_of_equivalence (ULiftHom (ULift J)) (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) C _ J
hJ (@Equivalence.symm J hJ (ULiftHom (ULift J)) (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) l) _
