English
Let C be a category, J a linearly ordered set with a top element j, F a functor from Set.Iio j to C, and c a cocone over F. There is a canonical family of morphisms between the extended objects in the cocone, indexed by i1 ≤ i2 ≤ j, defined by a specified explicit construction. These morphisms form a coherent directed system: they exist for all comparable indices, satisfy identity on the same index, and compose along chains.
Русский
Пусть C — категория, J — линейно упорядоченная множество с верхним элементом j, F — частичный функтор Set.Iio j ⥤ C, и c — кокон над F. Существует каноническая family морфизмов между расширенными объектами кокона, индексируемая парами i1 ≤ i2 ≤ j, заданная конкретной формулой. Эти морфизмы образуют непрерывную направленную систему: существуют для любых сравнимых индексов, тождественны на одинаковом индексе и компонуются по цепочке.
LaTeX
$$$\\text{Let } C \\text{ be a category } J \\text{ a linearly ordered set with a top element } j, \\ F: \\mathbf{Set}^{I\\!I\\!o j} \\to C, \\text{ and } c: \\mathrm{Cocone}(F). \\text{ Then for all } i_1 \\le i_2 \\le j, \\ \\mathrm{f}_{i_1,i_2}: \\mathrm{obj}(c,i_1) \\to \\mathrm{obj}(c,i_2) \\text{ is defined; } \\mathrm{f}_{i,i}=\\mathrm{id}, \\ \\mathrm{f}_{i_1,i_3}=\\mathrm{f}_{i_2,i_3} \\circ \\mathrm{f}_{i_1,i_2}.$$$
Lean4
/-- Auxiliary definition for `ofCocone`. -/
def map (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ ≤ j) : obj c i₁ ⟶ obj c i₂ :=
if h₂ : i₂ < j then (objIso c i₁ (lt_of_le_of_lt hi h₂)).hom ≫ F.map (homOfLE hi) ≫ (objIso c i₂ h₂).inv
else
have h₂' : i₂ = j := le_antisymm hi₂ (by simpa using h₂)
if h₁ : i₁ < j then (objIso c i₁ h₁).hom ≫ c.ι.app ⟨i₁, h₁⟩ ≫ (objIsoPt c).inv ≫ eqToHom (by subst h₂'; rfl)
else
have h₁' : i₁ = j := le_antisymm (hi.trans hi₂) (by simpa using h₁)
eqToHom (by subst h₁' h₂'; rfl)
