cocone_naturality_components — Mathlib

English

For a functor F: J → RingCat, and objects j,j'∈J with f: j → j', the naturality of the cocone morphisms with respect to map along f holds: applying the cocone morphism at j' to F.map f x equals applying the cocone morphism at j to x.

Русский

Пусть F: J → RingCat; для объектов j,j'∈J и стрелки f: j → j' естественность кокон-морфонтов относительно отображения вдоль f: coconeMorphism F j' (F.map f x) = coconeMorphism F j x.

LaTeX

$$$ (\mathrm{coconeMorphism} F j') (F.map f x) = (\mathrm{coconeMorphism} F j) x $$$

Lean4

@[simp]
theorem cocone_naturality_components (j j' : J) (f : j ⟶ j') (x : F.obj j) :
    (coconeMorphism F j') (F.map f x) = (coconeMorphism F j) x := by rw [← cocone_naturality F f, comp_apply]

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