English
For shape J, the existence of all J-shaped limits in C is equivalent to the constant J-functor being left adjoint; i.e., HasLimitsOfShape J C iff const J is left adjoint.
Русский
Существование ограничений по форме J в C эквивалентно тому, что константный функтор J является левым акомпонентом; HasLimitsOfShape J C эквивалентен const J как левый соседний функтор.
LaTeX
$$$\\mathrm{HasLimitsOfShape}(J,C) \\iff (\\mathrm{const}\\, J : C \\to _) \\text{ is left adjoint}$$$
Lean4
theorem hasLimitsOfShape_iff_isLeftAdjoint_const : HasLimitsOfShape J C ↔ IsLeftAdjoint (const J : C ⥤ _) :=
calc
HasLimitsOfShape J C ↔ ∀ F : J ⥤ C, HasLimit F := ⟨fun h => h.has_limit, fun h => HasLimitsOfShape.mk⟩
_ ↔ ∀ F : J ⥤ C, HasTerminal (Cone F) := (forall_congr' hasLimit_iff_hasTerminal_cone)
_ ↔ ∀ F : J ⥤ C, HasTerminal (CostructuredArrow (const J) F) :=
(forall_congr' fun F => (Cone.equivCostructuredArrow F).hasTerminal_iff)
_ ↔ (IsLeftAdjoint (const J : C ⥤ _)) := isLeftAdjoint_iff_hasTerminal_costructuredArrow.symm
