cocone_naturality — Mathlib

English

In MonCat with filtered colimits, the cocone morphism is natural in the indexing map; i.e., composing with the diagram map equals the cocone morphism at the source.

Русский

В MonCat с фильтрованными коллимами морфизм кокона натуральен по индексационной карте; то есть композиция с отображением диаграммы равна кокон-морфизму в источнике.

LaTeX

$$$F.map f \;\gg\; \mathrm{coconeMorphism}(F, j') = \mathrm{coconeMorphism}(F, j).$$$

Lean4

@[to_additive (attr := simp)]
theorem cocone_naturality {j j' : J} (f : j ⟶ j') : F.map f ≫ coconeMorphism.{v, u} F j' = coconeMorphism F j :=
  MonCat.ext fun x => congr_fun ((Types.TypeMax.colimitCocone (F ⋙ forget MonCat)).ι.naturality f) x

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