ι_naturality_apply — Mathlib

English

The injections ι_j in CoconeTypes are natural in j with respect to map F.map; applying map to x and then injecting equals injecting x before mapping.

Русский

Векторные инъекции ι_j в CoconeTypes естественны по отношению к отображению F.map: применение отображения к x затем инъекция эквивалентны инъекции к x до отображения.

LaTeX

$$$c.ι j' (F.map f x) = c.ι j x$$$

Lean4

@[simp]
theorem ι_naturality_apply (c : CoconeTypes.{w₁} F) {j j' : J} (f : j ⟶ j') (x : F.obj j) :
    c.ι j' (F.map f x) = c.ι j x :=
  congr_fun (c.ι_naturality f) x

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