ι_map_apply — Mathlib

English

If f: j → j' and w: F.map f x = x', then colimit.ι F j x = colimit.ι F j' x'.

Русский

Если есть стрелка f: j → j' и равенство F.map f x = x', то colimit.ι F j x = colimit.ι F j' x'.

LaTeX

$$$$ \text{colimit.ι } F\ j\ x = \text{colimit.ι } F\ j'\ x' \quad \text{whenever } F.map f\ x = x'. $$$$

Lean4

@[simp]
theorem ι_map_apply {F G : J ⥤ Type u} [HasColimitsOfShape J (Type u)] (α : F ⟶ G) (j : J) (x : F.obj j) :
    colim.map α (colimit.ι F j x) = colimit.ι G j (α.app j x) :=
  congr_fun (colimit.ι_map α j) x

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