initial_iff_empty_of_preserves_of_reflects

English

Initial X exists iff ToType X is empty, given preservation and reflection of colimits by forgetful functor.

Русский

Начальный X существует тогда и только тогда, когда ToType X пуст, при условии сохранения и отражения колимитов забывающим функтором.

LaTeX

$$$ \\text{initial_iff_empty_of_preserves_of_reflects } $$$

Lean4

/-- If `forget C` preserves and reflects initials, then `X` is initial if and only if
`ToType X` is empty. -/
theorem initial_iff_empty_of_preserves_of_reflects [PreservesColimit (Functor.empty.{0} C) (forget C)]
    [ReflectsColimit (Functor.empty.{0} C) (forget C)] (X : C) : Nonempty (IsInitial X) ↔ IsEmpty (ToType X) :=
  by
  rw [← Types.initial_iff_empty, (IsInitial.isInitialIffObj (forget C) X).nonempty_congr]
  rfl

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