initial_fromPUnit_of_isInitial — Mathlib

English

If c is initial, the functor from the one-point category to c is initial.

Русский

Если c начальное, то fromPUnit(c): 1 → C начальная.

LaTeX

$$$\operatorname{IsInitial}(c) \Rightarrow \operatorname{Initial}(\operatorname{fromPUnit}(c))$$$

Lean4

theorem initial_fromPUnit_of_isInitial (hc : Limits.IsInitial c) : (fromPUnit c).Initial where
  out
    c' := by
    letI : Inhabited (CostructuredArrow (fromPUnit c) c') := ⟨.mk (Y := default) (hc.to c')⟩
    letI : Subsingleton (CostructuredArrow (fromPUnit c) c') :=
      ⟨fun i j ↦ CostructuredArrow.obj_ext _ _ (by cat_disch) (hc.hom_ext _ _)⟩
    infer_instance

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