ι_colimitIso_hom — Mathlib

English

For HasColimit G, the morphism colimit.ι (F ⋙ G) X followed by (colimitIso F G).hom equals colimit.ι G (F.obj X).

Русский

При наличии колимита G композиция colimit.ι(F ⋙ G)(X) затем гомоморфизм colimitIso F G совпадает с colimit.ι G (F.obj X).

LaTeX

$$$$ \operatorname{colimit.\iota} (F \circ G)(X) \;\;\; \gg \; (\operatorname{colimitIso} F G)^{\mathrm{h}om} = \operatorname{colimit.\iota} G (F(X)). $$$$

Lean4

@[reassoc (attr := simp)]
theorem ι_colimitIso_hom [HasColimit G] (X : C) : colimit.ι (F ⋙ G) X ≫ (colimitIso F G).hom = colimit.ι G (F.obj X) :=
  by simp [colimitIso]

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