pre_id — Mathlib

English

For F : J ⥤ C, the precomposition with the identity on J gives the canonical isomorphism: colimit.pre F (id_J) = colim.map (Functor.leftUnitor F).hom.

Русский

Для F : J ⥤ C предсоставление через идентичность на J есть каноническое изоморфизм: colimit.pre F (id_J) = colim.map (Functor.leftUnitor F).hom.

LaTeX

$$$ \\operatorname{colimit.pre} F (\\mathrm{Id}_J) = \\operatorname{colim.map} (\\mathrm{Functor.leftUnitor} F).\\mathrm{hom} $$$

Lean4

theorem pre_id (F : J ⥤ C) : colimit.pre F (𝟭 _) = colim.map (Functor.leftUnitor F).hom := by cat_disch

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