preserves_desc_mapCocone — Mathlib

English

If G preserves cocone limits, then the desc map of the image cocone equals the image of the desc map.

Русский

Если G сохраняет коллимиты коконов, то desc отображение изображения кокона равно изображению desc.

LaTeX

$$$\\bigl(\\mathrm{isColimitOfPreserves}\\;G\\;t\\bigr).desc\\bigl(G.mapCocone\\;\\_\\bigr) = G.map\\bigl(t.desc\\;\\_\\bigr)$$$

Lean4

@[simp]
theorem preserves_desc_mapCocone (c₁ c₂ : Cocone F) (t : IsColimit c₁) :
    (isColimitOfPreserves G t).desc (G.mapCocone _) = G.map (t.desc c₂) :=
  ((isColimitOfPreserves G t).uniq (G.mapCocone _) _ (by simp [← G.map_comp])).symm

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