cocone_naturality_components — Mathlib

English

The componentwise naturality of cocone morphisms holds in CommRingCat, mirroring the RingCat version but in the commutative setting.

Русский

Компонентная естественность отображений кокона выполняется в CommRingCat.

LaTeX

$$$\forall f:\, j\to j',\; (coconeMorphism F j')(F.map f x) = (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]

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