ι_preservesColimitIso_hom — Mathlib

English

The forward projection under preservesColimitIso equals the image of the projection: G.map (colimit.ι F j) ≫ preservesColimitIso.hom = colimit.ι (F ⋙ G) j.

Русский

Прямая проекция под preservesColimitIso равна изображению проекции: G.map(ι_F_j) ≫ hom = ι_{F⋅G}^j.

LaTeX

$$$G.map (\\mathrm{colimit.\\,ι} F j) \\; ≫ (\\mathrm{preservesColimitIso}\\ G\\ F)\\mathrm{hom} = \\mathrm{colimit.\\,ι} (F \\cdot G) j$$$

Lean4

@[reassoc (attr := simp)]
theorem ι_preservesColimitIso_hom (j : J) :
    G.map (colimit.ι F j) ≫ (preservesColimitIso G F).hom = colimit.ι (F ⋙ G) j :=
  (isColimitOfPreserves G (colimit.isColimit _)).comp_coconePointUniqueUpToIso_hom _ j

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