w_apply — Mathlib

English

For any α: F ⟶ G between type-valued functors, any j ∈ J and x ∈ F(j), the map commutes with injections: colim.map α (colimit.ι F j x) = colimit.ι G j (α.app j x).

Русский

Для любóго α: F ⟶ G между диаграммами типов, для любого j ∈ J и x ∈ F(j), отображение colim/map α совместимо с инъекциями: colim.map α (colimit.ι F j x) = colimit.ι G j (α.app j x).

LaTeX

$$$$ \text{colim.map }\alpha\ (\text{colimit.}\iota F\ j\ x) = \text{colimit.}\iota G\ j\ (\alpha.app\ j\ x). $$$$

Lean4

@[simp]
theorem w_apply {j j' : J} {x : F.obj j} (f : j ⟶ j') : colimit.ι F j' (F.map f x) = colimit.ι F j x :=
  congr_fun (colimit.w F f) x

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