hasColimitsOfShape_iff_isRightAdjoint_const

English

There is an equivalence between having colimits of shape J in C and const J being a right adjoint.

Русский

Существование коллатимов формы J в C эквивалентно тому, что константный функтор Δ_J является правым адаптом.

LaTeX

$$HasColimitsOfShape J C \\iff IsRightAdjoint (const J : C ⥤ (J ⥤ C))$$

Lean4

theorem hasColimitsOfShape_iff_isRightAdjoint_const : HasColimitsOfShape J C ↔ IsRightAdjoint (const J : C ⥤ _) :=
  calc
    HasColimitsOfShape J C ↔ ∀ F : J ⥤ C, HasColimit F := ⟨fun h => h.has_colimit, fun h => HasColimitsOfShape.mk⟩
    _ ↔ ∀ F : J ⥤ C, HasInitial (Cocone F) := (forall_congr' hasColimit_iff_hasInitial_cocone)
    _ ↔ ∀ F : J ⥤ C, HasInitial (StructuredArrow F (const J)) :=
      (forall_congr' fun F => (Cocone.equivStructuredArrow F).hasInitial_iff)
    _ ↔ (IsRightAdjoint (const J : C ⥤ _)) := isRightAdjoint_iff_hasInitial_structuredArrow.symm

Похожие утверждения