initial_const_of_isInitial — Mathlib

English

If D has an initial object X and C is any category, then the constant functor ΔC sending every object of C to X (and every morphism to id_X) is an initial functor.

Русский

Пусть у D есть начальный объект X. Тогда константный функтор Δ: C → D, отправляющий каждый объект C в X и каждое отображение в id_X, является начальным функтором.

LaTeX

$$$\\text{If } X \\text{ is initial in } D, \\ \\Delta_C X : C \\to D \\text{ is initial}$$$

Lean4

/-- The inclusion of an initial object is initial. -/
theorem initial_const_of_isInitial [IsCofiltered C] {X : D} (hX : IsInitial X) : ((Functor.const C).obj X).Initial :=
  Functor.initial_of_exists_of_isCofiltered _ (fun _ => ⟨IsCofiltered.nonempty.some, ⟨hX.to _⟩⟩)
    (fun {_ c} _ _ => ⟨c, 𝟙 _, hX.hom_ext _ _⟩)

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