hasInitial_of_hasInitial_of_preservesColimit

English

If C has an initial object and G preserves initial objects, then D has an initial object.

Русский

Если в C имеется начальный объект и G сохраняет начальные объекты, то в D также имеется начальный объект.

LaTeX

$$$[\\HasInitial C] \\land [PreservesColimit(\\mathrm{empty}, G)] \\Rightarrow \\text{HasInitial}(D).$$$

Lean4

/-- If `C` has an initial object and `G` preserves initial objects, then `D` has an initial object
also.
Note this property is somewhat unique to colimits of the empty diagram: for general `J`, if `C`
has colimits of shape `J` and `G` preserves them, then `D` does not necessarily have colimits of
shape `J`.
-/
theorem hasInitial_of_hasInitial_of_preservesColimit [PreservesColimit (Functor.empty.{0} C) G] : HasInitial D :=
  ⟨fun F => by
    haveI := HasColimit.mk ⟨_, isColimitOfHasInitialOfPreservesColimit G⟩
    apply hasColimit_of_iso F.uniqueFromEmpty⟩

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