map_desc — Mathlib

English

Let F : J ⥤ C, E : K ⥤ J, G : J ⥤ C, α : F ⟶ G. Then colimit.pre F E ≫ colim.map α = colim.map (whiskerLeft E α) ≫ colimit.pre G E.

Русский

Пусть F : J ⥤ C, E : K ⥤ J, G : J ⥤ C, α : F ⟶ G. Тогда colimit.pre F E ≫ colim.map α = colim.map (whiskerLeft E α) ≫ colimit.pre G E.

LaTeX

$$$ \\operatorname{colimit.pre} F E \\; \\circ \\operatorname{colim.map} \\alpha = \\operatorname{colim.map} (\\mathrm{whiskerLeft} \\ E \\ alpha) \\; \\circ \\operatorname{colimit.pre} G E $$$

Lean4

@[reassoc (attr := simp)]
theorem map_desc (c : Cocone G) : colimMap α ≫ colimit.desc G c = colimit.desc F ((Cocones.precompose α).obj c) :=
  by
  ext j
  simp [colimit.ι_desc, colimit.ι_desc]

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