initial_const_initial — Mathlib

English

If C is a cofiltered category and D has an initial object X, then the constant functor ΔC with value X is initial.

Русский

Пусть C — кофильтрованная категория и в D есть начальный объект X. Тогда константный функтор ΔC с значением X является начальним.

LaTeX

$$$[\\text{IsCofiltered } C] \\Rightarrow (\\text{Initial}(\\Delta_C X))$$$

Lean4

/-- The inclusion of the initial object is initial. -/
theorem initial_const_initial [IsCofiltered C] [HasInitial D] : ((Functor.const C).obj (⊥_ D)).Initial :=
  Functor.initial_const_of_isInitial initialIsInitial

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