ι_colimMap — Mathlib

English

For F,G with colimits and α: F ⟶ G, and j ∈ J, we have colimit.ι F j ≫ colimMap α = α.app j ≫ colimit.ι G j.

Русский

Для F,G с колимитами и α: F ⟶ G выполняется colimit.ι F j ≫ colimMap α = α.app j ≫ colimit.ι G j.

LaTeX

$$$\\operatorname{colimit.ι}_F(j) \\;\\gg\\; \\operatorname{colimMap}_\\alpha = \\alpha.j \\;\\gg\\; \\operatorname{colimit.ι}_G j$$$

Lean4

@[reassoc (attr := simp)]
theorem ι_colimMap {F G : J ⥤ C} [HasColimit F] [HasColimit G] (α : F ⟶ G) (j : J) :
    colimit.ι F j ≫ colimMap α = α.app j ≫ colimit.ι G j :=
  colimit.ι_desc _ j

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