ι_colimitConstInitial_hom — Mathlib

English

For the colimit of the constant diagram at the initial object, the canonical injections followed by the distinguished map to the initial object agree with the obvious initial morphism.

Русский

Для колимита константной диаграммы, сфокусированной на начальном объекте, канонические включения, композиция с особым отображением к начальному объекту совпадает с очевидной начальнoй стрелкой.

LaTeX

$$$$\\mathrm{colimit.ι}((\\mathrm{const}\\ J).\\mathrm{obj}(\\perp_C))\\,j \\;\\gg\\; \\mathrm{colimitConstInitial.hom} = \\mathrm{initial.to}_{\\perp_C}.$$$$

Lean4

@[reassoc (attr := simp)]
theorem ι_colimitConstInitial_hom {J : Type*} [Category J] {C : Type*} [Category C] [HasInitial C] {j : J} :
    colimit.ι ((CategoryTheory.Functor.const J).obj (⊥_ C)) j ≫ colimitConstInitial.hom = initial.to _ := by cat_disch

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