ι_colimitDesc — Mathlib

English

For any cocone t and any index j, the leg from F(j) to colimit F composed with colimitDesc F t equals the j-th leg of t.

Русский

Для любой коконы t и любого индекса j, компоновка от F(j) к колимиту F через colimitDesc F t даёт тот же их j-ты разрез t.

LaTeX

$$$\forall t\ (j\in J),\; (\text{colimitCocone }F).\iota_{j} \;\circ\; \mathrm{colimitDesc} F t = t.\iota_{j}$$$

Lean4

@[reassoc (attr := simp)]
theorem ι_colimitDesc (t : Cocone F) (j : J) : (colimitCocone F).ι.app j ≫ colimitDesc F t = t.ι.app j :=
  (forget₂ _ AddCommGrpCat).map_injective
    ((AddCommGrpCat.FilteredColimits.colimitCoconeIsColimit (F ⋙ forget₂ _ _)).fac _ _)

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