ι_map — Mathlib

English

For J with shape J and F,G : J ⥤ C, any α : F ⟶ G, and any j ∈ J we have colimit.ι F j ≫ colim.map α = α.app j ≫ colimit.ι G j.

Русский

Для J и функторов F,G : J ⥤ C, любого натурального преобразования α : F ⟶ G и любого j ∈ J выполнено: colimit.ι F j ≫ colim.map α = α.app j ≫ colimit.ι G j.

LaTeX

$$$ \\operatorname{colimit.ι} F j \\; \\circ \\operatorname{colim.map} \\alpha = \\alpha.{\\mathrm{app}}\, j \\; \\circ \\operatorname{colimit.ι} G j $$$

Lean4

@[reassoc]
theorem ι_map (j : J) : colimit.ι F j ≫ colim.map α = α.app j ≫ colimit.ι G j := by simp

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